From 44da34d72fe45737b64ef90f914c72fea4b4f3d9 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@covariant.me>
Date: Thu, 18 May 2017 17:43:19 +0200
Subject: [PATCH 1/8] Add a general hit recursion tactic.

The tactic resolves the induction principle for a HIT
using Canonical Structures, following the suggestion of @gallais
---
 FinSets.v    | 180 ++++++++++++++++++---------------------------------
 HitTactics.v |  72 +++++++++++++++++++++
 Mod2.v       |  60 ++++++++---------
 _CoqProject  |   1 +
 4 files changed, 162 insertions(+), 151 deletions(-)
 create mode 100644 HitTactics.v

diff --git a/FinSets.v b/FinSets.v
index 3b9d2c0..6bbeafc 100644
--- a/FinSets.v
+++ b/FinSets.v
@@ -1,5 +1,5 @@
-Require Import HoTT.
 Require Export HoTT.
+Require Import HitTactics.
 
 Module Export FinSet.
 
@@ -45,6 +45,10 @@ Fixpoint FinSets_rec
            (FinSets_rec A P e l u assocP commP nlP nrP idemP z)
       end) assocP commP nlP nrP idemP.
 
+Definition FinSetsCL A : HitRec.class (FinSets A) _ := 
+   HitRec.Class (FinSets A) (fun x P e l u aP cP lP rP iP => FinSets_rec A P e l u aP cP lP rP iP x).
+Canonical Structure FinSetsTy A : HitRec.type := HitRec.Pack _ _ (FinSetsCL A).
+
 Axiom FinSets_beta_assoc : forall
   (A : Type)
   (P : Type)
@@ -133,129 +137,66 @@ Axiom FinSets_beta_idem : forall
   idemP x.
 End FinSet.
 
-Definition isIn : forall 
-  (A : Type)
-  (eq : A -> A -> Bool),
-  A -> FinSets A -> Bool.
+Section functions.
+Parameter A : Type.
+Parameter eq : A -> A -> Bool.
+Definition isIn : A -> FinSets A -> Bool.
 Proof.
-intro A.
-intro eq.
-intro a.
-refine (FinSets_rec A _ _ _ _ _ _ _ _ _).
-  Unshelve.
-
-  Focus 6.
-  apply false.
-
-  Focus 6.
-  intro a'.
-  apply (eq a a').
-
-  Focus 6.
-  intro b.
-  intro b'.
-  apply (orb b b').
-
-  Focus 3.
-  intros.
-  compute.
-  reflexivity.
-
-  Focus 1.
-  intros.
-  compute.
-  destruct x.
-  reflexivity.
-  destruct y.
-  reflexivity.
-  reflexivity.
-
-  Focus 1.
-  intros.
-  compute.
-  destruct x.
-  destruct y.
-  reflexivity.
-  reflexivity.
-  destruct y.
-  reflexivity.
-  reflexivity.
-
-  Focus 1.
-  intros.
-  compute.
-  destruct x.
-  reflexivity.
-  reflexivity.
-
-  intros.
-  compute.
-  destruct (eq a x).
-  reflexivity.
-  reflexivity.
+intros a X.
+hrecursion X.
+- exact false.
+- intro a'. apply (eq a a').
+- apply orb. 
+- intros x y z. compute. destruct x; reflexivity.
+- intros x y. compute. destruct x, y; reflexivity.
+- intros x. compute. reflexivity. 
+- intros x. compute. destruct x; reflexivity.
+- intros a'. compute. destruct (eq a a'); reflexivity.
 Defined.
 
-Definition comprehension : forall
-  (A : Type)
-  (eq : A -> A -> Bool),
+
+Definition comprehension : 
   (A -> Bool) -> FinSets A -> FinSets A.
 Proof.
-intro A.
-intro eq.
-intro phi.
-refine (FinSets_rec A _ _ _ _ _ _ _ _ _).
-  Unshelve.
-
-  Focus 6.
-  apply empty.
-
-  Focus 6.
-  intro a.
-  apply (if (phi a) then L A a else (empty A)).
-
-  Focus 6.
-  intro x.
-  intro y.
-  apply (U A x y).
-
-  Focus 3.
-  intros.
-  compute.
-  apply nl.
-
-  Focus 1.
-  intros.
-  compute.
-  apply assoc.
-
-  Focus 1.
-  intros.
-  compute.
-  apply comm.
-
-  Focus 1.
-  intros.
-  compute.
-  apply nr.
-
-  intros.
-  compute.
-  destruct (phi x).
-  apply idem.
-  apply nl.
+intros P X.
+hrecursion X.
+- apply empty.
+- intro a.
+  refine (if (P a) then L A a else empty A).
+- intros X Y.
+  apply (U A X Y).
+- intros. cbv. apply assoc.
+- intros. cbv. apply comm.
+- intros. cbv. apply nl.
+- intros. cbv. apply nr.
+- intros. cbv. 
+  destruct (P x); simpl.
+  + apply idem.
+  + apply nl.
 Defined.
 
-Definition intersection : forall (A : Type) (eq : A -> A -> Bool), 
+Definition intersection : 
   FinSets A -> FinSets A -> FinSets A.
 Proof.
-intro A.
-intro eq.
-intro x.
-intro y.
-apply (comprehension A eq (fun (a : A) => isIn A eq a x) y).
+intros X Y.
+apply (comprehension (fun (a : A) => isIn a X) Y).
 Defined.
 
-Definition subset (A : Type) (eq : A -> A -> Bool) (x : FinSets A) (y : FinSets A) : Bool.
+Definition subset (x : FinSets A) (y : FinSets A) : Bool.
+Proof.
+hrecursion x.
+- apply true.
+- intro a. apply (isIn a y).
+- apply andb.
+- intros a b c. compute. destruct a; reflexivity.
+- intros a b. compute. destruct a, b; reflexivity.
+- intros x. compute. reflexivity.
+- intros x. compute. destruct x;reflexivity.
+- intros a. simpl. 
+  destruct (isIn a y); reflexivity.
+Defined.
+
+Definition subset' (x : FinSets A) (y : FinSets A) : Bool.
 Proof.
 refine (FinSets_rec A _ _ _ _ _ _ _ _ _ _).
   Unshelve.
@@ -268,7 +209,7 @@ refine (FinSets_rec A _ _ _ _ _ _ _ _ _ _).
 
   Focus 6.
   intro a.
-  apply (isIn A eq a y).
+  apply (isIn a y).
 
   Focus 6.
   intro b.
@@ -308,15 +249,16 @@ refine (FinSets_rec A _ _ _ _ _ _ _ _ _ _).
   reflexivity.
 
   intros.
-  destruct (isIn A eq x0 y).
+  destruct (isIn x0 y).
   compute.
   reflexivity.
   compute.
   reflexivity.
 Defined.
+(* TODO: subset = subset' *)
 
-Definition equal_set (A : Type) (eq : A -> A -> Bool) (x : FinSets A) (y : FinSets A) : Bool
-  := andb (subset A eq x y) (subset A eq y x).
+Definition equal_set (x : FinSets A) (y : FinSets A) : Bool
+  := andb (subset x y) (subset y x).
 
 Fixpoint eq_nat n m : Bool :=
   match n, m with
@@ -324,4 +266,6 @@ Fixpoint eq_nat n m : Bool :=
     | O, S _ => false
     | S _, O => false
     | S n1, S m1 => eq_nat n1 m1
-  end.
\ No newline at end of file
+  end.
+
+End functions.
\ No newline at end of file
diff --git a/HitTactics.v b/HitTactics.v
new file mode 100644
index 0000000..d43f35b
--- /dev/null
+++ b/HitTactics.v
@@ -0,0 +1,72 @@
+Module HitRec.
+Record class (H : Type) (* The HIT type itself *)
+             (recTy : H -> Type) (* The type of the recursion principle *)
+             := Class { recursion_term : forall (x : H), recTy x }.
+Structure type := Pack { obj : Type ; rec : obj -> Type ; class_of : class obj rec }.
+Definition hrecursion (e : type) : forall x, rec e x :=
+  let 'Pack _ _ (Class r) := e
+  in r.
+Arguments hrecursion {e} x : simpl never.
+Arguments Class H {recTy} recursion_term.
+End HitRec.
+
+Ltac hrecursion_ target :=
+  generalize dependent target;
+  match goal with
+  | [ |- forall target, ?P] => intro target;
+    match type of (HitRec.hrecursion target) with
+    | ?Q => 
+      match (eval simpl in Q) with
+      | forall Y , Y target =>
+        simple refine (HitRec.hrecursion target (fun target => P) _)
+      | forall Y _, Y target  =>
+        simple refine (HitRec.hrecursion target (fun target => P) _)
+      | forall Y _ _, Y target  =>
+        simple refine (HitRec.hrecursion target (fun target => P) _ _)
+      | forall Y _ _ _, Y target  =>
+        let hrec:=(eval hnf in (HitRec.hrecursion target)) in
+        simple refine (hrec (fun target => P) _ _ _)
+      | forall Y _ _ _ _, Y target  =>
+        simple refine (HitRec.hrecursion target (fun target => P) _ _ _ _)
+      | forall Y _ _ _ _ _, Y target  =>
+        simple refine (HitRec.hrecursion target (fun target => P) _ _ _ _ _)
+      | forall Y _ _ _ _ _ _, Y target  =>
+        simple refine (HitRec.hrecursion target (fun target => P) _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _, Y target  =>
+        simple refine (HitRec.hrecursion target (fun target => P) _ _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _, Y target  =>
+        simple refine (HitRec.hrecursion target (fun target => P) _ _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _ _, Y target  =>
+        simple refine (HitRec.hrecursion target (fun target => P) _ _ _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _ _ _, Y target  =>
+        simple refine (HitRec.hrecursion target (fun target => P) _ _ _ _ _ _ _ _ _)
+      | forall Y, Y =>
+        simple refine (HitRec.hrecursion target P)
+      | forall Y _, Y  =>
+        simple refine (HitRec.hrecursion target P _)
+      | forall Y _ _, Y =>
+        simple refine (HitRec.hrecursion target P _ _)
+      | forall Y _ _ _, Y  =>
+        simple refine (HitRec.hrecursion target P _ _ _)
+      | forall Y _ _ _ _, Y  =>
+        simple refine (HitRec.hrecursion target P _ _ _ _)
+      | forall Y _ _ _ _ _, Y =>
+        simple refine (HitRec.hrecursion target P _ _ _ _ _)
+      | forall Y _ _ _ _ _ _, Y =>
+        simple refine (HitRec.hrecursion target P _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _, Y =>
+        simple refine (HitRec.hrecursion target P _ _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _ _, Y =>
+        simple refine (HitRec.hrecursion target P _ _ _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _ _ _, Y =>
+        simple refine (HitRec.hrecursion target P _ _ _ _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _ _ _ _, Y =>
+        simple refine (HitRec.hrecursion target P _ _ _ _ _ _ _ _ _ _)
+      | _ => fail "Cannot handle the recursion principle (too many parameters?) :("
+     end
+    end
+  end.
+
+Ltac hrecursion x := hrecursion_ x; simpl; try (clear x).
+
+
diff --git a/Mod2.v b/Mod2.v
index b65a225..2f9bc8d 100644
--- a/Mod2.v
+++ b/Mod2.v
@@ -1,6 +1,6 @@
-Require Import HoTT.
 Require Export HoTT.
 
+Require Import HitTactics.
 Module Export modulo.
 
 Private Inductive Mod2 : Type0 :=
@@ -51,44 +51,38 @@ Axiom Mod2_rec_beta_mod : forall
   (mod' : a = s (s a))
   , ap (Mod2_rec P a s mod') mod = mod'.
 
+
+Definition Mod2CL : HitRec.class Mod2 _ := 
+   HitRec.Class Mod2 (fun x P a s p => Mod2_ind P a s p x).
+Canonical Structure Mod2ty : HitRec.type := HitRec.Pack Mod2 _ Mod2CL.
+
 End modulo.
 
-Definition negate : Mod2 -> Mod2.
-Proof.
-refine (Mod2_ind _ _ _ _).
- Unshelve.
- Focus 2.
- apply (succ Z).
-
- Focus 2.
- intros.
- apply (succ H).
-
- simpl.
- rewrite transport_const.
- rewrite <- mod.
- reflexivity.
-Defined.
 
 Theorem modulo2 : forall n : Mod2, n = succ(succ n).
 Proof.
-refine (Mod2_ind _ _ _ _).
- Unshelve.
- Focus 2.
- apply mod.
+intro n.
+hrecursion n.
+- apply mod.
+- intros n p.
+  apply (ap succ p).
+- simpl.
+  etransitivity.
+  eapply (@transport_paths_FlFr _ _ idmap (fun n => succ (succ n))).
+  hott_simpl.
+  apply ap_compose.
+Defined.
 
- Focus 2.
- intro n.
- intro p.
- apply (ap succ p).
-
- simpl.
- rewrite @HoTT.Types.Paths.transport_paths_FlFr.
- rewrite ap_idmap.
- rewrite concat_Vp.
- rewrite concat_1p.
- rewrite ap_compose.
- reflexivity.
+Definition negate : Mod2 -> Mod2.
+Proof.
+intro x.
+hrecursion x.
+- apply Z. 
+- intros. apply (succ H).
+- simpl.
+  etransitivity.
+  eapply transport_const.
+  eapply modulo2.
 Defined.
 
 Definition plus : Mod2 -> Mod2 -> Mod2.
diff --git a/_CoqProject b/_CoqProject
index bba943f..8c51bd5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,5 +1,6 @@
 -R . "" COQC = hoqc COQDEP = hoqdep
 
+HitTactics.v
 Mod2.v
 FinSets.v
 Expressions.v

From 399fab467b2e2e36d13df6902e4be0f5d9eec079 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@covariant.me>
Date: Sat, 20 May 2017 14:05:46 +0200
Subject: [PATCH 2/8] Package both the induction and recursion principles in
 the same record

---
 FinSets.v    |  10 ++--
 HitTactics.v |  74 +++++++++++++++++------------
 Mod2.v       | 128 ++++++++++++++-------------------------------------
 3 files changed, 84 insertions(+), 128 deletions(-)

diff --git a/FinSets.v b/FinSets.v
index 6bbeafc..5bab981 100644
--- a/FinSets.v
+++ b/FinSets.v
@@ -45,10 +45,6 @@ Fixpoint FinSets_rec
            (FinSets_rec A P e l u assocP commP nlP nrP idemP z)
       end) assocP commP nlP nrP idemP.
 
-Definition FinSetsCL A : HitRec.class (FinSets A) _ := 
-   HitRec.Class (FinSets A) (fun x P e l u aP cP lP rP iP => FinSets_rec A P e l u aP cP lP rP iP x).
-Canonical Structure FinSetsTy A : HitRec.type := HitRec.Pack _ _ (FinSetsCL A).
-
 Axiom FinSets_beta_assoc : forall
   (A : Type)
   (P : Type)
@@ -135,6 +131,12 @@ Axiom FinSets_beta_idem : forall
   ap (FinSets_rec A P e l u assocP commP nlP nrP idemP) (idem A x)
   =
   idemP x.
+
+(* TODO: add an induction principle *)
+Definition FinSetsCL A : HitRec.class (FinSets A) _ _ := 
+   HitRec.Class (FinSets A) (fun x P e l u aP cP lP rP iP => FinSets_rec A P e l u aP cP lP rP iP x) (fun x P e l u aP cP lP rP iP => FinSets_rec A P e l u aP cP lP rP iP x).
+Canonical Structure FinSetsTy A : HitRec.type := HitRec.Pack _ _ _ (FinSetsCL A).
+
 End FinSet.
 
 Section functions.
diff --git a/HitTactics.v b/HitTactics.v
index d43f35b..19e082f 100644
--- a/HitTactics.v
+++ b/HitTactics.v
@@ -1,45 +1,29 @@
 Module HitRec.
 Record class (H : Type) (* The HIT type itself *)
+             (indTy : H -> Type) (* The type of the induciton principle *)
              (recTy : H -> Type) (* The type of the recursion principle *)
-             := Class { recursion_term : forall (x : H), recTy x }.
-Structure type := Pack { obj : Type ; rec : obj -> Type ; class_of : class obj rec }.
+             := Class { 
+    H_recursor : forall (x : H), recTy x;
+    H_inductor : forall (x : H), indTy x  }.
+Structure type := Pack { obj : Type ; ind : obj -> Type ; rec : obj -> Type ; class_of : class obj ind rec }.
 Definition hrecursion (e : type) : forall x, rec e x :=
-  let 'Pack _ _ (Class r) := e
+  let 'Pack _ _ _ (Class r _) := e
   in r.
+Definition hinduction (e : type) : forall x, ind e x :=
+  let 'Pack _ _ _ (Class _ i) := e
+  in i.
 Arguments hrecursion {e} x : simpl never.
-Arguments Class H {recTy} recursion_term.
+Arguments hinduction {e} x : simpl never.
+Arguments Class H {indTy recTy} H_recursor H_inductor.
 End HitRec.
 
 Ltac hrecursion_ target :=
   generalize dependent target;
   match goal with
-  | [ |- forall target, ?P] => intro target;
+  | [ |- _ -> ?P ] => intro target;
     match type of (HitRec.hrecursion target) with
     | ?Q => 
       match (eval simpl in Q) with
-      | forall Y , Y target =>
-        simple refine (HitRec.hrecursion target (fun target => P) _)
-      | forall Y _, Y target  =>
-        simple refine (HitRec.hrecursion target (fun target => P) _)
-      | forall Y _ _, Y target  =>
-        simple refine (HitRec.hrecursion target (fun target => P) _ _)
-      | forall Y _ _ _, Y target  =>
-        let hrec:=(eval hnf in (HitRec.hrecursion target)) in
-        simple refine (hrec (fun target => P) _ _ _)
-      | forall Y _ _ _ _, Y target  =>
-        simple refine (HitRec.hrecursion target (fun target => P) _ _ _ _)
-      | forall Y _ _ _ _ _, Y target  =>
-        simple refine (HitRec.hrecursion target (fun target => P) _ _ _ _ _)
-      | forall Y _ _ _ _ _ _, Y target  =>
-        simple refine (HitRec.hrecursion target (fun target => P) _ _ _ _ _ _)
-      | forall Y _ _ _ _ _ _ _, Y target  =>
-        simple refine (HitRec.hrecursion target (fun target => P) _ _ _ _ _ _ _)
-      | forall Y _ _ _ _ _ _ _, Y target  =>
-        simple refine (HitRec.hrecursion target (fun target => P) _ _ _ _ _ _ _)
-      | forall Y _ _ _ _ _ _ _ _, Y target  =>
-        simple refine (HitRec.hrecursion target (fun target => P) _ _ _ _ _ _ _ _)
-      | forall Y _ _ _ _ _ _ _ _ _, Y target  =>
-        simple refine (HitRec.hrecursion target (fun target => P) _ _ _ _ _ _ _ _ _)
       | forall Y, Y =>
         simple refine (HitRec.hrecursion target P)
       | forall Y _, Y  =>
@@ -63,10 +47,40 @@ Ltac hrecursion_ target :=
       | forall Y _ _ _ _ _ _ _ _ _ _, Y =>
         simple refine (HitRec.hrecursion target P _ _ _ _ _ _ _ _ _ _)
       | _ => fail "Cannot handle the recursion principle (too many parameters?) :("
+      end
+    end
+  | [ |- forall target, ?P] => intro target;
+    match type of (HitRec.hinduction target) with
+    | ?Q => 
+      match (eval simpl in Q) with
+      | forall Y , Y target =>
+        simple refine (HitRec.hinduction target (fun target => P) _)
+      | forall Y _, Y target  =>
+        simple refine (HitRec.hinduction target (fun target => P) _)
+      | forall Y _ _, Y target  =>
+        simple refine (HitRec.hinduction target (fun target => P) _ _)
+      | forall Y _ _ _, Y target  =>
+        let hrec:=(eval hnf in (HitRec.hinduction target)) in
+        simple refine (hrec (fun target => P) _ _ _)
+      | forall Y _ _ _ _, Y target  =>
+        simple refine (HitRec.hinduction target (fun target => P) _ _ _ _)
+      | forall Y _ _ _ _ _, Y target  =>
+        simple refine (HitRec.hinduction target (fun target => P) _ _ _ _ _)
+      | forall Y _ _ _ _ _ _, Y target  =>
+        simple refine (HitRec.hinduction target (fun target => P) _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _, Y target  =>
+        simple refine (HitRec.hinduction target (fun target => P) _ _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _, Y target  =>
+        simple refine (HitRec.hinduction target (fun target => P) _ _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _ _, Y target  =>
+        simple refine (HitRec.hinduction target (fun target => P) _ _ _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _ _ _, Y target  =>
+        simple refine (HitRec.hinduction target (fun target => P) _ _ _ _ _ _ _ _ _)
+      | _ => fail "Cannot handle the induction principle (too many parameters?) :("
      end
     end
+  (*| _ => fail "I am sorry, but something went wrong!"*)
   end.
 
 Ltac hrecursion x := hrecursion_ x; simpl; try (clear x).
-
-
+Ltac hinduction x := hrecursion x.
diff --git a/Mod2.v b/Mod2.v
index 2f9bc8d..c342950 100644
--- a/Mod2.v
+++ b/Mod2.v
@@ -52,9 +52,9 @@ Axiom Mod2_rec_beta_mod : forall
   , ap (Mod2_rec P a s mod') mod = mod'.
 
 
-Definition Mod2CL : HitRec.class Mod2 _ := 
-   HitRec.Class Mod2 (fun x P a s p => Mod2_ind P a s p x).
-Canonical Structure Mod2ty : HitRec.type := HitRec.Pack Mod2 _ Mod2CL.
+Definition Mod2CL : HitRec.class Mod2 _ _ := 
+   HitRec.Class Mod2 (fun x P a s p => Mod2_rec P a s p x) (fun x P a s p => Mod2_ind P a s p x).
+Canonical Structure Mod2ty : HitRec.type := HitRec.Pack Mod2 _ _ Mod2CL.
 
 End modulo.
 
@@ -79,132 +79,72 @@ intro x.
 hrecursion x.
 - apply Z. 
 - intros. apply (succ H).
-- simpl.
-  etransitivity.
-  eapply transport_const.
-  eapply modulo2.
+- simpl. apply mod.
 Defined.
 
 Definition plus : Mod2 -> Mod2 -> Mod2.
 Proof.
-intro n.
-refine (Mod2_ind _ _ _ _).
-  Unshelve.
-
-  Focus 2.
-  apply n.
-
-  Focus 2.
-  intro m.
-  intro k.
-  apply (succ k).
-
-  simpl.
-  rewrite transport_const.
-  apply modulo2.
+intros n m.
+hrecursion m.
+- exact n.
+- apply succ.
+- apply modulo2.
 Defined.
 
 Definition Bool_to_Mod2 : Bool -> Mod2.
 Proof.
 intro b.
 destruct b.
- apply (succ Z).
-
- apply Z.
++ apply (succ Z).
++ apply Z.
 Defined.
 
 Definition Mod2_to_Bool : Mod2 -> Bool.
 Proof.
-refine (Mod2_ind _ _ _ _).
- Unshelve.
- Focus 2.
- apply false.
-
- Focus 2.
- intro n.
- apply negb.
-
- Focus 1.
- simpl.
- apply transport_const.
+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.
- Focus 1.
- compute.
- reflexivity.
-
- compute.
- reflexivity.
+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^.
-
- compute.
- apply reflexivity.
+destruct x; compute.
++ apply mod^.
++ apply reflexivity.
 Defined.
 
 Theorem eq2 : forall n : Mod2, Bool_to_Mod2 (Mod2_to_Bool n) = n.
 Proof.
-refine (Mod2_ind _ _ _ _).
-  Unshelve.
-  Focus 2.
-  compute.
-  reflexivity.
-
-  Focus 2.
-  intro n.
-  intro IHn.
-  symmetry.
-  transitivity (succ (Bool_to_Mod2 (Mod2_to_Bool n))).
-
-    Focus 1.
-    symmetry.
-    apply (ap succ IHn).
-
-    transitivity (Bool_to_Mod2 (negb (Mod2_to_Bool n))).
-    apply Bool_to_Mod2_negb.
-    enough (negb (Mod2_to_Bool n) = Mod2_to_Bool (succ n)).
-    apply (ap Bool_to_Mod2 X).
-
-    compute.
-    reflexivity.
-    simpl.
-    rewrite concat_p1.
-    rewrite concat_1p.
-    rewrite @HoTT.Types.Paths.transport_paths_FlFr.
-    rewrite concat_p1.
-    rewrite ap_idmap.
-    rewrite ap_compose.
-
-    enough (ap Mod2_to_Bool mod = reflexivity false).
-    rewrite X.
-    simpl.
-    rewrite concat_1p.
-    rewrite inv_V.
-    reflexivity.
-
-    enough (IsHSet Bool).
-    apply axiomK_hset.
-    apply X.
-    apply hset_bool.
+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.
+  + unfold Mod2_to_Bool. unfold HitRec.hrecursion. 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.
-enough (IsHSet Bool).
-apply set_path2.
 apply hset_bool.
 Defined.
 

From 5e594d10f08dff45f6521ab9ebbf93e500857adf Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@covariant.me>
Date: Mon, 22 May 2017 17:01:19 +0200
Subject: [PATCH 3/8] Some modifications to the finset module

---
 FinSets.v | 344 +++++++++++++++++++++++++++++++++++++++++++-----------
 1 file changed, 279 insertions(+), 65 deletions(-)

diff --git a/FinSets.v b/FinSets.v
index 5bab981..ff0ab46 100644
--- a/FinSets.v
+++ b/FinSets.v
@@ -2,30 +2,38 @@ Require Export HoTT.
 Require Import HitTactics.
 
 Module Export FinSet.
+Section FSet.
+Variable A : Type.
 
-Private Inductive FinSets (A : Type) : Type :=
-  | empty : FinSets A
-  | L : A -> FinSets A
-  | U : FinSets A -> FinSets A -> FinSets A.
+Private Inductive FSet : Type :=
+  | E : FSet
+  | L : A -> FSet
+  | U : FSet -> FSet -> FSet.
 
-Axiom assoc : forall (A : Type) (x y z : FinSets A),
-  U A x (U A y z) = U A (U A x y) z.
+Notation "{| x |}" :=  (L x).
+Infix "∪" := U (at level 8, right associativity).
+Notation "∅" := E.
 
-Axiom comm : forall (A : Type) (x y : FinSets A),
-  U A x y = U A y x.
+Axiom assoc : forall (x y z : FSet ),
+  x ∪ (y ∪ z) = (x ∪ y) ∪ z.
 
-Axiom nl : forall (A : Type) (x : FinSets A),
-  U A (empty A) x = x.
+Axiom comm : forall (x y : FSet),
+  x ∪ y = y ∪ x.
 
-Axiom nr : forall (A : Type) (x : FinSets A),
-  U A x (empty A) = x.
+Axiom nl : forall (x : FSet),
+  ∅ ∪ x = x.
 
-Axiom idem : forall (A : Type) (x : A),
-  U A (L A x) (L A x) = L A x.
+Axiom nr : forall (x : FSet),
+  x ∪ ∅ = x.
 
-Fixpoint FinSets_rec
-  (A : Type)
+Axiom idem : forall (x : A),
+  {| x |} ∪ {|x|} = {|x|}.
+
+Axiom trunc : IsHSet FSet.
+
+Fixpoint FSet_rec
   (P : Type)
+  (H: IsHSet P)
   (e : P)
   (l : A -> P)
   (u : P -> P -> P)
@@ -34,20 +42,20 @@ Fixpoint FinSets_rec
   (nlP : forall (x : P), u e x = x)
   (nrP : forall (x : P), u x e = x)
   (idemP : forall (x : A), u (l x) (l x) = l x)
-  (x : FinSets A)
+  (x : FSet)
   {struct x}
   : P
-  := (match x return _ -> _ -> _ -> _ -> _ -> P with
-        | empty => fun _ => fun _ => fun _ => fun _ => fun _ => e
-        | L a => fun _ => fun _ => fun _ => fun _ => fun _ => l a
-        | U y z => fun _ => fun _ => fun _ => fun _ => fun _ => u 
-           (FinSets_rec A P e l u assocP commP nlP nrP idemP y)
-           (FinSets_rec A P e l u assocP commP nlP nrP idemP z)
-      end) assocP commP nlP nrP idemP.
+  := (match x return _ -> _ -> _ -> _ -> _ -> _ -> P with
+        | E => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => e
+        | L a => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => l a
+        | U y z => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => u 
+           (FSet_rec P H e l u assocP commP nlP nrP idemP y)
+           (FSet_rec P H e l u assocP commP nlP nrP idemP z)
+      end) assocP commP nlP nrP idemP H.
 
-Axiom FinSets_beta_assoc : forall
-  (A : Type)
+Axiom FSet_rec_beta_assoc : forall
   (P : Type)
+  (H: IsHSet P)
   (e : P)
   (l : A -> P)
   (u : P -> P -> P)
@@ -56,17 +64,17 @@ Axiom FinSets_beta_assoc : forall
   (nlP : forall (x : P), u e x = x)
   (nrP : forall (x : P), u x e = x)
   (idemP : forall (x : A), u (l x) (l x) = l x)
-  (x y z : FinSets A),
-  ap (FinSets_rec A P e l u assocP commP nlP nrP idemP) (assoc A x y z)
+  (x y z : FSet),
+  ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (assoc x y z) 
   =
-  (assocP (FinSets_rec A P e l u assocP commP nlP nrP idemP x)
-          (FinSets_rec A P e l u assocP commP nlP nrP idemP y)
-          (FinSets_rec A P e l u assocP commP nlP nrP idemP z)
+  (assocP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
+          (FSet_rec P H e l u assocP commP nlP nrP idemP y)
+          (FSet_rec P H e l u assocP commP nlP nrP idemP z)
   ).
 
-Axiom FinSets_beta_comm : forall
-  (A : Type)
+Axiom FSet_rec_beta_comm : forall
   (P : Type)
+  (H: IsHSet P)
   (e : P)
   (l : A -> P)
   (u : P -> P -> P)
@@ -75,16 +83,16 @@ Axiom FinSets_beta_comm : forall
   (nlP : forall (x : P), u e x = x)
   (nrP : forall (x : P), u x e = x)
   (idemP : forall (x : A), u (l x) (l x) = l x)
-  (x y : FinSets A),
-  ap (FinSets_rec A P e l u assocP commP nlP nrP idemP) (comm A x y)
+  (x y : FSet),
+  ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (comm x y)
   =
-  (commP (FinSets_rec A P e l u assocP commP nlP nrP idemP x)
-         (FinSets_rec A P e l u assocP commP nlP nrP idemP y)
+  (commP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
+         (FSet_rec P H e l u assocP commP nlP nrP idemP y)
   ).
 
-Axiom FinSets_beta_nl : forall
-  (A : Type)
+Axiom FSet_rec_beta_nl : forall
   (P : Type)
+  (H: IsHSet P)
   (e : P)
   (l : A -> P)
   (u : P -> P -> P)
@@ -93,15 +101,15 @@ Axiom FinSets_beta_nl : forall
   (nlP : forall (x : P), u e x = x)
   (nrP : forall (x : P), u x e = x)
   (idemP : forall (x : A), u (l x) (l x) = l x)
-  (x : FinSets A),
-  ap (FinSets_rec A P e l u assocP commP nlP nrP idemP) (nl A x)
+  (x : FSet),
+  ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (nl x)
   =
-  (nlP (FinSets_rec A P e l u assocP commP nlP nrP idemP x)
+  (nlP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
   ).
 
-Axiom FinSets_beta_nr : forall
-  (A : Type)
+Axiom FSet_rec_beta_nr : forall
   (P : Type)
+  (H: IsHSet P)
   (e : P)
   (l : A -> P)
   (u : P -> P -> P)
@@ -110,15 +118,15 @@ Axiom FinSets_beta_nr : forall
   (nlP : forall (x : P), u e x = x)
   (nrP : forall (x : P), u x e = x)
   (idemP : forall (x : A), u (l x) (l x) = l x)
-  (x : FinSets A),
-  ap (FinSets_rec A P e l u assocP commP nlP nrP idemP) (nr A x)
+  (x : FSet),
+  ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (nr x)
   =
-  (nrP (FinSets_rec A P e l u assocP commP nlP nrP idemP x)
+  (nrP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
   ).
 
-Axiom FinSets_beta_idem : forall
-  (A : Type)
+Axiom FSet_rec_beta_idem : forall
   (P : Type)
+  (H: IsHSet P)
   (e : P)
   (l : A -> P)
   (u : P -> P -> P)
@@ -128,21 +136,206 @@ Axiom FinSets_beta_idem : forall
   (nrP : forall (x : P), u x e = x)
   (idemP : forall (x : A), u (l x) (l x) = l x)
   (x : A),
-  ap (FinSets_rec A P e l u assocP commP nlP nrP idemP) (idem A x)
+  ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (idem x)
   =
   idemP x.
 
+
+(* Induction principle *)
+Fixpoint FSet_ind
+  (P : FSet -> Type)
+  (H :  forall a : FSet, IsHSet (P a))
+  (eP : P E)
+  (lP : forall a: A, P (L a))
+  (uP : forall (x y: FSet), P x -> P y -> P (U x y))
+  (assocP : forall (x y z : FSet) 
+                   (px: P x) (py: P y) (pz: P z),
+  assoc x y z #
+   (uP      x    (U y z)          px        (uP y z py pz)) 
+  = 
+   (uP   (U x y)    z       (uP x y px py)          pz))
+  (commP : forall (x y: FSet) (px: P x) (py: P y),
+  comm x y #
+  uP x y px py = uP y x py px) 
+  (nlP : forall (x : FSet) (px: P x), 
+  nl x # uP E x eP px = px)
+  (nrP : forall (x : FSet) (px: P x), 
+  nr x # uP x E px eP = px)
+  (idemP : forall (x : A), 
+  idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
+  (x : FSet)
+  {struct x}
+  : P x
+  := (match x return _ -> _ -> _ -> _ -> _ -> _ -> P x with
+        | E => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => eP
+        | L a => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => lP a
+        | U y z => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => uP y z
+           (FSet_ind P H eP lP uP assocP commP nlP nrP idemP y)
+           (FSet_ind P H eP lP uP assocP commP nlP nrP idemP z)
+      end) H assocP commP nlP nrP idemP.
+
+
+Axiom FSet_ind_beta_assoc : forall
+  (P : FSet -> Type)
+  (H :  forall a : FSet, IsHSet (P a))
+  (eP : P E)
+  (lP : forall a: A, P (L a))
+  (uP : forall (x y: FSet), P x -> P y -> P (U x y))
+  (assocP : forall (x y z : FSet) 
+                   (px: P x) (py: P y) (pz: P z),
+  assoc x y z #
+   (uP      x    (U y z)          px        (uP y z py pz)) 
+  = 
+   (uP   (U x y)    z       (uP x y px py)          pz))
+  (commP : forall (x y: FSet) (px: P x) (py: P y),
+  comm x y #
+  uP x y px py = uP y x py px) 
+  (nlP : forall (x : FSet) (px: P x), 
+  nl x # uP E x eP px = px)
+  (nrP : forall (x : FSet) (px: P x), 
+  nr x # uP x E px eP = px)
+  (idemP : forall (x : A), 
+  idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
+  (x y z : FSet),
+  apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) 
+      (assoc x y z)
+  =
+  (assocP x y z 
+          (FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
+          (FSet_ind P H eP lP uP assocP commP nlP nrP idemP y)
+          (FSet_ind P H eP lP uP assocP commP nlP nrP idemP z)
+  ).
+
+
+
+Axiom FSet_ind_beta_comm : forall  
+  (P : FSet -> Type)
+  (H :  forall a : FSet, IsHSet (P a))
+  (eP : P E)
+  (lP : forall a: A, P (L a))
+  (uP : forall (x y: FSet), P x -> P y -> P (U x y))
+  (assocP : forall (x y z : FSet) 
+                   (px: P x) (py: P y) (pz: P z),
+  assoc x y z #
+   (uP      x    (U y z)          px        (uP y z py pz)) 
+  = 
+   (uP   (U x y)    z       (uP x y px py)          pz))
+  (commP : forall (x y : FSet) (px: P x) (py: P y),
+  comm x y #
+  uP x y px py = uP y x py px) 
+  (nlP : forall (x : FSet) (px: P x), 
+  nl x # uP E x eP px = px)
+  (nrP : forall (x : FSet) (px: P x), 
+  nr x # uP x E px eP = px)
+  (idemP : forall (x : A), 
+  idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
+  (x y : FSet),
+  apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (comm x y)
+  =
+  (commP x y 
+         (FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
+         (FSet_ind P H eP lP uP assocP commP nlP nrP idemP y)
+  ).
+
+Axiom FSet_ind_beta_nl : forall
+  (P : FSet -> Type)
+  (H :  forall a : FSet, IsHSet (P a))
+  (eP : P E)
+  (lP : forall a: A, P (L a))
+  (uP : forall (x y: FSet), P x -> P y -> P (U x y))
+  (assocP : forall (x y z : FSet) 
+                   (px: P x) (py: P y) (pz: P z),
+  assoc x y z #
+   (uP      x    (U y z)          px        (uP y z py pz)) 
+  = 
+   (uP   (U x y)    z       (uP x y px py)          pz))
+  (commP : forall (x y : FSet) (px: P x) (py: P y),
+  comm x y #
+  uP x y px py = uP y x py px) 
+  (nlP : forall (x : FSet) (px: P x), 
+  nl x # uP E x eP px = px)
+  (nrP : forall (x : FSet) (px: P x), 
+  nr x # uP x E px eP = px)
+  (idemP : forall (x : A), 
+  idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
+  (x : FSet),
+  apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (nl x)
+  =
+  (nlP x (FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
+  ).
+
+Axiom FSet_ind_beta_nr : forall
+  (P : FSet -> Type)
+  (H :  forall a : FSet, IsHSet (P a))
+  (eP : P E)
+  (lP : forall a: A, P (L a))
+  (uP : forall (x y: FSet), P x -> P y -> P (U x y))
+  (assocP : forall (x y z : FSet) 
+                   (px: P x) (py: P y) (pz: P z),
+  assoc x y z #
+   (uP      x    (U y z)          px        (uP y z py pz)) 
+  = 
+   (uP   (U x y)    z       (uP x y px py)          pz))
+  (commP : forall (x y : FSet) (px: P x) (py: P y),
+  comm x y #
+  uP x y px py = uP y x py px) 
+  (nlP : forall (x : FSet) (px: P x), 
+  nl x # uP E x eP px = px)
+  (nrP : forall (x : FSet) (px: P x), 
+  nr x # uP x E px eP = px)
+  (idemP : forall (x : A), 
+  idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
+  (x : FSet),
+  apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (nr x)
+  =
+  (nrP x (FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
+  ).
+
+Axiom FSet_ind_beta_idem : forall
+  (P : FSet -> Type)
+  (H :  forall a : FSet, IsHSet (P a))
+  (eP : P E)
+  (lP : forall a: A, P (L a))
+  (uP : forall (x y: FSet), P x -> P y -> P (U x y))
+  (assocP : forall (x y z : FSet) 
+                   (px: P x) (py: P y) (pz: P z),
+  assoc x y z #
+   (uP      x    (U y z)          px        (uP y z py pz)) 
+  = 
+   (uP   (U x y)    z       (uP x y px py)          pz))
+  (commP : forall (x y : FSet) (px: P x) (py: P y),
+  comm x y #
+  uP x y px py = uP y x py px) 
+  (nlP : forall (x : FSet) (px: P x), 
+  nl x # uP E x eP px = px)
+  (nrP : forall (x : FSet) (px: P x), 
+  nr x # uP x E px eP = px)
+  (idemP : forall (x : A), 
+  idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
+  (x : A),
+  apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (idem x)
+  =
+  idemP x.
+
+End FSet.
+
 (* TODO: add an induction principle *)
-Definition FinSetsCL A : HitRec.class (FinSets A) _ _ := 
-   HitRec.Class (FinSets A) (fun x P e l u aP cP lP rP iP => FinSets_rec A P e l u aP cP lP rP iP x) (fun x P e l u aP cP lP rP iP => FinSets_rec A P e l u aP cP lP rP iP x).
-Canonical Structure FinSetsTy A : HitRec.type := HitRec.Pack _ _ _ (FinSetsCL A).
+Definition FSetCL A : HitRec.class (FSet A) _ _ := 
+   HitRec.Class (FSet A) (fun x P H e l u aP cP lP rP iP => FSet_rec A P H e l u aP cP lP rP iP x) (fun x P H e l u aP cP lP rP iP => FSet_ind A P H e l u aP cP lP rP iP x).
+Canonical Structure FSetTy A : HitRec.type := HitRec.Pack _ _ _ (FSetCL A).
+
+Arguments E {_}.
+Arguments U {_} _ _.
+Arguments L {_} _.
 
 End FinSet.
 
 Section functions.
 Parameter A : Type.
 Parameter eq : A -> A -> Bool.
-Definition isIn : A -> FinSets A -> Bool.
+Parameter eq_refl: forall a:A, eq a a = true.
+
+Definition isIn : A -> FSet A -> Bool.
 Proof.
 intros a X.
 hrecursion X.
@@ -156,17 +349,15 @@ hrecursion X.
 - intros a'. compute. destruct (eq a a'); reflexivity.
 Defined.
 
-
 Definition comprehension : 
-  (A -> Bool) -> FinSets A -> FinSets A.
+  (A -> Bool) -> FSet A -> FSet A.
 Proof.
 intros P X.
 hrecursion X.
-- apply empty.
+- apply E.
 - intro a.
-  refine (if (P a) then L A a else empty A).
-- intros X Y.
-  apply (U A X Y).
+  refine (if (P a) then L a else E).
+- apply U.
 - intros. cbv. apply assoc.
 - intros. cbv. apply comm.
 - intros. cbv. apply nl.
@@ -176,15 +367,37 @@ hrecursion X.
   + apply idem.
   + apply nl.
 Defined.
+Require Import FunextAxiom.
+Lemma comprehension_idem: 
+   forall (X:FSet A), forall Y, comprehension (fun x => isIn x (U X Y)) X = X.
+Proof.
+simple refine (FSet_ind _ _ _ _ _ _ _ _ _ _ _); simpl.
+- intro Y. cbv. reflexivity.
+- intros a Y. unfold comprehension. unfold HitRec.hrecursion. simpl.
+  enough (isIn a (U (L a) Y) = true).
+  + rewrite X. reflexivity.
+  + unfold isIn. unfold HitRec.hrecursion. simpl.
+    rewrite eq_refl. auto.
+- intros X1 X2 IH1 IH2 Y.
+  unfold comprehension. unfold  HitRec.hrecursion. simpl.
+  rewrite <- (assoc _ X1 X2 Y).
+  f_ap. 
+  + apply (IH1 (U X2 Y)).
+  + rewrite (assoc _ X1 X2 Y).
+    rewrite (comm _ X1 X2).
+    rewrite <- (assoc _ X2 X1 Y).
+    apply (IH2 (U X1 Y)).
+Admitted.
+
 
 Definition intersection : 
-  FinSets A -> FinSets A -> FinSets A.
+  FSet A -> FSet A -> FSet A.
 Proof.
 intros X Y.
 apply (comprehension (fun (a : A) => isIn a X) Y).
 Defined.
 
-Definition subset (x : FinSets A) (y : FinSets A) : Bool.
+Definition subset (x : FSet A) (y : FSet A) : Bool.
 Proof.
 hrecursion x.
 - apply true.
@@ -198,9 +411,10 @@ hrecursion x.
   destruct (isIn a y); reflexivity.
 Defined.
 
-Definition subset' (x : FinSets A) (y : FinSets A) : Bool.
+
+Definition subset' (x : FSet A) (y : FSet A) : Bool.
 Proof.
-refine (FinSets_rec A _ _ _ _ _ _ _ _ _ _).
+refine (FSet_rec A _ _ _ _ _ _ _ _ _ _).
   Unshelve.
 
   Focus 6.
@@ -259,7 +473,7 @@ refine (FinSets_rec A _ _ _ _ _ _ _ _ _ _).
 Defined.
 (* TODO: subset = subset' *)
 
-Definition equal_set (x : FinSets A) (y : FinSets A) : Bool
+Definition equal_set (x : FSet A) (y : FSet A) : Bool
   := andb (subset x y) (subset y x).
 
 Fixpoint eq_nat n m : Bool :=

From f23d4aeacbb8c17547ef037c67c73dbe3faf5f19 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@covariant.me>
Date: Mon, 22 May 2017 21:06:13 +0200
Subject: [PATCH 4/8] Replace the canonical structures mechanism for recursion
 with type classes

See changes in HitTactics.v
---
 FinSets.v    | 139 +++++++++++++++++++------------------------------
 HitTactics.v | 143 +++++++++++++++++++++++++--------------------------
 Mod2.v       |  18 +++----
 3 files changed, 131 insertions(+), 169 deletions(-)

diff --git a/FinSets.v b/FinSets.v
index ff0ab46..3b27490 100644
--- a/FinSets.v
+++ b/FinSets.v
@@ -319,10 +319,9 @@ Axiom FSet_ind_beta_idem : forall
 
 End FSet.
 
-(* TODO: add an induction principle *)
-Definition FSetCL A : HitRec.class (FSet A) _ _ := 
-   HitRec.Class (FSet A) (fun x P H e l u aP cP lP rP iP => FSet_rec A P H e l u aP cP lP rP iP x) (fun x P H e l u aP cP lP rP iP => FSet_ind A P H e l u aP cP lP rP iP x).
-Canonical Structure FSetTy A : HitRec.type := HitRec.Pack _ _ _ (FSetCL A).
+Instance FSet_recursion A : HitRecursion (FSet A) := {
+  indTy := _; recTy := _; 
+  H_inductor := FSet_ind A; H_recursor := FSet_rec A }.
 
 Arguments E {_}.
 Arguments U {_} _ _.
@@ -332,28 +331,45 @@ End FinSet.
 
 Section functions.
 Parameter A : Type.
-Parameter eq : A -> A -> Bool.
-Parameter eq_refl: forall a:A, eq a a = true.
-
+Parameter A_eqdec : forall (x y : A), Decidable (x = y).
+Definition deceq (x y : A) :=
+  if dec (x = y) then true else false.
 Definition isIn : A -> FSet A -> Bool.
 Proof.
-intros a X.
-hrecursion X.
+intros a.
+hrecursion.
 - exact false.
-- intro a'. apply (eq a a').
+- intro a'. apply (deceq a a').
 - apply orb. 
 - intros x y z. compute. destruct x; reflexivity.
 - intros x y. compute. destruct x, y; reflexivity.
 - intros x. compute. reflexivity. 
 - intros x. compute. destruct x; reflexivity.
-- intros a'. compute. destruct (eq a a'); reflexivity.
+- intros a'. compute. destruct (A_eqdec a a'); reflexivity.
 Defined.
 
+Lemma isIn_eq a b : isIn a (L b) = true -> a = b.
+Proof. cbv.
+destruct (A_eqdec a b). intro. apply p.
+intro X. 
+pose (false_ne_true X). contradiction.
+Defined.
+
+Lemma isIn_empt_false a : isIn a E = true -> Empty.
+Proof. 
+cbv. intro X.
+pose (false_ne_true X). contradiction.
+Defined.
+
+Lemma isIn_union a X Y : isIn a (U X Y) = orb (isIn a X) (isIn a Y).
+Proof. reflexivity. Qed. 
+
+
 Definition comprehension : 
   (A -> Bool) -> FSet A -> FSet A.
 Proof.
-intros P X.
-hrecursion X.
+intros P.
+hrecursion.
 - apply E.
 - intro a.
   refine (if (P a) then L a else E).
@@ -367,29 +383,40 @@ hrecursion X.
   + apply idem.
   + apply nl.
 Defined.
+
+Lemma comprehension_false Y : comprehension (fun a => isIn a E) Y = E.
+Proof.
+hrecursion Y; try (intros; apply set_path2).
+- cbn. reflexivity.
+- cbn. reflexivity.
+- intros x y IHa IHb.
+  cbn.
+  rewrite IHa.
+  rewrite IHb.
+  rewrite nl.
+  reflexivity.
+Defined.
+
 Require Import FunextAxiom.
 Lemma comprehension_idem: 
    forall (X:FSet A), forall Y, comprehension (fun x => isIn x (U X Y)) X = X.
 Proof.
-simple refine (FSet_ind _ _ _ _ _ _ _ _ _ _ _); simpl.
+hinduction; try (intros; apply set_path2).
 - intro Y. cbv. reflexivity.
-- intros a Y. unfold comprehension. unfold HitRec.hrecursion. simpl.
-  enough (isIn a (U (L a) Y) = true).
-  + rewrite X. reflexivity.
-  + unfold isIn. unfold HitRec.hrecursion. simpl.
-    rewrite eq_refl. auto.
+- intros a Y. cbn.
+  unfold deceq;
+  destruct (dec (a = a)); simpl.
+  + reflexivity.
+  + contradiction n. reflexivity.
 - intros X1 X2 IH1 IH2 Y.
-  unfold comprehension. unfold  HitRec.hrecursion. simpl.
-  rewrite <- (assoc _ X1 X2 Y).
+  cbn -[isIn].
   f_ap. 
-  + apply (IH1 (U X2 Y)).
-  + rewrite (assoc _ X1 X2 Y).
-    rewrite (comm _ X1 X2).
+  + rewrite <- assoc. apply (IH1 (U X2 Y)).
+  + rewrite (comm _ X1 X2).
     rewrite <- (assoc _ X2 X1 Y).
     apply (IH2 (U X1 Y)).
 Admitted.
 
-
 Definition intersection : 
   FSet A -> FSet A -> FSet A.
 Proof.
@@ -411,68 +438,6 @@ hrecursion x.
   destruct (isIn a y); reflexivity.
 Defined.
 
-
-Definition subset' (x : FSet A) (y : FSet A) : Bool.
-Proof.
-refine (FSet_rec A _ _ _ _ _ _ _ _ _ _).
-  Unshelve.
-
-  Focus 6.
-  apply x.
-
-  Focus 6.
-  apply true.
-
-  Focus 6.
-  intro a.
-  apply (isIn a y).
-
-  Focus 6.
-  intro b.
-  intro b'.
-  apply (andb b b').
-
-  Focus 1.
-  intros.
-  compute.
-  destruct x0.
-  destruct y0.
-  reflexivity.
-  reflexivity.
-  reflexivity.
-
-  Focus 1.
-  intros.
-  compute.
-  destruct x0.
-  destruct y0.
-  reflexivity.
-  reflexivity.
-  destruct y0.
-  reflexivity.
-  reflexivity.
-
-  Focus 1.
-  intros.
-  compute.
-  reflexivity.
-
-  Focus 1.
-  intros.
-  compute.
-  destruct x0.
-  reflexivity.
-  reflexivity.
-
-  intros.
-  destruct (isIn x0 y).
-  compute.
-  reflexivity.
-  compute.
-  reflexivity.
-Defined.
-(* TODO: subset = subset' *)
-
 Definition equal_set (x : FSet A) (y : FSet A) : Bool
   := andb (subset x y) (subset y x).
 
diff --git a/HitTactics.v b/HitTactics.v
index 19e082f..cd2a77d 100644
--- a/HitTactics.v
+++ b/HitTactics.v
@@ -1,86 +1,85 @@
-Module HitRec.
-Record class (H : Type) (* The HIT type itself *)
-             (indTy : H -> Type) (* The type of the induciton principle *)
-             (recTy : H -> Type) (* The type of the recursion principle *)
-             := Class { 
-    H_recursor : forall (x : H), recTy x;
-    H_inductor : forall (x : H), indTy x  }.
-Structure type := Pack { obj : Type ; ind : obj -> Type ; rec : obj -> Type ; class_of : class obj ind rec }.
-Definition hrecursion (e : type) : forall x, rec e x :=
-  let 'Pack _ _ _ (Class r _) := e
-  in r.
-Definition hinduction (e : type) : forall x, ind e x :=
-  let 'Pack _ _ _ (Class _ i) := e
-  in i.
-Arguments hrecursion {e} x : simpl never.
-Arguments hinduction {e} x : simpl never.
-Arguments Class H {indTy recTy} H_recursor H_inductor.
-End HitRec.
+Class HitRecursion (H : Type) := {
+  indTy : Type;
+  recTy : Type;
+  H_inductor : indTy;
+  H_recursor : recTy
+}.
 
-Ltac hrecursion_ target :=
-  generalize dependent target;
-  match goal with
-  | [ |- _ -> ?P ] => intro target;
-    match type of (HitRec.hrecursion target) with
+Definition hrecursion (H : Type) {HR : HitRecursion H} : @recTy H HR :=
+  @H_recursor H HR.
+
+Definition hinduction (H : Type) {HR : HitRecursion H} : @indTy H HR :=
+  @H_inductor H HR.
+
+Ltac hrecursion_ :=
+  lazymatch goal with
+  | [ |- ?T -> ?P ] => 
+    let hrec1 := eval cbv[hrecursion H_recursor] in (hrecursion T) in
+    let hrec := eval simpl in hrec1 in
+    match type of hrec with
     | ?Q => 
       match (eval simpl in Q) with
-      | forall Y, Y =>
-        simple refine (HitRec.hrecursion target P)
-      | forall Y _, Y  =>
-        simple refine (HitRec.hrecursion target P _)
-      | forall Y _ _, Y =>
-        simple refine (HitRec.hrecursion target P _ _)
-      | forall Y _ _ _, Y  =>
-        simple refine (HitRec.hrecursion target P _ _ _)
-      | forall Y _ _ _ _, Y  =>
-        simple refine (HitRec.hrecursion target P _ _ _ _)
-      | forall Y _ _ _ _ _, Y =>
-        simple refine (HitRec.hrecursion target P _ _ _ _ _)
-      | forall Y _ _ _ _ _ _, Y =>
-        simple refine (HitRec.hrecursion target P _ _ _ _ _ _)
-      | forall Y _ _ _ _ _ _ _, Y =>
-        simple refine (HitRec.hrecursion target P _ _ _ _ _ _ _)
-      | forall Y _ _ _ _ _ _ _ _, Y =>
-        simple refine (HitRec.hrecursion target P _ _ _ _ _ _ _ _)
-      | forall Y _ _ _ _ _ _ _ _ _, Y =>
-        simple refine (HitRec.hrecursion target P _ _ _ _ _ _ _ _ _)
-      | forall Y _ _ _ _ _ _ _ _ _ _, Y =>
-        simple refine (HitRec.hrecursion target P _ _ _ _ _ _ _ _ _ _)
+      | forall Y, T -> Y =>
+        simple refine (hrec P)
+      | forall Y _, T -> Y  =>
+        simple refine (hrec P _)
+      | forall Y _ _, T -> Y =>
+        simple refine (hrec P _ _)
+      | forall Y _ _ _, T -> Y  =>
+        simple refine (hrec P _ _ _)
+      | forall Y _ _ _ _, T -> Y  =>
+        simple refine (hrec P _ _ _ _)
+      | forall Y _ _ _ _ _, T -> Y =>
+        simple refine (hrec P _ _ _ _ _)
+      | forall Y _ _ _ _ _ _, T -> Y =>
+        simple refine (hrec P _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _, T -> Y =>
+        simple refine (hrec P _ _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _ _, T -> Y =>
+        simple refine (hrec P _ _ _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _ _ _, T -> Y => 
+        simple refine (hrec P _ _ _ _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _ _ _ _, T -> Y =>
+        simple refine (hrec P _ _ _ _ _ _ _ _ _ _) 
       | _ => fail "Cannot handle the recursion principle (too many parameters?) :("
       end
     end
-  | [ |- forall target, ?P] => intro target;
-    match type of (HitRec.hinduction target) with
+  | [ |- forall (target:?T), ?P] => 
+    let hind1 := eval cbv[hinduction H_inductor] in (hinduction T) in
+    let hind := eval simpl in hind1 in
+    match type of hind with
     | ?Q => 
       match (eval simpl in Q) with
-      | forall Y , Y target =>
-        simple refine (HitRec.hinduction target (fun target => P) _)
-      | forall Y _, Y target  =>
-        simple refine (HitRec.hinduction target (fun target => P) _)
-      | forall Y _ _, Y target  =>
-        simple refine (HitRec.hinduction target (fun target => P) _ _)
-      | forall Y _ _ _, Y target  =>
-        let hrec:=(eval hnf in (HitRec.hinduction target)) in
-        simple refine (hrec (fun target => P) _ _ _)
-      | forall Y _ _ _ _, Y target  =>
-        simple refine (HitRec.hinduction target (fun target => P) _ _ _ _)
-      | forall Y _ _ _ _ _, Y target  =>
-        simple refine (HitRec.hinduction target (fun target => P) _ _ _ _ _)
-      | forall Y _ _ _ _ _ _, Y target  =>
-        simple refine (HitRec.hinduction target (fun target => P) _ _ _ _ _ _)
-      | forall Y _ _ _ _ _ _ _, Y target  =>
-        simple refine (HitRec.hinduction target (fun target => P) _ _ _ _ _ _ _)
-      | forall Y _ _ _ _ _ _ _, Y target  =>
-        simple refine (HitRec.hinduction target (fun target => P) _ _ _ _ _ _ _)
-      | forall Y _ _ _ _ _ _ _ _, Y target  =>
-        simple refine (HitRec.hinduction target (fun target => P) _ _ _ _ _ _ _ _)
-      | forall Y _ _ _ _ _ _ _ _ _, Y target  =>
-        simple refine (HitRec.hinduction target (fun target => P) _ _ _ _ _ _ _ _ _)
+      | forall Y , (forall x, Y x) =>
+        simple refine (hind (fun target => P) _)
+      | forall Y _, (forall x, Y x)  =>
+        simple refine (hind (fun target => P) _)
+      | forall Y _ _, (forall x, Y x)  =>
+        simple refine (hind (fun target => P) _ _)
+      | forall Y _ _ _, (forall x, Y x)  =>       
+        simple refine (hind (fun target => P) _ _ _)
+      | forall Y _ _ _ _, (forall x, Y x)  =>
+        simple refine (hind (fun target => P) _ _ _ _)
+      | forall Y _ _ _ _ _, (forall x, Y x)  =>
+        simple refine (hind (fun target => P) _ _ _ _ _)
+      | forall Y _ _ _ _ _ _, (forall x, Y x)  =>
+        simple refine (hind (fun target => P) _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _, (forall x, Y x)  =>
+        simple refine (hind (fun target => P) _ _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _, (forall x, Y x)  =>
+        simple refine (hind (fun target => P) _ _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _ _, (forall x, Y x)  =>
+        simple refine (hind (fun target => P) _ _ _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _ _ _, (forall x, Y x)  =>
+        simple refine (hind (fun target => P) _ _ _ _ _ _ _ _ _)
       | _ => fail "Cannot handle the induction principle (too many parameters?) :("
      end
     end
   (*| _ => fail "I am sorry, but something went wrong!"*)
   end.
 
-Ltac hrecursion x := hrecursion_ x; simpl; try (clear x).
-Ltac hinduction x := hrecursion x.
+Tactic Notation "hrecursion" := hrecursion_; simpl.
+Tactic Notation "hrecursion" ident(x) := revert x; hrecursion.
+Tactic Notation "hinduction" := hrecursion_; simpl.
+Tactic Notation "hinduction" ident(x) := revert x; hrecursion.
+
diff --git a/Mod2.v b/Mod2.v
index c342950..49ba3b8 100644
--- a/Mod2.v
+++ b/Mod2.v
@@ -1,6 +1,6 @@
 Require Export HoTT.
-
 Require Import HitTactics.
+
 Module Export modulo.
 
 Private Inductive Mod2 : Type0 :=
@@ -51,10 +51,10 @@ Axiom Mod2_rec_beta_mod : forall
   (mod' : a = s (s a))
   , ap (Mod2_rec P a s mod') mod = mod'.
 
-
-Definition Mod2CL : HitRec.class Mod2 _ _ := 
-   HitRec.Class Mod2 (fun x P a s p => Mod2_rec P a s p x) (fun x P a s p => Mod2_ind P a s p x).
-Canonical Structure Mod2ty : HitRec.type := HitRec.Pack Mod2 _ _ Mod2CL.
+Instance: HitRecursion Mod2 := {
+  indTy := _; recTy := _; 
+  H_inductor := Mod2_ind;
+  H_recursor := Mod2_rec }.
 
 End modulo.
 
@@ -62,7 +62,7 @@ End modulo.
 Theorem modulo2 : forall n : Mod2, n = succ(succ n).
 Proof.
 intro n.
-hrecursion n.
+hinduction n.
 - apply mod.
 - intros n p.
   apply (ap succ p).
@@ -75,8 +75,7 @@ Defined.
 
 Definition negate : Mod2 -> Mod2.
 Proof.
-intro x.
-hrecursion x.
+hrecursion.
 - apply Z. 
 - intros. apply (succ H).
 - simpl. apply mod.
@@ -137,8 +136,7 @@ hinduction n.
   rewrite ap_compose. 
   enough (ap Mod2_to_Bool mod = idpath).
   + rewrite X. hott_simpl.
-  + unfold Mod2_to_Bool. unfold HitRec.hrecursion. simpl. 
-    apply (Mod2_rec_beta_mod Bool false negb 1).
+  + apply (Mod2_rec_beta_mod Bool false negb 1).
 Defined.
 
 Theorem adj : 

From 2f68e833afc6b528fc9c929051f9268884324343 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@covariant.me>
Date: Tue, 23 May 2017 00:17:33 +0200
Subject: [PATCH 5/8] Finish the comprehension_idem proof with functional
 extensionality

---
 FinSets.v | 30 ++++++++++++++++++++++++++----
 1 file changed, 26 insertions(+), 4 deletions(-)

diff --git a/FinSets.v b/FinSets.v
index 3b27490..d186572 100644
--- a/FinSets.v
+++ b/FinSets.v
@@ -334,6 +334,19 @@ Parameter A : Type.
 Parameter A_eqdec : forall (x y : A), Decidable (x = y).
 Definition deceq (x y : A) :=
   if dec (x = y) then true else false.
+
+Lemma union_idem : forall (X : FSet A), U X X = X.
+Proof.
+hinduction; try (intros; apply set_path2).
+- apply nr.
+- intros. apply idem.
+- intros X Y HX HY. etransitivity.
+  rewrite assoc. rewrite (comm _ X Y). rewrite <- (assoc _ Y X X).
+  rewrite comm.  
+  rewrite assoc. rewrite HX. rewrite HY. reflexivity.
+  rewrite comm. reflexivity.
+Defined.
+
 Definition isIn : A -> FSet A -> Bool.
 Proof.
 intros a.
@@ -397,11 +410,11 @@ hrecursion Y; try (intros; apply set_path2).
   reflexivity.
 Defined.
 
-Require Import FunextAxiom.
-Lemma comprehension_idem: 
+Lemma comprehension_idem' `{Funext}: 
    forall (X:FSet A), forall Y, comprehension (fun x => isIn x (U X Y)) X = X.
 Proof.
-hinduction; try (intros; apply set_path2).
+hinduction.
+all: try (intros; apply path_forall; intro; apply set_path2).
 - intro Y. cbv. reflexivity.
 - intros a Y. cbn.
   unfold deceq;
@@ -415,7 +428,16 @@ hinduction; try (intros; apply set_path2).
   + rewrite (comm _ X1 X2).
     rewrite <- (assoc _ X2 X1 Y).
     apply (IH2 (U X1 Y)).
-Admitted.
+Defined.
+
+Lemma comprehension_idem `{Funext}: 
+   forall (X:FSet A), comprehension (fun x => isIn x X) X = X.
+Proof.
+intros X.
+enough (comprehension (fun x : A => isIn x (U X X)) X = X).
+rewrite (union_idem) in X0. assumption.
+apply comprehension_idem'.
+Defined.
 
 Definition intersection : 
   FSet A -> FSet A -> FSet A.

From afdc4a3e6be07b0b6f0645e84ed3ebf499c09847 Mon Sep 17 00:00:00 2001
From: Leon Gondelman <lgondelmann@gmail.com>
Date: Tue, 23 May 2017 11:50:52 +0200
Subject: [PATCH 6/8] intersection_comm

---
 FinSets.v | 75 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 75 insertions(+)

diff --git a/FinSets.v b/FinSets.v
index d186572..ca9461b 100644
--- a/FinSets.v
+++ b/FinSets.v
@@ -397,6 +397,46 @@ hrecursion.
   + apply nl.
 Defined.
 
+Lemma comprehension_union X Y Z : 
+	U (comprehension (fun a => isIn a Y) X)
+	  (comprehension (fun a => isIn a Z) X) =
+	  comprehension (fun a => isIn a (U Y Z)) X.
+	
+Proof.
+hrecursion X.
+- cbn. apply nl.
+- cbn. intro a. 
+		destruct (isIn a Y); simpl;
+		destruct (isIn a Z); simpl.
+		apply idem.
+		apply nr.
+		apply nl.
+		apply nl.
+- cbn. intros X1 X2 IH1 IH2.
+	rewrite assoc.
+	rewrite (comm _ (comprehension (fun a : A => isIn a Y) X1) 
+				  (comprehension (fun a : A => isIn a Y) X2)).
+  rewrite <- (assoc _   
+  				  (comprehension (fun a : A => isIn a Y) X2)
+       		 (comprehension (fun a : A => isIn a Y) X1)
+       		 (comprehension (fun a : A => isIn a Z) X1)
+       		 ).
+  rewrite IH1.
+  rewrite comm.
+  rewrite assoc. 
+  rewrite (comm _ (comprehension (fun a : A => isIn a Z) X2) _).
+  rewrite IH2.
+  rewrite comm.
+  reflexivity.
+- intros. apply set_path2.
+- intros; apply set_path2.
+- intros; apply set_path2.
+- intros; apply set_path2.
+- intros; apply set_path2.
+Defined.
+
+
+
 Lemma comprehension_false Y : comprehension (fun a => isIn a E) Y = E.
 Proof.
 hrecursion Y; try (intros; apply set_path2).
@@ -446,6 +486,41 @@ intros X Y.
 apply (comprehension (fun (a : A) => isIn a X) Y).
 Defined.
 
+
+Lemma intersection_comm X Y: intersection X Y = intersection Y X.
+Proof.
+hrecursion X;  try (intros; apply set_path2).
+- cbn. unfold intersection. apply comprehension_false.
+- cbn. unfold intersection. intros a.
+  hrecursion Y; try (intros; apply set_path2).
+  + cbn. reflexivity.
+  + cbn. intros. unfold deceq. 
+  		destruct  (dec (a0 = a)). 
+  		rewrite p. destruct (dec (a=a)).
+  		reflexivity.
+  		contradiction n. 
+  		reflexivity. 
+		destruct  (dec (a = a0)).
+		contradiction n. apply p^. reflexivity.
+ 	+ cbn -[isIn]. intros Y1 Y2 IH1 IH2.
+ 	 	rewrite IH1. 
+ 	 	rewrite IH2.
+ 	 	symmetry.
+ 	 	rewrite 	(comprehension_union (L a)).
+ 	 	reflexivity.
+- intros X1 X2 IH1 IH2.
+  cbn.
+  unfold intersection in *.
+  rewrite <- IH1.
+  rewrite <- IH2.
+	rewrite comprehension_union.
+	reflexivity.
+Defined.
+
+	
+	
+
+
 Definition subset (x : FSet A) (y : FSet A) : Bool.
 Proof.
 hrecursion x.

From 9d9b7a47132c228a3c2d613f393918175ca009bf Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@covariant.me>
Date: Tue, 23 May 2017 11:58:09 +0200
Subject: [PATCH 7/8] Prettify FinSets

---
 FinSets.v | 47 ++++++++++++++++++++++++-----------------------
 1 file changed, 24 insertions(+), 23 deletions(-)

diff --git a/FinSets.v b/FinSets.v
index d186572..5cc9be8 100644
--- a/FinSets.v
+++ b/FinSets.v
@@ -331,10 +331,15 @@ End FinSet.
 
 Section functions.
 Parameter A : Type.
-Parameter A_eqdec : forall (x y : A), Decidable (x = y).
+Context (A_eqdec: forall (x y : A), Decidable (x = y)).
 Definition deceq (x y : A) :=
   if dec (x = y) then true else false.
 
+Notation "{| x |}" :=  (L x).
+Infix "∪" := U (at level 8, right associativity).
+Notation "∅" := E.
+
+(** Properties of union *)
 Lemma union_idem : forall (X : FSet A), U X X = X.
 Proof.
 hinduction; try (intros; apply set_path2).
@@ -347,6 +352,7 @@ hinduction; try (intros; apply set_path2).
   rewrite comm. reflexivity.
 Defined.
 
+(** Membership predicate *)
 Definition isIn : A -> FSet A -> Bool.
 Proof.
 intros a.
@@ -361,23 +367,25 @@ hrecursion.
 - intros a'. compute. destruct (A_eqdec a a'); reflexivity.
 Defined.
 
-Lemma isIn_eq a b : isIn a (L b) = true -> a = b.
+Infix "∈" := isIn (at level 9, right associativity).
+
+Lemma isIn_singleton_eq a b : a ∈ {| b |} = true -> a = b.
 Proof. cbv.
 destruct (A_eqdec a b). intro. apply p.
 intro X. 
-pose (false_ne_true X). contradiction.
+contradiction (false_ne_true X).
 Defined.
 
-Lemma isIn_empt_false a : isIn a E = true -> Empty.
+Lemma isIn_empty_false a : a ∈ ∅ = true -> Empty.
 Proof. 
 cbv. intro X.
-pose (false_ne_true X). contradiction.
+contradiction (false_ne_true X). 
 Defined.
 
-Lemma isIn_union a X Y : isIn a (U X Y) = orb (isIn a X) (isIn a Y).
+Lemma isIn_union a X Y : a ∈ (X ∪ Y) = (a ∈ X || a ∈ Y)%Bool.
 Proof. reflexivity. Qed. 
 
-
+(** Set comprehension *)
 Definition comprehension : 
   (A -> Bool) -> FSet A -> FSet A.
 Proof.
@@ -397,7 +405,7 @@ hrecursion.
   + apply nl.
 Defined.
 
-Lemma comprehension_false Y : comprehension (fun a => isIn a E) Y = E.
+Lemma comprehension_false Y : comprehension (fun a => a ∈ ∅) Y = E.
 Proof.
 hrecursion Y; try (intros; apply set_path2).
 - cbn. reflexivity.
@@ -411,7 +419,7 @@ hrecursion Y; try (intros; apply set_path2).
 Defined.
 
 Lemma comprehension_idem' `{Funext}: 
-   forall (X:FSet A), forall Y, comprehension (fun x => isIn x (U X Y)) X = X.
+   forall (X:FSet A), forall Y, comprehension (fun x => x ∈ (U X Y)) X = X.
 Proof.
 hinduction.
 all: try (intros; apply path_forall; intro; apply set_path2).
@@ -431,7 +439,7 @@ all: try (intros; apply path_forall; intro; apply set_path2).
 Defined.
 
 Lemma comprehension_idem `{Funext}: 
-   forall (X:FSet A), comprehension (fun x => isIn x X) X = X.
+   forall (X:FSet A), comprehension (fun x => x ∈ X) X = X.
 Proof.
 intros X.
 enough (comprehension (fun x : A => isIn x (U X X)) X = X).
@@ -439,6 +447,7 @@ rewrite (union_idem) in X0. assumption.
 apply comprehension_idem'.
 Defined.
 
+(** Set intersection *)
 Definition intersection : 
   FSet A -> FSet A -> FSet A.
 Proof.
@@ -446,12 +455,13 @@ intros X Y.
 apply (comprehension (fun (a : A) => isIn a X) Y).
 Defined.
 
-Definition subset (x : FSet A) (y : FSet A) : Bool.
-Proof.
+(** Subset ordering *)
+Definition subset : forall (x : FSet A) (y : FSet A), Bool.
+Proof. intros x y.
 hrecursion x.
 - apply true.
 - intro a. apply (isIn a y).
-- apply andb.
+- intros a b. apply (andb a b).
 - intros a b c. compute. destruct a; reflexivity.
 - intros a b. compute. destruct a, b; reflexivity.
 - intros x. compute. reflexivity.
@@ -460,15 +470,6 @@ hrecursion x.
   destruct (isIn a y); reflexivity.
 Defined.
 
-Definition equal_set (x : FSet A) (y : FSet A) : Bool
-  := andb (subset x y) (subset y x).
-
-Fixpoint eq_nat n m : Bool :=
-  match n, m with
-    | O, O => true
-    | O, S _ => false
-    | S _, O => false
-    | S n1, S m1 => eq_nat n1 m1
-  end.
+Infix "⊆" := subset (at level 8, right associativity).
 
 End functions.
\ No newline at end of file

From 5abf0acf060ad1d992ce5f83f8940361686392f6 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@covariant.me>
Date: Tue, 23 May 2017 12:12:22 +0200
Subject: [PATCH 8/8] Switch to the DecidablePaths typeclass

---
 FinSets.v | 20 +++++++-------------
 1 file changed, 7 insertions(+), 13 deletions(-)

diff --git a/FinSets.v b/FinSets.v
index 797f18e..93a8a4c 100644
--- a/FinSets.v
+++ b/FinSets.v
@@ -331,9 +331,7 @@ End FinSet.
 
 Section functions.
 Parameter A : Type.
-Context (A_eqdec: forall (x y : A), Decidable (x = y)).
-Definition deceq (x y : A) :=
-  if dec (x = y) then true else false.
+Context {A_eqdec: DecidablePaths A}.
 
 Notation "{| x |}" :=  (L x).
 Infix "∪" := U (at level 8, right associativity).
@@ -358,7 +356,7 @@ Proof.
 intros a.
 hrecursion.
 - exact false.
-- intro a'. apply (deceq a a').
+- intro a'. destruct (dec (a = a')); [exact true | exact false].
 - apply orb. 
 - intros x y z. compute. destruct x; reflexivity.
 - intros x y. compute. destruct x, y; reflexivity.
@@ -457,7 +455,6 @@ hinduction.
 all: try (intros; apply path_forall; intro; apply set_path2).
 - intro Y. cbv. reflexivity.
 - intros a Y. cbn.
-  unfold deceq;
   destruct (dec (a = a)); simpl.
   + reflexivity.
   + contradiction n. reflexivity.
@@ -494,7 +491,7 @@ hrecursion X;  try (intros; apply set_path2).
 - cbn. unfold intersection. intros a.
   hrecursion Y; try (intros; apply set_path2).
   + cbn. reflexivity.
-  + cbn. intros. unfold deceq. 
+  + cbn. intros.
   		destruct  (dec (a0 = a)). 
   		rewrite p. destruct (dec (a=a)).
   		reflexivity.
@@ -504,17 +501,14 @@ hrecursion X;  try (intros; apply set_path2).
 		contradiction n. apply p^. reflexivity.
  	+ cbn -[isIn]. intros Y1 Y2 IH1 IH2.
  	 	rewrite IH1. 
- 	 	rewrite IH2.
- 	 	symmetry.
- 	 	rewrite 	(comprehension_union (L a)).
- 	 	reflexivity.
+ 	 	rewrite IH2. 	 	
+ 	 	apply 	(comprehension_union (L a)).
 - intros X1 X2 IH1 IH2.
   cbn.
   unfold intersection in *.
   rewrite <- IH1.
-  rewrite <- IH2.
-	rewrite comprehension_union.
-	reflexivity.
+  rewrite <- IH2. symmetry.
+	apply comprehension_union.
 Defined.