Merge remote-tracking branch 'origin/bloop' into properties

FiniteSets/operations.v

@@ -1,6 +1,5 @@
 Require Import HoTT HitTactics.
 Require Import definition.
-
 Section operations.
 
 Context {A : Type}.
@@ -48,4 +47,22 @@ intros X Y.
 apply (comprehension (fun (a : A) => isIn a X) Y).
 Defined.
 
+
+Definition subset :
+	FSet A -> FSet A -> Bool.
+Proof.
+intros X Y.
+hrecursion X. 
+- exact true.
+- exact (fun a => (a ∈ Y)).
+- exact andb.
+- intros. compute. destruct x; reflexivity.
+- intros x y; compute; destruct x, y; reflexivity. 
+- intros x; compute; destruct x; reflexivity.
+- intros x; compute; destruct x; reflexivity.
+- intros x; cbn; destruct (x ∈ Y); reflexivity.
+Defined.
+
+Notation "⊆" := subset.
+
 End operations.

FiniteSets/properties.v

@@ -1,5 +1,5 @@
 Require Import HoTT HitTactics.
-Require Import definition operations.
+Require Export definition operations.
 
 Section properties.
 
@@ -20,8 +20,7 @@ try (intros ; apply set_path2) ; cbn.
   rewrite P.
   rewrite (comm y x).
   rewrite <- (assoc x y y).
-  rewrite Q.
+  f_ap. 
-  reflexivity.
 Defined.
 
   
@@ -177,26 +176,29 @@ Defined.
 
 Theorem intersection_idem : forall (X : FSet A), intersection X X = X.
 Proof.
-hinduction; try (intros; apply set_path2).
+hinduction; try (intros ; apply set_path2).
 - reflexivity.
 - intro a.
   destruct (dec (a = a)).
   * reflexivity.
   * contradiction (n idpath).
 - intros X Y IHX IHY.
+  f_ap;
   unfold intersection in *.
-  rewrite comprehension_or.
+  + transitivity (U (comprehension (fun a => isIn a X) X) (comprehension (fun a => isIn a Y) X)).
-  rewrite comprehension_or.
+    apply comprehension_or.
-  rewrite IHX.
+    rewrite IHX.
-  rewrite IHY.
+    rewrite (comm X).    
-  rewrite comprehension_subset.
+    apply comprehension_subset.
-  rewrite (comm X).
+  + transitivity (U (comprehension (fun a => isIn a X) Y) (comprehension (fun a => isIn a Y) Y)).
-  rewrite comprehension_subset.
+    apply comprehension_or.
-  reflexivity.
+    rewrite IHY.
+    apply comprehension_subset.
 Defined.
 
 (** assorted lattice laws *)
-Lemma distributive_La (z : FSet A) (a : A) : forall Y : FSet A, intersection (U (L a) z) Y = U (intersection (L a) Y) (intersection z Y).
+Lemma distributive_La (z : FSet A) (a : A) : forall Y : FSet A, 
+       intersection (U (L a) z) Y = U (intersection (L a) Y) (intersection z Y).
 Proof.
 hinduction; try (intros ; apply set_path2) ; cbn.
 - symmetry ; apply nl.
@@ -265,11 +267,10 @@ hinduction x; try (intros ; apply set_path2) ; cbn.
   cbn.
   rewrite P.
   rewrite Q.
-  destruct (isIn a X1) ; destruct (isIn a X2) ; destruct (isIn a y) ; reflexivity.
+  destruct (isIn a X1) ; destruct (isIn a X2) ; destruct (isIn a y) ; 
+  reflexivity.
 Defined.
 
-
-
 Theorem intersection_assoc (X Y Z: FSet A) :
     intersection X (intersection Y Z) = intersection (intersection X Y) Z.
 Proof.
@@ -312,14 +313,12 @@ hinduction; try (intros ; apply set_path2).
   * reflexivity.
   * contradiction (n idpath).
 - intros X1 X2 P Q.
-  rewrite comprehension_or.
+  f_ap; (etransitivity; [ apply comprehension_or |]).
-  rewrite comprehension_or.
+  rewrite P. rewrite (comm X1).
-  rewrite P.
+  apply comprehension_subset.
+
   rewrite Q.
-  rewrite comprehension_subset.
+  apply comprehension_subset.
-  rewrite (comm X1).
-  rewrite comprehension_subset.
-  reflexivity.
 Defined.
 
   
@@ -336,17 +335,22 @@ hinduction X1; try (intros ; apply set_path2) ; cbn.
   rewrite p.
   rewrite comprehension_subset.
   reflexivity.
-- intros. unfold intersection. (* TODO isIn is simplified too much *)
+- intros.
-  rewrite comprehension_or.
+  assert (Y = intersection (U (L a) Y) Y) as HY.
-  rewrite comprehension_or.
+  { unfold intersection. symmetry.
-  (* rewrite intersection_La. *)
+    transitivity (U (comprehension (fun x => isIn x (L a)) Y) (comprehension (fun x => isIn x Y) Y)).
+    apply comprehension_or.
+    rewrite comprehension_all.
+    apply comprehension_subset. }
+  rewrite <- HY.
   admit.
 - unfold intersection.
-  cbn.
   intros Z1 Z2 P Q.
   rewrite comprehension_or.
-  assert (U (U (comprehension (fun a : A => isIn a Z1) X2) (comprehension (fun a : A => isIn a Z2) X2))
+  assert (U (U (comprehension (fun a : A => isIn a Z1) X2) 
-    Y = U (U (comprehension (fun a : A => isIn a Z1) X2) (comprehension (fun a : A => isIn a Z2) X2))
+  	(comprehension (fun a : A => isIn a Z2) X2))
+    Y = U (U (comprehension (fun a : A => isIn a Z1) X2) 
+  (comprehension (fun a : A => isIn a Z2) X2))
     (U Y Y)).
     rewrite (union_idem Y).
     reflexivity.
@@ -354,20 +358,24 @@ hinduction X1; try (intros ; apply set_path2) ; cbn.
   rewrite <- assoc.
   rewrite (assoc (comprehension (fun a : A => isIn a Z2) X2)).
   rewrite Q.
-  rewrite (comm (U (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) X2)
+  cbn.
-                   (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) Y)) Y).
+  rewrite 
+  (comm (U (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) X2)
+           (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) Y)) Y).
   rewrite assoc.
   rewrite P.
-  rewrite <- assoc.
+  rewrite <- assoc. cbn.
   rewrite (assoc (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) Y)).
   rewrite (comm (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) Y)).
   rewrite <- assoc.
   rewrite assoc.
   enough (C : (U (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) X2)
-             (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) X2)) = (comprehension (fun a : A => (isIn a Z1 || isIn a Z2 || isIn a Y)%Bool) X2)).
+             (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) X2)) 
+ = (comprehension (fun a : A => (isIn a Z1 || isIn a Z2 || isIn a Y)%Bool) X2)).
   rewrite C. 
   enough (D :  (U (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) Y)
-                  (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) Y)) = (comprehension (fun a : A => (isIn a Z1 || isIn a Z2 || isIn a Y)%Bool) Y)).
+                  (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) Y)) 
+ = (comprehension (fun a : A => (isIn a Z1 || isIn a Z2 || isIn a Y)%Bool) Y)).
   rewrite D.
   reflexivity.
   * repeat (rewrite comprehension_or).
@@ -429,10 +437,166 @@ hrecursion X; try (intros ; apply set_path2).
   rewrite <- Q.
 Admitted.
 
+<<<<<<< HEAD
 Theorem union_isIn (X Y : FSet A) (a : A) : isIn a (U X Y) = orb (isIn a X) (isIn a Y).
 Proof.
 reflexivity.  
 Defined.
                                                                 
   
+=======
+
+(* Properties about subset relation. *)
+Lemma subset_union `{Funext} (X Y : FSet A) : 
+  subset X Y = true -> U X Y = Y.
+Proof.
+hinduction X; try (intros; apply path_forall; intro; apply set_path2).
+- intros. apply nl.
+- intros a. hinduction Y;
+  try (intros; apply path_forall; intro; apply set_path2).
+  + intro. contradiction (false_ne_true).
+  + intros. destruct (dec (a = a0)).
+    rewrite p; apply idem.
+    contradiction (false_ne_true).
+  + intros X1 X2 IH1 IH2.
+    intro Ho.
+    destruct (isIn a X1);
+      destruct (isIn a X2).
+    * specialize (IH1 idpath).
+      rewrite assoc. f_ap. 
+    * specialize (IH1 idpath).
+      rewrite assoc. f_ap. 
+    * specialize (IH2 idpath).
+      rewrite (comm X1 X2).
+      rewrite assoc. f_ap. 
+    * contradiction (false_ne_true). 
+- intros X1 X2 IH1 IH2 G. 
+  destruct (subset X1 Y);
+    destruct (subset X2 Y).
+  * specialize (IH1 idpath).    
+    specialize (IH2 idpath).
+    rewrite <- assoc. rewrite IH2. apply IH1. 
+  * contradiction (false_ne_true).
+  * contradiction (false_ne_true).
+  * contradiction (false_ne_true).
+Defined.
+
+Lemma eq1 (X Y : FSet A) : X = Y <~> (U Y X = X) * (U X Y = Y).
+Proof.
+  unshelve eapply BuildEquiv.
+  { intro H. rewrite H. split; apply union_idem. }
+  unshelve esplit.
+  { intros [H1 H2]. etransitivity. apply H1^.
+    rewrite comm. apply H2. }
+  intro; apply path_prod; apply set_path2. 
+  all: intro; apply set_path2.  
+Defined.
+
+
+Lemma subset_union_l `{Funext} X :
+  forall Y, subset X (U X Y) = true.
+hinduction X;
+  try (intros; apply path_forall; intro; apply set_path2).
+- reflexivity.
+- intros a Y. destruct (dec (a = a)).
+  * reflexivity.
+  * by contradiction n.
+- intros X1 X2 HX1 HX2 Y.
+  enough (subset X1 (U (U X1 X2) Y) = true).
+  enough (subset X2 (U (U X1 X2) Y) = true).
+  rewrite X. rewrite X0. reflexivity.
+  { rewrite (comm X1 X2).
+    rewrite <- (assoc X2 X1 Y).
+    apply (HX2 (U X1 Y)). }
+  { rewrite <- (assoc X1 X2 Y). apply (HX1 (U X2 Y)). }
+Defined.
+
+Lemma subset_union_equiv `{Funext}
+  : forall X Y : FSet A, subset X Y = true <~> U X Y = Y.
+Proof.
+  intros X Y.
+  unshelve eapply BuildEquiv.
+  apply subset_union.
+  unshelve esplit.
+  { intros HXY. rewrite <- HXY. clear HXY.
+    apply subset_union_l. }
+  all: intro; apply set_path2.
+Defined.
+
+Lemma eq_subset `{Funext} (X Y : FSet A) :
+  X = Y <~> ((subset Y X = true) * (subset X Y = true)).
+Proof.
+  transitivity ((U Y X = X) * (U X Y = Y)).
+  apply eq1.
+  symmetry.
+  eapply equiv_functor_prod'; apply subset_union_equiv.
+Defined.
+
+Lemma subset_isIn `{FE : Funext} (X Y : FSet A) :
+  (forall (a : A), isIn a X = true -> isIn a Y = true)
+  <-> (subset X Y = true).
+Proof.
+  split.
+  - hinduction X ; try (intros ; apply path_forall ; intro ; apply set_path2).
+    * intros ; reflexivity.
+    * intros a H. 
+      apply H.
+      destruct (dec (a = a)).
+      + reflexivity.
+      + contradiction (n idpath).
+    * intros X1 X2 H1 H2 H.
+      enough (subset X1 Y = true).
+      rewrite X.
+      enough (subset X2 Y = true).
+      rewrite X0.
+      reflexivity.
+      + apply H2.
+        intros a Ha.
+        apply H.
+        rewrite Ha.
+        destruct (isIn a X1) ; reflexivity.
+      + apply H1.
+        intros a Ha.
+        apply H.
+        rewrite Ha.
+        reflexivity.        
+  - hinduction X .
+    * intros. contradiction (false_ne_true X0).
+    * intros b H a.
+      destruct (dec (a = b)).
+      + intros ; rewrite p ; apply H.
+      + intros X ; contradiction (false_ne_true X).
+        * intros X1 X2.
+          intros IH1 IH2 H1 a H2.
+          destruct (subset X1 Y) ; destruct (subset X2 Y);
+            cbv in H1; try by contradiction false_ne_true.
+          specialize (IH1 idpath a). specialize (IH2 idpath a).
+          destruct (isIn a X1); destruct (isIn a X2);
+            cbv in H2; try by contradiction false_ne_true.
+          by apply IH1.
+          by apply IH1.
+          by apply IH2.
+        * repeat (intro; intros; apply path_forall).
+          intros; intro; intros; apply set_path2.
+        * repeat (intro; intros; apply path_forall).
+          intros; intro; intros; apply set_path2.
+        * repeat (intro; intros; apply path_forall).
+          intros; intro; intros; apply set_path2.
+        * repeat (intro; intros; apply path_forall).
+          intros; intro; intros; apply set_path2.
+        * repeat (intro; intros; apply path_forall);
+          intros; intro; intros; apply set_path2.
+Defined.
+
+Theorem fset_ext `{Funext} (X Y : FSet A) :
+  X = Y <~> (forall (a : A), isIn a X = isIn a Y).
+Proof.
+  etransitivity. apply eq_subset.
+  transitivity
+    ((forall a, isIn a Y = true -> isIn a X = true)
+     *(forall a, isIn a X = true -> isIn a Y = true)).
+  - eapply equiv_functor_prod'. admit. admit.
+  - eapply equiv_functor_prod'. 
+Admitted.
+
 End properties.