From f8ed41e5fe9a1c52bd9a03632e72bfde36caf00d Mon Sep 17 00:00:00 2001 From: Leon Gondelman Date: Fri, 26 May 2017 12:28:07 +0200 Subject: [PATCH] trailing white spaces --- FiniteSets/operations.v | 10 +++--- FiniteSets/properties.v | 70 +++++++++++++++++++++-------------------- 2 files changed, 41 insertions(+), 39 deletions(-) diff --git a/FiniteSets/operations.v b/FiniteSets/operations.v index bd21a0d..5299d39 100644 --- a/FiniteSets/operations.v +++ b/FiniteSets/operations.v @@ -19,7 +19,6 @@ hrecursion. - intros a'. compute. destruct (A_deceq a a'); reflexivity. Defined. -Infix "∈" := isIn (at level 9, right associativity). Definition comprehension : (A -> Bool) -> FSet A -> FSet A. @@ -54,15 +53,16 @@ Proof. intros X Y. hrecursion X. - exact true. -- exact (fun a => (a ∈ Y)). +- exact (fun a => (isIn 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. +- intros x; cbn; destruct (isIn x Y); reflexivity. Defined. -Notation "⊆" := subset. - End operations. + +Infix "∈" := isIn (at level 9, right associativity). +Infix "⊆" := subset (at level 10, right associativity). \ No newline at end of file diff --git a/FiniteSets/properties.v b/FiniteSets/properties.v index 365ef68..6cfa9b3 100644 --- a/FiniteSets/properties.v +++ b/FiniteSets/properties.v @@ -9,7 +9,7 @@ Context {A_deceq : DecidablePaths A}. (** union properties *) Theorem union_idem : forall x: FSet A, U x x = x. Proof. -hinduction; +hinduction; try (intros ; apply set_path2) ; cbn. - apply nl. - apply idem. @@ -24,24 +24,24 @@ try (intros ; apply set_path2) ; cbn. reflexivity. Defined. - + (** isIn properties *) Lemma isIn_singleton_eq (a b: A) : isIn a (L b) = true -> a = b. -Proof. unfold isIn. simpl. +Proof. unfold isIn. simpl. destruct (dec (a = b)). intro. apply p. -intro X. +intro X. contradiction (false_ne_true X). Defined. Lemma isIn_empty_false (a: A) : isIn a E = true -> Empty. -Proof. +Proof. cbv. intro X. -contradiction (false_ne_true X). +contradiction (false_ne_true X). Defined. -Lemma isIn_union (a: A) (X Y: FSet A) : +Lemma isIn_union (a: A) (X Y: FSet A) : isIn a (U X Y) = (isIn a X || isIn a Y)%Bool. -Proof. reflexivity. Qed. +Proof. reflexivity. Qed. (** comprehension properties *) Lemma comprehension_false Y : comprehension (fun a => isIn a E) Y = E. @@ -58,20 +58,20 @@ hrecursion Y; try (intros; apply set_path2). Defined. Theorem comprehension_or : forall ϕ ψ (x: FSet A), - comprehension (fun a => orb (ϕ a) (ψ a)) x = U (comprehension ϕ x) + comprehension (fun a => orb (ϕ a) (ψ a)) x = U (comprehension ϕ x) (comprehension ψ x). Proof. intros ϕ ψ. -hinduction; try (intros; apply set_path2). +hinduction; try (intros; apply set_path2). - cbn. symmetry ; apply nl. - cbn. intros. destruct (ϕ a) ; destruct (ψ a) ; symmetry. * apply idem. - * apply nr. + * apply nr. * apply nl. * apply nl. - simpl. intros x y P Q. - cbn. + cbn. rewrite P. rewrite Q. rewrite <- assoc. @@ -105,8 +105,8 @@ Defined. (** intersection properties *) Lemma intersection_0l: forall X: FSet A, intersection E X = E. -Proof. -hinduction; +Proof. +hinduction; try (intros ; apply set_path2). - reflexivity. - intro a. @@ -144,7 +144,7 @@ hinduction; try (intros ; apply set_path2). destruct (isIn a x) ; destruct (isIn a y). * apply idem. * apply nr. - * apply nl. + * apply nl. * apply nl. Defined. @@ -163,7 +163,7 @@ hrecursion X; try (intros; apply set_path2). * destruct (dec (b = a)) as [pb|]; [|reflexivity]. by contradiction npa. + cbn -[isIn]. intros Y1 Y2 IH1 IH2. - rewrite IH1. + rewrite IH1. rewrite IH2. symmetry. apply (comprehension_or (fun a => isIn a Y1) (fun a => isIn a Y2) (L a)). @@ -171,7 +171,7 @@ hrecursion X; try (intros; apply set_path2). cbn. unfold intersection in *. rewrite <- IH1. - rewrite <- IH2. + rewrite <- IH2. apply comprehension_or. Defined. @@ -196,7 +196,7 @@ hinduction; try (intros; apply set_path2). Defined. (** assorted lattice laws *) -Lemma distributive_La (z : FSet A) (a : A) : forall Y : FSet A, +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. @@ -266,7 +266,7 @@ 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) ; + destruct (isIn a X1) ; destruct (isIn a X2) ; destruct (isIn a y) ; reflexivity. Defined. @@ -292,7 +292,7 @@ hinduction X; try (intros ; apply set_path2). + reflexivity. + reflexivity. * rewrite intersection_0l. - reflexivity. + reflexivity. - unfold intersection. cbn. intros X1 X2 P Q. rewrite comprehension_or. @@ -324,7 +324,7 @@ hinduction; try (intros ; apply set_path2). reflexivity. Defined. - + Theorem distributive_U_int (X1 X2 Y : FSet A) : U (intersection X1 X2) Y = intersection (U X1 Y) (U X2 Y). Proof. @@ -347,9 +347,9 @@ 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) + 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) + 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). @@ -358,7 +358,7 @@ hinduction X1; try (intros ; apply set_path2) ; cbn. rewrite <- assoc. rewrite (assoc (comprehension (fun a : A => isIn a Z2) X2)). rewrite Q. - rewrite + 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. @@ -369,11 +369,11 @@ 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 Z2 || isIn a Y)%Bool) X2)) = (comprehension (fun a : A => (isIn a Z1 || isIn a Z2 || isIn a Y)%Bool) X2)). - rewrite C. + 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 Z2 || isIn a Y)%Bool) Y)) = (comprehension (fun a : A => (isIn a Z1 || isIn a Z2 || isIn a Y)%Bool) Y)). rewrite D. reflexivity. @@ -438,12 +438,12 @@ Admitted. (* Properties about subset relation. *) -Lemma subsect_intersection `{Funext} (X Y : FSet A) : - subset X Y = true -> U X Y = Y. +Lemma subsect_intersection `{Funext} (X Y : FSet A) : + 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; +- intros a. hinduction Y; try (intros; apply path_forall; intro; apply set_path2). (*intros. apply equiv_hprop_allpath.*) + intro. cbn. contradiction (false_ne_true). @@ -460,10 +460,10 @@ hinduction X; try (intros; apply path_forall; intro; apply set_path2). specialize (IH1 idpath). rewrite assoc. rewrite IH1. reflexivity. specialize (IH2 idpath). - rewrite assoc. rewrite (comm (L a)). rewrite <- assoc. rewrite IH2. + rewrite assoc. rewrite (comm (L a)). rewrite <- assoc. rewrite IH2. reflexivity. - cbn in Ho. contradiction (false_ne_true). -- intros X1 X2 IH1 IH2 G. + cbn in Ho. contradiction (false_ne_true). +- intros X1 X2 IH1 IH2 G. destruct (subset X1 Y); destruct (subset X2 Y). specialize (IH1 idpath). @@ -479,4 +479,6 @@ hinduction X; try (intros; apply path_forall; intro; apply set_path2). rewrite <- assoc. rewrite IH2. rewrite IH1. reflexivity. Defined. -End properties. +Theorem + +End properties.