Removed View_rec2

FiniteSets/implementations/interface.v

@@ -130,6 +130,8 @@ Section quotient_surjection.
 
 End quotient_surjection.
 
+Arguments quotient_iso {_} {_} _ {_} {_} {_}.
+  
 Ltac reduce T :=
   intros ;
   repeat (rewrite (f_empty T _)
@@ -137,12 +139,6 @@ Ltac reduce T :=
           || rewrite (f_union T _)
           || rewrite (f_filter T _)
           || rewrite (f_member T _)).
-Ltac simplify T := intros ; autounfold in * ; apply reflect_eq ; reduce T.
-Ltac reflect_equality T := simplify T ; eauto with lattice_hints typeclass_instances.
-Ltac reflect_eq T := autounfold
-                     ; repeat (hinduction ; try (intros ; apply path_ishprop) ; intro)
-                     ; apply related_classes_eq
-                     ; reflect_equality T.
 
 Section quotient_properties.
   Variable (T : Type -> Type).
@@ -152,42 +148,70 @@ Section quotient_properties.
   Definition set_eq A := f_eq (T A) (FSet A) (f A).
   Definition View A : Type := quotientB (T A) (FSet A) (f A).
 
-  Definition View_rec2 {A} (P : Type) (HP : IsHSet P) (u : T A -> T A -> P)
+  Instance f_is_surjective A : IsSurjection (f A).
-    (Hresp : forall (x x' y y': T A), set_eq A x x' -> set_eq A y y' -> u x y = u x' y')
-    : forall (x y : View A), P.
   Proof.
-    unfold View ; hrecursion.
+    apply (f_surjective T f A).
-    - intros a.
-      hrecursion.
-      + apply (u a). 
-      + intros b b' Hbb'.
-        apply Hresp.
-        ++ reflexivity.
-        ++ assumption.
-    - intros ; simpl.
-      apply path_forall.
-      red.
-      hinduction ; try (intros ; apply path_ishprop).
-      intros b.
-      apply Hresp.
-      ++ assumption.
-      ++ reflexivity.
   Defined.
     
-  Definition well_defined_union (A : Type) (X1 X2 Y1 Y2 : T A) :
+  Global Instance view_union (A : Type) : hasUnion (View A).
-    set_eq A X1 Y1 -> set_eq A X2 Y2 -> set_eq A (union X1 X2) (union Y1 Y2).
   Proof.
-    intros HXY1 HXY2.
+    intros X Y.
-    simplify T.
+    apply (quotient_iso _)^-1.
-    by rewrite HXY1, HXY2.
+    simple refine (union _ _).
+    - simple refine (quotient_iso (f A) X).
+    - simple refine (quotient_iso (f A) Y).
   Defined.
 
-  Definition well_defined_filter (A : Type) (ϕ : A -> Bool) (X Y : T A) :
+  Definition well_defined_union (A : Type) (X Y : T A) :
-    set_eq A X Y -> set_eq A (filter ϕ X) (filter ϕ Y).
+    (class_of _ X) ∪ (class_of _ Y) = class_of _ (X ∪ Y).
   Proof.
-    intros HXY.
+    rewrite <- (eissect (quotient_iso _)).
-    simplify T.
+    simpl.
-    by rewrite HXY.
+    rewrite (f_union T _).
+    reflexivity.
+  Defined.
+
+  Global Instance view_comprehension (A : Type) : hasComprehension (View A) A.
+  Proof.
+    intros ϕ X.
+    apply (quotient_iso _)^-1.
+    simple refine ({|_ & ϕ|}).
+    apply (quotient_iso (f A) X).
+  Defined.
+
+  Definition well_defined_filter (A : Type) (ϕ : A -> Bool) (X : T A) :
+    {|class_of _ X & ϕ|} = class_of _ {|X & ϕ|}.
+  Proof.
+    rewrite <- (eissect (quotient_iso _)).
+    simpl.
+    rewrite (f_filter T _).
+    reflexivity.
+  Defined.
+
+  Global Instance View_empty A : hasEmpty (View A).
+  Proof.
+    apply ((quotient_iso _)^-1 ∅).
+  Defined.
+
+  Definition well_defined_empty A : ∅ = class_of (set_eq A) ∅.
+  Proof.
+    rewrite <- (eissect (quotient_iso _)).
+    simpl.
+    rewrite (f_empty T _).
+    reflexivity.
+  Defined.  
+
+  Global Instance View_singleton A: hasSingleton (View A) A.
+  Proof.
+    intro a ; apply ((quotient_iso _)^-1 {|a|}).
+  Defined.
+
+  Definition well_defined_sungleton A (a : A) : {|a|} = class_of _ {|a|}.
+  Proof.
+    rewrite <- (eissect (quotient_iso _)).
+    simpl.
+    rewrite (f_singleton T _).
+    reflexivity.
   Defined.  
   
   Global Instance View_member A : hasMembership (View A) A.
@@ -200,54 +224,30 @@ Section quotient_properties.
       apply (ap _ HXY).
   Defined.
 
-  Global Instance View_empty A: hasEmpty (View A).
-  Proof.
-    apply (class_of _ ∅).
-  Defined.
-
-  Global Instance View_singleton A: hasSingleton (View A) A.
-  Proof.
-    intros a.
-    apply (class_of _ {|a|}).
-  Defined.
-
   Instance View_max A : maximum (View A).
   Proof.
-    simple refine (View_rec2 _ _ _ _).
+    apply view_union.
-    - intros a b.
-      apply (class_of _ (union a b)).
-    - intros x x' Hxx' y y' Hyy' ; simpl.
-      apply related_classes_eq.
-      eapply well_defined_union ; eauto.
   Defined.
 
-  Global Instance View_union A: hasUnion (View A).
+  Hint Unfold Commutative Associative Idempotent NeutralL NeutralR View_max view_union.
-  Proof.
-    apply max_L.
-  Defined.
-
-  Global Instance View_comprehension A: hasComprehension (View A) A.
-  Proof.
-    intros ϕ ; unfold View.
-    hrecursion.
-    - intros X.
-      apply (class_of _ (filter ϕ X)).
-    - intros X X' HXX' ; simpl.
-      apply related_classes_eq.
-      eapply well_defined_filter ; eauto.
-  Defined.
-
-  Hint Unfold Commutative Associative Idempotent NeutralL NeutralR.
 
   Instance bottom_view A : bottom (View A).
   Proof.
-    unfold bottom.
+    apply View_empty.
-    apply ∅.
   Defined.
 
+  Ltac sq1 := autounfold ; intros ; try f_ap
+                         ; rewrite ?(eisretr (quotient_iso _))
+                         ; eauto with lattice_hints typeclass_instances.
+
+  Ltac sq2 := autounfold ; intros
+              ; rewrite <- (eissect (quotient_iso _)), ?(eisretr (quotient_iso _))
+              ; f_ap ; simpl
+              ; reduce T ; eauto with lattice_hints typeclass_instances.
+
   Global Instance view_lattice A : JoinSemiLattice (View A).
   Proof.
-    split ; reflect_eq T.
+    split ; try sq1 ; try sq2.
   Defined.
 
 End quotient_properties.
@@ -294,20 +294,8 @@ Section properties.
     refine (same_class _ _ _ _ _ _) ; assumption.
   Defined.
 
-  Lemma class_union (A : Type) (X Y : T A) :
+  Ltac via_quotient := intros ; apply reflect_f_eq ; simpl
-      class_of (set_eq f) (X ∪ Y) = (class_of (set_eq f) X) ∪ (class_of (set_eq f) Y).
+                       ; rewrite <- ?(well_defined_union T _), <- ?(well_defined_empty T _)
-  Proof.
-    reflexivity.
-  Defined.
-
-  Lemma class_filter (A : Type) (X : T A) (ϕ : A -> Bool) :
-    class_of (set_eq f) ({|X & ϕ|}) = {|(class_of (set_eq f) X) & ϕ|}.
-  Proof.
-    reflexivity.
-  Defined.
-
-  Ltac via_quotient := intros ; apply reflect_f_eq
-                       ; rewrite ?class_union, ?class_filter
                        ; eauto with lattice_hints typeclass_instances.  
 
   Lemma union_comm : forall A (X Y : T A),
@@ -328,10 +316,16 @@ Section properties.
     via_quotient.
   Defined.
 
-  Lemma union_neutral : forall A (X : T A),
+  Lemma union_neutralL : forall A (X : T A),
     set_eq f (∅ ∪ X) X.
   Proof.
     via_quotient.
   Defined.
 
+  Lemma union_neutralR : forall A (X : T A),
+    set_eq f (X ∪ ∅) X.
+  Proof.
+    via_quotient.
+  Defined.
+  
 End properties.