From 6e66d5c76d0b791504e13863228f1deb5ffa3423 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Mon, 29 Jul 2024 17:45:35 -0500 Subject: [PATCH] exercises --- Exercises1.v | 2 +- Lecture1.typ | 2 +- Lol.agda | 39 +++ coq_exercises.v | 190 +++++++++++++ fundamentals_lecture.v | 631 +++++++++++++++++++++++++++++++++++++++++ unimath2024.agda-lib | 2 +- 6 files changed, 863 insertions(+), 3 deletions(-) create mode 100644 Lol.agda create mode 100644 coq_exercises.v create mode 100644 fundamentals_lecture.v diff --git a/Exercises1.v b/Exercises1.v index d9be398..1c50b7d 100644 --- a/Exercises1.v +++ b/Exercises1.v @@ -53,4 +53,4 @@ Show Proof. (* Slide 44, Exercise: neg *) -(* Definition slide44_exercise {A : Type} : not *) \ No newline at end of file +(* Definition slide44_exercise {A : Type} : not *) \ No newline at end of file diff --git a/Lecture1.typ b/Lecture1.typ index af22adf..ca6d03a 100644 --- a/Lecture1.typ +++ b/Lecture1.typ @@ -317,7 +317,7 @@ So $sym(x, x, refl(x)) :defeq refl(x)$ [$unit$], [], [$top$], [$empty$], [], [$bot$], [$A times B$], [cartesian product], [$A and B$], - [$A + B$], [disjoint unions $A B$], [$A or B$], + [$A + B$], [disjoint unions $A product.co B$], [$A or B$], [$A -> B$], [set of functions $A -> B$], [$A => B$], [$x : A tack.r B(x)$], [], [predicate $B$ on $A$], [$sum_(x : A) B(x)$], [], [$exists x in A, B(x)$], diff --git a/Lol.agda b/Lol.agda new file mode 100644 index 0000000..7594ff1 --- /dev/null +++ b/Lol.agda @@ -0,0 +1,39 @@ +{-# OPTIONS --cubical #-} + +open import Cubical.Foundations.Prelude + +data ℕ : Set where + zero : ℕ + suc : ℕ → ℕ + +add : ℕ → ℕ → ℕ +add zero n = n +add (suc m) n = add m (suc n) + +data ℤ₀ : Set where + pos : ℕ → ℤ₀ + negsuc : ℕ → ℤ₀ + +data ℤ : Set where + z : ℕ → ℕ → ℤ + p : (m n : ℕ) → z m n ≡ z (suc m) (suc n) + +ℤ→ℤ₀ : ℤ → ℤ₀ +ℤ→ℤ₀ (z zero zero) = pos zero +ℤ→ℤ₀ (z zero (suc x₁)) = negsuc x₁ +ℤ→ℤ₀ (z (suc x) zero) = pos (suc x) +ℤ→ℤ₀ (z (suc x) (suc x₁)) = ℤ→ℤ₀ (z x x₁) +ℤ→ℤ₀ (p m n i) = ℤ→ℤ₀ {! !} + +ℤ₀→ℤ : ℤ₀ → ℤ +ℤ₀→ℤ (pos x) = z x zero +ℤ₀→ℤ (negsuc x) = z zero (suc x) + +ap : ∀ {A B x y} → (f : A → B) → (x ≡ y) → (f x ≡ f y) +ap f x i = f (x i) + +add-ℤ : ℤ → ℤ → ℤ +add-ℤ (z x x₁) (z x₂ x₃) = z (add x x₂) (add x₁ x₃) +add-ℤ (z x x₁) (p m n i) = z (add x {! !}) {! !} +add-ℤ (p m n i) (z x x₁) = {! !} +add-ℤ (p m n i) (p m₁ n₁ i₁) = {! !} \ No newline at end of file diff --git a/coq_exercises.v b/coq_exercises.v new file mode 100644 index 0000000..2d22337 --- /dev/null +++ b/coq_exercises.v @@ -0,0 +1,190 @@ +(** Exercise sheet for lecture 2: Fundamentals of Coq. + +The goal is to replace all of the "..." by suitable Coq code +satisfying the specification below. + +Written by Anders Mörtberg. +Minor modifications made by Marco Maggesi. + +*) +Require Import UniMath.Foundations.Preamble. + +Definition idfun : forall (A : UU), A -> A := fun (A : UU) (a : A) => a. + +Definition const (A B : UU) (a : A) (b : B) : A := a. + +(** * Booleans *) + +Definition ifbool (A : UU) (x y : A) : bool -> A := + bool_rect (fun _ : bool => A) x y. + +Definition negbool : bool -> bool := + ifbool bool false true. + +Definition andbool (b : bool) : bool -> bool := + ifbool (bool -> bool) (idfun bool) (const bool bool false) b. + +(** Exercise: define boolean or: *) + +Definition orbool (b : bool) : bool -> bool := + ifbool (bool -> bool) (const bool bool true) (idfun bool) b. + +(* This should satisfy: *) +Eval compute in orbool true true. (* true *) +Eval compute in orbool true false. (* true *) +Eval compute in orbool false true. (* true *) +Eval compute in orbool false false. (* false *) + +(** * Natural numbers *) +Definition nat_rec (A : UU) (a : A) (f : nat -> A -> A) : nat -> A := + nat_rect (fun _ : nat => A) a f. + +Definition pred : nat -> nat := nat_rec nat 0 (const nat nat). + +Definition even : nat -> bool := nat_rec bool true (fun _ b => negbool b). + +(** Exercise: define a function odd that tests if a number is odd *) + +Definition odd : nat -> bool := nat_rec bool false (fun _ b => negbool b). + +(* This should satisfy *) +Eval compute in odd 24. (* false *) +Eval compute in odd 19. (* true *) + +(* +Beware of big numbers: [UniMath.Foundations.Preamble] only defines notation up to 24. +*) + +(** Exercise: define a notation "myif b then x else y" for "ifbool _ x y b" +and rewrite negbool and andbool using this notation. *) + +Notation "'myif' b 'then' x 'else' y" := (ifbool _ x y b) (at level 1). + +(** Note that we cannot introduce the notation "if b then x else y" as +this is already used. *) + +Definition negbool' (b : bool) : bool := myif b then false else true. + +(* This should satisfy: *) +Eval compute in negbool' true. (* false *) +Eval compute in negbool' false. (* true *) + +Definition andbool' (b1 b2 : bool) : bool := myif b1 then b2 else false. + +(* This should satisfy: *) +Eval compute in andbool true true. (* true *) +Eval compute in andbool true false. (* false *) +Eval compute in andbool false true. (* false *) +Eval compute in andbool false false. (* false *) + +Definition add (m : nat) : nat -> nat := nat_rec nat m (fun _ y => S y). + +Definition iter (A : UU) (a : A) (f : A → A) : nat → A := + nat_rec A a (λ _ y, f y). + +(* Type space and then \hat to enter the symbol ̂. *) +Notation "f ̂ n" := (λ x, iter _ x f n) (at level 10). + +Definition sub (m n : nat) : nat := pred ̂ n m. + +(** Exercise: define addition using iter and S *) + +Definition add' (m : nat) : nat → nat := iter nat m S. + +(* This should satisfy: *) +Eval compute in add' 4 9. (* 13 *) + +Definition is_zero : nat -> bool := nat_rec bool true (fun _ _ => false). + +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). + +(** Exercises: define <, >, ≤, ≥ *) + +Check nat_rec. + +Definition ltnat (m n : nat) : bool := + nat_rec bool false (fun _ _ => true) (sub n m). +(* Fixpoint ltnat (m n : nat) : bool := + match m with + | O => match n with O => false | S _ => true end + | S m' => match n with O => false | S n' => ltnat m' n' end + end. *) + +Notation "x < y" := (ltnat x y). + +(* This should satisfy: *) +Eval compute in (2 < 3). (* true *) +Eval compute in (3 < 3). (* false *) +Eval compute in (4 < 3). (* false *) + +Definition gtnat (m n : nat) : bool := + nat_rec bool false (fun _ _ => true) (sub m n). + +Notation "x > y" := (gtnat x y). + +(* This should satisfy: *) +Eval compute in (2 > 3). (* false *) +Eval compute in (3 > 3). (* false *) +Eval compute in (4 > 3). (* true *) + +Definition leqnat (m n : nat) : bool := negbool (gtnat m n). + +Notation "x ≤ y" := (leqnat x y) (at level 10). + +(* This should satisfy: *) +Eval compute in (2 ≤ 3). (* true *) +Eval compute in (3 ≤ 3). (* true *) +Eval compute in (4 ≤ 3). (* false *) + +Definition geqnat (m n : nat) : bool := negbool (ltnat m n). + +Notation "x ≥ y" := (geqnat x y) (at level 10). + +(* This should satisfy: *) +Eval compute in (2 ≥ 3). (* false *) +Eval compute in (3 ≥ 3). (* true *) +Eval compute in (4 ≥ 3). (* true *) + +(** * Coproduct and integers *) + +Definition coprod_rec {A B C : UU} (f : A → C) (g : B → C) : A ⨿ B → C := + @coprod_rect A B (λ _, C) f g. + +Definition Z : UU := coprod nat nat. + +Notation "⊹ x" := (inl x) (at level 20). +Notation "─ x" := (inr x) (at level 40). + +Definition Z1 : Z := ⊹ 1. +Definition Z0 : Z := ⊹ 0. +Definition Zn3 : Z := ─ 2. + +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). + +(** Exercise (harder): define addition for Z *) + +Definition Zdiff : nat -> nat -> Z := fun x y => + if x > y then inl (sub x y) + else (if x < y then inr (sub y x) else inl O). + +Definition Zadd : Z -> Z -> Z := + fun x y => Zcase (Z -> Z) + (fun x' => Zcase Z (fun y' => inl (add x' y')) (fun y' => Zdiff x' y')) + (fun x' => Zcase Z (fun y' => Zdiff y' x') (fun y' => inr (S (add x' y')))) + x y. + +(* This should satisfy: *) +Eval compute in Zadd Z0 Z0. (* ⊹ 0 *) +Eval compute in Zadd Z1 Z1. (* ⊹ 2 *) +Eval compute in Zadd Z1 Zn3. (* ─ 1 *) (* recall that negative numbers are off-by-one *) +Eval compute in Zadd Zn3 Z1. (* ─ 1 *) +Eval compute in Zadd Zn3 Zn3. (* ─ 5 *) +Eval compute in Zadd (Zadd Zn3 Zn3) Zn3. (* ─ 8 *) +Eval compute in Zadd Z0 (negate (Zn3)). (* ⊹ 3 *) diff --git a/fundamentals_lecture.v b/fundamentals_lecture.v new file mode 100644 index 0000000..6e07cf1 --- /dev/null +++ b/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/unimath2024.agda-lib b/unimath2024.agda-lib index b053ed9..57f2676 100644 --- a/unimath2024.agda-lib +++ b/unimath2024.agda-lib @@ -1,2 +1,2 @@ -depend: agda-unimath +depend: agda-unimath cubical include: . \ No newline at end of file