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