Proofs of the lattice properties (via extensionality)

FiniteSets/Lattice.v

@@ -0,0 +1,225 @@
+Require Import HoTT.
+
+Definition operation (A : Type) := A -> A -> A.
+
+Section Defs.
+  Variable A : Type.
+  Variable f : A -> A -> A.
+
+  Class Commutative :=
+    commutative : forall x y, f x y = f y x.
+
+  Class Associative :=
+    associativity : forall x y z, f (f x y) z = f x (f y z).
+
+  Class Idempotent :=
+    idempotency : forall x, f x x = x.
+
+  Variable g : operation A.
+
+  Class Absorption :=
+    absrob : forall x y, f x (g x y) = x.
+
+  Variable n : A.
+
+  Class NeutralL :=
+    neutralityL : forall x, f x n = x.
+
+  Class NeutralR :=
+    neutralityR : forall x, f n x = x.
+
+End Defs.
+
+Arguments Commutative {_} _.
+Arguments Associative {_} _.
+Arguments Idempotent {_} _.
+Arguments NeutralL {_} _ _.
+Arguments NeutralR {_} _ _.
+Arguments Absorption {_} _ _.
+
+Section Lattice.
+  Variable A : Type.
+  Variable min max : operation A.
+  Variable empty : A.
+
+  Class Lattice :=
+    {
+      commutative_min :> Commutative min ;
+      commutative_max :> Commutative max ;
+      associative_min :> Associative min ;
+      associative_max :> Associative max ;
+      idempotent_min :> Idempotent min ;
+      idempotent_max :> Idempotent max ;
+      neutralL_min :> NeutralL min empty ;
+      neutralR_min :> NeutralR min empty ;
+      absorption_min_max :> Absorption min max ;
+      absorption_max_min :> Absorption max min
+    }.
+                     
+End Lattice.
+
+Arguments Lattice {_} _ _ _.
+
+Ltac solve := 
+  repeat (intro x ; destruct x) 
+  ; compute
+  ; auto
+  ; try contradiction.
+
+Section BoolLattice.
+
+  Instance min_com : Commutative orb.
+  Proof.
+    solve.
+  Defined.
+
+  Instance max_com : Commutative andb.
+  Proof.
+    solve.
+  Defined.
+
+  Instance min_assoc : Associative orb.
+  Proof.
+    solve.
+  Defined.
+
+  Instance max_assoc : Associative andb.
+  Proof.
+    solve.
+  Defined.
+
+  Instance min_idem : Idempotent orb.
+  Proof.
+    solve.
+  Defined.
+
+  Instance max_idem : Idempotent andb.
+  Proof.
+    solve.
+  Defined.
+
+  Instance min_nl : NeutralL orb false.
+  Proof.
+    solve.
+  Defined.
+
+  Instance min_nr : NeutralR orb false.
+  Proof.
+    solve.
+  Defined.
+
+  Instance bool_absorption_min_max : Absorption orb andb.
+  Proof.
+    solve.
+  Defined.
+
+  Instance bool_absorption_max_min : Absorption andb orb.
+  Proof.
+    solve.
+  Defined.
+  
+  Global Instance lattice_bool : Lattice orb andb false :=
+  { commutative_min := _ ;
+      commutative_max := _ ;
+      associative_min := _ ;
+      associative_max := _ ;
+      idempotent_min := _ ;
+      idempotent_max := _ ;
+      neutralL_min := _ ;
+      neutralR_min := _ ;
+      absorption_min_max := _ ;
+      absorption_max_min := _
+  }.
+
+End BoolLattice.
+
+Require Import definition.
+Require Import properties.
+
+Section SetLattice.
+
+  Context {A : Type}.
+  Context {A_deceq : DecidablePaths A}.
+  Context `{Funext}.
+
+  Lemma ext `{Funext} : forall S T, (forall a, isIn a S = isIn a T) -> S = T.
+  Proof.
+    intros.
+    destruct (fset_ext S T).
+    destruct equiv_isequiv.
+    apply equiv_inv.
+    apply X.
+  Defined.
+
+  Ltac simplify_isIn :=
+  repeat (rewrite ?intersection_isIn ;
+          rewrite ?union_isIn).
+  
+  Ltac toBool :=
+    intros ; apply ext ; intros ; simplify_isIn.
+
+  Instance union_com : Commutative (@U A).
+  Proof.
+    unfold Commutative ; toBool ; apply min_com.
+  Defined.
+
+  Instance intersection_com : Commutative intersection.
+  Proof.
+    unfold Commutative ; toBool ; apply max_com.
+  Defined.
+
+  Instance union_assoc : Associative (@U A).
+  Proof.
+    unfold Associative ; toBool ; apply min_assoc.
+  Defined.
+
+  Instance intersection_assoc : Associative intersection.
+  Proof.
+    unfold Associative ; toBool ; apply max_assoc.
+  Defined.
+
+  Instance union_idem : Idempotent (@U A).
+  Proof.
+    unfold Idempotent ; toBool ; apply min_idem.
+  Defined.
+
+  Instance intersection_idem : Idempotent intersection.
+  Proof.
+    unfold Idempotent ; toBool ; apply max_idem.
+  Defined.
+
+  Instance union_nl : NeutralL (@U A) (@E A).
+  Proof.
+    unfold NeutralL ; toBool ; apply min_nl.
+  Defined.
+
+  Instance union_nr : NeutralR (@U A) (@E A).
+  Proof.
+    unfold NeutralR ; toBool ; apply min_nr.
+  Defined.
+
+  Instance set_absorption_intersection_union : Absorption (@U A) intersection.
+  Proof.
+    unfold Absorption ; toBool ; apply bool_absorption_min_max.
+  Defined.
+
+  Instance set_absorption_union_intersection : Absorption intersection (@U A).
+  Proof.
+    unfold Absorption ; toBool ; apply bool_absorption_max_min.
+  Defined.
+  
+  Instance lattice_set : Lattice (@U A) intersection (@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.

FiniteSets/_CoqProject

@@ -6,3 +6,4 @@ properties.v
 empty_set.v
 ordered.v
 cons_repr.v
+Lattice.v

FiniteSets/properties.v

@@ -49,9 +49,11 @@ hrecursion Y; try (intros; apply set_path2).
 - cbn. reflexivity.
 - cbn. reflexivity.
 - intros x y IHa IHb.
+  cbn.
   rewrite IHa.
   rewrite IHb.
-  apply union_idem.
+  rewrite nl.
+  reflexivity.
 Defined.
 
 Theorem comprehension_or : forall ϕ ψ (x: FSet A),
@@ -60,7 +62,7 @@ Theorem comprehension_or : forall ϕ ψ (x: FSet A),
 Proof.
 intros ϕ ψ.
 hinduction; try (intros; apply set_path2). 
-- cbn. apply (union_idem _)^.
+- cbn. symmetry ; apply nl.
 - cbn. intros.
   destruct (ϕ a) ; destruct (ψ a) ; symmetry.
   * apply idem.
@@ -84,7 +86,7 @@ Theorem comprehension_subset : forall ϕ (X : FSet A),
 Proof.
 intros ϕ.
 hrecursion; try (intros ; apply set_path2) ; cbn.
-- apply union_idem.
+- apply nl.
 - intro a.
   destruct (ϕ a).
   * apply union_idem.
@@ -102,13 +104,15 @@ Defined.
 
 (** intersection properties *)
 Lemma intersection_0l: forall X: FSet A, intersection E X = E.
-Proof.       
+Proof.
 hinduction; 
 try (intros ; apply set_path2).
 - reflexivity.
 - intro a.
   reflexivity.
-- intros x y P Q.
+- unfold intersection.
+  intros x y P Q.
+  cbn.
   rewrite P.
   rewrite Q.
   apply nl.
@@ -146,26 +150,27 @@ Defined.
 Lemma intersection_comm X Y: intersection X Y = intersection Y X.
 Proof.
 hrecursion X;  try (intros; apply set_path2).
-- apply intersection_0l.
+- cbn. unfold intersection. apply comprehension_false.
-- intro a.
+- cbn. unfold intersection. intros a.
   hrecursion Y; try (intros; apply set_path2).
-  + reflexivity.
+  + cbn. reflexivity.
-  + intros b.
+  + cbn. intros b.
     destruct  (dec (a = b)) as [pa|npa].
     * rewrite pa.
       destruct (dec (b = b)) as [|nb]; [reflexivity|].
       by contradiction nb.
     * destruct (dec (b = a)) as [pb|]; [|reflexivity].
       by contradiction npa.
-  + intros Y1 Y2 IH1 IH2.
+  + cbn -[isIn]. intros Y1 Y2 IH1 IH2.
     rewrite IH1. 
     rewrite IH2.
     symmetry.
     apply (comprehension_or (fun a => isIn a Y1) (fun a => isIn a Y2) (L a)).
 - intros X1 X2 IH1 IH2.
+  cbn.
+  unfold intersection in *.
   rewrite <- IH1.
-  rewrite <- IH2.
+  rewrite <- IH2. 
-  unfold intersection. simpl.
   apply comprehension_or.
 Defined.
 
@@ -437,7 +442,6 @@ Proof.
 reflexivity.  
 Defined.
 
-(* Proof of the extensionality axiom  *)
 (* Properties about subset relation. *)
 Lemma subset_union `{Funext} (X Y : FSet A) : 
   subset X Y = true -> U X Y = Y.
@@ -473,9 +477,20 @@ hinduction X; try (intros; apply path_forall; intro; apply set_path2).
   * 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.
-Proof.
 hinduction X;
   try (intros; apply path_forall; intro; apply set_path2).
 - reflexivity.
@@ -483,45 +498,37 @@ hinduction X;
   * reflexivity.
   * by contradiction n.
 - intros X1 X2 HX1 HX2 Y.
-  refine (ap (fun z => (X1 ⊆ z && X2 ⊆ (X1 ∪ X2) ∪ Y))%Bool (assoc X1 X2 Y)^ @ _).
+  enough (subset X1 (U (U X1 X2) Y) = true).
-  refine (ap (fun z => (X1 ⊆ _ && X2 ⊆ z ∪ Y))%Bool (comm _ _) @ _).
+  enough (subset X2 (U (U X1 X2) Y) = true).
-  refine (ap (fun z => (X1 ⊆ _ && X2 ⊆ z))%Bool (assoc _ _ _)^ @ _).
+  rewrite X. rewrite X0. reflexivity.
-  rewrite HX1. simpl. apply HX2.  
+  { 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.
-  eapply equiv_iff_hprop_uncurried.
+  unshelve eapply BuildEquiv.
-  split.
+  apply subset_union.
-  - apply subset_union.
+  unshelve esplit.
-  - intros HXY. etransitivity.
+  { intros HXY. rewrite <- HXY. clear HXY.
-    apply (ap _ HXY^).
+    apply subset_union_l. }
-    apply subset_union_l.
+  all: intro; apply set_path2.
-Defined.
-
-Lemma eq_subset' (X Y : FSet A) : X = Y <~> (U Y X = X) * (U X Y = Y).
-Proof.
-  eapply equiv_iff_hprop_uncurried.
-  split.
-  - intro H. split.
-    apply (comm Y X @ ap (U X) H^ @ union_idem X).
-    apply (ap (U X) H^ @ union_idem X @ H).
-  - intros [H1 H2]. etransitivity. apply H1^.
-    apply (comm Y X @ H2).
 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 eq_subset'.
+  apply eq1.
   symmetry.
   eapply equiv_functor_prod'; apply subset_union_equiv.
 Defined.
 
-Lemma subset_isIn `{FE :Funext} (X Y : FSet A) :
+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.
@@ -555,26 +562,44 @@ Proof.
       destruct (dec (a = b)).
       + intros ; rewrite p ; apply H.
       + intros X ; contradiction (false_ne_true X).
-    * intros X1 X2.
+        * intros X1 X2.
-      intros IH1 IH2 H1 a H2.
+          intros IH1 IH2 H1 a H2.
-      destruct (subset X1 Y) ; destruct (subset X2 Y);
+          destruct (subset X1 Y) ; destruct (subset X2 Y);
-        cbv in H1; try by contradiction false_ne_true.
+            cbv in H1; try by contradiction false_ne_true.
-      specialize (IH1 idpath a). specialize (IH2 idpath a).
+          specialize (IH1 idpath a). specialize (IH2 idpath a).
-      destruct (isIn a X1); destruct (isIn a X2);
+          destruct (isIn a X1); destruct (isIn a X2);
-        cbv in H2; try by contradiction false_ne_true.
+            cbv in H2; try by contradiction false_ne_true.
-      by apply IH1.
+          by apply IH1.
-      by apply IH1.
+          by apply IH1.
-      by apply IH2.
+          by apply IH2.
-    * repeat (intro; intros; apply path_forall).
+        * repeat (intro; intros; apply path_forall).
-      intros; intro; intros; apply set_path2.
+          intros; intro; intros; apply set_path2.
-    * repeat (intro; intros; apply path_forall).
+        * repeat (intro; intros; apply path_forall).
-      intros; intro; intros; apply set_path2.
+          intros; intro; intros; apply set_path2.
-    * repeat (intro; intros; apply path_forall).
+        * repeat (intro; intros; apply path_forall).
-      intros; intro; intros; apply set_path2.
+          intros; intro; intros; apply set_path2.
-    * repeat (intro; intros; apply path_forall).
+        * repeat (intro; intros; apply path_forall).
-      intros; intro; intros; apply set_path2.
+          intros; intro; intros; apply set_path2.
-    * repeat (intro; intros; apply path_forall);
+        * repeat (intro; intros; apply path_forall);
-      intros; intro; intros; apply set_path2.
+          intros; intro; intros; apply set_path2.
+Defined.
+
+Lemma HPropEquiv (X Y : Type) (P : IsHProp X) (Q : IsHProp Y) :
+  (X <-> Y) -> (X <~> Y).
+Proof.
+intros [f g].
+simple refine (BuildEquiv _ _ _ _).  
+apply f.
+simple refine (BuildIsEquiv _ _ _ _ _ _ _).
+- apply g.
+- unfold Sect.
+  intro x.  
+  apply Q.
+- unfold Sect.
+  intro x.
+  apply P.
+- intros.
+  apply set_path2.
 Defined.
 
 Theorem fset_ext `{Funext} (X Y : FSet A) :
@@ -584,10 +609,18 @@ Proof.
   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';
+  - eapply equiv_functor_prod'.
-    apply equiv_iff_hprop_uncurried;
+    apply HPropEquiv.
+    exact _.
+    exact _.
     split ; apply subset_isIn.
-  - apply equiv_iff_hprop_uncurried.
+    apply HPropEquiv.
+    exact _.
+    exact _.
+    split ; apply subset_isIn.
+  - apply HPropEquiv.
+    exact _.
+    exact _.
     split.
     * intros [H1 H2 a].
       specialize (H1 a) ; specialize (H2 a).
@@ -604,4 +637,37 @@ Proof.
         apply H2.
 Defined.
 
-End properties.
+Ltac solve := 
+  repeat (intro x ; destruct x) 
+  ; compute
+  ; auto
+  ; try contradiction.
+
+Ltac simplify_isIn :=
+  repeat (rewrite ?intersection_isIn ;
+          rewrite ?union_isIn).
+
+Lemma ext `{Funext} : forall S T, (forall a, isIn a S = isIn a T) -> S = T.
+Proof.
+  intros.
+  destruct (fset_ext S T).
+  destruct equiv_isequiv.
+  apply equiv_inv.
+  apply X.
+Defined.
+
+Ltac toBool :=
+  intros ; apply ext ; intros ; simplify_isIn.
+
+Lemma andb_comm : forall x y, andb x y = andb y x.
+Proof.
+  solve.
+Defined.
+
+Lemma intersectioncomm `{Funext} : forall x y, intersection x y = intersection y x.
+Proof.
+  toBool.
+  destruct_all bool. apply andb_comm.
+Defined.  
+
+End properties.