diff options
Diffstat (limited to 'theories/Structures')
| -rw-r--r-- | theories/Structures/Equalities.v | 10 | ||||
| -rw-r--r-- | theories/Structures/GenericMinMax.v | 90 | ||||
| -rw-r--r-- | theories/Structures/Orders.v | 54 | ||||
| -rw-r--r-- | theories/Structures/OrdersFacts.v | 6 |
4 files changed, 86 insertions, 74 deletions
diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v index 4143dba547..346c300ee5 100644 --- a/theories/Structures/Equalities.v +++ b/theories/Structures/Equalities.v @@ -158,8 +158,10 @@ Module HasEqDec2Bool (E:Eq)(F:HasEqDec E) <: HasEqBool E. Lemma eqb_eq : forall x y, eqb x y = true <-> E.eq x y. Proof. intros x y. unfold eqb. destruct F.eq_dec as [EQ|NEQ]. - auto with *. - split. discriminate. intro EQ; elim NEQ; auto. + - auto with *. + - split. + + discriminate. + + intro EQ; elim NEQ; auto. Qed. End HasEqDec2Bool. @@ -168,8 +170,8 @@ Module HasEqBool2Dec (E:Eq)(F:HasEqBool E) <: HasEqDec E. Proof. intros x y. assert (H:=F.eqb_eq x y). destruct (F.eqb x y); [left|right]. - apply -> H; auto. - intro EQ. apply H in EQ. discriminate. + - apply -> H; auto. + - intro EQ. apply H in EQ. discriminate. Defined. End HasEqBool2Dec. diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index 4d04667c01..c314f3f982 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -47,8 +47,8 @@ Module GenericMinMax (Import O:OrderedTypeFull') <: HasMinMax O. intros H H'. apply (StrictOrder_Irreflexive x). rewrite le_lteq in *; destruct H as [H|H]. - transitivity y; auto. - rewrite H in H'; auto. + - transitivity y; auto. + - rewrite H in H'; auto. Qed. Lemma max_l x y : y<=x -> max x y == x. @@ -142,8 +142,8 @@ Proof. intros Eqf Lef x y. destruct (max_spec x y) as [(H,E)|(H,E)]; rewrite E; destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. - assert (f x <= f y) by (apply Lef; order). order. - assert (f y <= f x) by (apply Lef; order). order. + - assert (f x <= f y) by (apply Lef; order). order. + - assert (f y <= f x) by (apply Lef; order). order. Qed. (** *** Semi-lattice algebraic properties of [max] *) @@ -194,7 +194,11 @@ Proof. Qed. Lemma max_le_iff n m p : p <= max n m <-> p <= n \/ p <= m. -Proof. split. apply max_le. solve_max. Qed. +Proof. + split. + - apply max_le. + - solve_max. +Qed. Lemma max_lt_iff n m p : p < max n m <-> p < n \/ p < m. Proof. @@ -282,8 +286,8 @@ Proof. intros Eqf Lef x y. destruct (min_spec x y) as [(H,E)|(H,E)]; rewrite E; destruct (min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. - assert (f x <= f y) by (apply Lef; order). order. - assert (f y <= f x) by (apply Lef; order). order. + - assert (f x <= f y) by (apply Lef; order). order. + - assert (f y <= f x) by (apply Lef; order). order. Qed. Lemma min_id n : min n n == n. @@ -330,7 +334,11 @@ Proof. Qed. Lemma min_le_iff n m p : min n m <= p <-> n <= p \/ m <= p. -Proof. split. apply min_le. solve_min. Qed. +Proof. + split. + - apply min_le. + - solve_min. +Qed. Lemma min_lt_iff n m p : min n m < p <-> n < p \/ m < p. Proof. @@ -377,16 +385,16 @@ Lemma min_max_absorption n m : max n (min n m) == n. Proof. intros. destruct (min_spec n m) as [(C,E)|(C,E)]; rewrite E. - apply max_l. order. - destruct (max_spec n m); intuition; order. + - apply max_l. order. + - destruct (max_spec n m); intuition; order. Qed. Lemma max_min_absorption n m : min n (max n m) == n. Proof. intros. destruct (max_spec n m) as [(C,E)|(C,E)]; rewrite E. - destruct (min_spec n m) as [(C',E')|(C',E')]; auto. order. - apply min_l; auto. order. + - destruct (min_spec n m) as [(C',E')|(C',E')]; auto. order. + - apply min_l; auto. order. Qed. (** Distributivity *) @@ -395,16 +403,16 @@ Lemma max_min_distr n m p : max n (min m p) == min (max n m) (max n p). Proof. symmetry. apply min_mono. - eauto with *. - repeat red; intros. apply max_le_compat_l; auto. + - eauto with *. + - repeat red; intros. apply max_le_compat_l; auto. Qed. Lemma min_max_distr n m p : min n (max m p) == max (min n m) (min n p). Proof. symmetry. apply max_mono. - eauto with *. - repeat red; intros. apply min_le_compat_l; auto. + - eauto with *. + - repeat red; intros. apply min_le_compat_l; auto. Qed. (** Modularity *) @@ -415,8 +423,8 @@ Proof. rewrite <- max_min_distr. destruct (max_spec n p) as [(C,E)|(C,E)]; rewrite E; auto with *. destruct (min_spec m n) as [(C',E')|(C',E')]; rewrite E'. - rewrite 2 max_l; try order. rewrite min_le_iff; auto. - rewrite 2 max_l; try order. rewrite min_le_iff; auto. + - rewrite 2 max_l; try order. rewrite min_le_iff; auto. + - rewrite 2 max_l; try order. rewrite min_le_iff; auto. Qed. Lemma min_max_modular n m p : @@ -425,8 +433,8 @@ Proof. intros. rewrite <- min_max_distr. destruct (min_spec n p) as [(C,E)|(C,E)]; rewrite E; auto with *. destruct (max_spec m n) as [(C',E')|(C',E')]; rewrite E'. - rewrite 2 min_l; try order. rewrite max_le_iff; right; order. - rewrite 2 min_l; try order. rewrite max_le_iff; auto. + - rewrite 2 min_l; try order. rewrite max_le_iff; right; order. + - rewrite 2 min_l; try order. rewrite max_le_iff; auto. Qed. (** Disassociativity *) @@ -448,8 +456,8 @@ Proof. intros Eqf Lef x y. destruct (min_spec x y) as [(H,E)|(H,E)]; rewrite E; destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. - assert (f y <= f x) by (apply Lef; order). order. - assert (f x <= f y) by (apply Lef; order). order. + - assert (f y <= f x) by (apply Lef; order). order. + - assert (f x <= f y) by (apply Lef; order). order. Qed. Lemma min_max_antimono f : @@ -460,8 +468,8 @@ Proof. intros Eqf Lef x y. destruct (max_spec x y) as [(H,E)|(H,E)]; rewrite E; destruct (min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. - assert (f y <= f x) by (apply Lef; order). order. - assert (f x <= f y) by (apply Lef; order). order. + - assert (f y <= f x) by (apply Lef; order). order. + - assert (f x <= f y) by (apply Lef; order). order. Qed. End MinMaxLogicalProperties. @@ -479,12 +487,12 @@ Lemma max_case_strong n m (P:t -> Type) : Proof. intros Compat Hl Hr. destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT]. -assert (n<=m) by (rewrite le_lteq; auto). -apply (Compat m), Hr; auto. symmetry; apply max_r; auto. -assert (n<=m) by (rewrite le_lteq; auto). -apply (Compat m), Hr; auto. symmetry; apply max_r; auto. -assert (m<=n) by (rewrite le_lteq; auto). -apply (Compat n), Hl; auto. symmetry; apply max_l; auto. +- assert (n<=m) by (rewrite le_lteq; auto). + apply (Compat m), Hr; auto. symmetry; apply max_r; auto. +- assert (n<=m) by (rewrite le_lteq; auto). + apply (Compat m), Hr; auto. symmetry; apply max_r; auto. +- assert (m<=n) by (rewrite le_lteq; auto). + apply (Compat n), Hl; auto. symmetry; apply max_l; auto. Defined. Lemma max_case n m (P:t -> Type) : @@ -508,12 +516,12 @@ Lemma min_case_strong n m (P:O.t -> Type) : Proof. intros Compat Hl Hr. destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT]. -assert (n<=m) by (rewrite le_lteq; auto). -apply (Compat n), Hl; auto. symmetry; apply min_l; auto. -assert (n<=m) by (rewrite le_lteq; auto). -apply (Compat n), Hl; auto. symmetry; apply min_l; auto. -assert (m<=n) by (rewrite le_lteq; auto). -apply (Compat m), Hr; auto. symmetry; apply min_r; auto. +- assert (n<=m) by (rewrite le_lteq; auto). + apply (Compat n), Hl; auto. symmetry; apply min_l; auto. +- assert (n<=m) by (rewrite le_lteq; auto). + apply (Compat n), Hl; auto. symmetry; apply min_l; auto. +- assert (m<=n) by (rewrite le_lteq; auto). + apply (Compat m), Hr; auto. symmetry; apply min_r; auto. Defined. Lemma min_case n m (P:O.t -> Type) : @@ -624,11 +632,11 @@ Module TOMaxEqDec_to_Compare Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). Proof. intros; unfold compare; repeat destruct eq_dec; auto; constructor. - destruct (lt_total x y); auto. - absurd (x==y); auto. transitivity (max x y); auto. - symmetry. apply max_l. rewrite le_lteq; intuition. - destruct (lt_total y x); auto. - absurd (max x y == y); auto. apply max_r; rewrite le_lteq; intuition. + - destruct (lt_total x y); auto. + absurd (x==y); auto. transitivity (max x y); auto. + symmetry. apply max_l. rewrite le_lteq; intuition. + - destruct (lt_total y x); auto. + absurd (max x y == y); auto. apply max_r; rewrite le_lteq; intuition. Qed. End TOMaxEqDec_to_Compare. diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v index 310a22a0a4..7fcf517457 100644 --- a/theories/Structures/Orders.v +++ b/theories/Structures/Orders.v @@ -143,8 +143,8 @@ Module Compare2EqBool (Import O:DecStrOrder') <: HasEqBool O. Proof. unfold eqb. intros x y. destruct (compare_spec x y) as [H|H|H]; split; auto; try discriminate. - intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H). - intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H). + - intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H). + - intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H). Qed. End Compare2EqBool. @@ -252,9 +252,11 @@ Module OTF_to_TTLB (Import O : OrderedTypeFull') <: TotalTransitiveLeBool. Proof. intros. unfold leb. rewrite le_lteq. destruct (compare_spec x y) as [EQ|LT|GT]; split; auto. - discriminate. - intros LE. elim (StrictOrder_Irreflexive x). - destruct LE as [LT|EQ]. now transitivity y. now rewrite <- EQ in GT. + - discriminate. + - intros LE. elim (StrictOrder_Irreflexive x). + destruct LE as [LT|EQ]. + + now transitivity y. + + now rewrite <- EQ in GT. Qed. Lemma leb_total : forall x y, leb x y \/ leb y x. @@ -267,10 +269,10 @@ Module OTF_to_TTLB (Import O : OrderedTypeFull') <: TotalTransitiveLeBool. Proof. intros x y z. rewrite !leb_le, !le_lteq. intros [Hxy|Hxy] [Hyz|Hyz]. - left; transitivity y; auto. - left; rewrite <- Hyz; auto. - left; rewrite Hxy; auto. - right; transitivity y; auto. + - left; transitivity y; auto. + - left; rewrite <- Hyz; auto. + - left; rewrite Hxy; auto. + - right; transitivity y; auto. Qed. Definition t := t. @@ -302,10 +304,10 @@ Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull. Proof. intros. unfold compare. case_eq (x <=? y). - case_eq (y <=? x). - constructor. split; auto. - constructor. split; congruence. - constructor. destruct (leb_total x y); split; congruence. + - case_eq (y <=? x). + + constructor. split; auto. + + constructor. split; congruence. + - constructor. destruct (leb_total x y); split; congruence. Qed. Definition eqb x y := (x <=? y) && (y <=? x). @@ -321,19 +323,19 @@ Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull. Instance eq_equiv : Equivalence eq. Proof. split. - intros x; unfold eq, le. destruct (leb_total x x); auto. - intros x y; unfold eq, le. intuition. - intros x y z; unfold eq, le. intuition; apply leb_trans with y; auto. + - intros x; unfold eq, le. destruct (leb_total x x); auto. + - intros x y; unfold eq, le. intuition. + - intros x y z; unfold eq, le. intuition; apply leb_trans with y; auto. Qed. Instance lt_strorder : StrictOrder lt. Proof. split. - intros x. unfold lt; red; intuition. - intros x y z; unfold lt, le. intuition. - apply leb_trans with y; auto. - absurd (z <=? y); auto. - apply leb_trans with x; auto. + - intros x. unfold lt; red; intuition. + - intros x y z; unfold lt, le. intuition. + + apply leb_trans with y; auto. + + absurd (z <=? y); auto. + apply leb_trans with x; auto. Qed. Instance lt_compat : Proper (eq ==> eq ==> iff) lt. @@ -341,11 +343,11 @@ Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull. apply proper_sym_impl_iff_2; auto with *. intros x x' Hx y y' Hy' H. unfold eq, lt, le in *. intuition. - apply leb_trans with x; auto. - apply leb_trans with y; auto. - absurd (y <=? x); auto. - apply leb_trans with x'; auto. - apply leb_trans with y'; auto. + - apply leb_trans with x; auto. + apply leb_trans with y; auto. + - absurd (y <=? x); auto. + apply leb_trans with x'; auto. + apply leb_trans with y'; auto. Qed. Definition le_lteq : forall x y, le x y <-> lt x y \/ eq x y. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 1fb0a37e16..182b781fe1 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -290,9 +290,9 @@ Module Type CompareBasedOrderFacts Lemma compare_spec x y : CompareSpec (x==y) (x<y) (y<x) (x?=y). Proof. case_eq (compare x y); intros H; constructor. - now apply compare_eq_iff. - now apply compare_lt_iff. - rewrite compare_antisym, CompOpp_iff in H. now apply compare_lt_iff. + - now apply compare_eq_iff. + - now apply compare_lt_iff. + - rewrite compare_antisym, CompOpp_iff in H. now apply compare_lt_iff. Qed. Lemma compare_eq x y : (x ?= y) = Eq -> x==y. |