From 140b02e9f427efe188730f93d81f367dd3c1f0b9 Mon Sep 17 00:00:00 2001 From: Leon Gondelman Date: Wed, 24 May 2017 18:28:24 +0200 Subject: [PATCH 1/4] subset --- FiniteSets/operations.v | 19 +++++++++++- FiniteSets/properties.v | 68 +++++++++++++++++++++++++++++++++++------ 2 files changed, 77 insertions(+), 10 deletions(-) diff --git a/FiniteSets/operations.v b/FiniteSets/operations.v index fb599f2..bd21a0d 100644 --- a/FiniteSets/operations.v +++ b/FiniteSets/operations.v @@ -1,6 +1,5 @@ Require Import HoTT HitTactics. Require Import definition. - Section operations. Context {A : Type}. @@ -48,4 +47,22 @@ intros X Y. apply (comprehension (fun (a : A) => isIn a X) Y). Defined. + +Definition subset : + FSet A -> FSet A -> Bool. +Proof. +intros X Y. +hrecursion X. +- exact true. +- exact (fun a => (a ∈ Y)). +- exact andb. +- intros. compute. destruct x; reflexivity. +- intros x y; compute; destruct x, y; reflexivity. +- intros x; compute; destruct x; reflexivity. +- intros x; compute; destruct x; reflexivity. +- intros x; cbn; destruct (x ∈ Y); reflexivity. +Defined. + +Notation "⊆" := subset. + End operations. diff --git a/FiniteSets/properties.v b/FiniteSets/properties.v index 8891de1..365ef68 100644 --- a/FiniteSets/properties.v +++ b/FiniteSets/properties.v @@ -196,7 +196,8 @@ hinduction; try (intros; apply set_path2). Defined. (** assorted lattice laws *) -Lemma distributive_La (z : FSet A) (a : A) : forall Y : FSet A, intersection (U (L a) z) Y = U (intersection (L a) Y) (intersection z Y). +Lemma distributive_La (z : FSet A) (a : A) : forall Y : FSet A, + intersection (U (L a) z) Y = U (intersection (L a) Y) (intersection z Y). Proof. hinduction; try (intros ; apply set_path2) ; cbn. - symmetry ; apply nl. @@ -265,7 +266,8 @@ hinduction x; try (intros ; apply set_path2) ; cbn. cbn. rewrite P. rewrite Q. - destruct (isIn a X1) ; destruct (isIn a X2) ; destruct (isIn a y) ; reflexivity. + destruct (isIn a X1) ; destruct (isIn a X2) ; destruct (isIn a y) ; + reflexivity. Defined. @@ -345,8 +347,10 @@ hinduction X1; try (intros ; apply set_path2) ; cbn. cbn. intros Z1 Z2 P Q. rewrite comprehension_or. - assert (U (U (comprehension (fun a : A => isIn a Z1) X2) (comprehension (fun a : A => isIn a Z2) X2)) - Y = U (U (comprehension (fun a : A => isIn a Z1) X2) (comprehension (fun a : A => isIn a Z2) X2)) + assert (U (U (comprehension (fun a : A => isIn a Z1) X2) + (comprehension (fun a : A => isIn a Z2) X2)) + Y = U (U (comprehension (fun a : A => isIn a Z1) X2) + (comprehension (fun a : A => isIn a Z2) X2)) (U Y Y)). rewrite (union_idem Y). reflexivity. @@ -354,8 +358,9 @@ hinduction X1; try (intros ; apply set_path2) ; cbn. rewrite <- assoc. rewrite (assoc (comprehension (fun a : A => isIn a Z2) X2)). rewrite Q. - rewrite (comm (U (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) X2) - (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) Y)) Y). + rewrite + (comm (U (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) X2) + (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) Y)) Y). rewrite assoc. rewrite P. rewrite <- assoc. @@ -364,10 +369,12 @@ hinduction X1; try (intros ; apply set_path2) ; cbn. rewrite <- assoc. rewrite assoc. enough (C : (U (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) X2) - (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) X2)) = (comprehension (fun a : A => (isIn a Z1 || isIn a Z2 || isIn a Y)%Bool) X2)). + (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) X2)) + = (comprehension (fun a : A => (isIn a Z1 || isIn a Z2 || isIn a Y)%Bool) X2)). rewrite C. enough (D : (U (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) Y) - (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) Y)) = (comprehension (fun a : A => (isIn a Z1 || isIn a Z2 || isIn a Y)%Bool) Y)). + (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) Y)) + = (comprehension (fun a : A => (isIn a Z1 || isIn a Z2 || isIn a Y)%Bool) Y)). rewrite D. reflexivity. * repeat (rewrite comprehension_or). @@ -428,5 +435,48 @@ hrecursion X; try (intros ; apply set_path2). rewrite <- P. rewrite <- Q. Admitted. - + + +(* Properties about subset relation. *) +Lemma subsect_intersection `{Funext} (X Y : FSet A) : + subset X Y = true -> 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). + (*intros. apply equiv_hprop_allpath.*) + + intro. cbn. contradiction (false_ne_true). + + intros. destruct (dec (a = a0)). + rewrite p; apply idem. + contradiction (false_ne_true). + + intros X1 X2 IH1 IH2. + intro Ho. + destruct (isIn a X1); + destruct (isIn a X2). + specialize (IH1 idpath). + specialize (IH2 idpath). + rewrite assoc. rewrite IH1. reflexivity. + specialize (IH1 idpath). + rewrite assoc. rewrite IH1. reflexivity. + specialize (IH2 idpath). + rewrite assoc. rewrite (comm (L a)). rewrite <- assoc. rewrite IH2. + reflexivity. + cbn in Ho. contradiction (false_ne_true). +- intros X1 X2 IH1 IH2 G. + destruct (subset X1 Y); + destruct (subset X2 Y). + specialize (IH1 idpath). + specialize (IH2 idpath). + rewrite <- assoc. rewrite IH2. rewrite IH1. reflexivity. + specialize (IH1 idpath). + apply IH2 in G. + rewrite <- assoc. rewrite G. rewrite IH1. reflexivity. + specialize (IH2 idpath). + apply IH1 in G. + rewrite <- assoc. rewrite IH2. rewrite G. reflexivity. + specialize (IH1 G). specialize (IH2 G). + rewrite <- assoc. rewrite IH2. rewrite IH1. reflexivity. +Defined. + End properties. From 9202c6489d630d9a536fb179e18457d9cc0b9772 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Thu, 25 May 2017 15:11:41 +0200 Subject: [PATCH 2/4] Speed up the compilation of properties.v a little bit --- FiniteSets/properties.v | 112 +++++++++++++++++++--------------------- 1 file changed, 53 insertions(+), 59 deletions(-) diff --git a/FiniteSets/properties.v b/FiniteSets/properties.v index 365ef68..a1e68ff 100644 --- a/FiniteSets/properties.v +++ b/FiniteSets/properties.v @@ -20,8 +20,7 @@ try (intros ; apply set_path2) ; cbn. rewrite P. rewrite (comm y x). rewrite <- (assoc x y y). - rewrite Q. - reflexivity. + f_ap. Defined. @@ -177,22 +176,24 @@ Defined. Theorem intersection_idem : forall (X : FSet A), intersection X X = X. Proof. -hinduction; try (intros; apply set_path2). +hinduction; try (intros ; apply set_path2). - reflexivity. - intro a. destruct (dec (a = a)). * reflexivity. * contradiction (n idpath). - intros X Y IHX IHY. + f_ap; unfold intersection in *. - rewrite comprehension_or. - rewrite comprehension_or. - rewrite IHX. - rewrite IHY. - rewrite comprehension_subset. - rewrite (comm X). - rewrite comprehension_subset. - reflexivity. + + transitivity (U (comprehension (fun a => isIn a X) X) (comprehension (fun a => isIn a Y) X)). + apply comprehension_or. + rewrite IHX. + rewrite (comm X). + apply comprehension_subset. + + transitivity (U (comprehension (fun a => isIn a X) Y) (comprehension (fun a => isIn a Y) Y)). + apply comprehension_or. + rewrite IHY. + apply comprehension_subset. Defined. (** assorted lattice laws *) @@ -270,8 +271,6 @@ hinduction x; try (intros ; apply set_path2) ; cbn. reflexivity. Defined. - - Theorem intersection_assoc (X Y Z: FSet A) : intersection X (intersection Y Z) = intersection (intersection X Y) Z. Proof. @@ -314,14 +313,12 @@ hinduction; try (intros ; apply set_path2). * reflexivity. * contradiction (n idpath). - intros X1 X2 P Q. - rewrite comprehension_or. - rewrite comprehension_or. - rewrite P. + f_ap; (etransitivity; [ apply comprehension_or |]). + rewrite P. rewrite (comm X1). + apply comprehension_subset. + rewrite Q. - rewrite comprehension_subset. - rewrite (comm X1). - rewrite comprehension_subset. - reflexivity. + apply comprehension_subset. Defined. @@ -338,13 +335,16 @@ hinduction X1; try (intros ; apply set_path2) ; cbn. rewrite p. rewrite comprehension_subset. reflexivity. -- intros. unfold intersection. (* TODO isIn is simplified too much *) - rewrite comprehension_or. - rewrite comprehension_or. - (* rewrite intersection_La. *) +- intros. + assert (Y = intersection (U (L a) Y) Y) as HY. + { unfold intersection. symmetry. + transitivity (U (comprehension (fun x => isIn x (L a)) Y) (comprehension (fun x => isIn x Y) Y)). + apply comprehension_or. + rewrite comprehension_all. + apply comprehension_subset. } + rewrite <- HY. admit. - unfold intersection. - cbn. intros Z1 Z2 P Q. rewrite comprehension_or. assert (U (U (comprehension (fun a : A => isIn a Z1) X2) @@ -358,12 +358,13 @@ hinduction X1; try (intros ; apply set_path2) ; cbn. rewrite <- assoc. rewrite (assoc (comprehension (fun a : A => isIn a Z2) X2)). rewrite Q. + cbn. rewrite (comm (U (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) X2) (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) Y)) Y). rewrite assoc. rewrite P. - rewrite <- assoc. + rewrite <- assoc. cbn. rewrite (assoc (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) Y)). rewrite (comm (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) Y)). rewrite <- assoc. @@ -443,40 +444,33 @@ Lemma subsect_intersection `{Funext} (X Y : FSet A) : 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). - (*intros. apply equiv_hprop_allpath.*) - + intro. cbn. contradiction (false_ne_true). - + intros. destruct (dec (a = a0)). - rewrite p; apply idem. - contradiction (false_ne_true). - + intros X1 X2 IH1 IH2. - intro Ho. - destruct (isIn a X1); - destruct (isIn a X2). - specialize (IH1 idpath). - specialize (IH2 idpath). - rewrite assoc. rewrite IH1. reflexivity. - specialize (IH1 idpath). - rewrite assoc. rewrite IH1. reflexivity. - specialize (IH2 idpath). - rewrite assoc. rewrite (comm (L a)). rewrite <- assoc. rewrite IH2. - reflexivity. - cbn in Ho. contradiction (false_ne_true). +- intros a. hinduction Y; + try (intros; apply path_forall; intro; apply set_path2). + + intro. contradiction (false_ne_true). + + intros. destruct (dec (a = a0)). + rewrite p; apply idem. + contradiction (false_ne_true). + + intros X1 X2 IH1 IH2. + intro Ho. + destruct (isIn a X1); + destruct (isIn a X2). + * specialize (IH1 idpath). + rewrite assoc. f_ap. + * specialize (IH1 idpath). + rewrite assoc. f_ap. + * specialize (IH2 idpath). + rewrite (comm X1 X2). + rewrite assoc. f_ap. + * contradiction (false_ne_true). - intros X1 X2 IH1 IH2 G. - destruct (subset X1 Y); - destruct (subset X2 Y). - specialize (IH1 idpath). - specialize (IH2 idpath). - rewrite <- assoc. rewrite IH2. rewrite IH1. reflexivity. - specialize (IH1 idpath). - apply IH2 in G. - rewrite <- assoc. rewrite G. rewrite IH1. reflexivity. - specialize (IH2 idpath). - apply IH1 in G. - rewrite <- assoc. rewrite IH2. rewrite G. reflexivity. - specialize (IH1 G). specialize (IH2 G). - rewrite <- assoc. rewrite IH2. rewrite IH1. reflexivity. + destruct (subset X1 Y); + destruct (subset X2 Y). + * specialize (IH1 idpath). + specialize (IH2 idpath). + rewrite <- assoc. rewrite IH2. apply IH1. + * contradiction (false_ne_true). + * contradiction (false_ne_true). + * contradiction (false_ne_true). Defined. End properties. From 294f818b07d85407c69717bf21f2904e141ee6f2 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Thu, 25 May 2017 16:28:09 +0200 Subject: [PATCH 3/4] Add [eq_subset] equivalence MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X = Y <~> X ⊂ Y /\ Y ⊂ X --- FiniteSets/properties.v | 73 +++++++++++++++++++++++++++++++++++++++-- 1 file changed, 70 insertions(+), 3 deletions(-) diff --git a/FiniteSets/properties.v b/FiniteSets/properties.v index a1e68ff..93020ac 100644 --- a/FiniteSets/properties.v +++ b/FiniteSets/properties.v @@ -1,5 +1,5 @@ Require Import HoTT HitTactics. -Require Import definition operations. +Require Export definition operations. Section properties. @@ -439,8 +439,8 @@ Admitted. (* Properties about subset relation. *) -Lemma subsect_intersection `{Funext} (X Y : FSet A) : - subset X Y = true -> U X Y = Y. +Lemma subset_union `{Funext} (X Y : FSet A) : + subset X Y = true -> U X Y = Y. Proof. hinduction X; try (intros; apply path_forall; intro; apply set_path2). - intros. apply nl. @@ -473,4 +473,71 @@ 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. +hinduction X; + try (intros; apply path_forall; intro; apply set_path2). +- reflexivity. +- intros a Y. destruct (dec (a = a)). + * reflexivity. + * by contradiction n. +- intros X1 X2 HX1 HX2 Y. + enough (subset X1 (U (U X1 X2) Y) = true). + enough (subset X2 (U (U X1 X2) Y) = true). + rewrite X. rewrite X0. reflexivity. + { 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. + unshelve eapply BuildEquiv. + apply subset_union. + unshelve esplit. + { intros HXY. rewrite <- HXY. clear HXY. + apply subset_union_l. } + all: intro; apply set_path2. +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 eq1. + symmetry. + eapply equiv_functor_prod'; apply subset_union_equiv. +Defined. + +Lemma subset_isIn (X Y : FSet A) : + (forall (a : A), isIn a X = true -> isIn a Y = true) + <-> (subset X Y = true). +Admitted. + +Theorem fset_ext `{Funext} (X Y : FSet A) : + X = Y <~> (forall (a : A), isIn a X = isIn a Y). +Proof. + etransitivity. apply eq_subset. + transitivity + ((forall a, isIn a Y = true -> isIn a X = true) + *(forall a, isIn a X = true -> isIn a Y = true)). + - admit. + - admit. +Admitted. + End properties. From 06dc8a0acdec2cb412c019ae0ce097e772ab90ae Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Thu, 25 May 2017 18:59:18 +0200 Subject: [PATCH 4/4] A proof of subset_isIn --- FiniteSets/properties.v | 59 ++++++++++++++++++++++++++++++++++++++--- 1 file changed, 55 insertions(+), 4 deletions(-) diff --git a/FiniteSets/properties.v b/FiniteSets/properties.v index 93020ac..d1317e1 100644 --- a/FiniteSets/properties.v +++ b/FiniteSets/properties.v @@ -524,10 +524,61 @@ Proof. eapply equiv_functor_prod'; apply subset_union_equiv. Defined. -Lemma subset_isIn (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). -Admitted. +Proof. + split. + - hinduction X ; try (intros ; apply path_forall ; intro ; apply set_path2). + * intros ; reflexivity. + * intros a H. + apply H. + destruct (dec (a = a)). + + reflexivity. + + contradiction (n idpath). + * intros X1 X2 H1 H2 H. + enough (subset X1 Y = true). + rewrite X. + enough (subset X2 Y = true). + rewrite X0. + reflexivity. + + apply H2. + intros a Ha. + apply H. + rewrite Ha. + destruct (isIn a X1) ; reflexivity. + + apply H1. + intros a Ha. + apply H. + rewrite Ha. + reflexivity. + - hinduction X . + * intros. contradiction (false_ne_true X0). + * intros b H a. + destruct (dec (a = b)). + + intros ; rewrite p ; apply H. + + intros X ; contradiction (false_ne_true X). + * intros X1 X2. + intros IH1 IH2 H1 a H2. + destruct (subset X1 Y) ; destruct (subset X2 Y); + cbv in H1; try by contradiction false_ne_true. + specialize (IH1 idpath a). specialize (IH2 idpath a). + destruct (isIn a X1); destruct (isIn a X2); + cbv in H2; try by contradiction false_ne_true. + by apply IH1. + by apply IH1. + by apply IH2. + * repeat (intro; intros; apply path_forall). + intros; intro; intros; apply set_path2. + * repeat (intro; intros; apply path_forall). + intros; intro; intros; apply set_path2. + * repeat (intro; intros; apply path_forall). + intros; intro; intros; apply set_path2. + * repeat (intro; intros; apply path_forall). + intros; intro; intros; apply set_path2. + * repeat (intro; intros; apply path_forall); + intros; intro; intros; apply set_path2. +Defined. Theorem fset_ext `{Funext} (X Y : FSet A) : X = Y <~> (forall (a : A), isIn a X = isIn a Y). @@ -536,8 +587,8 @@ Proof. transitivity ((forall a, isIn a Y = true -> isIn a X = true) *(forall a, isIn a X = true -> isIn a Y = true)). - - admit. - - admit. + - eapply equiv_functor_prod'. admit. admit. + - eapply equiv_functor_prod'. Admitted. End properties.