Separated lemmas for extensionality for properties, added tactic toHProp

2017-08-08 13:35:28 +02:00 · 2017-08-08 13:35:28 +02:00 · c1dfef3cc1
parent 4ade6e60cc
commit c1dfef3cc1
7 changed files with 108 additions and 155 deletions
--- a/FiniteSets/_CoqProject
+++ b/FiniteSets/_CoqProject
@ -9,9 +9,9 @@ fsets/operations_cons_repr.v
 fsets/properties_cons_repr.v
 fsets/isomorphism.v
 fsets/operations.v
-fsets/properties.v
 fsets/operations_decidable.v
 fsets/extensionality.v
+fsets/properties.v
 fsets/properties_decidable.v
 fsets/length.v
 fsets/monad.v
--- a/FiniteSets/fsets/extensionality.v
+++ b/FiniteSets/fsets/extensionality.v
@ -1,12 +1,55 @@
 (** Extensionality of the FSets *)
 Require Import HoTT HitTactics.
-From representations Require Import definition.
-From fsets Require Import operations properties.
+Require Import representations.definition fsets.operations.

 Section ext.
  Context {A : Type}.
  Context `{Univalence}.

+  Lemma subset_union (X Y : FSet A) : 
+    X ⊆ Y -> 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 subset_union_l (X : FSet A) :
+    forall Y, X ⊆ X ∪ Y.
+  Proof.
+    hinduction X ; try (repeat (intro; intros; apply path_forall);
+                        intro ; apply equiv_hprop_allpath ; apply _).
+    - apply (fun _ => tt).
+    - intros a Y.
+      apply (tr(inl(tr idpath))).
+    - intros X1 X2 HX1 HX2 Y.
+      split. 
+      * rewrite <- assoc. apply HX1.
+      * rewrite (comm X1 X2). rewrite <- assoc. apply HX2.
+  Defined.
+
  Lemma subset_union_equiv
    : forall X Y : FSet A, X ⊆ Y <~> X ∪ Y = Y.
  Proof.
--- a/FiniteSets/fsets/length.v
+++ b/FiniteSets/fsets/length.v
@ -19,14 +19,16 @@ Section Length.
      pose (y' := FSetC_to_FSet y).
      exact (if isIn_b a y' then n else (S n)).
    - intros. rewrite transport_const. cbn.
-      simplify_isIn. simpl. reflexivity.
+      simplify_isIn_b. simpl. reflexivity.
    - intros. rewrite transport_const. cbn.
-      simplify_isIn.
+      simplify_isIn_b.
      destruct (dec (a = b)) as [Hab | Hab].
-      + rewrite Hab. simplify_isIn. simpl. reflexivity.
-      + rewrite ?L_isIn_b_false; auto. simpl. 
-        destruct (isIn_b a (FSetC_to_FSet x0)), (isIn_b b (FSetC_to_FSet x0)) ; reflexivity.
-        intro p. contradiction (Hab p^).
+      + rewrite Hab. simplify_isIn_b. simpl. reflexivity.
+      + rewrite ?L_isIn_b_false; auto.
+        ++ simpl. 
+           destruct (isIn_b a (FSetC_to_FSet x0)), (isIn_b b (FSetC_to_FSet x0))
+           ; reflexivity.
+        ++ intro p. contradiction (Hab p^).
  Defined.

  Definition length_FSet (x: FSet A) := length (FSet_to_FSetC x).
--- a/FiniteSets/fsets/operations.v
+++ b/FiniteSets/fsets/operations.v
@ -76,24 +76,7 @@ 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 single_product (a : A) : FSet B -> FSet (A * B).
+  Definition single_product {B : Type} (a : A) : FSet B -> FSet (A * B).
  Proof.
    hrecursion.
    - apply ∅.
@ -107,7 +90,7 @@ Section operations.
    - intros ; apply idem.
  Defined.
        
-  Definition product : FSet A -> FSet B -> FSet (A * B).
+  Definition product {B : Type} : FSet A -> FSet B -> FSet (A * B).
  Proof.
    intros X Y.
    hrecursion X.
@ -119,7 +102,7 @@ Section operations.
    - intros ; apply comm.
    - intros ; apply nl.
    - intros ; apply nr.
-    - intros ; apply union_idemL.
+    - intros ; apply union_idem.
  Defined.
  
 End operations.
--- a/FiniteSets/fsets/properties.v
+++ b/FiniteSets/fsets/properties.v
@ -1,102 +1,9 @@
 Require Import HoTT HitTactics.
-Require Export representations.definition disjunction fsets.operations.
+From fsets Require Import operations extensionality.
+Require Export representations.definition disjunction.

 (* Lemmas relating operations to the membership predicate *)
-Section operations_isIn.
-
-  Context {A : Type}.
-  Context `{Univalence}.
-
-  Lemma union_idem : forall x: FSet A, 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.
-
-  (** ** Properties about subset relation. *)
-  Lemma subset_union (X Y : FSet A) : 
-    X ⊆ Y -> 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 subset_union_l (X : FSet A) :
-    forall Y, X ⊆ X ∪ Y.
-  Proof.
-    hinduction X ; try (repeat (intro; intros; apply path_forall);
-                        intro ; apply equiv_hprop_allpath ; apply _).
-    - apply (fun _ => tt).
-    - intros a Y.
-      apply (tr(inl(tr idpath))).
-    - intros X1 X2 HX1 HX2 Y.
-      split. 
-      * rewrite <- assoc. apply HX1.
-      * rewrite (comm X1 X2). rewrite <- assoc. apply HX2.
-  Defined.
-
-  (* simplify it using extensionality *)
-  Lemma comprehension_or : forall ϕ ψ (x: FSet A),
-      comprehension (fun a => orb (ϕ a) (ψ a)) x
-      = (comprehension ϕ x) ∪ (comprehension ψ x).
-  Proof.
-    intros ϕ ψ.
-    hinduction ; try (intros; apply set_path2). 
-    - apply (union_idem _)^.
-    - 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.
-
+Section characterize_isIn.
  Context {A : Type}.
  Context `{Univalence}.

@ -196,39 +103,42 @@ Section properties.
        ** left ; split ; assumption.
        ** right ; split ; assumption.
  Defined.
+End characterize_isIn.
+
+Ltac simplify_isIn :=
+  repeat (rewrite union_isIn
+          || rewrite comprehension_isIn).
+
+Ltac toHProp :=
+  repeat intro;
+  apply fset_ext ; intros ;
+  simplify_isIn ; eauto with lattice_hints typeclass_instances.
+
+(* Other properties *)
+Section properties.
+  Context {A : Type}.
+  Context `{Univalence}.

-  (* The proof can be simplified using extensionality *)
  (** comprehension properties *)
  Lemma comprehension_false Y : comprehension (fun (_ : A) => false) Y = ∅.
  Proof.
-    hrecursion Y; try (intros; apply set_path2).
-    - reflexivity.
-    - reflexivity.
-    - intros x y IHa IHb.
-      rewrite IHa, IHb.
-      apply union_idem.
+    toHProp.
  Defined.

-  (* Can be simplified using extensionality *)
  Lemma comprehension_subset : forall ϕ (X : FSet A),
      (comprehension ϕ X) ∪ X = X.
  Proof.
-    intros ϕ.
-    hrecursion; try (intros ; apply set_path2) ; cbn.
-    - apply union_idem.
-    - intro a.
-      destruct (ϕ a).
-      * apply union_idem.
-      * apply nl.
-    - intros X Y P Q.
-      rewrite assoc.
-      rewrite <- (assoc (comprehension ϕ X) (comprehension ϕ Y) X).
-      rewrite (comm (comprehension ϕ Y) X).
-      rewrite assoc.
-      rewrite P.
-      rewrite <- assoc.
-      rewrite Q.
-      reflexivity.
+    toHProp.
+    destruct (ϕ a) ; eauto with lattice_hints typeclass_instances.
+  Defined.
+
+  Lemma comprehension_or : forall ϕ ψ (x: FSet A),
+      comprehension (fun a => orb (ϕ a) (ψ a)) x
+      = (comprehension ϕ x) ∪ (comprehension ψ x).
+  Proof.
+    toHProp.
+    symmetry ; destruct (ϕ a) ; destruct (ψ a)
+    ; eauto with lattice_hints typeclass_instances.
  Defined.
  
  Lemma merely_choice : forall X : FSet A, hor (X = ∅) (hexists (fun a => a ∈ X)).
@ -257,6 +167,7 @@ Section properties.
        apply (tr (inl Xa)).
  Defined.

+(*
  Lemma separation : forall (X : FSet A) (f : {a | a ∈ X} -> B),
      hexists (fun Y : FSet B => forall (b : B),
                   b ∈ Y = hexists (fun a => hexists (fun (p : a ∈ X) => f (a;p) = b))).
@ -358,5 +269,6 @@ Section properties.
           repeat f_ap.
           apply path_ishprop.
  Defined.
+*)
  
 End properties.
--- a/FiniteSets/fsets/properties_decidable.v
+++ b/FiniteSets/fsets/properties_decidable.v
@ -87,10 +87,8 @@ Section operations_isIn.

 End operations_isIn.

-Global Opaque isIn_b.
-
 (* Some suporting tactics *)
-Ltac simplify_isIn :=
+Ltac simplify_isIn_b :=
  repeat (rewrite union_isIn_b
        || rewrite L_isIn_b_aa
        || rewrite intersection_isIn_b
@ -99,7 +97,7 @@ Ltac simplify_isIn :=
 Ltac toBool :=
  repeat intro;
  apply ext ; intros ;
-  simplify_isIn ; eauto with bool_lattice_hints typeclass_instances.
+  simplify_isIn_b ; eauto with bool_lattice_hints typeclass_instances.

 Section SetLattice.

--- a/FiniteSets/representations/definition.v
+++ b/FiniteSets/representations/definition.v
@ -197,3 +197,18 @@ End FSet.
 Notation "{| x |}" :=  (L x).
 Infix "∪" := U (at level 8, right associativity).
 Notation "∅" := E.
+
+Lemma union_idem {A : Type} : forall x: FSet A, 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.