(* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *) Inductive paths {A : Type} (a : A) : A -> Type := | idpath : paths a a. Infix "=" := paths. Infix "=" := paths : type_scope. Arguments idpath {A a}. Hint Resolve idpath. (* Program a boolean test of equality eq_nat : nat -> nat -> bool *) Fixpoint eq_nat (n m : nat) : bool := match n, m with |O, O => true |S k, S l => eq_nat k l |_, _ => false end. (* Prove the following lemma. There is a (small) trick. *) Lemma eq_nat_eq (n m : nat) : eq_nat n m = true -> n = m. Proof. revert m. induction n as [|n ihn], m. - intros ?. apply idpath. - simpl. intros. inversion H. - simpl; intros. inversion H. - simpl. intros e. rewrite (ihn _ e). apply idpath. Qed. Section HowToExplainLogicalLaws. Variable T : Type. (* A type which depends on T *) Variable P : T -> Type. (* f is an inhabitant of a dependent product type *) Variable f : forall x : T, P x. (* Dependent sums in Coq *) (* In order to forge new inhabitants: *) Check existT. (* In order to project the pair on its first component: *) Check projT1. (* In order to project the pair on its second component: *) Check projT2. (* Let us have a try: *) (* (sigT B) is denoted {x : A & B x} *) Definition sig_witness {T} {P : T -> Type} (t : T) (ht : P t) : {x : T & P x} := existT _ t ht. About sig_witness. (* The type of disjoint sums *) Inductive disjoint_sum (A B : Type) : Type := |in_left : A -> disjoint_sum A B |in_right : B -> disjoint_sum A B. Inductive Empty : Set :=. Inductive Unit : Set := tt : Unit. Lemma Empty_elim (R : Type) : Empty -> R. Proof. intros x. case x. Qed. Definition Not (T : Type) := T -> Empty. (* Now we can start our definitions *) Definition prop (T : Type) := forall x y : T, x = y. Definition set (T : Type) := forall x y : T, prop (x = y). End HowToExplainLogicalLaws. Section RulesForEquality. Variables A : Type. (* We dispose of Martin-Löf's proposal for equality: *) Check (@paths A). Check (@idpath A). Check (@paths_ind A). (* Let us prove the 'vacuum cleaner power chord' principle *) Definition Sing (a : A) := {x : A & a = x}. (* Let us check that (a, eq_refl) is in *) Variable a : A. Check (existT _ a idpath : Sing a). Definition sing_elt (x : A) (p : a = x) : Sing a := existT _ x p. Remark vacuum_cleaner_power_chord : forall z : Sing a, z = sing_elt a idpath. Proof. intros z. red in z. case z as [x p]. unfold sing_elt. (* The 'destruct' tactic realizes the 'retraction' of the path *) destruct p. exact idpath. Qed. Lemma Sing_prop : prop (Sing a). Proof. intros x y. rewrite (vacuum_cleaner_power_chord x). rewrite (vacuum_cleaner_power_chord y). exact idpath. Qed. End RulesForEquality. Section ConstructiveMathematics. Definition decidable (T : Type) := disjoint_sum T (Not T). Definition discrete (T : Type) := forall x y : T, decidable (x = y). Proposition discrete_Empty : discrete Empty. Proof. intros x y. case x. Qed. Proposition discrete_Unit : discrete Unit. Proof. intros x y. case x. case y. apply in_left. exact idpath. Qed. (* N2 is bool *) (* Boolean negation *) Definition eqb (b1 b2 : bool) : bool := match b1, b2 with |true, true | false, false => true |_, _ => false end. Lemma eq_eqbP (b1 b2 : bool) : b1 = b2 -> eqb b1 b2 = true. Proof. case b1; case b2; simpl; trivial; intros H; inversion H. Qed. Lemma eqb_eqP (b1 b2 : bool) : eqb b1 b2 = true -> b1 = b2. Proof. case b1; case b2; simpl; trivial; intros H; inversion H. Qed. Proposition discrete_bool : discrete bool. Proof. intros b1 b2. generalize (idpath (a:=eqb b1 b2)). destruct (eqb b1 b2) at 2; intros eb12. - apply in_left. apply eqb_eqP. exact eb12. - apply in_right. intros e. rewrite (eq_eqbP _ _ e) in eb12. inversion eb12. Qed. Scheme paths_elim := Minimality for paths Sort Type. (* What is the discriminate tactic doing? *) Definition bool_discriminate (T : Type) : true = false -> T. intros h. apply Empty_elim. About paths_elim. pose (C := (fun (b : bool) => if b then Unit else Empty) : bool -> Type). About paths_elim. exact (paths_elim _ true C tt false h). Qed. (* The previous proof can be adapted to any equality between two terms presenting distinct head constructors. *) Lemma not_prop_bool : Not (prop bool). Proof. intros p. pose (h := p true false). apply bool_discriminate. exact h. Qed. (* All these proofs are in fact instances of the same pattern *) Section DiscreteFromBoolEq. Variable T : Type. Variable eqT : T -> T -> bool. Hypothesis eq_eqTP : forall t1 t2 : T, t1 = t2 -> eqT t1 t2 = true. Hypothesis eqT_eqP : forall t1 t2 : T, eqT t1 t2 = true -> t1 = t2. Proposition discrete_bool_eq : discrete T. Proof. intros t1 t2. generalize (idpath(a:=eqT t1 t2)). destruct (eqT t1 t2) at 2; intros et12. - apply in_left. apply eqT_eqP. exact et12. - apply in_right. intros e. rewrite (eq_eqTP _ _ e) in et12. inversion et12. Qed. End DiscreteFromBoolEq. Lemma eq_eq_natP (n1 n2 : nat) : n1 = n2 -> eq_nat n1 n2 = true. Proof. revert n2. induction n1 as [|n1 ihn1]; case n2 as [| n2]; simpl; trivial. - intros H; inversion H. - intros H; inversion H. - intros h. apply ihn1. inversion h. reflexivity. Qed. Lemma eq_nat_eqP (n1 n2 : nat) : eq_nat n1 n2 = true -> n1 = n2. revert n2. induction n1 as [|n1 ihn1]; case n2 as [| n2]; simpl; trivial. - intros H; inversion H. - intros H; inversion H. - intros h. rewrite (ihn1 n2); trivial. Qed. Proposition discrete_nat : discrete nat. Proof. exact (discrete_bool_eq _ _ eq_eq_natP eq_nat_eqP). Qed. End ConstructiveMathematics. Section GroupoidProps. Definition mapOnPaths {A B : Type} {x y : A} (f : A -> B) : x = y -> f x = f y. Proof. intros p. destruct p. exact idpath. Defined. (* These two terms are convertible *) Remark mapOnPaths1 {A B : Type} (f : A -> B) (x : A) : mapOnPaths f (@idpath A x) = idpath. Proof. compute. exact idpath. Qed. Context {A : Type}. Definition comp {a b : A} (p : a = b) {c : A} (q : b = c) : a = c. Proof. destruct p. exact q. Defined. Remark comp1p {a b : A} (p : a = b) : comp idpath p = p. Proof. compute. exact idpath. Qed. Remark compp1 {a b : A} (p : a = b) : comp p idpath = p. Proof. case p. exact idpath. Qed. Lemma comp_simpl {a b} (r : a = b) {c : A} (p q : b = c) : comp r p = comp r q -> p = q. destruct r. compute. intros h. exact h. Qed. End GroupoidProps. Section Hedberg. Variable A : Type. Lemma lemma1 (f : forall x y : A, x = y -> x = y) (x y : A) (p : x = y) : f _ _ p = comp (f _ _ idpath) p. Proof. destruct p. rewrite compp1. exact idpath. Qed. Definition contr_im {C : Type} (f : C -> C) := forall x y : C, f x = f y. Lemma lemma2 (C : Type) (h : decidable C) : {f : C -> C & contr_im f}. Proof. case h as [c | nC]. - exists (fun x => c). intros u v; exact idpath. - exists (fun x : C => Empty_elim _ (nC x)). exact (fun x : C => Empty_elim _ (nC x)). Qed. Theorem Hedberg : discrete A -> set A. Proof. intros hdiscr a b p q. assert (h : forall (x y : A), {f : x = y -> x = y & contr_im f}). intros x y. apply lemma2. exact (hdiscr x y). pose (g x y := projT1 (h x y)). assert (hgpq : g _ _ p = g _ _ q). apply (projT2 (h a b)). assert (e : comp (g a a idpath) p = comp (g a a idpath) q). pose (hg1 := (lemma1 g a b p)). rewrite <- hg1. pose (hg2 := (lemma1 g a b q)). rewrite <- hg2. exact hgpq. exact (comp_simpl _ p q e). Qed. End Hedberg. Section Equivalence. Section EquivDef. Definition fiber {A B : Type} (f : A -> B) (b : B) := {x : A & f x = b}. Record is_contr (T : Type) := IsContr { contr_elt : T; contr_eltE : prop T}. (* Alternative definition of equivalence *) Definition is_equiv {A B : Type} (f : A -> B) := forall b : B, is_contr (fiber f b). Definition equiv (A B : Type) := {f : A -> B & is_equiv f}. Lemma id_is_equiv (A : Type) : is_equiv (fun x : A => x). Proof. intros a. apply IsContr. - pose (w := existT _ a idpath : fiber (fun x : A => x) a). exact w. - intros p q. case p as [x pax]. case q as [y pay]. destruct pax. destruct pay. apply idpath. Qed. Definition is_section {A B : Type} (f : A -> B) (g : B -> A) := forall b : B, f (g b) = b. Lemma equiv_section (A B : Type) (f : A -> B) : is_equiv f -> {g : B -> A & is_section f g}. Proof. intros hequiv. pose (g := fun b => projT1 (contr_elt _ (hequiv b))). exists g. intros b. exact (projT2 (contr_elt _ (hequiv b))). Qed. Definition univalence_fun {A B : Type} (p : A = B) : equiv A B. Proof. destruct p. exists (fun x : A => x). exact (id_is_equiv A). Defined. Definition univalence (A B : Type) := is_equiv (@univalence_fun A B). Definition is_retract {A B : Type} (f : A -> B) (g : B -> A) := forall x, g (f x) = x. Section CoherentToEquiv. Context {A B : Type}. Variables (f : A -> B) (g : B -> A). Hypothesis hsection : is_section g f. Hypothesis hretract : is_retract g f. Hypothesis hcoherent : forall x, hretract (f x) = mapOnPaths f (hsection x). Lemma coherent_is_equiv : is_equiv f. Proof. intros b. assert (alt_contr : {a : fiber f b & forall x, x = a}). pose (w := sig_witness (g b) (hretract b) : fiber f b). exists w; intros x; case x as [a ha]. destruct ha. unfold w, sig_witness. rewrite hcoherent. destruct (hsection a). exact idpath. case alt_contr as [a ha]. apply IsContr. - exact a. - intros p q. rewrite (ha p). rewrite (ha q). apply idpath. Qed. End CoherentToEquiv.