From 53e38f023892c3a67911c8dbb9e7639f30ece2d1 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Wed, 2 Aug 2017 17:08:40 +0200 Subject: [PATCH 1/2] Try out HoTTClasses --- FiniteSets/_CoqProject | 2 + FiniteSets/classes.v | 182 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 184 insertions(+) create mode 100644 FiniteSets/classes.v diff --git a/FiniteSets/_CoqProject b/FiniteSets/_CoqProject index 49624cd..3c9a5d1 100644 --- a/FiniteSets/_CoqProject +++ b/FiniteSets/_CoqProject @@ -1,7 +1,9 @@ -R . "" COQC = hoqc COQDEP = hoqdep -R ../prelude "" +-R ../../HoTTClasses/theories HoTTClasses lattice.v disjunction.v +classes.v representations/bad.v representations/definition.v representations/cons_repr.v diff --git a/FiniteSets/classes.v b/FiniteSets/classes.v new file mode 100644 index 0000000..cf16938 --- /dev/null +++ b/FiniteSets/classes.v @@ -0,0 +1,182 @@ +Require Import HoTT. +From HoTTClasses Require Import interfaces.abstract_algebra tactics.ring_tac. + +Section hProp_lattice. +Context `{Univalence}. + +Definition lor (X Y : hProp) : hProp := BuildhProp (Trunc (-1) (sum X Y)). +Definition land (P Q : hProp) := BuildhProp (prod P Q). +Global Instance join_hprop : Join hProp := lor. +Global Instance meet_hprop : Meet hProp := land. +Global Instance land_associative : Associative land. +Proof. + intros P Q R. + apply path_hprop. + apply equiv_prod_assoc. +Defined. +Global Instance lor_associative : Associative lor. +Proof. + intros P Q R. symmetry. + apply path_iff_hprop ; cbn. + * simple refine (Trunc_ind _ _). + intros [xy | z] ; cbn. + + simple refine (Trunc_ind _ _ xy). + intros [x | y]. + ++ apply (tr (inl x)). + ++ apply (tr (inr (tr (inl y)))). + + apply (tr (inr (tr (inr z)))). + * simple refine (Trunc_ind _ _). + intros [x | yz] ; cbn. + + apply (tr (inl (tr (inl x)))). + + simple refine (Trunc_ind _ _ yz). + intros [y | z]. + ++ apply (tr (inl (tr (inr y)))). + ++ apply (tr (inr z)). +Defined. + +Global Instance land_commutative : Commutative land. +Proof. + intros P Q. + apply path_hprop. + apply equiv_prod_symm. +Defined. + +Global Instance lor_commutative : Commutative lor. +Proof. + intros P Q. symmetry. + apply path_iff_hprop ; cbn. + * simple refine (Trunc_ind _ _). + intros [x | y]. + + apply (tr (inr x)). + + apply (tr (inl y)). + * simple refine (Trunc_ind _ _). + intros [y | x]. + + apply (tr (inr y)). + + apply (tr (inl x)). +Defined. + +Global Instance joinsemilattice_hprop : JoinSemiLattice hProp. +Proof. + split. + - split; [ split | ]; apply _. + - compute-[lor]. intros P. + apply path_iff_hprop ; cbn. + + simple refine (Trunc_ind _ _). + intros [x | x] ; apply x. + + apply (fun x => tr (inl x)). +Defined. + +Global Instance meetsemilattice_hprop : MeetSemiLattice hProp. +Proof. + split. + - split; [ split | ]; apply _. + - compute-[land]. intros x. + apply path_iff_hprop ; cbn. + + intros [a b] ; apply a. + + intros a ; apply (pair a a). +Defined. + +Global Instance lor_land_absorbtion : Absorption join meet. +Proof. +intros P Q. +apply path_iff_hprop ; cbn. +- intros X ; strip_truncations. + destruct X as [Xx | [Xy1 Xy2]] ; assumption. +- intros X. + apply (tr (inl X)). +Defined. + +Global Instance land_lor_absorbtion : Absorption meet join. +Proof. +intros P Q. +apply path_iff_hprop ; cbn. +- intros [X Y] ; strip_truncations. + assumption. +- intros X. + split. + * assumption. + * apply (tr (inl X)). +Defined. + +Global Instance hprop_lattice : Lattice hProp. +Proof. split; apply _. Defined. + +End hProp_lattice. + +(* Section lattice_semiring. *) +(* Context `{A : Type}. *) +(* Context `{Lattice A}. *) +(* Context `{Bottom A}. *) +(* Instance join_plus : Plus A := join. *) +(* Instance meet_plus : Mult A := meet. *) +(* Instance bot_zero : Zero A := bottom. *) + +(* End lattice_semiring. *) + +Create HintDb lattice_hints. +Hint Resolve associativity : lattice_hints. +Hint Resolve commutativity : lattice_hints. +Hint Resolve absorption : lattice_hints. +Hint Resolve idempotency : lattice_hints. + +Section fun_lattice. + Context {A B : Type}. + Context `{Univalence}. + Context `{Lattice B}. + + Definition max_fun (f g : (A -> B)) (a : A) : B + := f a ⊔ g a. + + Definition min_fun (f g : (A -> B)) (a : A) : B + := f a ⊓ g a. + + Global Instance fun_join : Join (A -> B) := max_fun. + Global Instance fun_meet : Meet (A -> B) := min_fun. + + Ltac solve_fun := + compute ; intros ; apply path_forall ; intro ; + eauto 10 with lattice_hints typeclass_instances. + + Global Instance fun_lattice : Lattice (A -> B). + Proof. + repeat (split; try (apply _ || solve_fun)). + Defined. +End fun_lattice. + +Section sub_lattice. + Context {A : Type} {P : A -> hProp}. + Context `{Lattice A}. + Context {Hmax : forall x y, P x -> P y -> P (join x y)}. + Context {Hmin : forall x y, P x -> P y -> P (meet x y)}. + + Definition AP : Type := sig P. + + Instance join_sub : Join AP := fun (x y : AP) => + match x, y with + | (a ; pa), (b ; pb) => + (join a b ; Hmax a b pa pb) + end. + + Instance meet_sub : Meet AP := fun (x y : AP) => + match x, y with + | (a ; pa), (b ; pb) => + (meet a b ; Hmin a b pa pb) + end. + + Local Instance hprop_sub : forall c, IsHProp (P c). + Proof. + apply _. + Defined. + + Ltac solve_sub := + repeat (intros [? ?]) + ; simple refine (path_sigma _ _ _ _ _); [ | apply hprop_sub ] + ; compute + ; eauto 10 with lattice_hints typeclass_instances. + + Global Instance sub_lattice : Lattice AP. + Proof. + repeat (split; try (apply _ || solve_sub)). + Defined. + +End sub_lattice. From a61265585b2d30df288f8a94bb5125950348cb42 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Wed, 2 Aug 2017 21:58:26 +0200 Subject: [PATCH 2/2] Start proving that Mod2 is a semiring --- int/Mod2.v | 192 ++++++++++++++++++++++++++++++++++++++++++++++++ int/Mod2_ring.v | 13 ++++ int/_CoqProject | 5 ++ 3 files changed, 210 insertions(+) create mode 100644 int/Mod2.v create mode 100644 int/Mod2_ring.v create mode 100644 int/_CoqProject diff --git a/int/Mod2.v b/int/Mod2.v new file mode 100644 index 0000000..401637f --- /dev/null +++ b/int/Mod2.v @@ -0,0 +1,192 @@ +Require Export HoTT. +Require Import HitTactics. + +Module Export modulo. + +Private Inductive Mod2 : Type0 := + | Z : Mod2 + | succ : Mod2 -> Mod2. + +Axiom mod : Z = succ(succ Z). + +Fixpoint Mod2_ind + (P : Mod2 -> Type) + (a : P Z) + (s : forall (n : Mod2), P n -> P (succ n)) + (mod' : mod # a = s (succ Z) (s Z a)) + (x : Mod2) + {struct x} + : P x + := + (match x return _ -> P x with + | Z => fun _ => a + | succ n => fun _ => s n ((Mod2_ind P a s mod') n) + end) mod'. + +Axiom Mod2_ind_beta_mod : forall + (P : Mod2 -> Type) + (a : P Z) + (s : forall (n : Mod2), P n -> P (succ n)) + (mod' : mod # a = s (succ Z) (s Z a)) + , apD (Mod2_ind P a s mod') mod = mod'. + +Fixpoint Mod2_rec + (P : Type) + (a : P) + (s : P -> P) + (mod' : a = s (s a)) + (x : Mod2) + {struct x} + : P + := + (match x return _ -> P with + | Z => fun _ => a + | succ n => fun _ => s ((Mod2_rec P a s mod') n) + end) mod'. + +Axiom Mod2_rec_beta_mod : forall + (P : Type) + (a : P) + (s : P -> P) + (mod' : a = s (s a)) + , ap (Mod2_rec P a s mod') mod = mod'. + +Instance: HitRecursion Mod2 := { + indTy := _; recTy := _; + H_inductor := Mod2_ind; + H_recursor := Mod2_rec }. + +End modulo. + +Definition negate : Mod2 -> Mod2. +Proof. +hrecursion. +- apply Z. +- intros. apply (succ H). +- simpl. apply mod. +Defined. + + +Definition Bool_to_Mod2 : Bool -> Mod2. +Proof. +intro b. +destruct b. ++ apply (succ Z). ++ apply Z. +Defined. + +Definition Mod2_to_Bool : Mod2 -> Bool. +Proof. +intro x. +hrecursion x. +- exact false. +- exact negb. +- simpl. reflexivity. +Defined. + +Theorem eq1 : forall n : Bool, Mod2_to_Bool (Bool_to_Mod2 n) = n. +Proof. +intro b. +destruct b; compute; reflexivity. +Qed. + +Theorem Bool_to_Mod2_negb : forall x : Bool, + succ (Bool_to_Mod2 x) = Bool_to_Mod2 (negb x). +Proof. +intros. +destruct x; compute. ++ apply mod^. ++ apply reflexivity. +Defined. + +Theorem eq2 : forall n : Mod2, Bool_to_Mod2 (Mod2_to_Bool n) = n. +Proof. +intro n. +hinduction n. +- reflexivity. +- intros n IHn. + symmetry. etransitivity. apply (ap succ IHn^). + etransitivity. apply Bool_to_Mod2_negb. + hott_simpl. +- rewrite @HoTT.Types.Paths.transport_paths_FlFr. + hott_simpl. + rewrite ap_compose. + enough (ap Mod2_to_Bool mod = idpath). + + rewrite X. hott_simpl. + + apply (Mod2_rec_beta_mod Bool false negb 1). +Defined. + +Theorem adj : + forall x : Mod2, eq1 (Mod2_to_Bool x) = ap Mod2_to_Bool (eq2 x). +Proof. +intro x. +apply hset_bool. +Defined. + +Instance: IsEquiv Mod2_to_Bool. +Proof. +apply (BuildIsEquiv Mod2 Bool Mod2_to_Bool Bool_to_Mod2 eq1 eq2 adj). +Qed. + +Definition Mod2_value : Mod2 <~> Bool := BuildEquiv _ _ Mod2_to_Bool _. + +Instance mod2_hset : IsHSet Mod2. +Proof. +apply (trunc_equiv Bool Mod2_value^-1). +Defined. + +Theorem modulo2 : forall n : Mod2, n = succ(succ n). +Proof. +hinduction. +- apply mod. +- intros n p. + apply (ap succ p). +- apply set_path2. +Defined. + +Definition plus : Mod2 -> Mod2 -> Mod2. +Proof. +intros n. +hrecursion. +- exact n. +- apply succ. +- apply modulo2. +Defined. + +Lemma plus_x_Z_x : forall x, plus x Z = x. +Proof. +hinduction; cbn. +- reflexivity. +- intros n. refine (ap succ). +- apply set_path2. +Defined. + +Lemma plus_S_x_S : forall x y, + plus (succ x) y = succ (plus x y). +Proof. +intros x. +hinduction; cbn. +- reflexivity. +- intros n Hn. refine (ap succ Hn). +- apply set_path2. +Defined. + +Lemma plus_x_x_Z : forall x, plus x x = Z. +Proof. +hinduction. +- reflexivity. +- intros n Hn. cbn. + refine (ap succ (plus_S_x_S n n) @ _). + refine (ap (succ o succ) Hn @ _). + apply mod^. +- apply set_path2. +Defined. + +Definition mult : Mod2 -> Mod2 -> Mod2. +intros x. hrecursion. +- exact Z. +- intros y. exact (plus x y). +- simpl. + refine (_ @ ap (plus x) (plus_x_Z_x _)^). + apply (plus_x_x_Z x)^. +Defined. diff --git a/int/Mod2_ring.v b/int/Mod2_ring.v new file mode 100644 index 0000000..4900716 --- /dev/null +++ b/int/Mod2_ring.v @@ -0,0 +1,13 @@ +Require Import HoTT HitTactics. +Require Export Mod2. + +From HoTTClasses Require Import interfaces.abstract_algebra tactics.ring_tac. + +Section Mod2_ring. + +Instance Mod2_plus : Plus Mod2 := Mod2.plus. +Instance Mod2_mult : Mult Mod2 := Mod2.mult. +Instance Mod2_zero : Zero Mod2 := Z. +Instance Mod2_one : One Mod2 := succ Z. + +End Mod2_ring. diff --git a/int/_CoqProject b/int/_CoqProject new file mode 100644 index 0000000..6c766a7 --- /dev/null +++ b/int/_CoqProject @@ -0,0 +1,5 @@ +-R . "" COQC = hoqc COQDEP = hoqdep +-R ../prelude "" +-R ../../HoTTClasses/theories HoTTClasses +Mod2.v +Mod2_ring.v