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] 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 :