Changed lattice

FiniteSets/_CoqProject

@@ -16,8 +16,8 @@ fsets/properties_decidable.v
 fsets/length.v
 fsets/monad.v
 FSets.v
+Sub.v
 implementations/lists.v
 variations/enumerated.v
-variations/k_finite.v
 #empty_set.v
 #ordered.v

FiniteSets/disjunction.v

@@ -2,7 +2,7 @@
 Require Import HoTT.
 Require Import lattice.
 
-Definition lor (X Y : hProp) : hProp := BuildhProp (Trunc (-1) (sum X Y)).
+Instance lor : maximum hProp := fun X Y => BuildhProp (Trunc (-1) (sum X Y)).
 
 Delimit Scope logic_scope with L.
 Notation "A ∨ B" := (lor A B) (at level 20, right associativity) : logic_scope.
@@ -75,7 +75,8 @@ Section lor_props.
 
 End lor_props.
 
-Definition land (X Y : hProp) : hProp := BuildhProp (prod X Y).
+Instance land : minimum hProp := fun X Y => BuildhProp (prod X Y).
+Instance lfalse : bottom hProp := False_hp.
 
 Notation "A ∧ B" := (land A B) (at level 20, right associativity) : logic_scope.
 Arguments land _%L _%L.
@@ -84,7 +85,7 @@ Open Scope logic_scope.
 Section hPropLattice.
   Context `{Univalence}.
 
-  Global Instance lor_commutative : Commutative lor.
+  Instance lor_commutative : Commutative lor.
   Proof.
     unfold Commutative.
     intros.
@@ -131,21 +132,21 @@ Section hPropLattice.
     - intros a ; apply (pair a a).
   Defined.
   
-  Instance lor_neutrall : NeutralL lor False_hp.
+  Instance lor_neutrall : NeutralL lor lfalse.
   Proof.
     unfold NeutralL.
     intros.
     apply lor_nl.
   Defined.
 
-  Instance lor_neutralr : NeutralR lor False_hp.
+  Instance lor_neutralr : NeutralR lor lfalse.
   Proof.
     unfold NeutralR.
     intros.
     apply lor_nr.
   Defined.
 
-  Instance bool_absorption_orb_andb : Absorption lor land.
+  Instance absorption_orb_andb : Absorption lor land.
   Proof.
     unfold Absorption.
     intros.
@@ -156,7 +157,7 @@ Section hPropLattice.
       apply (tr (inl X)).
   Defined.
 
-  Instance bool_absorption_andb_orb : Absorption land lor.
+  Instance absorption_andb_orb : Absorption land lor.
   Proof.
     unfold Absorption.
     intros.
@@ -169,15 +170,15 @@ Section hPropLattice.
       * apply (tr (inl X)).
   Defined.
   
-  Global Instance lattice_hprop : Lattice land lor False_hp :=
+  Global Instance lattice_hprop : Lattice hProp :=
     { commutative_min := _ ;
       commutative_max := _ ;
       associative_min := _ ;
       associative_max := _ ;
       idempotent_min := _ ;
       idempotent_max := _ ;
-      neutralL_min := _ ;
+      neutralL_max := _ ;
-      neutralR_min := _ ;
+      neutralR_max := _ ;
       absorption_min_max := _ ;
       absorption_max_min := _
   }.

FiniteSets/fsets/operations.v

@@ -75,11 +75,11 @@ Proof.
   - apply true.
   - apply (fun _ => false).
   - apply andb.
-  - intros. symmetry. eauto with bool_lattice_hints.
+  - intros. symmetry. eauto with lattice_hints typeclass_instances.
-  - eauto with bool_lattice_hints.
+  - eauto with bool_lattice_hints typeclass_instances.
-  - eauto with bool_lattice_hints.
+  - eauto with bool_lattice_hints typeclass_instances.
-  - eauto with bool_lattice_hints.
+  - eauto with bool_lattice_hints typeclass_instances.
-  - eauto with bool_lattice_hints.
+  - eauto with bool_lattice_hints typeclass_instances.
 Defined.    
   
 End operations.

FiniteSets/fsets/operations_decidable.v

@@ -12,7 +12,14 @@ Section decidable_A.
     intros a.
     hinduction ; try (intros ; apply path_ishprop).
     - apply _.
-    - intros. apply _.
+    - intros.
+      unfold Decidable.
+      destruct (dec (a = a0)) as [p | np].
+      * apply (inl (tr p)).
+      * right.
+        intro p.
+        strip_truncations.
+        contradiction.
     - intros. apply _. 
   Defined.
 

FiniteSets/fsets/properties.v

@@ -4,153 +4,151 @@ Require Export representations.definition disjunction fsets.operations.
 (* Lemmas relating operations to the membership predicate *)
 Section operations_isIn.
 
-Context {A : Type}.
+  Context {A : Type}.
-Context `{Univalence}.
+  Context `{Univalence}.
 
+  Lemma union_idem : forall x: FSet A, U 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. 
+  Qed.
 
+  (** ** Properties about subset relation. *)
+  Lemma subset_union (X Y : FSet A) : 
+    subset X Y -> 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.
+      + intro a0.
+        simple refine (Trunc_ind _ _).
+        intro p ; simpl. 
+        rewrite p; apply idem.
+      + intros X1 X2 IH1 IH2.
+        simple refine (Trunc_ind _ _).
+        intros [e1 | e2].
+        ++ rewrite assoc.
+           rewrite (IH1 e1).
+           reflexivity.
+        ++ rewrite comm.
+           rewrite <- assoc.
+           rewrite (comm X2).
+           rewrite (IH2 e2).
+           reflexivity.
+    - intros X1 X2 IH1 IH2 [G1 G2].
+      rewrite <- assoc.
+      rewrite (IH2 G2).
+      apply (IH1 G1).
+  Defined.
 
-Lemma union_idem : forall x: FSet A, U x x = x.
+  Lemma subset_union_l (X : FSet A) :
-Proof.
+    forall Y, subset X (U X Y).
-hinduction; 
+  Proof.
-try (intros ; apply set_path2) ; cbn.
+    hinduction X ;
-- apply nl.
+      try (repeat (intro; intros; apply path_forall); intro; apply equiv_hprop_allpath ; apply _).
-- apply idem.
+    - apply (fun _ => tt).
-- intros x y P Q.
+    - intros a Y.
-  rewrite assoc.
+      apply tr ; left ; apply tr ; reflexivity.
-  rewrite (comm x y).
+    - intros X1 X2 HX1 HX2 Y.
-  rewrite <- (assoc y x x).
+      split. 
-  rewrite P.
+      * rewrite <- assoc. apply HX1.
-  rewrite (comm y x).
+      * rewrite (comm X1 X2). rewrite <- assoc. apply HX2.
-  rewrite <- (assoc x y y).
+  Defined.
-  f_ap. 
-Defined.
 
-(** ** Properties about subset relation. *)
+  (* Union and membership *)
-Lemma subset_union (X Y : FSet A) : 
+  Lemma union_isIn (X Y : FSet A) (a : A) :
-  subset X Y -> U X Y = Y.
+    isIn a (U X Y) = isIn a X ∨ isIn a Y.
-Proof.
+  Proof.
-hinduction X; try (intros; apply path_forall; intro; apply set_path2).
+    reflexivity.
-- intros. apply nl.
+  Defined.
-- intros a. hinduction Y;
-  try (intros; apply path_forall; intro; apply set_path2).
-  + intro.
-    contradiction.
-  + intro a0.
-    simple refine (Trunc_ind _ _).
-    intro p ; cbn. 
-    rewrite p; apply idem.
-  + intros X1 X2 IH1 IH2.
-    simple refine (Trunc_ind _ _).
-    intros [e1 | e2].
-    ++ rewrite assoc.
-       rewrite (IH1 e1).
-       reflexivity.
-    ++ rewrite comm.
-       rewrite <- assoc.
-       rewrite (comm X2).
-       rewrite (IH2 e2).
-       reflexivity.
-- intros X1 X2 IH1 IH2 [G1 G2].
-  rewrite <- assoc.
-  rewrite (IH2 G2).
-  apply (IH1 G1).
-Defined.
 
-Lemma subset_union_l (X : FSet A) :
+  Lemma comprehension_or : forall ϕ ψ (x: FSet A),
-  forall Y, subset X (U X Y).
+      comprehension (fun a => orb (ϕ a) (ψ a)) x = U (comprehension ϕ x) 
-Proof.
+                                                     (comprehension ψ x).
-hinduction X ;
+  Proof.
-  try (repeat (intro; intros; apply path_forall); intro; apply equiv_hprop_allpath ; apply _).
+    intros ϕ ψ.
-- apply (fun _ => tt).
+    hinduction; try (intros; apply set_path2). 
-- intros a Y.
+    - apply (union_idem _)^.
-  apply tr ; left ; apply tr ; reflexivity.
+    - intros.
-- intros X1 X2 HX1 HX2 Y.
+      destruct (ϕ a) ; destruct (ψ a) ; symmetry.
-  split. 
+      * apply union_idem.
-  * rewrite <- assoc. apply HX1.
+      * apply nr. 
-  * rewrite (comm X1 X2). rewrite <- assoc. apply HX2.
+      * apply nl.
-Defined.
+      * apply union_idem.
-
+    - simpl. intros x y P Q.
-(* Union and membership *)
+      rewrite P.
-Lemma union_isIn (X Y : FSet A) (a : A) :
+      rewrite Q.
-  isIn a (U X Y) = isIn a X ∨ isIn a Y.
+      rewrite <- assoc.
-Proof.
+      rewrite (assoc  (comprehension ψ x)).
-  reflexivity.
+      rewrite (comm  (comprehension ψ x) (comprehension ϕ y)).
-Defined.
+      rewrite <- assoc.
-
+      rewrite <- assoc.
-Lemma comprehension_or : forall ϕ ψ (x: FSet A),
+      reflexivity.
-    comprehension (fun a => orb (ϕ a) (ψ a)) x = U (comprehension ϕ x) 
+  Defined.
-    (comprehension ψ x).
-Proof.
-intros ϕ ψ.
-hinduction; try (intros; apply set_path2). 
-- cbn. apply (union_idem _)^.
-- cbn. intros.
-  destruct (ϕ a) ; destruct (ψ a) ; symmetry.
-  * apply union_idem.
-  * apply nr. 
-  * apply nl.
-  * apply union_idem.
-- simpl. intros x y P Q.
-  rewrite P.
-  rewrite Q.
-  rewrite <- assoc.
-  rewrite (assoc  (comprehension ψ x)).
-  rewrite (comm  (comprehension ψ x) (comprehension ϕ y)).
-  rewrite <- assoc.
-  rewrite <- assoc.
-  reflexivity.
-Defined.
 
 End operations_isIn.
 
 (* Other properties *)
 Section properties.
 
-Context {A : Type}.
+  Context {A : Type}.
-Context `{Univalence}.
+  Context `{Univalence}.
 
-(** isIn properties *)
+  (** isIn properties *)
-Lemma singleton_isIn (a b: A) : isIn a (L b) -> Trunc (-1) (a = b).
+  Lemma singleton_isIn (a b: A) : isIn a (L b) -> Trunc (-1) (a = b).
-Proof.
+  Proof.
-  apply idmap.
+    apply idmap.
-Defined.
+  Defined.
 
-Lemma empty_isIn (a: A) : isIn a E -> Empty.
+  Lemma empty_isIn (a: A) : isIn a E -> Empty.
-Proof. 
+  Proof. 
-  apply idmap.
+    apply idmap.
-Defined.
+  Defined.
 
-(** comprehension properties *)
+  (** comprehension properties *)
-Lemma comprehension_false Y : comprehension (fun (_ : A) => false) Y = E.
+  Lemma comprehension_false Y : comprehension (fun (_ : A) => false) Y = E.
-Proof.
+  Proof.
-hrecursion Y; try (intros; apply set_path2).
+    hrecursion Y; try (intros; apply set_path2).
-- reflexivity.
+    - reflexivity.
-- reflexivity.
+    - reflexivity.
-- intros x y IHa IHb.
+    - intros x y IHa IHb.
-  rewrite IHa.
+      rewrite IHa.
-  rewrite IHb.
+      rewrite IHb.
-  apply union_idem.
+      apply union_idem.
-Defined.
+  Defined.
 
-Lemma comprehension_subset : forall ϕ (X : FSet A),
+  Lemma comprehension_subset : forall ϕ (X : FSet A),
-    U (comprehension ϕ X) X = X.
+      U (comprehension ϕ X) X = X.
-Proof.
+  Proof.
-intros ϕ.
+    intros ϕ.
-hrecursion; try (intros ; apply set_path2) ; cbn.
+    hrecursion; try (intros ; apply set_path2) ; cbn.
-- apply union_idem.
+    - apply union_idem.
-- intro a.
+    - intro a.
-  destruct (ϕ a).
+      destruct (ϕ a).
-  * apply union_idem.
+      * apply union_idem.
-  * apply nl.
+      * apply nl.
-- intros X Y P Q.
+    - intros X Y P Q.
-  rewrite assoc.
+      rewrite assoc.
-  rewrite <- (assoc (comprehension ϕ X) (comprehension ϕ Y) X).
+      rewrite <- (assoc (comprehension ϕ X) (comprehension ϕ Y) X).
-  rewrite (comm (comprehension ϕ Y) X).
+      rewrite (comm (comprehension ϕ Y) X).
-  rewrite assoc.
+      rewrite assoc.
-  rewrite P.
+      rewrite P.
-  rewrite <- assoc.
+      rewrite <- assoc.
-  rewrite Q.
+      rewrite Q.
-  reflexivity.
+      reflexivity.
-Defined.
+  Defined.
 
 End properties.

FiniteSets/fsets/properties_decidable.v

@@ -6,135 +6,142 @@ Require Export lattice.
 (* Lemmas relating operations to the membership predicate *)
 Section operations_isIn.
 
-Context {A : Type} `{DecidablePaths A} `{Univalence}.
+  Context {A : Type} `{DecidablePaths A} `{Univalence}.
 
-Lemma ext : forall (S T : FSet A), (forall a, isIn_b a S = isIn_b a T) -> S = T.
+  Lemma ext : forall (S T : FSet A), (forall a, isIn_b a S = isIn_b a T) -> S = T.
-Proof.
+  Proof.
-  intros X Y H2.
+    intros X Y H2.
-  apply fset_ext.
+    apply fset_ext.
-  intro a.
+    intro a.
-  specialize (H2 a).
+    specialize (H2 a).
-  unfold isIn_b, dec in H2.
+    unfold isIn_b, dec in H2.
-  destruct (isIn_decidable a X) ; destruct (isIn_decidable a Y).
+    destruct (isIn_decidable a X) ; destruct (isIn_decidable a Y).
-  - apply path_iff_hprop ; intro ; assumption.
+    - apply path_iff_hprop ; intro ; assumption.
-  - contradiction (true_ne_false).
+    - contradiction (true_ne_false).
-  - contradiction (true_ne_false) ; apply H2^.
+    - contradiction (true_ne_false) ; apply H2^.
-  - apply path_iff_hprop ; intro ; contradiction.
+    - apply path_iff_hprop ; intro ; contradiction.
-Defined.
+  Defined.
 
-Lemma empty_isIn (a : A) :
+  Lemma empty_isIn (a : A) :
-  isIn_b a ∅ = false.
+    isIn_b a ∅ = false.
-Proof.
+  Proof.
-  reflexivity.
+    reflexivity.
-Defined.
+  Defined.
 
-Lemma L_isIn (a b : A) :
+  Lemma L_isIn (a b : A) :
-  isIn a {|b|} -> a = b.
+    isIn a {|b|} -> a = b.
-Proof.
+  Proof.
-  intros. strip_truncations. assumption.
+    intros. strip_truncations. assumption.
-Defined.
+  Defined.
 
-Lemma L_isIn_b_true (a b : A) (p : a = b) :
+  Lemma L_isIn_b_true (a b : A) (p : a = b) :
-  isIn_b a {|b|} = true.
+    isIn_b a {|b|} = true.
-Proof.
+  Proof.
-  unfold isIn_b, dec.
+    unfold isIn_b, dec.
-  destruct (isIn_decidable a {|b|}) as [n | n] .
+    destruct (isIn_decidable a {|b|}) as [n | n] .
-  - reflexivity.
+    - reflexivity.
-  - simpl in n.
+    - simpl in n.
-    contradiction (n (tr p)).
+      contradiction (n (tr p)).
-Defined.
+  Defined.
 
-Lemma L_isIn_b_aa (a : A) :
+  Lemma L_isIn_b_aa (a : A) :
-  isIn_b a {|a|} = true.
+    isIn_b a {|a|} = true.
-Proof.
+  Proof.
-  apply L_isIn_b_true ; reflexivity.
+    apply L_isIn_b_true ; reflexivity.
-Defined.
+  Defined.
 
-Lemma L_isIn_b_false (a b : A) (p : a <> b) :
+  Lemma L_isIn_b_false (a b : A) (p : a <> b) :
-  isIn_b a {|b|} = false.
+    isIn_b a {|b|} = false.
-Proof.
+  Proof.
-  unfold isIn_b, dec.
+    unfold isIn_b, dec.
-  destruct (isIn_decidable a {|b|}).
+    destruct (isIn_decidable a {|b|}).
-  - simpl in t.
+    - simpl in t.
-    strip_truncations.
+      strip_truncations.
-    contradiction.
+      contradiction.
-  - reflexivity.
+    - reflexivity.
-Defined.
+  Defined.
   
-(* Union and membership *)
+  (* Union and membership *)
-Lemma union_isIn (X Y : FSet A) (a : A) :
+  Lemma union_isIn (X Y : FSet A) (a : A) :
-  isIn_b a (U X Y) = orb (isIn_b a X) (isIn_b a Y).
+    isIn_b a (U X Y) = orb (isIn_b a X) (isIn_b a Y).
-Proof.
+  Proof.
-  unfold isIn_b ; unfold dec.
+    unfold isIn_b ; unfold dec.
-  simpl.
+    simpl.
-  destruct (isIn_decidable a X) ; destruct (isIn_decidable a Y) ; reflexivity.
+    destruct (isIn_decidable a X) ; destruct (isIn_decidable a Y) ; reflexivity.
-Defined.
+  Defined.
 
-Lemma intersection_isIn (X Y: FSet A) (a : A) :
+  Lemma intersection_isIn (X Y: FSet A) (a : A) :
     isIn_b a (intersection X Y) = andb (isIn_b a X) (isIn_b a Y).
-Proof.
+  Proof.
-  hinduction X; try (intros ; apply set_path2).
+    hinduction X; try (intros ; apply set_path2).
-  - reflexivity.
+    - reflexivity.
-  - intro b.
+    - intro b.
-    destruct (dec (a = b)).
+      destruct (dec (a = b)).
-    * rewrite p.
+      * rewrite p.
-      destruct (isIn_b b Y) ; symmetry ; eauto with bool_lattice_hints.
+        destruct (isIn_b b Y) ; symmetry ; eauto with bool_lattice_hints.
-    * destruct (isIn_b b Y) ; destruct (isIn_b a Y) ; symmetry ; eauto with bool_lattice_hints.
+      * destruct (isIn_b b Y) ; destruct (isIn_b a Y) ; symmetry ; eauto with bool_lattice_hints.
       + rewrite and_false.
         symmetry.
         apply (L_isIn_b_false a b n).
       + rewrite and_true.
         apply (L_isIn_b_false a b n).
-  - intros X1 X2 P Q.
+    - intros X1 X2 P Q.
-    rewrite union_isIn ; rewrite union_isIn.
+      rewrite union_isIn ; rewrite union_isIn.
-    rewrite P.
+      rewrite P.
-    rewrite Q.
+      rewrite Q.
-    unfold isIn_b, dec.
+      unfold isIn_b, dec.
-    destruct (isIn_decidable a X1)
+      destruct (isIn_decidable a X1)
-    ; destruct (isIn_decidable a X2)
+      ; destruct (isIn_decidable a X2)
-    ; destruct (isIn_decidable a Y)
+      ; destruct (isIn_decidable a Y)
-    ; reflexivity.
+      ; reflexivity.
-Defined.
+  Defined.
 
-Lemma comprehension_isIn (Y : FSet A) (ϕ : A -> Bool) (a : A) :
+  Lemma comprehension_isIn (Y : FSet A) (ϕ : A -> Bool) (a : A) :
-  isIn_b a (comprehension ϕ Y) = andb (isIn_b a Y) (ϕ a).
+    isIn_b a (comprehension ϕ Y) = andb (isIn_b a Y) (ϕ a).
-Proof.
+  Proof.
-  hinduction Y ; try (intros; apply set_path2). 
+    hinduction Y ; try (intros; apply set_path2). 
-  - apply empty_isIn.
+    - apply empty_isIn.
-  - intro b.
+    - intro b.
-    destruct (isIn_decidable a {|b|}).
+      destruct (isIn_decidable a {|b|}).
-    * simpl in t.
+      * simpl in t.
-      strip_truncations.
+        strip_truncations.
-      rewrite t.
+        rewrite t.
-      destruct (ϕ b).
+        destruct (ϕ b).
-      ** rewrite (L_isIn_b_true _ _ idpath).
+        ** rewrite (L_isIn_b_true _ _ idpath).
-         eauto with bool_lattice_hints.
+           eauto with bool_lattice_hints.
-      ** rewrite empty_isIn ; rewrite (L_isIn_b_true _ _ idpath).
+        ** rewrite empty_isIn ; rewrite (L_isIn_b_true _ _ idpath).
-         eauto with bool_lattice_hints.
+           eauto with bool_lattice_hints.
-    * destruct (ϕ b).
+      * destruct (ϕ b).
-      ** rewrite L_isIn_b_false.
+        ** rewrite L_isIn_b_false.
-         *** eauto with bool_lattice_hints.
+           *** eauto with bool_lattice_hints.
-         *** intro. 
+           *** intro. 
-             apply (n (tr X)).
+               apply (n (tr X)).
-      ** rewrite empty_isIn.
+        ** rewrite empty_isIn.
-         rewrite L_isIn_b_false.
+           rewrite L_isIn_b_false.
-         *** eauto with bool_lattice_hints.
+           *** eauto with bool_lattice_hints.
-         *** intro.
+           *** intro.
-             apply (n (tr X)).
+               apply (n (tr X)).
-  - intros.
+    - intros.
-    Opaque isIn_b.
+      Opaque isIn_b.
-    rewrite ?union_isIn.
+      rewrite ?union_isIn.
-    rewrite X.
+      rewrite X.
-    rewrite X0.
+      rewrite X0.
-    assert (forall b1 b2 b3,
+      assert (forall b1 b2 b3,
-               (b1 && b2 || b3 && b2)%Bool = ((b1 || b3) && b2)%Bool).
+                 (b1 && b2 || b3 && b2)%Bool = ((b1 || b3) && b2)%Bool).
-    { intros ; destruct b1, b2, b3 ; reflexivity. }
+      { intros ; destruct b1, b2, b3 ; reflexivity. }
-    apply X1.
+      apply X1.
-Defined.
+  Defined.
 End operations_isIn.
 
-Global Opaque isIn_b.
 (* Some suporting tactics *)
+(*
+Ltac simplify_isIn :=
+  repeat (rewrite union_isIn
+          || rewrite L_isIn_b_aa      
+          || rewrite intersection_isIn
+          || rewrite comprehension_isIn).
+ *)
+
 Ltac simplify_isIn :=
   repeat (rewrite union_isIn
        || rewrite L_isIn_b_aa      
@@ -142,7 +149,7 @@ Ltac simplify_isIn :=
        || rewrite comprehension_isIn).
 
 Ltac toBool := try (intro) ;
-    intros ; apply ext ; intros ; simplify_isIn ; eauto with bool_lattice_hints.
+               intros ; apply ext ; intros ; simplify_isIn ; eauto with bool_lattice_hints typeclass_instances.
 
 Section SetLattice.
 
@@ -150,70 +157,15 @@ Section SetLattice.
   Context {A_deceq : DecidablePaths A}.
   Context `{Univalence}.
 
-  Instance fset_union_com : Commutative (@U A).
+  Instance fset_max : maximum (FSet A) := U.
-  Proof.
+  Instance fset_min : minimum (FSet A) := intersection.
-    toBool.
+  Instance fset_bot : bottom (FSet A) := E.
-  Defined.
 
-  Instance fset_intersection_com : Commutative intersection.
+  Instance lattice_fset : Lattice (FSet A).
   Proof.
-    toBool.
+    split ; toBool.      
   Defined.
   
-  Instance fset_union_assoc : Associative (@U A).
-  Proof.
-    toBool.
-  Defined.
-
-  Instance fset_intersection_assoc : Associative intersection.
-  Proof.
-    toBool.
-  Defined.
-
-  Instance fset_union_idem : Idempotent (@U A).
-  Proof.
-    exact union_idem.
-  Defined.
-
-  Instance fset_intersection_idem : Idempotent intersection.
-  Proof.
-    toBool.
-  Defined.
-
-  Instance fset_union_nl : NeutralL (@U A) (@E A).
-  Proof.
-    toBool.
-  Defined.
-
-  Instance fset_union_nr : NeutralR (@U A) (@E A).
-  Proof.
-    toBool.
-  Defined.
-
-  Instance fset_absorption_intersection_union : Absorption (@U A) intersection.
-  Proof.
-    toBool.
-  Defined.
-
-  Instance fset_absorption_union_intersection : Absorption intersection (@U A).
-  Proof.
-    toBool.
-  Defined.
-  
-  Instance lattice_fset : Lattice intersection (@U A)  (@E A) :=
-    {
-      commutative_min := _ ;
-      commutative_max := _ ;
-      associative_min := _ ;
-      associative_max := _ ;
-      idempotent_min := _ ;
-      idempotent_max := _ ;
-      neutralL_min := _ ;
-      neutralR_min := _ ;
-      absorption_min_max := _ ;
-      absorption_max_min := _
-    }.
-
 End SetLattice.
 
 (* Comprehension properties *)
@@ -236,16 +188,16 @@ Section comprehension_properties.
   Lemma comprehension_false Y : comprehension (fun (_ : A) => false) Y = E.
   Proof.
     toBool.
-  Defined.
+  Qed.
 
   Lemma comprehension_all : forall (X : FSet A),
       comprehension (fun a => isIn_b a X) X = X.
   Proof.
     toBool.
-  Defined.
+  Qed.
   
   Lemma comprehension_subset : forall ϕ (X : FSet A),
-    U (comprehension ϕ X) X = X.
+      U (comprehension ϕ X) X = X.
   Proof.
     toBool.
   Defined.

FiniteSets/lattice.v

@@ -1,7 +1,24 @@
 (* Typeclass for lattices *)
 Require Import HoTT.
 
-Definition operation (A : Type) := A -> A -> A.
+Section binary_operation.
+  Variable A : Type.
+  
+  Definition operation := A -> A -> A.
+
+  Class maximum :=
+    max_L : operation.
+
+  Class minimum :=
+    min_L : operation.
+
+  Class bottom :=
+    empty : A.
+End binary_operation.
+
+Arguments max_L {_} _ _.
+Arguments min_L {_} _ _.
+Arguments empty {_}.
 
 Section Defs.
   Variable A : Type.
@@ -19,7 +36,7 @@ Section Defs.
   Variable g : operation A.
 
   Class Absorption :=
-    absrob : forall x y, f x (g x y) = x.
+    absorb : forall x y, f x (g x y) = x.
 
   Variable n : A.
 
@@ -40,27 +57,32 @@ Arguments Absorption {_} _ _.
 
 Section Lattice.
   Variable A : Type.
-  Variable min max : operation A.
+  Context {max_L : maximum A} {min_L : minimum A} {empty_L : bottom A}.
-  Variable empty : A.
 
   Class Lattice :=
     {
-      commutative_min :> Commutative min ;
+      commutative_min :> Commutative min_L ;
-      commutative_max :> Commutative max ;
+      commutative_max :> Commutative max_L ;
-      associative_min :> Associative min ;
+      associative_min :> Associative min_L ;
-      associative_max :> Associative max ;
+      associative_max :> Associative max_L ;
-      idempotent_min :> Idempotent min ;
+      idempotent_min :> Idempotent min_L ;
-      idempotent_max :> Idempotent max ;
+      idempotent_max :> Idempotent max_L ;
-      neutralL_max :> NeutralL max empty ;
+      neutralL_max :> NeutralL max_L empty_L ;
-      neutralR_max :> NeutralR max empty ;
+      neutralR_max :> NeutralR max_L empty_L ;
-      absorption_min_max :> Absorption min max ;
+      absorption_min_max :> Absorption min_L max_L ;
-      absorption_max_min :> Absorption max min
+      absorption_max_min :> Absorption max_L min_L
     }.
-                     
 End Lattice.
 
-Arguments Lattice {_} _ _ _.
+Arguments Lattice _ {_} {_} {_}.
 
+Create HintDb lattice_hints.
+Hint Resolve associativity : lattice_hints.
+Hint Resolve commutative : lattice_hints.
+Hint Resolve absorb : lattice_hints.
+Hint Resolve idempotency : lattice_hints.
+Hint Resolve neutralityL : lattice_hints.
+Hint Resolve neutralityR : lattice_hints.
 
 Section BoolLattice.
 
@@ -71,69 +93,15 @@ Section BoolLattice.
     ; auto
     ; try contradiction.
 
-  Instance orb_com : Commutative orb.
+  Instance maximum_bool : maximum Bool := orb.
-  Proof.
+  Instance minimum_bool : minimum Bool := andb.
-    solve_bool.
+  Instance bottom_bool : bottom Bool := false.
-  Defined.
   
-  Instance andb_com : Commutative andb.
+  Global Instance lattice_bool : Lattice Bool.
   Proof.
-    solve_bool.
+    split ; solve_bool.
   Defined.
   
-  Instance orb_assoc : Associative orb.
-  Proof.
-    solve_bool.
-  Defined.
-
-  Instance andb_assoc : Associative andb.
-  Proof.
-    solve_bool.
-  Defined.
-
-  Instance orb_idem : Idempotent orb.
-  Proof.
-    solve_bool.
-  Defined.
-
-  Instance andb_idem : Idempotent andb.
-  Proof.
-    solve_bool.
-  Defined.
-
-  Instance orb_nl : NeutralL orb false.
-  Proof.
-    solve_bool.
-  Defined.
-
-  Instance orb_nr : NeutralR orb false.
-  Proof.
-    solve_bool.
-  Defined.
-
-  Instance bool_absorption_orb_andb : Absorption orb andb.
-  Proof.
-    solve_bool.
-  Defined.
-
-  Instance bool_absorption_andb_orb : Absorption andb orb.
-  Proof.
-    solve_bool.
-  Defined.
-  
-  Global Instance lattice_bool : Lattice andb orb false :=
-    { commutative_min := _ ;
-      commutative_max := _ ;
-      associative_min := _ ;
-      associative_max := _ ;
-      idempotent_min := _ ;
-      idempotent_max := _ ;
-      neutralL_max := _ ;
-      neutralR_max := _ ;
-      absorption_min_max := _ ;
-      absorption_max_min := _
-  }.
-
   Definition and_true : forall b, andb b true = b.
   Proof.
     solve_bool.
@@ -165,123 +133,52 @@ Section BoolLattice.
 End BoolLattice.
 
 Section fun_lattice.
-  Context {A B : Type} {maxB minB : B -> B -> B} {botB : B}.
+  Context {A B : Type}.
-  Context `{Lattice B minB maxB botB}.
+  Context `{Lattice B}.
   Context `{Funext}.
 
-  Definition max_fun (f g : (A -> B)) (a : A) : B
+  Global Instance max_fun : maximum (A -> B) :=
-    := maxB (f a) (g a).
+    fun (f g : A -> B) (a : A) => max_L0 (f a) (g a).
 
-  Definition min_fun (f g : (A -> B)) (a : A) : B
+  Global Instance min_fun : minimum (A -> B) :=
-    := minB (f a) (g a).
+    fun (f g : A -> B) (a : A) => min_L0 (f a) (g a).
 
-  Definition bot_fun (a : A) : B
+  Global Instance bot_fun : bottom (A -> B)
-    := botB.
+    := fun _ => empty_L.
 
-  Hint Unfold max_fun min_fun bot_fun.
+  Ltac solve_fun :=
+    compute ; intros ; apply path_forall ; intro ;
+    eauto with lattice_hints typeclass_instances.
 
-  Ltac solve_fun := compute ; intros ; apply path_forall ; intro.
+  Global Instance lattice_fun : Lattice (A -> B).
-  
-  Instance max_fun_com : Commutative max_fun.
   Proof.
-    solve_fun.
+    split ; solve_fun.
-    refine (commutative_max _ _ _ _ _ _).
   Defined.
   
-  Instance min_fun_com : Commutative min_fun.
-  Proof.
-    solve_fun.
-    refine (commutative_min _ _ _ _ _ _).
-  Defined.
-
-  Instance max_fun_assoc : Associative max_fun.
-  Proof.
-    solve_fun.
-    refine (associative_max _ _ _ _ _ _ _).
-  Defined.
-
-  Instance min_fun_assoc : Associative min_fun.
-  Proof.
-    solve_fun.
-    refine (associative_min _ _ _ _ _ _ _).
-  Defined.
-
-  Instance max_fun_idem : Idempotent max_fun.
-  Proof.
-    solve_fun.
-    refine (idempotent_max _ _ _ _ _).
-  Defined.
-
-  Instance min_fun_idem : Idempotent min_fun.
-  Proof.
-    solve_fun.
-    refine (idempotent_min _ _ _ _ _).
-  Defined.
-
-  Instance max_fun_nl : NeutralL max_fun bot_fun.
-  Proof.
-    solve_fun.
-    simple refine (neutralL_max _ _ _ _ _).
-  Defined.
-
-  Instance max_fun_nr : NeutralR max_fun bot_fun.
-  Proof.
-    solve_fun.
-    simple refine (neutralR_max _ _ _ _ _).
-  Defined.
-
-  Instance absorption_max_fun_min_fun : Absorption max_fun min_fun.
-  Proof.
-    solve_fun.
-    simple refine (absorption_max_min _ _ _ _ _ _).
-  Defined.
-
-  Instance absorption_min_fun_max_fun : Absorption min_fun max_fun.
-  Proof.
-    solve_fun.
-    simple refine (absorption_min_max _ _ _ _ _ _).
-  Defined.
-  
-  Global Instance lattice_fun : Lattice min_fun max_fun bot_fun :=
-    { commutative_min := _ ;
-      commutative_max := _ ;
-      associative_min := _ ;
-      associative_max := _ ;
-      idempotent_min := _ ;
-      idempotent_max := _ ;
-      neutralL_max := _ ;
-      neutralR_max := _ ;
-      absorption_min_max := _ ;
-      absorption_max_min := _
-  }.
 End fun_lattice.
 
 Section sub_lattice.
-  Context {A : Type} {P : A -> hProp} {maxA minA : A -> A -> A} {botA : A}.
+  Context {A : Type} {P : A -> hProp}.
-  Context {Hmax : forall x y, P x -> P y -> P (maxA x y)}.
+  Context `{Lattice A}.
-  Context {Hmin : forall x y, P x -> P y -> P (minA x y)}.
+  Context {Hmax : forall x y, P x -> P y -> P (max_L0 x y)}.
-  Context {Hbot : P botA}.
+  Context {Hmin : forall x y, P x -> P y -> P (min_L0 x y)}.
-  Context `{Lattice A minA maxA botA}.
+  Context {Hbot : P empty_L}.
 
   Definition AP : Type := sig P.
   
-  Definition botAP : AP := (botA ; Hbot).
+  Instance botAP : bottom AP := (empty_L ; Hbot).
 
-  Definition maxAP (x y : AP) : AP :=
+  Instance maxAP : maximum AP :=
-    match x with
+    fun x y =>
-    | (a ; pa) => match y with
+      match x, y with
-                  | (b ; pb) => (maxA a b ; Hmax a b pa pb)
+      | (a ; pa), (b ; pb) => (max_L0 a b ; Hmax a b pa pb)
-                  end
+      end.
-    end.
 
-  Definition minAP (x y : AP) : AP :=
+  Instance minAP : minimum AP :=
-    match x with
+    fun x y =>
-    | (a ; pa) => match y with
+      match x, y with
-                  | (b ; pb) => (minA a b ; Hmin a b pa pb)
+      | (a ; pa), (b ; pb) => (min_L0 a b ; Hmin a b pa pb)
-                  end
+      end.
-    end.
-
-  Hint Unfold maxAP minAP botAP.
 
   Instance hprop_sub : forall c, IsHProp (P c).
   Proof.
@@ -291,85 +188,28 @@ Section sub_lattice.
   Ltac solve_sub :=
     let x := fresh in
     repeat (intro x ; destruct x) 
-    ; simple refine (path_sigma _ _ _ _ _) ; try (apply hprop_sub).
+    ; simple refine (path_sigma _ _ _ _ _)
+    ; simpl
+    ; try (apply hprop_sub)
+    ; eauto 3 with lattice_hints typeclass_instances.
   
-  Instance max_sub_com : Commutative maxAP.
+  Global Instance lattice_sub : Lattice AP.
   Proof.
-    solve_sub.
+    split ; solve_sub.
-    refine (commutative_max _ _ _ _ _ _).
   Defined.
   
-  Instance min_sub_com : Commutative minAP.
-  Proof.
-    solve_sub.
-    refine (commutative_min _ _ _ _ _ _).
-  Defined.
-
-  Instance max_sub_assoc : Associative maxAP.
-  Proof.
-    solve_sub.
-    refine (associative_max _ _ _ _ _ _ _).
-  Defined.
-
-  Instance min_sub_assoc : Associative minAP.
-  Proof.
-    solve_sub.
-    refine (associative_min _ _ _ _ _ _ _).
-  Defined.
-
-  Instance max_sub_idem : Idempotent maxAP.
-  Proof.
-    solve_sub.
-    refine (idempotent_max _ _ _ _ _).
-  Defined.
-
-  Instance min_sub_idem : Idempotent minAP.
-  Proof.
-    solve_sub.
-    refine (idempotent_min _ _ _ _ _).
-  Defined.
-
-  Instance max_sub_nl : NeutralL maxAP botAP.
-  Proof.
-    solve_sub.
-    simple refine (neutralL_max _ _ _ _ _).
-  Defined.
-
-  Instance max_sub_nr : NeutralR maxAP botAP.
-  Proof.
-    solve_sub.
-    simple refine (neutralR_max _ _ _ _ _).
-  Defined.
-
-  Instance absorption_max_sub_min_sub : Absorption maxAP minAP.
-  Proof.
-    solve_sub.
-    simple refine (absorption_max_min _ _ _ _ _ _).
-  Defined.
-
-  Instance absorption_min_sub_max_sub : Absorption minAP maxAP.
-  Proof.
-    solve_sub.
-    simple refine (absorption_min_max _ _ _ _ _ _).
-  Defined.
-  
-  Global Instance lattice_sub : Lattice minAP maxAP botAP :=
-    { commutative_min := _ ;
-      commutative_max := _ ;
-      associative_min := _ ;
-      associative_max := _ ;
-      idempotent_min := _ ;
-      idempotent_max := _ ;
-      neutralL_max := _ ;
-      neutralR_max := _ ;
-      absorption_min_max := _ ;
-      absorption_max_min := _
-  }.
-
 End sub_lattice.
 
+Create HintDb bool_lattice_hints.
+Hint Resolve associativity : bool_lattice_hints.
+Hint Resolve commutative : bool_lattice_hints.
+Hint Resolve absorb : bool_lattice_hints.
+Hint Resolve idempotency : bool_lattice_hints.
+Hint Resolve neutralityL : bool_lattice_hints.
+Hint Resolve neutralityR : bool_lattice_hints.
+
 Hint Resolve
-     orb_com andb_com orb_assoc andb_assoc orb_idem andb_idem orb_nl orb_nr
+     associativity
-     bool_absorption_orb_andb bool_absorption_andb_orb and_true and_false
+     and_true and_false
      dist₁ dist₂ max_min
  : bool_lattice_hints.