diff --git a/2024-07-Minneapolis/2_Coq/Fundamentals_Coq.pdf b/2024-07-Minneapolis/2_Coq/Fundamentals_Coq.pdf new file mode 100644 index 0000000..e76d635 Binary files /dev/null and b/2024-07-Minneapolis/2_Coq/Fundamentals_Coq.pdf differ diff --git a/2024-07-Minneapolis/2_Coq/fundamentals_lecture.v b/2024-07-Minneapolis/2_Coq/fundamentals_lecture.v new file mode 100644 index 0000000..6e07cf1 --- /dev/null +++ b/2024-07-Minneapolis/2_Coq/fundamentals_lecture.v @@ -0,0 +1,631 @@ +(** + +<< + 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 ⋆⋆⋆⋆⋆⋆*) diff --git a/README.md b/README.md index d7e06c6..0015a74 100644 --- a/README.md +++ b/README.md @@ -5,6 +5,10 @@ ### Lecture 1: Type Theory (by Paige Randall North) - [Lecture](2024-07-Minneapolis/1_Type-Theory/minneapolis_lecture_1.pdf) +### Lecture 2: Type Theory (by Niels van der Weide) +- [Lecture](2024-07-Minneapolis/2_Coq/Fundamentals_Coq.pdf) +- [Coq file](2024-07-Minneapolis/2_Coq/fundamentals_lecture.v) + ## School on Univalent Mathematics, Cortona, 2022