Added basis for reflection in interface

FiniteSets/fsets/properties.v

@@ -181,4 +181,33 @@ Section properties.
         apply (tr (inl Xa)).
   Defined.
 
+  Lemma comprehension_isIn (ϕ : A -> Bool) (a : A) : forall X : FSet A,
+      isIn a (comprehension ϕ X) = if ϕ a then isIn a X else False_hp.
+  Proof.
+    hinduction ; try (intros ; apply set_path2) ; cbn.
+    - destruct (ϕ a) ; reflexivity.
+    - intros b.
+      assert (forall c d, ϕ a = c -> ϕ b = d ->
+                          a ∈ (if ϕ b then {|b|} else ∅)
+                          =
+                          (if ϕ a then BuildhProp (Trunc (-1) (a = b)) else False_hp)) as X.
+      {
+        intros c d Hc Hd.
+        destruct c ; destruct d ; rewrite Hc, Hd ; try reflexivity
+        ; apply path_iff_hprop ; try contradiction ; intros ; strip_truncations
+        ; apply (false_ne_true).
+        * apply (Hd^ @ ap ϕ X^ @ Hc). 
+        * apply (Hc^ @ ap ϕ X @ Hd).
+      }
+      apply (X (ϕ a) (ϕ b) idpath idpath).
+    - intros X Y H1 H2.
+      rewrite H1, H2.
+      destruct (ϕ a).
+      * reflexivity.
+      * apply path_iff_hprop.
+        ** intros Z ; strip_truncations.
+           destruct Z ; assumption.
+        ** intros ; apply tr ; right ; assumption.
+  Defined.
+  
 End properties.

FiniteSets/implementations/interface.v

@@ -41,3 +41,69 @@ Section interface.
       f_member : forall A a X, member a X = isIn a (f A X)
     }.
 End interface.
+
+Section properties.
+  Context `{Univalence}.
+  Variable (T : Type -> Type) (f : forall A, T A -> FSet A).
+  Context `{sets T f}.
+
+  Definition set_eq : forall A, T A -> T A -> hProp := fun A X Y =>  (BuildhProp (f A X = f A Y)).
+
+  Definition set_subset : forall A, T A -> T A -> hProp := fun A X Y => subset (f A X) (f A Y).
+
+  Ltac reduce := intros ; repeat (rewrite ?(f_empty _ _) ; rewrite ?(f_singleton _ _) ;
+                         rewrite ?(f_union _ _) ; rewrite ?(f_filter _ _) ;
+                         rewrite ?(f_member _ _)).
+
+  Definition empty_isIn : forall (A : Type) (a : A), member a empty = False_hp.
+  Proof.
+    reduce.
+    reflexivity.
+  Defined.
+
+  Definition singleton_isIn : forall (A : Type) (a b : A),
+      member a (singleton b) = BuildhProp (Trunc (-1) (a = b)).
+  Proof.
+    reduce.
+    reflexivity.
+  Defined.
+
+  Definition union_isIn : forall (A : Type) (a : A) (X Y : T A),
+      member a (union X Y) = lor (member a X) (member a Y).
+  Proof.
+    reduce.
+    reflexivity.
+  Defined.
+
+  Definition filter_isIn : forall (A : Type) (a : A) (ϕ : A -> Bool) (X : T A),
+      member a (filter ϕ X) = if ϕ a then member a X else False_hp.
+  Proof.
+    reduce.
+    apply properties.comprehension_isIn.
+  Defined.
+
+  Definition reflect_eq : forall (A : Type) (X Y : T A),
+      f A X = f A Y -> set_eq A X Y.
+  Proof.
+    auto.
+  Defined.
+
+  Definition reflect_subset : forall (A : Type) (X Y : T A),
+      subset (f A X) (f A Y) -> set_subset A X Y.
+  Proof.
+    auto.
+  Defined.
+
+  Variable (A : Type).
+  Context `{DecidablePaths A}.
+  
+  Lemma union_comm : forall (X Y : T A),
+      set_eq A (union X Y) (union Y X).
+  Proof.
+    intros.
+    apply reflect_eq.
+    reduce.
+    apply lattice_fset.
+  Defined.
+
+End properties.