Merge branch 'classes' of https://github.com/nmvdw/HITs-Examples into classes

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

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.

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.

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.

int/_CoqProject

@@ -0,0 +1,5 @@
+-R . "" COQC = hoqc COQDEP = hoqdep
+-R ../prelude ""
+-R ../../HoTTClasses/theories HoTTClasses
+Mod2.v
+Mod2_ring.v