fundamentals_lecture.v

(**

<<
                   Lecture 2: Fundamentals of Coq
      -------------------------------------------------------------
        Anders Mörtberg (Carnegie Mellon and Stockholm University)
        Minor modifications made by Marco Maggesi (Univesity of Florence).
        Minor modifications made by Niels van der Weide (Radboud University).
>>

The Coq proof assistant is a programming language for writing
proofs: https://coq.inria.fr/

It has been around since 1984 and was initially implemented by Thierry
Coquand and his PhD supervisor Gérard Huet. The first version, called
CoC, implemented the Calculus of Constructions as presented in:

"The Calculus of Constructions"
Thierry Coquand and Gérard Huet
Information and Computation 76(2–3): 95–120. 1988.

It was later extended to the Calculus of Inductive Constructions and
the name changed to Coq. These type theories are similar to Martin-Löf
type theory. As Coq is supposed to be a programming language for
developing proofs all programs have to be terminating, so it can be
seen as a "total" programming language.

The Coq system has a very long and detailed reference manual:

https://coq.inria.fr/distrib/current/refman/

However, UniMath is only using a small subset of Coq, so there is a
lot of information that is not relevant for UniMath development in
there. The fragment of Coq that UniMath uses consists of:

- Pi-types (with judgmental eta)
- Sigma-types (with judgmental eta)
- The inductive types of natural numbers, booleans, unit and empty
- Coproduct types
- A universe UU

The reason UniMath only relies on this subset is that everything in UniMath
has to be motivated by the model in simplicial sets:

https://arxiv.org/abs/1211.2851

In this lecture I will show some things than can be done in UniMath as
a programming language. In the later lectures we will also see how to
prove properties about the programs that we can write in UniMath.

The UniMath library can be found at:

https://github.com/UniMath/UniMath

This whole file is a Coq file and it hence has the file ending ".v" (v
for "vernacular") and can be processed using:

- emacs with proof-general: https://proofgeneral.github.io/
- Coq IDE
- VSCode

I use emacs as it is also an extremely powerful text editor, but if
you never saw emacs before it might be quite overwhelming. An
alternative that might be easier for newcomers is Coq IDE (interactive
development environment). It also has some features that emacs doesn't
have so some Coq experts use it as well, but in this talk I will use
emacs.

In order to make emacs interact with Coq one should install Proof
General. This is an extension to emacs that enables it to interact
with a range of proof assistants, including Coq. For UniMath
development one should also install agda-mode in order to be able to
properly insert unicode characters.

The basic keybinding that I use when working in Proof General are:
<<
C-c C-n      -- Process one line
C-c C-u      -- Unprocess a line
C-c C-ENTER  -- Process the whole buffer up until the cursor
C-c C-b      -- Process the whole file
C-c C-r      -- Unprocess (retract) the whole file
C-x C-c      -- Kill the Coq process
>>
For more commands see:

https://proofgeneral.github.io/doc/master/userman/Basic-Script-Management/#Script-processing-commands
https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General/#Coq_002dspecific-commands

Here C = CTRL and M = ALT on a standard emacs setup, so "C-c C-n"
means "press c while holding CTRL and then press n while still holding
CTRL" (note that the keybindings are case sensitive). ENTER is the
"return" key on my keyboard.

Various basic emacs commands:
<<
C-x C-f      -- Find file
C-x C-s      -- Save file
C-x C-x      -- Exit emacs
C-x b        -- Kill buffer
C-_          -- Undo
C-x 1        -- Maximize buffer
C-x 2        -- Split buffer horizontally
C-x 3        -- Split buffer vertically
M-%          -- Search-and-replace
M-;          -- Comment region
>>
For more commands see: https://www.gnu.org/software/emacs/ (or just
Google "emacs tutorial")

*)

(** To import a file write:
<<
Require Import Dir.Filename.
>>
*)

(**

This will import the file Filename in the directory Dir. This assumes
that directory Dir is visible to Coq, that is, in the list of
directories in which Coq looks for files to import. If you are working
in the UniMath directory then Coq will be able to find all of the
files in the UniMath library, but if you are in another directory you
need to the update your LoadPath by running
<<
Add LoadPath "/path/to/UniMath".
>>
(where "/path/to/UniMath/" is replaced to the path where UniMath is
located on your computer).

Coq has a fancy module system which allows you to import and export
definitions in various complicated ways. We extremely rarely use
this in UniMath so you can safely ignore it for now. The only thing
you need to know is that there is an alternative to Require Import:
<<
Require Export Dir.Filename.
>>
that is used in some files. This will make the file you are working
on import all of the definitions in Dir.Filename and then export
them again so that any file that imports this file also gets the
definitions in Dir.Filename. I personally only use Require Import.

*)

(* Let's import one of the most basic UniMath file: *)
Require Import UniMath.Foundations.Preamble.
(* This file contains definition of the inductive types of UniMath,
makes UU the name for the universe and various other basic things. *)

(** * Definitions, lambda terms *)

(** The polymorphic identity function *)
Definition idfun : forall (A : UU), A -> A := fun (A : UU) (a : A) => a.

(** forall = Pi *)
(** fun = lambda *)

Check idfun.  (* Or use Ctrl-Alt-C or Ctrl-Cmd-C on idfun. *)
Print idfun.  (* Or use Ctrl-Alt-P or Ctrl-Cmd-P on idfun. *)

Definition idfun' (A : UU) (a : A) : A := a.

Check idfun'.
Print idfun'.

Definition idfun'' {A : UU} (a : A) : A := a.

Check idfun' nat 3.

(** The constant function that returns its first argument *)
Definition const (A B : UU) (a : A) (b : B) : A := a.

(** The booleans are defined in UniMath.Foundations.Preamble *)
About bool.
Print bool.
Locate bool.

(** These are generated by true and false *)
Check true.
Check false.

(** They also come with an induction principle *)
About bool_rect.

(*
  bool_rect : ∏ P : bool → Type, P true → P false → ∏ b : bool, P b
 *)

(** Using this we can define a "recursion" principle *)
Definition ifbool (A : UU) (x y : A) : bool -> A :=
  bool_rect (fun _ : bool => A) x y.

(*
  bool_rect (fun _ : bool => A) x y

  P = fun _ : bool => A
  x : P true   [ A ]
  y : P false  [ A ]
  b : bool
 *)

(** We can define boolean negation: *)
Definition negbool : bool -> bool :=
  ifbool bool false true.

Eval compute in negbool true.

(* Alternative definition using pattern matching.
   Idiomatic in Coq, but we avoid doing this in UniMath. *)

Definition negbool' (b : bool) : bool :=
  match b with
  | true => false
  | false => true
  end.

(** The normalization of negbool and negbool' give the same term. *)
Eval compute in negbool.
Eval compute in negbool'.

Print bool_rect.

(** and compute with it *)
Eval compute in negbool true.

(** Coq supports many evaluation strategies, like cbn and cbv, for
details see:

https://coq.inria.fr/refman/tactics.html#Conversion-tactics

*)

(** boolean and *)
Definition andbool (b : bool) : bool -> bool :=
  ifbool (bool -> bool) (idfun bool) (const bool bool false) b.

Definition andbool' (b1 b2 : bool) : bool
  := ifbool bool b2 false b1.

(*
  if b1 is true
  then b2
  else false
 *)

Eval compute in andbool' false true.
Eval compute in andbool' false false.
Eval compute in andbool' true false.
Eval compute in andbool' true true.

Eval compute in andbool true true.
Eval compute in andbool true false.
Eval compute in andbool false true.
Eval compute in andbool false false.

(** The natural numbers are defined in UniMath.Foundations.Preamble *)
About nat.
Print nat.

(** They are defined as Peano numbers, but we can use numerals *)
Check (S(S(S 0))).
Check 3.

(** This type also comes with an induction principle *)
Check nat_rect.

(** We can define the recursor: *)
Definition nat_rec (A : UU) (a : A) (f : nat -> A -> A) : nat -> A :=
  nat_rect (fun _ : nat => A) a f.

(*
Definition nat_rec (A : UU) (a : A) (f : A -> A) : nat -> A :=
  nat_rect (fun _ : nat => A) a f.
 *)

(**

This can be understood as a function defined by the following clauses:
<<
nat_rec m f 0 = m
nat_rec m f (S n) = f n (nat_rec m f n)
>>

lecture 1 where f : A -> A
<<
nat_rec m f 0 = m
nat_rec m f (S n) = f (nat_rec m f n)
>>

 *)

(** We can look at the normal form of the recursor by *)
Eval compute in nat_rec.

(** This contains a both a "fix" and "match _ with _". These primitives
of Coq are not allowed in UniMath. Instead we write everything using
recursors. The reason is that everything we write in UniMath has to be
justified by the simplicial set model and the situation for general
inductive types with match is not spelled out in detail. *)

(** If you are used to regular programming languages it might seem very
strange to only program with the recursors, but it's actually not too
bad and we can do many programs quite directly. *)

(** Truncated predecessor function *)
Definition pred : nat -> nat := nat_rec nat 0 (const nat nat).

Definition pred' : nat -> nat := nat_rec nat 0 (fun n m => n).

(*

<<
pred 0 = 0
pred (S n) = n
>>

*)

Eval compute in pred 3.
Eval compute in pred 1.
Eval compute in pred 0.

(** We can test if a number is even by: *)
Definition even : nat -> bool := nat_rec bool true (fun _ b => negbool b).

Eval compute in even 3.
Eval compute in even 4.

(** Addition *)
Definition add (m : nat) : nat -> nat := nat_rec nat m (fun _ y => S y).

Eval compute in add 2 3.

(** We can define a nice notation for addition by: *)
Notation "x + y" := (add x y).

Eval compute in 4 + 9.

Check (add 3 4).  (* 3 + 4 : nat *)

(** To find information about a notation we can write: *)
Locate "+".
Locate add.

(** Coq allows us to write very sophisticated notations, for details
see: https://coq.inria.fr/refman/syntax-extensions.html *)

(** In UniMath we use a lot of unicode symbols. To input a unicode
symbol type \ and then the name of the symbol. For example \alpha
gives α. To get information about a unicode character, including
how to write it, put the cursor on top of the symbol and type:
M-x describe-char

We can write:
<<
  λ x, e        instead of   fun x => e
  ∏ (x : A), T  instead of   forall (x : A), T
  A → B         instead of   A -> B
>>
*)

(** Iterate a function n times *)
Definition iter (A : UU) (a : A) (f : A → A) (n : nat) : A :=
  nat_rec A a (λ _ y, f y) n.

Notation "f ^ n" := (λ x, iter _ x f n).

Eval compute in (pred ^ 2) 5.

Definition sub (m n : nat) : nat := (pred ^ n) m.

Eval compute in sub 15 4.
Eval compute in sub 11 15.

Definition is_zero : nat → bool := nat_rec bool true (λ _ _, false).

Eval compute in is_zero 3.
Eval compute in is_zero 0.

Definition eqnat (m n : nat) : bool :=
  andbool (is_zero (sub m n)) (is_zero (sub n m)).

Notation "m == n" := (eqnat m n) (at level 50).

Eval compute in 1 + 1 == 2.
Eval compute in 5 == 3.
Eval compute in 9 == 5.

(** Note that I could omit the A from the definition of f ̂ n and just
replace it by _. The reason is that Coq very often can infer what
arguments are so that we can omit them. *)

(** For example if I omit nat in *)
Check idfun _ 3.
(** Coq will figure it out for us. *)

(** We can tell Coq to always put _ for an argument by using curly
braces in the definition: *)

(** Such an argument is called an "implicit" and these are very useful
to get definitions that don't take too many arguments. However, it is
sometimes necessary to be able to give some of the arguments
explicitly, this is using "@". *)

Check @idfun'' nat 3.


(** * More inductive types *)

(** The inductive types we have seen so far come from the standard
library, but Coq allows us to define any inductive types we want. In
UniMath we don't allow this and the additional inductive types we have
are defined in Foundations. *)

(** One of these is the coproduct (disjoint union) of types *)
About coprod.
Print coprod.
Check ii1.
Check ii2.
Print inl.
Print inr.

Check (λ A B C : UU, @coprod_rect A B (λ _, C)).

Definition coprod_rec {A B C : UU} (f : A → C) (g : B → C) : coprod A B → C :=
  @coprod_rect A B (λ _, C) f g.

(** We can define integers as a coproduct of nat with itself *)

Definition Z : UU := coprod nat nat.

(* NB: Use \hermitconjmatrix to type the symbol ⊹.
       Use \minus to type the symbol − *)
Notation "⊹ x" := (inl x) (at level 20).
Notation "─ x" := (inr x) (at level 40).

(** +1 = inl 1 *)
(** 0 = inl 0 *)
(** -1 = inr 0 *)
(** Note that we get the negative numbers "off-by-one". *)


Definition Z1 : Z := ⊹ 1.
Definition Z0 : Z := ⊹ 0.
Definition Zn3 : Z := ─ 2.

(** We can define a function by case on whether the number is ⊹ n or ─ n *)
Definition Zcase (A : UU) (fpos : nat → A) (fneg : nat → A) : Z → A :=
  coprod_rec fpos fneg.

Definition negate : Z → Z :=
  Zcase Z (λ x, ifbool Z Z0 (─ pred x) (is_zero x)) (λ x, ⊹ S x).

Eval compute in negate Z0.
Eval compute in negate Z1.
Eval compute in negate Zn3.

(** We also have two more inductive types: *)

(** The unit type with one inhabitant tt *)
About unit.
Print unit.

(** The empty type with no inhabitants *)
About empty.
Print empty.

(** Terms as proofs.  *)
(* Proof that true and false are different. *)

Require Import UniMath.Foundations.PartA.

(** Section's can be very useful to only write parameters that are used
many times once and for all. They are also useful for organizing your
files into logical sections. *)
Section True_not_False.

Variable (p : true = false).

Definition P : bool → UU :=
  bool_rect _ unit ∅.

Definition true_eq_false_imp_empty : ∅ :=
  (transportf P p tt).

End True_not_False.

About true_eq_false_imp_empty.

Definition true_not_false : true != false :=
  true_eq_false_imp_empty.

(* Alternative definition, in one shot. *)
Definition true_not_false' : true != false :=
  λ p, transportf (bool_rect _ unit ∅) p tt.

(* Normalization of the proof term. *)
Eval compute in true_not_false.

(** * Sigma types *)

(** Sigma types are called total2 and this is the only example of a
Record in the whole UniMath library. The reason we use a record is so
that we can get the eta principle definitionally. *)

About total2.
Print total2.

(** We have a notation ∑ (x : A), B for Sigma types *)

(** To form a pair use *)
Check tpair.
Locate ",,".

(** and to project out of a pair use *)
Check pr1.
Check pr2.

(** In PartA.v we define the direct product as a Sigma type *)
Definition dirprod (X Y : UU) : UU := ∑ x : X, Y.

Notation "A × B" := (dirprod A B) (at level 75, right associativity) : type_scope.

Definition dirprod_pr1 {X Y : UU} : X × Y → X := pr1.
Definition dirprod_pr2 {X Y : UU} : X × Y → Y := pr2.

Definition dirprodf {X Y X' Y' : UU} (f : X → Y) (f' : X' → Y')
  (xx' : X × X') : Y × Y' := (f (pr1 xx'),,f' (pr2 xx')).

Definition swap {X Y : UU} (xy : X × Y) : Y × X :=
  dirprodf dirprod_pr2 dirprod_pr1 (xy,,xy).

(** We can define the type of even numbers as a Sigma-type: *)
Definition even_nat : UU := ∑ (n : nat), ifbool _ unit empty (even n).

Print even_nat.

Definition test20 : even_nat := (20,,tt).

(** This Definition does not work *)
Fail Definition test3 : even_nat := (3,,tt).

Section curry.

Variables A B C : UU.

(** To make these arguments implicit use:
<<
Context {A B C : UU}.
>>
*)

Definition curry : (A × B → C) → (A → B → C) :=
  λ (f : A × B → C) (a : A) (b : B), f (a,,b).

Definition uncurry : (A → B → C) → (A × B → C) :=
  λ (f : A → B → C) (ab : A × B), f (pr1 ab) (pr2 ab).

End curry.

Check curry.
Print curry.
Check uncurry.
Print uncurry.


(** These were all the basics for interacting with Coq in this
lecture. The UniMath library is a very large library and so far we
have only seen parts of Preamble.v. When writing programs and proofs
in UniMath it is very important to be able to search the library so
that you don't do something someone else has already done. *)

(** To find everything about nat type: *)
Search nat.

(** To search for all lemmas involving the pattern *)
Search _ (_ -> _ -> _).

(** To find information about a notation *)
Locate "+".

(** More information about searching can be found in the reference
manual:

https://coq.inria.fr/distrib/current/refman/proof-engine/vernacular-commands.html?highlight=search#coq:cmd.search
*)

(**

One can also generate HTML documentation for UniMath that is a bit
easier to browse than reading text files. This is done by typing:
<<
> make html
>>
You can then open this documentation in your browser:
<<
> firefox html/toc.html
>>
In order to have your comments display properly in the HTML use the
following format:

(** This comment will be displayed *)
(** * This will be displayed as a section header *)
(** ** This will be a subsection *)

For more details see:

https://coq.inria.fr/distrib/current/refman/tools.html#coqdoc

*)

(**

The UniMath library is organized into a collection of packages that
can be found in the UniMath folder. The library is then compiled using
a Makefile which specifies in which order things has to be compiled
and how they should be compiled.

In order to have your file get compiled when you type "make" add it to
the .package/files file of the package where it belongs. See for
example: UniMath/UniMath/Foundations/.package/files

If you're working on a new package then you need to add it to the
Makefile by writing:

PACKAGES += MyPackage

*)

               (*⋆⋆⋆⋆⋆⋆ THE END ⋆⋆⋆⋆⋆⋆*)