Added product

FiniteSets/fsets/operations.v

@@ -76,6 +76,47 @@ Section operations.
     intros ; symmetry ; eauto with lattice_hints typeclass_instances.
   Defined.
 
+  Lemma union_idemL Z : forall x: FSet Z, x ∪ x = x.
+  Proof.
+    hinduction ; try (intros ; apply set_path2).
+    - apply nl.
+    - apply idem.
+    - intros x y P Q.
+      rewrite assoc.
+      rewrite (comm x y).
+      rewrite <- (assoc y x x).
+      rewrite P.
+      rewrite (comm y x).
+      rewrite <- (assoc x y y).
+      f_ap. 
+  Defined.
+
+  Context {B : Type}.
+  
+  Definition product : FSet A -> FSet B -> FSet (A * B).
+  Proof.
+    intros X Y.
+    hrecursion X.
+    - apply ∅.
+    - intro a.
+      hrecursion Y ; simpl in *.
+      * apply ∅.
+      * intro b.
+        apply {|(a, b)|}.
+      * apply U.
+      * intros X Y Z ; apply assoc.
+      * intros X Y ; apply comm.
+      * intros ; apply nl.
+      * intros ; apply nr.
+      * intros ; apply idem.
+    - apply U.
+    - intros ; apply assoc.
+    - intros ; apply comm.
+    - intros ; apply nl.
+    - intros ; apply nr.
+    - intros ; apply union_idemL.
+  Defined.
+  
 End operations.
 
 Infix "∈" := isIn (at level 9, right associativity).

FiniteSets/fsets/properties.v

@@ -137,6 +137,36 @@ Section properties.
         ** intros ; apply tr ; right ; assumption.
   Defined.
 
+  Context {B : Type}.
+  
+  Definition isIn_product : forall (a : A) (b : B) (X : FSet A) (Y : FSet B),
+      isIn a X -> isIn b Y -> isIn (a,b) (product X Y).
+  Proof.
+    intros a b X Y.
+    hinduction X ; try (intros ; apply path_forall ; intro ; apply path_ishprop).
+    - contradiction.
+    - intros c Hc.
+      hinduction Y ; try (intros ; apply path_forall ; intro ; apply path_ishprop).
+      * contradiction.
+      * intros d Hd.
+        strip_truncations.
+        apply tr.
+        rewrite Hc, Hd.
+        reflexivity.
+      * intros Y1 Y2 HY1 HY2 HOr.
+        strip_truncations.
+        apply tr.
+        destruct HOr as [H1 | H2].
+        ** apply (inl (HY1 H1)).
+        ** apply (inr (HY2 H2)).
+    - intros X1 X2 HX1 HX2 Hor HY.
+      strip_truncations.
+      apply tr.
+      destruct Hor as [H1 | H2].
+      * apply (inl(HX1 H1 HY)).
+      * apply (inr (HX2 H2 HY)).
+  Defined.
+
   (* The proof can be simplified using extensionality *)
   (** comprehension properties *)
   Lemma comprehension_false Y : comprehension (fun (_ : A) => false) Y = ∅.