diff options
Diffstat (limited to 'theories/Structures')
| -rw-r--r-- | theories/Structures/DecidableType.v | 2 | ||||
| -rw-r--r-- | theories/Structures/DecidableTypeEx.v | 8 | ||||
| -rw-r--r-- | theories/Structures/Equalities.v | 77 | ||||
| -rw-r--r-- | theories/Structures/EqualitiesFacts.v | 23 | ||||
| -rw-r--r-- | theories/Structures/GenericMinMax.v | 425 | ||||
| -rw-r--r-- | theories/Structures/OrderedType.v | 47 | ||||
| -rw-r--r-- | theories/Structures/OrderedTypeAlt.v | 2 | ||||
| -rw-r--r-- | theories/Structures/OrderedTypeEx.v | 172 | ||||
| -rw-r--r-- | theories/Structures/Orders.v | 109 | ||||
| -rw-r--r-- | theories/Structures/OrdersAlt.v | 8 | ||||
| -rw-r--r-- | theories/Structures/OrdersEx.v | 12 | ||||
| -rw-r--r-- | theories/Structures/OrdersFacts.v | 324 | ||||
| -rw-r--r-- | theories/Structures/OrdersLists.v | 6 | ||||
| -rw-r--r-- | theories/Structures/OrdersTac.v | 69 |
14 files changed, 762 insertions, 522 deletions
diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v index 18153436..79e81771 100644 --- a/theories/Structures/DecidableType.v +++ b/theories/Structures/DecidableType.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: DecidableType.v 12641 2010-01-07 15:32:52Z letouzey $ *) - Require Export SetoidList. Require Equalities. diff --git a/theories/Structures/DecidableTypeEx.v b/theories/Structures/DecidableTypeEx.v index ac1f014b..971fcd7f 100644 --- a/theories/Structures/DecidableTypeEx.v +++ b/theories/Structures/DecidableTypeEx.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: DecidableTypeEx.v 12641 2010-01-07 15:32:52Z letouzey $ *) - Require Import DecidableType OrderedType OrderedTypeEx. Set Implicit Arguments. Unset Strict Implicit. @@ -81,9 +79,9 @@ End PairDecidableType. Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType. Definition t := prod D1.t D2.t. Definition eq := @eq t. - Definition eq_refl := @refl_equal t. - Definition eq_sym := @sym_eq t. - Definition eq_trans := @trans_eq t. + Definition eq_refl := @eq_refl t. + Definition eq_sym := @eq_sym t. + Definition eq_trans := @eq_trans t. Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }. Proof. intros (x1,x2) (y1,y2); diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v index 382511d9..eb537385 100644 --- a/theories/Structures/Equalities.v +++ b/theories/Structures/Equalities.v @@ -6,23 +6,28 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: Equalities.v 13475 2010-09-29 14:33:13Z letouzey $ *) - Require Export RelationClasses. +Require Import Bool Morphisms Setoid. Set Implicit Arguments. Unset Strict Implicit. +(** Structure with nothing inside. + Used to force a module type T into a module via Nop <+ T. (HACK!) *) + +Module Type Nop. +End Nop. + (** * Structure with just a base type [t] *) Module Type Typ. - Parameter Inline t : Type. + Parameter Inline(10) t : Type. End Typ. (** * Structure with an equality relation [eq] *) Module Type HasEq (Import T:Typ). - Parameter Inline eq : t -> t -> Prop. + Parameter Inline(30) eq : t -> t -> Prop. End HasEq. Module Type Eq := Typ <+ HasEq. @@ -61,10 +66,19 @@ End HasEqDec. (** Having [eq_dec] is the same as having a boolean equality plus a correctness proof. *) -Module Type HasEqBool (Import E:Eq'). +Module Type HasEqb (Import T:Typ). Parameter Inline eqb : t -> t -> bool. - Parameter eqb_eq : forall x y, eqb x y = true <-> x==y. -End HasEqBool. +End HasEqb. + +Module Type EqbSpec (T:Typ)(X:HasEq T)(Y:HasEqb T). + Parameter eqb_eq : forall x y, Y.eqb x y = true <-> X.eq x y. +End EqbSpec. + +Module Type EqbNotation (T:Typ)(E:HasEqb T). + Infix "=?" := E.eqb (at level 70, no associativity). +End EqbNotation. + +Module Type HasEqBool (E:Eq) := HasEqb E <+ EqbSpec E E. (** From these basic blocks, we can build many combinations of static standalone module types. *) @@ -102,8 +116,10 @@ Module Type EqualityTypeBoth' := EqualityTypeBoth <+ EqNotation. Module Type DecidableType' := DecidableType <+ EqNotation. Module Type DecidableTypeOrig' := DecidableTypeOrig <+ EqNotation. Module Type DecidableTypeBoth' := DecidableTypeBoth <+ EqNotation. -Module Type BooleanEqualityType' := BooleanEqualityType <+ EqNotation. -Module Type BooleanDecidableType' := BooleanDecidableType <+ EqNotation. +Module Type BooleanEqualityType' := + BooleanEqualityType <+ EqNotation <+ EqbNotation. +Module Type BooleanDecidableType' := + BooleanDecidableType <+ EqNotation <+ EqbNotation. Module Type DecidableTypeFull' := DecidableTypeFull <+ EqNotation. (** * Compatibility wrapper from/to the old version of @@ -162,6 +178,49 @@ Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType := E <+ HasEqBool2Dec. +(** Some properties of boolean equality *) + +Module BoolEqualityFacts (Import E : BooleanEqualityType'). + +(** [eqb] is compatible with [eq] *) + +Instance eqb_compat : Proper (E.eq ==> E.eq ==> Logic.eq) eqb. +Proof. +intros x x' Exx' y y' Eyy'. +apply eq_true_iff_eq. +now rewrite 2 eqb_eq, Exx', Eyy'. +Qed. + +(** Alternative specification of [eqb] based on [reflect]. *) + +Lemma eqb_spec x y : reflect (x==y) (x =? y). +Proof. +apply iff_reflect. symmetry. apply eqb_eq. +Defined. + +(** Negated form of [eqb_eq] *) + +Lemma eqb_neq x y : (x =? y) = false <-> x ~= y. +Proof. +now rewrite <- not_true_iff_false, eqb_eq. +Qed. + +(** Basic equality laws for [eqb] *) + +Lemma eqb_refl x : (x =? x) = true. +Proof. +now apply eqb_eq. +Qed. + +Lemma eqb_sym x y : (x =? y) = (y =? x). +Proof. +apply eq_true_iff_eq. now rewrite 2 eqb_eq. +Qed. + +(** Transitivity is a particular case of [eqb_compat] *) + +End BoolEqualityFacts. + (** * UsualDecidableType diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v index d9b1d76f..c69885b4 100644 --- a/theories/Structures/EqualitiesFacts.v +++ b/theories/Structures/EqualitiesFacts.v @@ -8,21 +8,8 @@ Require Import Equalities Bool SetoidList RelationPairs. -(** In a BooleanEqualityType, [eqb] is compatible with [eq] *) - -Module BoolEqualityFacts (Import E : BooleanEqualityType). - -Instance eqb_compat : Proper (E.eq ==> E.eq ==> Logic.eq) eqb. -Proof. -intros x x' Exx' y y' Eyy'. -apply eq_true_iff_eq. -rewrite 2 eqb_eq, Exx', Eyy'; auto with *. -Qed. - -End BoolEqualityFacts. - - (** * Keys and datas used in FMap *) + Module KeyDecidableType(Import D:DecidableType). Section Elt. @@ -42,9 +29,9 @@ Module KeyDecidableType(Import D:DecidableType). (* eqk, eqke are equalities, ltk is a strict order *) - Global Instance eqk_equiv : Equivalence eqk. + Global Instance eqk_equiv : Equivalence eqk := _. - Global Instance eqke_equiv : Equivalence eqke. + Global Instance eqke_equiv : Equivalence eqke := _. (* Additionnal facts *) @@ -156,7 +143,7 @@ Module PairDecidableType(D1 D2:DecidableType) <: DecidableType. Definition eq := (D1.eq * D2.eq)%signature. - Instance eq_equiv : Equivalence eq. + Instance eq_equiv : Equivalence eq := _. Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }. Proof. @@ -172,7 +159,7 @@ End PairDecidableType. Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType. Definition t := (D1.t * D2.t)%type. Definition eq := @eq t. - Program Instance eq_equiv : Equivalence eq. + Instance eq_equiv : Equivalence eq := _. Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }. Proof. intros (x1,x2) (y1,y2); diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index 68f20189..ffd0649a 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -40,34 +40,34 @@ Module GenericMinMax (Import O:OrderedTypeFull') <: HasMinMax O. Definition max := gmax O.compare. Definition min := gmin O.compare. - Lemma ge_not_lt : forall x y, y<=x -> x<y -> False. + Lemma ge_not_lt x y : y<=x -> x<y -> False. Proof. - intros x y H H'. + intros H H'. apply (StrictOrder_Irreflexive x). rewrite le_lteq in *; destruct H as [H|H]. transitivity y; auto. rewrite H in H'; auto. Qed. - Lemma max_l : forall x y, y<=x -> max x y == x. + Lemma max_l x y : y<=x -> max x y == x. Proof. intros. unfold max, gmax. case compare_spec; auto with relations. intros; elim (ge_not_lt x y); auto. Qed. - Lemma max_r : forall x y, x<=y -> max x y == y. + Lemma max_r x y : x<=y -> max x y == y. Proof. intros. unfold max, gmax. case compare_spec; auto with relations. intros; elim (ge_not_lt y x); auto. Qed. - Lemma min_l : forall x y, x<=y -> min x y == x. + Lemma min_l x y : x<=y -> min x y == x. Proof. intros. unfold min, gmin. case compare_spec; auto with relations. intros; elim (ge_not_lt y x); auto. Qed. - Lemma min_r : forall x y, y<=x -> min x y == y. + Lemma min_r x y : y<=x -> min x y == y. Proof. intros. unfold min, gmin. case compare_spec; auto with relations. intros; elim (ge_not_lt x y); auto. @@ -76,31 +76,30 @@ Module GenericMinMax (Import O:OrderedTypeFull') <: HasMinMax O. End GenericMinMax. -(** ** Consequences of the minimalist interface: facts about [max]. *) +(** ** Consequences of the minimalist interface: facts about [max] and [min]. *) -Module MaxLogicalProperties (Import O:TotalOrder')(Import M:HasMax O). - Module Import T := !MakeOrderTac O. +Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O). + Module Import Private_Tac := !MakeOrderTac O O. (** An alternative caracterisation of [max], equivalent to [max_l /\ max_r] *) -Lemma max_spec : forall n m, - (n < m /\ max n m == m) \/ (m <= n /\ max n m == n). +Lemma max_spec n m : + (n < m /\ max n m == m) \/ (m <= n /\ max n m == n). Proof. - intros n m. destruct (lt_total n m); [left|right]. - split; auto. apply max_r. rewrite le_lteq; auto. - assert (m <= n) by (rewrite le_lteq; intuition). - split; auto. apply max_l; auto. + - split; auto. apply max_r. rewrite le_lteq; auto. + - assert (m <= n) by (rewrite le_lteq; intuition). + split; auto. now apply max_l. Qed. (** A more symmetric version of [max_spec], based only on [le]. Beware that left and right alternatives overlap. *) -Lemma max_spec_le : forall n m, +Lemma max_spec_le n m : (n <= m /\ max n m == m) \/ (m <= n /\ max n m == n). Proof. - intros. destruct (max_spec n m); [left|right]; intuition; order. + destruct (max_spec n m); [left|right]; intuition; order. Qed. Instance : Proper (eq==>eq==>iff) le. @@ -108,25 +107,24 @@ Proof. repeat red. intuition order. Qed. Instance max_compat : Proper (eq==>eq==>eq) max. Proof. -intros x x' Hx y y' Hy. -assert (H1 := max_spec x y). assert (H2 := max_spec x' y'). -set (m := max x y) in *; set (m' := max x' y') in *; clearbody m m'. -rewrite <- Hx, <- Hy in *. -destruct (lt_total x y); intuition order. + intros x x' Hx y y' Hy. + assert (H1 := max_spec x y). assert (H2 := max_spec x' y'). + set (m := max x y) in *; set (m' := max x' y') in *; clearbody m m'. + rewrite <- Hx, <- Hy in *. + destruct (lt_total x y); intuition order. Qed. - (** A function satisfying the same specification is equal to [max]. *) -Lemma max_unicity : forall n m p, - ((n < m /\ p == m) \/ (m <= n /\ p == n)) -> p == max n m. +Lemma max_unicity n m p : + ((n < m /\ p == m) \/ (m <= n /\ p == n)) -> p == max n m. Proof. - intros. assert (Hm := max_spec n m). + assert (Hm := max_spec n m). destruct (lt_total n m); intuition; order. Qed. -Lemma max_unicity_ext : forall f, - (forall n m, (n < m /\ f n m == m) \/ (m <= n /\ f n m == n)) -> +Lemma max_unicity_ext f : + (forall n m, (n < m /\ f n m == m) \/ (m <= n /\ f n m == n)) -> (forall n m, f n m == max n m). Proof. intros. apply max_unicity; auto. @@ -134,12 +132,12 @@ Qed. (** [max] commutes with monotone functions. *) -Lemma max_mono: forall f, +Lemma max_mono f : (Proper (eq ==> eq) f) -> (Proper (le ==> le) f) -> forall x y, max (f x) (f y) == f (max x y). Proof. - intros f Eqf Lef x y. + 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. @@ -148,237 +146,232 @@ Qed. (** *** Semi-lattice algebraic properties of [max] *) -Lemma max_id : forall n, max n n == n. +Lemma max_id n : max n n == n. Proof. - intros. destruct (max_spec n n); intuition. + apply max_l; order. Qed. Notation max_idempotent := max_id (only parsing). -Lemma max_assoc : forall m n p, max m (max n p) == max (max m n) p. +Lemma max_assoc m n p : max m (max n p) == max (max m n) p. Proof. - intros. - destruct (max_spec n p) as [(H,Eq)|(H,Eq)]; rewrite Eq. - destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'. - destruct (max_spec m p); intuition; order. order. - destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'. order. - destruct (max_spec m p); intuition; order. + destruct (max_spec n p) as [(H,E)|(H,E)]; rewrite E; + destruct (max_spec m n) as [(H',E')|(H',E')]; rewrite E', ?E; try easy. + - apply max_r; order. + - symmetry. apply max_l; order. Qed. -Lemma max_comm : forall n m, max n m == max m n. +Lemma max_comm n m : max n m == max m n. Proof. - intros. - destruct (max_spec n m) as [(H,Eq)|(H,Eq)]; rewrite Eq. - destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order. - destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order. + destruct (max_spec m n) as [(H,E)|(H,E)]; rewrite E; + (apply max_r || apply max_l); order. Qed. +Ltac solve_max := + match goal with |- context [max ?n ?m] => + destruct (max_spec n m); intuition; order + end. + (** *** Least-upper bound properties of [max] *) -Lemma le_max_l : forall n m, n <= max n m. -Proof. - intros; destruct (max_spec n m); intuition; order. -Qed. +Lemma le_max_l n m : n <= max n m. +Proof. solve_max. Qed. -Lemma le_max_r : forall n m, m <= max n m. -Proof. - intros; destruct (max_spec n m); intuition; order. -Qed. +Lemma le_max_r n m : m <= max n m. +Proof. solve_max. Qed. -Lemma max_l_iff : forall n m, max n m == n <-> m <= n. -Proof. - split. intro H; rewrite <- H. apply le_max_r. apply max_l. -Qed. +Lemma max_l_iff n m : max n m == n <-> m <= n. +Proof. solve_max. Qed. -Lemma max_r_iff : forall n m, max n m == m <-> n <= m. -Proof. - split. intro H; rewrite <- H. apply le_max_l. apply max_r. -Qed. +Lemma max_r_iff n m : max n m == m <-> n <= m. +Proof. solve_max. Qed. -Lemma max_le : forall n m p, p <= max n m -> p <= n \/ p <= m. +Lemma max_le n m p : p <= max n m -> p <= n \/ p <= m. Proof. - intros n m p H; destruct (max_spec n m); - [right|left]; intuition; order. + destruct (max_spec n m); [right|left]; intuition; order. Qed. -Lemma max_le_iff : forall n m p, p <= max n m <-> p <= n \/ p <= m. -Proof. - intros. split. apply max_le. - destruct (max_spec n m); intuition; order. -Qed. +Lemma max_le_iff n m p : p <= max n m <-> p <= n \/ p <= m. +Proof. split. apply max_le. solve_max. Qed. -Lemma max_lt_iff : forall n m p, p < max n m <-> p < n \/ p < m. +Lemma max_lt_iff n m p : p < max n m <-> p < n \/ p < m. Proof. - intros. destruct (max_spec n m); intuition; + destruct (max_spec n m); intuition; order || (right; order) || (left; order). Qed. -Lemma max_lub_l : forall n m p, max n m <= p -> n <= p. -Proof. - intros; destruct (max_spec n m); intuition; order. -Qed. +Lemma max_lub_l n m p : max n m <= p -> n <= p. +Proof. solve_max. Qed. -Lemma max_lub_r : forall n m p, max n m <= p -> m <= p. -Proof. - intros; destruct (max_spec n m); intuition; order. -Qed. +Lemma max_lub_r n m p : max n m <= p -> m <= p. +Proof. solve_max. Qed. -Lemma max_lub : forall n m p, n <= p -> m <= p -> max n m <= p. -Proof. - intros; destruct (max_spec n m); intuition; order. -Qed. +Lemma max_lub n m p : n <= p -> m <= p -> max n m <= p. +Proof. solve_max. Qed. -Lemma max_lub_iff : forall n m p, max n m <= p <-> n <= p /\ m <= p. -Proof. - intros; destruct (max_spec n m); intuition; order. -Qed. +Lemma max_lub_iff n m p : max n m <= p <-> n <= p /\ m <= p. +Proof. solve_max. Qed. -Lemma max_lub_lt : forall n m p, n < p -> m < p -> max n m < p. -Proof. - intros; destruct (max_spec n m); intuition; order. -Qed. +Lemma max_lub_lt n m p : n < p -> m < p -> max n m < p. +Proof. solve_max. Qed. -Lemma max_lub_lt_iff : forall n m p, max n m < p <-> n < p /\ m < p. -Proof. - intros; destruct (max_spec n m); intuition; order. -Qed. +Lemma max_lub_lt_iff n m p : max n m < p <-> n < p /\ m < p. +Proof. solve_max. Qed. -Lemma max_le_compat_l : forall n m p, n <= m -> max p n <= max p m. -Proof. - intros. - destruct (max_spec p n) as [(LT,E)|(LE,E)]; rewrite E. - assert (LE' := le_max_r p m). order. - apply le_max_l. -Qed. +Lemma max_le_compat_l n m p : n <= m -> max p n <= max p m. +Proof. intros. apply max_lub_iff. solve_max. Qed. -Lemma max_le_compat_r : forall n m p, n <= m -> max n p <= max m p. -Proof. - intros. rewrite (max_comm n p), (max_comm m p). - auto using max_le_compat_l. -Qed. +Lemma max_le_compat_r n m p : n <= m -> max n p <= max m p. +Proof. intros. apply max_lub_iff. solve_max. Qed. -Lemma max_le_compat : forall n m p q, n <= m -> p <= q -> - max n p <= max m q. +Lemma max_le_compat n m p q : n <= m -> p <= q -> max n p <= max m q. Proof. - intros n m p q Hnm Hpq. + intros Hnm Hpq. assert (LE := max_le_compat_l _ _ m Hpq). assert (LE' := max_le_compat_r _ _ p Hnm). order. Qed. -End MaxLogicalProperties. - - -(** ** Properties concernant [min], then both [min] and [max]. +(** Properties of [min] *) - To avoid too much code duplication, we exploit that [min] can be - seen as a [max] of the reversed order. -*) - -Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O). - Include MaxLogicalProperties O M. - Import T. +Lemma min_spec n m : + (n < m /\ min n m == n) \/ (m <= n /\ min n m == m). +Proof. + destruct (lt_total n m); [left|right]. + - split; auto. apply min_l. rewrite le_lteq; auto. + - assert (m <= n) by (rewrite le_lteq; intuition). + split; auto. now apply min_r. +Qed. - Module ORev := TotalOrderRev O. - Module MRev <: HasMax ORev. - Definition max x y := M.min y x. - Definition max_l x y := M.min_r y x. - Definition max_r x y := M.min_l y x. - End MRev. - Module MPRev := MaxLogicalProperties ORev MRev. +Lemma min_spec_le n m : + (n <= m /\ min n m == n) \/ (m <= n /\ min n m == m). +Proof. + destruct (min_spec n m); [left|right]; intuition; order. +Qed. Instance min_compat : Proper (eq==>eq==>eq) min. -Proof. intros x x' Hx y y' Hy. apply MPRev.max_compat; assumption. Qed. +Proof. +intros x x' Hx y y' Hy. +assert (H1 := min_spec x y). assert (H2 := min_spec x' y'). +set (m := min x y) in *; set (m' := min x' y') in *; clearbody m m'. +rewrite <- Hx, <- Hy in *. +destruct (lt_total x y); intuition order. +Qed. -Lemma min_spec : forall n m, - (n < m /\ min n m == n) \/ (m <= n /\ min n m == m). -Proof. intros. exact (MPRev.max_spec m n). Qed. +Lemma min_unicity n m p : + ((n < m /\ p == n) \/ (m <= n /\ p == m)) -> p == min n m. +Proof. + assert (Hm := min_spec n m). + destruct (lt_total n m); intuition; order. +Qed. -Lemma min_spec_le : forall n m, - (n <= m /\ min n m == n) \/ (m <= n /\ min n m == m). -Proof. intros. exact (MPRev.max_spec_le m n). Qed. +Lemma min_unicity_ext f : + (forall n m, (n < m /\ f n m == n) \/ (m <= n /\ f n m == m)) -> + (forall n m, f n m == min n m). +Proof. + intros. apply min_unicity; auto. +Qed. -Lemma min_mono: forall f, +Lemma min_mono f : (Proper (eq ==> eq) f) -> (Proper (le ==> le) f) -> forall x y, min (f x) (f y) == f (min x y). Proof. - intros. apply MPRev.max_mono; auto. compute in *; eauto. + 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. Qed. -Lemma min_unicity : forall n m p, - ((n < m /\ p == n) \/ (m <= n /\ p == m)) -> p == min n m. -Proof. intros n m p. apply MPRev.max_unicity. Qed. - -Lemma min_unicity_ext : forall f, - (forall n m, (n < m /\ f n m == n) \/ (m <= n /\ f n m == m)) -> - (forall n m, f n m == min n m). -Proof. intros f H n m. apply MPRev.max_unicity, H; auto. Qed. - -Lemma min_id : forall n, min n n == n. -Proof. intros. exact (MPRev.max_id n). Qed. +Lemma min_id n : min n n == n. +Proof. + apply min_l; order. +Qed. Notation min_idempotent := min_id (only parsing). -Lemma min_assoc : forall m n p, min m (min n p) == min (min m n) p. -Proof. intros. symmetry; apply MPRev.max_assoc. Qed. +Lemma min_assoc m n p : min m (min n p) == min (min m n) p. +Proof. + destruct (min_spec n p) as [(H,E)|(H,E)]; rewrite E; + destruct (min_spec m n) as [(H',E')|(H',E')]; rewrite E', ?E; try easy. + - symmetry. apply min_l; order. + - apply min_r; order. +Qed. -Lemma min_comm : forall n m, min n m == min m n. -Proof. intros. exact (MPRev.max_comm m n). Qed. +Lemma min_comm n m : min n m == min m n. +Proof. + destruct (min_spec m n) as [(H,E)|(H,E)]; rewrite E; + (apply min_r || apply min_l); order. +Qed. -Lemma le_min_r : forall n m, min n m <= m. -Proof. intros. exact (MPRev.le_max_l m n). Qed. +Ltac solve_min := + match goal with |- context [min ?n ?m] => + destruct (min_spec n m); intuition; order + end. -Lemma le_min_l : forall n m, min n m <= n. -Proof. intros. exact (MPRev.le_max_r m n). Qed. +Lemma le_min_r n m : min n m <= m. +Proof. solve_min. Qed. -Lemma min_l_iff : forall n m, min n m == n <-> n <= m. -Proof. intros n m. exact (MPRev.max_r_iff m n). Qed. +Lemma le_min_l n m : min n m <= n. +Proof. solve_min. Qed. -Lemma min_r_iff : forall n m, min n m == m <-> m <= n. -Proof. intros n m. exact (MPRev.max_l_iff m n). Qed. +Lemma min_l_iff n m : min n m == n <-> n <= m. +Proof. solve_min. Qed. -Lemma min_le : forall n m p, min n m <= p -> n <= p \/ m <= p. -Proof. intros n m p H. destruct (MPRev.max_le _ _ _ H); auto. Qed. +Lemma min_r_iff n m : min n m == m <-> m <= n. +Proof. solve_min. Qed. -Lemma min_le_iff : forall n m p, min n m <= p <-> n <= p \/ m <= p. -Proof. intros n m p. rewrite (MPRev.max_le_iff m n p); intuition. Qed. +Lemma min_le n m p : min n m <= p -> n <= p \/ m <= p. +Proof. + destruct (min_spec n m); [left|right]; intuition; order. +Qed. + +Lemma min_le_iff n m p : min n m <= p <-> n <= p \/ m <= p. +Proof. split. apply min_le. solve_min. Qed. -Lemma min_lt_iff : forall n m p, min n m < p <-> n < p \/ m < p. -Proof. intros n m p. rewrite (MPRev.max_lt_iff m n p); intuition. Qed. +Lemma min_lt_iff n m p : min n m < p <-> n < p \/ m < p. +Proof. + destruct (min_spec n m); intuition; + order || (right; order) || (left; order). +Qed. -Lemma min_glb_l : forall n m p, p <= min n m -> p <= n. -Proof. intros n m. exact (MPRev.max_lub_r m n). Qed. +Lemma min_glb_l n m p : p <= min n m -> p <= n. +Proof. solve_min. Qed. -Lemma min_glb_r : forall n m p, p <= min n m -> p <= m. -Proof. intros n m. exact (MPRev.max_lub_l m n). Qed. +Lemma min_glb_r n m p : p <= min n m -> p <= m. +Proof. solve_min. Qed. -Lemma min_glb : forall n m p, p <= n -> p <= m -> p <= min n m. -Proof. intros. apply MPRev.max_lub; auto. Qed. +Lemma min_glb n m p : p <= n -> p <= m -> p <= min n m. +Proof. solve_min. Qed. -Lemma min_glb_iff : forall n m p, p <= min n m <-> p <= n /\ p <= m. -Proof. intros. rewrite (MPRev.max_lub_iff m n p); intuition. Qed. +Lemma min_glb_iff n m p : p <= min n m <-> p <= n /\ p <= m. +Proof. solve_min. Qed. -Lemma min_glb_lt : forall n m p, p < n -> p < m -> p < min n m. -Proof. intros. apply MPRev.max_lub_lt; auto. Qed. +Lemma min_glb_lt n m p : p < n -> p < m -> p < min n m. +Proof. solve_min. Qed. -Lemma min_glb_lt_iff : forall n m p, p < min n m <-> p < n /\ p < m. -Proof. intros. rewrite (MPRev.max_lub_lt_iff m n p); intuition. Qed. +Lemma min_glb_lt_iff n m p : p < min n m <-> p < n /\ p < m. +Proof. solve_min. Qed. -Lemma min_le_compat_l : forall n m p, n <= m -> min p n <= min p m. -Proof. intros n m. exact (MPRev.max_le_compat_r m n). Qed. +Lemma min_le_compat_l n m p : n <= m -> min p n <= min p m. +Proof. intros. apply min_glb_iff. solve_min. Qed. -Lemma min_le_compat_r : forall n m p, n <= m -> min n p <= min m p. -Proof. intros n m. exact (MPRev.max_le_compat_l m n). Qed. +Lemma min_le_compat_r n m p : n <= m -> min n p <= min m p. +Proof. intros. apply min_glb_iff. solve_min. Qed. -Lemma min_le_compat : forall n m p q, n <= m -> p <= q -> +Lemma min_le_compat n m p q : n <= m -> p <= q -> min n p <= min m q. -Proof. intros. apply MPRev.max_le_compat; auto. Qed. - +Proof. + intros Hnm Hpq. + assert (LE := min_le_compat_l _ _ m Hpq). + assert (LE' := min_le_compat_r _ _ p Hnm). + order. +Qed. (** *** Combined properties of min and max *) -Lemma min_max_absorption : forall n m, max n (min n m) == n. +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. @@ -386,7 +379,7 @@ Proof. destruct (max_spec n m); intuition; order. Qed. -Lemma max_min_absorption : forall n m, min n (max n m) == n. +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. @@ -396,35 +389,35 @@ Qed. (** Distributivity *) -Lemma max_min_distr : forall n m p, +Lemma max_min_distr n m p : max n (min m p) == min (max n m) (max n p). Proof. - intros. symmetry. apply min_mono. + symmetry. apply min_mono. eauto with *. repeat red; intros. apply max_le_compat_l; auto. Qed. -Lemma min_max_distr : forall n m p, +Lemma min_max_distr n m p : min n (max m p) == max (min n m) (min n p). Proof. - intros. symmetry. apply max_mono. + symmetry. apply max_mono. eauto with *. repeat red; intros. apply min_le_compat_l; auto. Qed. (** Modularity *) -Lemma max_min_modular : forall n m p, +Lemma max_min_modular n m p : max n (min m (max n p)) == min (max n m) (max n p). Proof. - intros. rewrite <- max_min_distr. + 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. Qed. -Lemma min_max_modular : forall n m p, +Lemma min_max_modular n m p : min n (max m (min n p)) == max (min n m) (min n p). Proof. intros. rewrite <- min_max_distr. @@ -436,7 +429,7 @@ Qed. (** Disassociativity *) -Lemma max_min_disassoc : forall n m p, +Lemma max_min_disassoc n m p : min n (max m p) <= max (min n m) p. Proof. intros. rewrite min_max_distr. @@ -445,24 +438,24 @@ Qed. (** Anti-monotonicity swaps the role of [min] and [max] *) -Lemma max_min_antimono : forall f, +Lemma max_min_antimono f : Proper (eq==>eq) f -> Proper (le==>inverse le) f -> forall x y, max (f x) (f y) == f (min x y). Proof. - intros f Eqf Lef x y. + 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. Qed. -Lemma min_max_antimono : forall f, +Lemma min_max_antimono f : Proper (eq==>eq) f -> Proper (le==>inverse le) f -> forall x y, min (f x) (f y) == f (max x y). Proof. - intros f Eqf Lef x y. + 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. @@ -478,11 +471,11 @@ Module MinMaxDecProperties (Import O:OrderedTypeFull')(Import M:HasMinMax O). (** Induction principles for [max]. *) -Lemma max_case_strong : forall n m (P:t -> Type), +Lemma max_case_strong n m (P:t -> Type) : (forall x y, x==y -> P x -> P y) -> (m<=n -> P n) -> (n<=m -> P m) -> P (max n m). Proof. -intros n m P Compat Hl Hr. +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. @@ -492,26 +485,26 @@ assert (m<=n) by (rewrite le_lteq; auto). apply (Compat n), Hl; auto. symmetry; apply max_l; auto. Defined. -Lemma max_case : forall n m (P:t -> Type), +Lemma max_case n m (P:t -> Type) : (forall x y, x == y -> P x -> P y) -> P n -> P m -> P (max n m). Proof. intros. apply max_case_strong; auto. Defined. (** [max] returns one of its arguments. *) -Lemma max_dec : forall n m, {max n m == n} + {max n m == m}. +Lemma max_dec n m : {max n m == n} + {max n m == m}. Proof. - intros n m. apply max_case; auto with relations. + apply max_case; auto with relations. intros x y H [E|E]; [left|right]; rewrite <-H; auto. Defined. (** Idem for [min] *) -Lemma min_case_strong : forall n m (P:O.t -> Type), +Lemma min_case_strong n m (P:O.t -> Type) : (forall x y, x == y -> P x -> P y) -> (n<=m -> P n) -> (m<=n -> P m) -> P (min n m). Proof. -intros n m P Compat Hl Hr. +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. @@ -521,12 +514,12 @@ assert (m<=n) by (rewrite le_lteq; auto). apply (Compat m), Hr; auto. symmetry; apply min_r; auto. Defined. -Lemma min_case : forall n m (P:O.t -> Type), +Lemma min_case n m (P:O.t -> Type) : (forall x y, x == y -> P x -> P y) -> P n -> P m -> P (min n m). Proof. intros. apply min_case_strong; auto. Defined. -Lemma min_dec : forall n m, {min n m == n} + {min n m == m}. +Lemma min_dec n m : {min n m == n} + {min n m == m}. Proof. intros. apply min_case; auto with relations. intros x y H [E|E]; [left|right]; rewrite <- E; auto with relations. @@ -556,19 +549,19 @@ Module UsualMinMaxLogicalProperties Include MinMaxLogicalProperties O M. - Lemma max_monotone : forall f, Proper (le ==> le) f -> + Lemma max_monotone f : Proper (le ==> le) f -> forall x y, max (f x) (f y) = f (max x y). Proof. intros; apply max_mono; auto. congruence. Qed. - Lemma min_monotone : forall f, Proper (le ==> le) f -> + Lemma min_monotone f : Proper (le ==> le) f -> forall x y, min (f x) (f y) = f (min x y). Proof. intros; apply min_mono; auto. congruence. Qed. - Lemma min_max_antimonotone : forall f, Proper (le ==> inverse le) f -> + Lemma min_max_antimonotone f : Proper (le ==> inverse le) f -> forall x y, min (f x) (f y) = f (max x y). Proof. intros; apply min_max_antimono; auto. congruence. Qed. - Lemma max_min_antimonotone : forall f, Proper (le ==> inverse le) f -> + Lemma max_min_antimonotone f : Proper (le ==> inverse le) f -> forall x y, max (f x) (f y) = f (min x y). Proof. intros; apply max_min_antimono; auto. congruence. Qed. @@ -578,29 +571,29 @@ End UsualMinMaxLogicalProperties. Module UsualMinMaxDecProperties (Import O:UsualOrderedTypeFull')(Import M:HasMinMax O). - Module P := MinMaxDecProperties O M. + Module Import Private_Dec := MinMaxDecProperties O M. Lemma max_case_strong : forall n m (P:t -> Type), (m<=n -> P n) -> (n<=m -> P m) -> P (max n m). - Proof. intros; apply P.max_case_strong; auto. congruence. Defined. + Proof. intros; apply max_case_strong; auto. congruence. Defined. Lemma max_case : forall n m (P:t -> Type), P n -> P m -> P (max n m). Proof. intros; apply max_case_strong; auto. Defined. Lemma max_dec : forall n m, {max n m = n} + {max n m = m}. - Proof. exact P.max_dec. Defined. + Proof. exact max_dec. Defined. Lemma min_case_strong : forall n m (P:O.t -> Type), (n<=m -> P n) -> (m<=n -> P m) -> P (min n m). - Proof. intros; apply P.min_case_strong; auto. congruence. Defined. + Proof. intros; apply min_case_strong; auto. congruence. Defined. Lemma min_case : forall n m (P:O.t -> Type), P n -> P m -> P (min n m). Proof. intros. apply min_case_strong; auto. Defined. Lemma min_dec : forall n m, {min n m = n} + {min n m = m}. - Proof. exact P.min_dec. Defined. + Proof. exact min_dec. Defined. End UsualMinMaxDecProperties. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index 57f491d2..75578195 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: OrderedType.v 12732 2010-02-10 22:46:59Z letouzey $ *) - Require Export SetoidList Morphisms OrdersTac. Set Implicit Arguments. Unset Strict Implicit. @@ -22,6 +20,10 @@ Inductive Compare (X : Type) (lt eq : X -> X -> Prop) (x y : X) : Type := | EQ : eq x y -> Compare lt eq x y | GT : lt y x -> Compare lt eq x y. +Arguments LT [X lt eq x y] _. +Arguments EQ [X lt eq x y] _. +Arguments GT [X lt eq x y] _. + Module Type MiniOrderedType. Parameter Inline t : Type. @@ -106,19 +108,21 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma lt_total : forall x y, lt x y \/ eq x y \/ lt y x. Proof. intros; destruct (compare x y); auto. Qed. - Module OrderElts <: Orders.TotalOrder. - Definition t := t. - Definition eq := eq. - Definition lt := lt. - Definition le x y := lt x y \/ eq x y. - Definition eq_equiv := eq_equiv. - Definition lt_strorder := lt_strorder. - Definition lt_compat := lt_compat. - Definition lt_total := lt_total. - Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y. - Proof. unfold le; intuition. Qed. - End OrderElts. - Module OrderTac := !MakeOrderTac OrderElts. + Module TO. + Definition t := t. + Definition eq := eq. + Definition lt := lt. + Definition le x y := lt x y \/ eq x y. + End TO. + Module IsTO. + Definition eq_equiv := eq_equiv. + Definition lt_strorder := lt_strorder. + Definition lt_compat := lt_compat. + Definition lt_total := lt_total. + Lemma le_lteq x y : TO.le x y <-> lt x y \/ eq x y. + Proof. reflexivity. Qed. + End IsTO. + Module OrderTac := !MakeOrderTac TO IsTO. Ltac order := OrderTac.order. Lemma le_eq x y z : ~lt x y -> eq y z -> ~lt x z. Proof. order. Qed. @@ -143,7 +147,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma elim_compare_eq : forall x y : t, - eq x y -> exists H : eq x y, compare x y = EQ _ H. + eq x y -> exists H : eq x y, compare x y = EQ H. Proof. intros; case (compare x y); intros H'; try (exfalso; order). exists H'; auto. @@ -151,7 +155,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma elim_compare_lt : forall x y : t, - lt x y -> exists H : lt x y, compare x y = LT _ H. + lt x y -> exists H : lt x y, compare x y = LT H. Proof. intros; case (compare x y); intros H'; try (exfalso; order). exists H'; auto. @@ -159,7 +163,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma elim_compare_gt : forall x y : t, - lt y x -> exists H : lt y x, compare x y = GT _ H. + lt y x -> exists H : lt y x, compare x y = GT H. Proof. intros; case (compare x y); intros H'; try (exfalso; order). exists H'; auto. @@ -318,16 +322,13 @@ Module KeyOrderedType(O:OrderedType). Hint Immediate eqk_sym eqke_sym. Global Instance eqk_equiv : Equivalence eqk. - Proof. split; eauto. Qed. + Proof. constructor; eauto. Qed. Global Instance eqke_equiv : Equivalence eqke. Proof. split; eauto. Qed. Global Instance ltk_strorder : StrictOrder ltk. - Proof. - split; eauto. - intros (x,e); compute; apply (StrictOrder_Irreflexive x). - Qed. + Proof. constructor; eauto. intros x; apply (irreflexivity (x:=fst x)). Qed. Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk. Proof. diff --git a/theories/Structures/OrderedTypeAlt.v b/theories/Structures/OrderedTypeAlt.v index f6c1532b..b054496e 100644 --- a/theories/Structures/OrderedTypeAlt.v +++ b/theories/Structures/OrderedTypeAlt.v @@ -5,8 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: OrderedTypeAlt.v 12384 2009-10-13 14:39:51Z letouzey $ *) - Require Import OrderedType. (** * An alternative (but equivalent) presentation for an Ordered Type diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v index 128cd576..83130deb 100644 --- a/theories/Structures/OrderedTypeEx.v +++ b/theories/Structures/OrderedTypeEx.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: OrderedTypeEx.v 13297 2010-07-19 23:32:42Z letouzey $ *) - Require Import OrderedType. Require Import ZArith. Require Import Omega. @@ -23,9 +21,9 @@ Module Type UsualOrderedType. Parameter Inline t : Type. Definition eq := @eq t. Parameter Inline lt : t -> t -> Prop. - Definition eq_refl := @refl_equal t. - Definition eq_sym := @sym_eq t. - Definition eq_trans := @trans_eq t. + Definition eq_refl := @eq_refl t. + Definition eq_sym := @eq_sym t. + Definition eq_trans := @eq_trans t. Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y. Parameter compare : forall x y : t, Compare lt eq x y. @@ -43,9 +41,9 @@ Module Nat_as_OT <: UsualOrderedType. Definition t := nat. Definition eq := @eq nat. - Definition eq_refl := @refl_equal t. - Definition eq_sym := @sym_eq t. - Definition eq_trans := @trans_eq t. + Definition eq_refl := @eq_refl t. + Definition eq_sym := @eq_sym t. + Definition eq_trans := @eq_trans t. Definition lt := lt. @@ -55,12 +53,12 @@ Module Nat_as_OT <: UsualOrderedType. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. Proof. unfold lt, eq; intros; omega. Qed. - Definition compare : forall x y : t, Compare lt eq x y. + Definition compare x y : Compare lt eq x y. Proof. - intros x y; destruct (nat_compare x y) as [ | | ]_eqn. - apply EQ. apply nat_compare_eq; assumption. - apply LT. apply nat_compare_Lt_lt; assumption. - apply GT. apply nat_compare_Gt_gt; assumption. + case_eq (nat_compare x y); intro. + - apply EQ. now apply nat_compare_eq. + - apply LT. now apply nat_compare_Lt_lt. + - apply GT. now apply nat_compare_Gt_gt. Defined. Definition eq_dec := eq_nat_dec. @@ -70,15 +68,15 @@ End Nat_as_OT. (** [Z] is an ordered type with respect to the usual order on integers. *) -Open Local Scope Z_scope. +Local Open Scope Z_scope. Module Z_as_OT <: UsualOrderedType. Definition t := Z. Definition eq := @eq Z. - Definition eq_refl := @refl_equal t. - Definition eq_sym := @sym_eq t. - Definition eq_trans := @trans_eq t. + Definition eq_refl := @eq_refl t. + Definition eq_sym := @eq_sym t. + Definition eq_trans := @eq_trans t. Definition lt (x y:Z) := (x<y). @@ -88,89 +86,73 @@ Module Z_as_OT <: UsualOrderedType. Lemma lt_not_eq : forall x y, x<y -> ~ x=y. Proof. intros; omega. Qed. - Definition compare : forall x y, Compare lt eq x y. + Definition compare x y : Compare lt eq x y. Proof. - intros x y; destruct (x ?= y) as [ | | ]_eqn. - apply EQ; apply Zcompare_Eq_eq; assumption. - apply LT; assumption. - apply GT; apply Zgt_lt; assumption. + case_eq (x ?= y); intro. + - apply EQ. now apply Z.compare_eq. + - apply LT. assumption. + - apply GT. now apply Z.gt_lt. Defined. - Definition eq_dec := Z_eq_dec. + Definition eq_dec := Z.eq_dec. End Z_as_OT. (** [positive] is an ordered type with respect to the usual order on natural numbers. *) -Open Local Scope positive_scope. +Local Open Scope positive_scope. Module Positive_as_OT <: UsualOrderedType. Definition t:=positive. Definition eq:=@eq positive. - Definition eq_refl := @refl_equal t. - Definition eq_sym := @sym_eq t. - Definition eq_trans := @trans_eq t. + Definition eq_refl := @eq_refl t. + Definition eq_sym := @eq_sym t. + Definition eq_trans := @eq_trans t. - Definition lt p q:= (p ?= q) Eq = Lt. + Definition lt := Pos.lt. - Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. - Proof. - unfold lt; intros x y z. - change ((Zpos x < Zpos y)%Z -> (Zpos y < Zpos z)%Z -> (Zpos x < Zpos z)%Z). - omega. - Qed. + Definition lt_trans := Pos.lt_trans. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. Proof. - intros; intro. - rewrite H0 in H. - unfold lt in H. - rewrite Pcompare_refl in H; discriminate. + intros x y H. contradict H. rewrite H. apply Pos.lt_irrefl. Qed. - Definition compare : forall x y : t, Compare lt eq x y. + Definition compare x y : Compare lt eq x y. Proof. - intros x y. destruct ((x ?= y) Eq) as [ | | ]_eqn. - apply EQ; apply Pcompare_Eq_eq; assumption. - apply LT; assumption. - apply GT; apply ZC1; assumption. + case_eq (x ?= y); intros H. + - apply EQ. now apply Pos.compare_eq. + - apply LT; assumption. + - apply GT. now apply Pos.gt_lt. Defined. - Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }. - Proof. - intros; unfold eq; decide equality. - Defined. + Definition eq_dec := Pos.eq_dec. End Positive_as_OT. (** [N] is an ordered type with respect to the usual order on natural numbers. *) -Open Local Scope positive_scope. - Module N_as_OT <: UsualOrderedType. Definition t:=N. Definition eq:=@eq N. - Definition eq_refl := @refl_equal t. - Definition eq_sym := @sym_eq t. - Definition eq_trans := @trans_eq t. + Definition eq_refl := @eq_refl t. + Definition eq_sym := @eq_sym t. + Definition eq_trans := @eq_trans t. - Definition lt:=Nlt. - Definition lt_trans := Nlt_trans. - Definition lt_not_eq := Nlt_not_eq. + Definition lt := N.lt. + Definition lt_trans := N.lt_trans. + Definition lt_not_eq := N.lt_neq. - Definition compare : forall x y : t, Compare lt eq x y. + Definition compare x y : Compare lt eq x y. Proof. - intros x y. destruct (x ?= y)%N as [ | | ]_eqn. - apply EQ; apply Ncompare_Eq_eq; assumption. - apply LT; assumption. - apply GT. apply Ngt_Nlt; assumption. + case_eq (x ?= y)%N; intro. + - apply EQ. now apply N.compare_eq. + - apply LT. assumption. + - apply GT. now apply N.gt_lt. Defined. - Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }. - Proof. - intros. unfold eq. decide equality. apply Positive_as_OT.eq_dec. - Defined. + Definition eq_dec := N.eq_dec. End N_as_OT. @@ -250,9 +232,9 @@ End PairOrderedType. Module PositiveOrderedTypeBits <: UsualOrderedType. Definition t:=positive. Definition eq:=@eq positive. - Definition eq_refl := @refl_equal t. - Definition eq_sym := @sym_eq t. - Definition eq_trans := @trans_eq t. + Definition eq_refl := @eq_refl t. + Definition eq_sym := @eq_sym t. + Definition eq_trans := @eq_trans t. Fixpoint bits_lt (p q:positive) : Prop := match p, q with @@ -296,38 +278,38 @@ Module PositiveOrderedTypeBits <: UsualOrderedType. Definition compare : forall x y : t, Compare lt eq x y. Proof. induction x; destruct y. - (* I I *) - destruct (IHx y). - apply LT; auto. - apply EQ; rewrite e; red; auto. - apply GT; auto. - (* I O *) - apply GT; simpl; auto. - (* I H *) - apply GT; simpl; auto. - (* O I *) - apply LT; simpl; auto. - (* O O *) - destruct (IHx y). - apply LT; auto. - apply EQ; rewrite e; red; auto. - apply GT; auto. - (* O H *) - apply LT; simpl; auto. - (* H I *) - apply LT; simpl; auto. - (* H O *) - apply GT; simpl; auto. - (* H H *) - apply EQ; red; auto. + - (* I I *) + destruct (IHx y). + apply LT; auto. + apply EQ; rewrite e; red; auto. + apply GT; auto. + - (* I O *) + apply GT; simpl; auto. + - (* I H *) + apply GT; simpl; auto. + - (* O I *) + apply LT; simpl; auto. + - (* O O *) + destruct (IHx y). + apply LT; auto. + apply EQ; rewrite e; red; auto. + apply GT; auto. + - (* O H *) + apply LT; simpl; auto. + - (* H I *) + apply LT; simpl; auto. + - (* H O *) + apply GT; simpl; auto. + - (* H H *) + apply EQ; red; auto. Qed. Lemma eq_dec (x y: positive): {x = y} + {x <> y}. Proof. - intros. case_eq ((x ?= y) Eq); intros. - left. apply Pcompare_Eq_eq; auto. - right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate. - right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate. + intros. case_eq (x ?= y); intros. + - left. now apply Pos.compare_eq. + - right. intro. subst y. now rewrite (Pos.compare_refl x) in *. + - right. intro. subst y. now rewrite (Pos.compare_refl x) in *. Qed. End PositiveOrderedTypeBits. diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v index 5567b743..1d025439 100644 --- a/theories/Structures/Orders.v +++ b/theories/Structures/Orders.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: Orders.v 13276 2010-07-10 14:34:44Z letouzey $ *) - Require Export Relations Morphisms Setoid Equalities. Set Implicit Arguments. Unset Strict Implicit. @@ -67,20 +65,34 @@ Module Type LeIsLtEq (Import E:EqLtLe'). Axiom le_lteq : forall x y, x<=y <-> x<y \/ x==y. End LeIsLtEq. -Module Type HasCompare (Import E:EqLt). +Module Type StrOrder := EqualityType <+ HasLt <+ IsStrOrder. +Module Type StrOrder' := StrOrder <+ EqLtNotation. + +(** Versions with a decidable ternary comparison *) + +Module Type HasCmp (Import T:Typ). Parameter Inline compare : t -> t -> comparison. - Axiom compare_spec : forall x y, CompSpec eq lt x y (compare x y). -End HasCompare. +End HasCmp. + +Module Type CmpNotation (T:Typ)(C:HasCmp T). + Infix "?=" := C.compare (at level 70, no associativity). +End CmpNotation. + +Module Type CmpSpec (Import E:EqLt')(Import C:HasCmp E). + Axiom compare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (compare x y). +End CmpSpec. + +Module Type HasCompare (E:EqLt) := HasCmp E <+ CmpSpec E. -Module Type StrOrder := EqualityType <+ HasLt <+ IsStrOrder. Module Type DecStrOrder := StrOrder <+ HasCompare. +Module Type DecStrOrder' := DecStrOrder <+ EqLtNotation <+ CmpNotation. + Module Type OrderedType <: DecidableType := DecStrOrder <+ HasEqDec. -Module Type OrderedTypeFull := OrderedType <+ HasLe <+ LeIsLtEq. +Module Type OrderedType' := OrderedType <+ EqLtNotation <+ CmpNotation. -Module Type StrOrder' := StrOrder <+ EqLtNotation. -Module Type DecStrOrder' := DecStrOrder <+ EqLtNotation. -Module Type OrderedType' := OrderedType <+ EqLtNotation. -Module Type OrderedTypeFull' := OrderedTypeFull <+ EqLtLeNotation. +Module Type OrderedTypeFull := OrderedType <+ HasLe <+ LeIsLtEq. +Module Type OrderedTypeFull' := + OrderedTypeFull <+ EqLtLeNotation <+ CmpNotation. (** NB: in [OrderedType], an [eq_dec] could be deduced from [compare]. But adding this redundant field allows to see an [OrderedType] as a @@ -169,50 +181,63 @@ Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder Local Coercion is_true : bool >-> Sortclass. Hint Unfold is_true. -Module Type HasLeBool (Import T:Typ). - Parameter Inline leb : t -> t -> bool. -End HasLeBool. - -Module Type HasLtBool (Import T:Typ). - Parameter Inline ltb : t -> t -> bool. -End HasLtBool. +Module Type HasLeb (Import T:Typ). + Parameter Inline leb : t -> t -> bool. +End HasLeb. -Module Type LeBool := Typ <+ HasLeBool. -Module Type LtBool := Typ <+ HasLtBool. +Module Type HasLtb (Import T:Typ). + Parameter Inline ltb : t -> t -> bool. +End HasLtb. -Module Type LeBoolNotation (E:LeBool). - Infix "<=?" := E.leb (at level 35). -End LeBoolNotation. +Module Type LebNotation (T:Typ)(E:HasLeb T). + Infix "<=?" := E.leb (at level 35). +End LebNotation. -Module Type LtBoolNotation (E:LtBool). - Infix "<?" := E.ltb (at level 35). -End LtBoolNotation. +Module Type LtbNotation (T:Typ)(E:HasLtb T). + Infix "<?" := E.ltb (at level 35). +End LtbNotation. -Module Type LeBool' := LeBool <+ LeBoolNotation. -Module Type LtBool' := LtBool <+ LtBoolNotation. +Module Type LebSpec (T:Typ)(X:HasLe T)(Y:HasLeb T). + Parameter leb_le : forall x y, Y.leb x y = true <-> X.le x y. +End LebSpec. -Module Type LeBool_Le (T:Typ)(X:HasLeBool T)(Y:HasLe T). - Parameter leb_le : forall x y, X.leb x y = true <-> Y.le x y. -End LeBool_Le. +Module Type LtbSpec (T:Typ)(X:HasLt T)(Y:HasLtb T). + Parameter ltb_lt : forall x y, Y.ltb x y = true <-> X.lt x y. +End LtbSpec. -Module Type LtBool_Lt (T:Typ)(X:HasLtBool T)(Y:HasLt T). - Parameter ltb_lt : forall x y, X.ltb x y = true <-> Y.lt x y. -End LtBool_Lt. +Module Type LeBool := Typ <+ HasLeb. +Module Type LtBool := Typ <+ HasLtb. +Module Type LeBool' := LeBool <+ LebNotation. +Module Type LtBool' := LtBool <+ LtbNotation. -Module Type LeBoolIsTotal (Import X:LeBool'). +Module Type LebIsTotal (Import X:LeBool'). Axiom leb_total : forall x y, (x <=? y) = true \/ (y <=? x) = true. -End LeBoolIsTotal. +End LebIsTotal. -Module Type TotalLeBool := LeBool <+ LeBoolIsTotal. -Module Type TotalLeBool' := LeBool' <+ LeBoolIsTotal. +Module Type TotalLeBool := LeBool <+ LebIsTotal. +Module Type TotalLeBool' := LeBool' <+ LebIsTotal. -Module Type LeBoolIsTransitive (Import X:LeBool'). +Module Type LebIsTransitive (Import X:LeBool'). Axiom leb_trans : Transitive X.leb. -End LeBoolIsTransitive. +End LebIsTransitive. + +Module Type TotalTransitiveLeBool := TotalLeBool <+ LebIsTransitive. +Module Type TotalTransitiveLeBool' := TotalLeBool' <+ LebIsTransitive. + +(** Grouping all boolean comparison functions *) + +Module Type HasBoolOrdFuns (T:Typ) := HasEqb T <+ HasLtb T <+ HasLeb T. + +Module Type HasBoolOrdFuns' (T:Typ) := + HasBoolOrdFuns T <+ EqbNotation T <+ LtbNotation T <+ LebNotation T. -Module Type TotalTransitiveLeBool := TotalLeBool <+ LeBoolIsTransitive. -Module Type TotalTransitiveLeBool' := TotalLeBool' <+ LeBoolIsTransitive. +Module Type BoolOrdSpecs (O:EqLtLe)(F:HasBoolOrdFuns O) := + EqbSpec O O F <+ LtbSpec O O F <+ LebSpec O O F. +Module Type OrderFunctions (E:EqLtLe) := + HasCompare E <+ HasBoolOrdFuns E <+ BoolOrdSpecs E. +Module Type OrderFunctions' (E:EqLtLe) := + HasCompare E <+ CmpNotation E <+ HasBoolOrdFuns' E <+ BoolOrdSpecs E. (** * From [OrderedTypeFull] to [TotalTransitiveLeBool] *) diff --git a/theories/Structures/OrdersAlt.v b/theories/Structures/OrdersAlt.v index 21ef8eb8..5dd917a7 100644 --- a/theories/Structures/OrdersAlt.v +++ b/theories/Structures/OrdersAlt.v @@ -11,8 +11,6 @@ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud * 91405 Orsay, France *) -(* $Id: OrdersAlt.v 12754 2010-02-12 16:21:48Z letouzey $ *) - Require Import OrderedType Orders. Set Implicit Arguments. @@ -142,7 +140,7 @@ Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType. Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z. Proof. unfold lt, eq; intros x y z Hxy Hyz. - destruct (compare x z) as [ ]_eqn:Hxz; auto. + destruct (compare x z) eqn:Hxz; auto. rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz. rewrite (compare_trans Hxz Hyz) in Hxy; discriminate. rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy. @@ -152,7 +150,7 @@ Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType. Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z. Proof. unfold lt, eq; intros x y z Hxy Hyz. - destruct (compare x z) as [ ]_eqn:Hxz; auto. + destruct (compare x z) eqn:Hxz; auto. rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy. rewrite (compare_trans Hxy Hxz) in Hyz; discriminate. rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz. @@ -171,7 +169,7 @@ Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType. Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). Proof. unfold eq, lt, compare; intros. - destruct (O.compare x y) as [ ]_eqn:H; auto. + destruct (O.compare x y) eqn:H; auto. apply CompGt. rewrite compare_sym, H; auto. Qed. diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v index 9f83d82b..e071d053 100644 --- a/theories/Structures/OrdersEx.v +++ b/theories/Structures/OrdersEx.v @@ -11,20 +11,18 @@ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud * 91405 Orsay, France *) -(* $Id: OrdersEx.v 12641 2010-01-07 15:32:52Z letouzey $ *) - -Require Import Orders NatOrderedType POrderedType NOrderedType - ZOrderedType RelationPairs EqualitiesFacts. +Require Import Orders NPeano POrderedType NArith + ZArith RelationPairs EqualitiesFacts. (** * Examples of Ordered Type structures. *) (** Ordered Type for [nat], [Positive], [N], [Z] with the usual order. *) -Module Nat_as_OT := NatOrderedType.Nat_as_OT. +Module Nat_as_OT := NPeano.Nat. Module Positive_as_OT := POrderedType.Positive_as_OT. -Module N_as_OT := NOrderedType.N_as_OT. -Module Z_as_OT := ZOrderedType.Z_as_OT. +Module N_as_OT := BinNat.N. +Module Z_as_OT := BinInt.Z. (** An OrderedType can now directly be seen as a DecidableType *) diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index a28b7977..2e9c0cf5 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -6,15 +6,76 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -Require Import Basics OrdersTac. +Require Import Bool Basics OrdersTac. Require Export Orders. Set Implicit Arguments. Unset Strict Implicit. -(** * Properties of [OrderedTypeFull] *) +(** * Properties of [compare] *) -Module OrderedTypeFullFacts (Import O:OrderedTypeFull'). +Module Type CompareFacts (Import O:DecStrOrder'). + + Local Infix "?=" := compare (at level 70, no associativity). + + Lemma compare_eq_iff x y : (x ?= y) = Eq <-> x==y. + Proof. + case compare_spec; intro H; split; try easy; intro EQ; + contradict H; rewrite EQ; apply irreflexivity. + Qed. + + Lemma compare_eq x y : (x ?= y) = Eq -> x==y. + Proof. + apply compare_eq_iff. + Qed. + + Lemma compare_lt_iff x y : (x ?= y) = Lt <-> x<y. + Proof. + case compare_spec; intro H; split; try easy; intro LT; + contradict LT; rewrite H; apply irreflexivity. + Qed. + + Lemma compare_gt_iff x y : (x ?= y) = Gt <-> y<x. + Proof. + case compare_spec; intro H; split; try easy; intro LT; + contradict LT; rewrite H; apply irreflexivity. + Qed. + + Lemma compare_nlt_iff x y : (x ?= y) <> Lt <-> ~(x<y). + Proof. + rewrite compare_lt_iff; intuition. + Qed. + + Lemma compare_ngt_iff x y : (x ?= y) <> Gt <-> ~(y<x). + Proof. + rewrite compare_gt_iff; intuition. + Qed. + + Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order. + + Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare. + Proof. + intros x x' Hxx' y y' Hyy'. + case (compare_spec x' y'); autorewrite with order; now rewrite Hxx', Hyy'. + Qed. + + Lemma compare_refl x : (x ?= x) = Eq. + Proof. + case compare_spec; intros; trivial; now elim irreflexivity with x. + Qed. + + Lemma compare_antisym x y : (y ?= x) = CompOpp (x ?= y). + Proof. + case (compare_spec x y); simpl; autorewrite with order; + trivial; now symmetry. + Qed. + +End CompareFacts. + + + (** * Properties of [OrderedTypeFull] *) + +Module Type OrderedTypeFullFacts (Import O:OrderedTypeFull'). Module OrderTac := OTF_to_OrderTac O. Ltac order := OrderTac.order. @@ -47,6 +108,18 @@ Module OrderedTypeFullFacts (Import O:OrderedTypeFull'). Lemma eq_is_le_ge : forall x y, x==y <-> x<=y /\ y<=x. Proof. iorder. Qed. + Include CompareFacts O. + + Lemma compare_le_iff x y : compare x y <> Gt <-> x<=y. + Proof. + rewrite le_not_gt_iff. apply compare_ngt_iff. + Qed. + + Lemma compare_ge_iff x y : compare x y <> Lt <-> y<=x. + Proof. + rewrite le_not_gt_iff. apply compare_nlt_iff. + Qed. + End OrderedTypeFullFacts. @@ -84,50 +157,9 @@ Module OrderedTypeFacts (Import O: OrderedType'). Definition lt_irrefl (x:t) : ~x<x := StrictOrder_Irreflexive x. - (** Some more about [compare] *) - - Lemma compare_eq_iff : forall x y, (x ?= y) = Eq <-> x==y. - Proof. - intros; elim_compare x y; intuition; try discriminate; order. - Qed. - - Lemma compare_lt_iff : forall x y, (x ?= y) = Lt <-> x<y. - Proof. - intros; elim_compare x y; intuition; try discriminate; order. - Qed. - - Lemma compare_gt_iff : forall x y, (x ?= y) = Gt <-> y<x. - Proof. - intros; elim_compare x y; intuition; try discriminate; order. - Qed. - - Lemma compare_ge_iff : forall x y, (x ?= y) <> Lt <-> y<=x. - Proof. - intros; rewrite compare_lt_iff; intuition. - Qed. - - Lemma compare_le_iff : forall x y, (x ?= y) <> Gt <-> x<=y. - Proof. - intros; rewrite compare_gt_iff; intuition. - Qed. - - Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order. - - Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare. - Proof. - intros x x' Hxx' y y' Hyy'. - elim_compare x' y'; autorewrite with order; order. - Qed. - - Lemma compare_refl : forall x, (x ?= x) = Eq. - Proof. - intros; elim_compare x x; auto; order. - Qed. - - Lemma compare_antisym : forall x y, (y ?= x) = CompOpp (x ?= y). - Proof. - intros; elim_compare x y; simpl; autorewrite with order; order. - Qed. + Include CompareFacts O. + Notation compare_le_iff := compare_ngt_iff (only parsing). + Notation compare_ge_iff := compare_nlt_iff (only parsing). (** For compatibility reasons *) Definition eq_dec := eq_dec. @@ -162,10 +194,6 @@ Module OrderedTypeFacts (Import O: OrderedType'). End OrderedTypeFacts. - - - - (** * Tests of the order tactic Is it at least capable of proving some basic properties ? *) @@ -208,7 +236,7 @@ Module OrderedTypeRev (O:OrderedTypeFull) <: OrderedTypeFull. Definition t := O.t. Definition eq := O.eq. -Instance eq_equiv : Equivalence eq. +Program Instance eq_equiv : Equivalence eq. Definition eq_dec := O.eq_dec. Definition lt := flip O.lt. @@ -232,3 +260,195 @@ Qed. End OrderedTypeRev. +Unset Implicit Arguments. + +(** * Order relations derived from a [compare] function. + + We factorize here some common properties for ZArith, NArith + and co, where [lt] and [le] are defined in terms of [compare]. + Note that we do not require anything here concerning compatibility + of [compare] w.r.t [eq], nor anything concerning transitivity. +*) + +Module Type CompareBasedOrder (Import E:EqLtLe')(Import C:HasCmp E). + Include CmpNotation E C. + Include IsEq E. + Axiom compare_eq_iff : forall x y, (x ?= y) = Eq <-> x == y. + Axiom compare_lt_iff : forall x y, (x ?= y) = Lt <-> x < y. + Axiom compare_le_iff : forall x y, (x ?= y) <> Gt <-> x <= y. + Axiom compare_antisym : forall x y, (y ?= x) = CompOpp (x ?= y). +End CompareBasedOrder. + +Module Type CompareBasedOrderFacts + (Import E:EqLtLe') + (Import C:HasCmp E) + (Import O:CompareBasedOrder E C). + + 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. + Qed. + + Lemma compare_eq x y : (x ?= y) = Eq -> x==y. + Proof. + apply compare_eq_iff. + Qed. + + Lemma compare_refl x : (x ?= x) = Eq. + Proof. + now apply compare_eq_iff. + Qed. + + Lemma compare_gt_iff x y : (x ?= y) = Gt <-> y<x. + Proof. + now rewrite <- compare_lt_iff, compare_antisym, CompOpp_iff. + Qed. + + Lemma compare_ge_iff x y : (x ?= y) <> Lt <-> y<=x. + Proof. + now rewrite <- compare_le_iff, compare_antisym, CompOpp_iff. + Qed. + + Lemma compare_ngt_iff x y : (x ?= y) <> Gt <-> ~(y<x). + Proof. + rewrite compare_gt_iff; intuition. + Qed. + + Lemma compare_nlt_iff x y : (x ?= y) <> Lt <-> ~(x<y). + Proof. + rewrite compare_lt_iff; intuition. + Qed. + + Lemma compare_nle_iff x y : (x ?= y) = Gt <-> ~(x<=y). + Proof. + rewrite <- compare_le_iff. + destruct compare; split; easy || now destruct 1. + Qed. + + Lemma compare_nge_iff x y : (x ?= y) = Lt <-> ~(y<=x). + Proof. + now rewrite <- compare_nle_iff, compare_antisym, CompOpp_iff. + Qed. + + Lemma lt_irrefl x : ~ (x<x). + Proof. + now rewrite <- compare_lt_iff, compare_refl. + Qed. + + Lemma lt_eq_cases n m : n <= m <-> n < m \/ n==m. + Proof. + rewrite <- compare_lt_iff, <- compare_le_iff, <- compare_eq_iff. + destruct (n ?= m); now intuition. + Qed. + +End CompareBasedOrderFacts. + +(** Basic facts about boolean comparisons *) + +Module Type BoolOrderFacts + (Import E:EqLtLe') + (Import C:HasCmp E) + (Import F:HasBoolOrdFuns' E) + (Import O:CompareBasedOrder E C) + (Import S:BoolOrdSpecs E F). + +Include CompareBasedOrderFacts E C O. + +(** Nota : apart from [eqb_compare] below, facts about [eqb] + are in BoolEqualityFacts *) + +(** Alternate specifications based on [BoolSpec] and [reflect] *) + +Lemma leb_spec0 x y : reflect (x<=y) (x<=?y). +Proof. + apply iff_reflect. symmetry. apply leb_le. +Defined. + +Lemma leb_spec x y : BoolSpec (x<=y) (y<x) (x<=?y). +Proof. + case leb_spec0; constructor; trivial. + now rewrite <- compare_lt_iff, compare_nge_iff. +Qed. + +Lemma ltb_spec0 x y : reflect (x<y) (x<?y). +Proof. + apply iff_reflect. symmetry. apply ltb_lt. +Defined. + +Lemma ltb_spec x y : BoolSpec (x<y) (y<=x) (x<?y). +Proof. + case ltb_spec0; constructor; trivial. + now rewrite <- compare_le_iff, compare_ngt_iff. +Qed. + +(** Negated variants of the specifications *) + +Lemma leb_nle x y : x <=? y = false <-> ~ (x <= y). +Proof. +now rewrite <- not_true_iff_false, leb_le. +Qed. + +Lemma leb_gt x y : x <=? y = false <-> y < x. +Proof. +now rewrite leb_nle, <- compare_lt_iff, compare_nge_iff. +Qed. + +Lemma ltb_nlt x y : x <? y = false <-> ~ (x < y). +Proof. +now rewrite <- not_true_iff_false, ltb_lt. +Qed. + +Lemma ltb_ge x y : x <? y = false <-> y <= x. +Proof. +now rewrite ltb_nlt, <- compare_le_iff, compare_ngt_iff. +Qed. + +(** Basic equality laws for boolean tests *) + +Lemma leb_refl x : x <=? x = true. +Proof. +apply leb_le. apply lt_eq_cases. now right. +Qed. + +Lemma leb_antisym x y : y <=? x = negb (x <? y). +Proof. +apply eq_true_iff_eq. now rewrite negb_true_iff, leb_le, ltb_ge. +Qed. + +Lemma ltb_irrefl x : x <? x = false. +Proof. +apply ltb_ge. apply lt_eq_cases. now right. +Qed. + +Lemma ltb_antisym x y : y <? x = negb (x <=? y). +Proof. +apply eq_true_iff_eq. now rewrite negb_true_iff, ltb_lt, leb_gt. +Qed. + +(** Relation bewteen [compare] and the boolean comparisons *) + +Lemma eqb_compare x y : + (x =? y) = match compare x y with Eq => true | _ => false end. +Proof. +apply eq_true_iff_eq. rewrite eqb_eq, <- compare_eq_iff. +destruct compare; now split. +Qed. + +Lemma ltb_compare x y : + (x <? y) = match compare x y with Lt => true | _ => false end. +Proof. +apply eq_true_iff_eq. rewrite ltb_lt, <- compare_lt_iff. +destruct compare; now split. +Qed. + +Lemma leb_compare x y : + (x <=? y) = match compare x y with Gt => false | _ => true end. +Proof. +apply eq_true_iff_eq. rewrite leb_le, <- compare_le_iff. +destruct compare; split; try easy. now destruct 1. +Qed. + +End BoolOrderFacts. diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v index 2ed07026..f83b6377 100644 --- a/theories/Structures/OrdersLists.v +++ b/theories/Structures/OrdersLists.v @@ -86,11 +86,11 @@ Module KeyOrderedType(Import O:OrderedType). (* eqk, eqke are equalities, ltk is a strict order *) - Global Instance eqk_equiv : Equivalence eqk. + Global Instance eqk_equiv : Equivalence eqk := _. - Global Instance eqke_equiv : Equivalence eqke. + Global Instance eqke_equiv : Equivalence eqke := _. - Global Instance ltk_strorder : StrictOrder ltk. + Global Instance ltk_strorder : StrictOrder ltk := _. Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk. Proof. unfold eqk, ltk; auto with *. Qed. diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v index 66a672c9..68ffc379 100644 --- a/theories/Structures/OrdersTac.v +++ b/theories/Structures/OrdersTac.v @@ -40,16 +40,26 @@ Definition trans_ord o o' := Local Infix "+" := trans_ord. -(** ** The requirements of the tactic : [TotalOrder]. +(** ** The tactic requirements : a total order - [TotalOrder] contains an equivalence [eq], - a strict order [lt] total and compatible with [eq], and - a larger order [le] synonym for [lt\/eq]. + We need : + - an equivalence [eq], + - a strict order [lt] total and compatible with [eq], + - a larger order [le] synonym for [lt\/eq]. + + This used to be provided here via a [TotalOrder], but + for technical reasons related to extraction, we now ask + for two sperate parts: relations in a [EqLtLe] + properties in + [IsTotalOrder]. Note that [TotalOrder = EqLtLe <+ IsTotalOrder] *) +Module Type IsTotalOrder (O:EqLtLe) := + IsEq O <+ IsStrOrder O <+ LeIsLtEq O <+ LtIsTotal O. + (** ** Properties that will be used by the [order] tactic *) -Module OrderFacts(Import O:TotalOrder'). +Module OrderFacts (Import O:EqLtLe)(P:IsTotalOrder O). +Include EqLtLeNotation O. (** Reflexivity rules *) @@ -57,7 +67,7 @@ Lemma eq_refl : forall x, x==x. Proof. reflexivity. Qed. Lemma le_refl : forall x, x<=x. -Proof. intros; rewrite le_lteq; right; reflexivity. Qed. +Proof. intros; rewrite P.le_lteq; right; reflexivity. Qed. Lemma lt_irrefl : forall x, ~ x<x. Proof. intros; apply StrictOrder_Irreflexive. Qed. @@ -69,7 +79,7 @@ Proof. auto with *. Qed. Lemma le_antisym : forall x y, x<=y -> y<=x -> x==y. Proof. - intros x y; rewrite 2 le_lteq. intuition. + intros x y; rewrite 2 P.le_lteq. intuition. elim (StrictOrder_Irreflexive x); transitivity y; auto. Qed. @@ -90,7 +100,7 @@ Local Notation "#" := interp_ord. Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z. Proof. -destruct o, o'; simpl; intros x y z; rewrite ?le_lteq; intuition; +destruct o, o'; simpl; intros x y z; rewrite ?P.le_lteq; intuition; subst_eqns; eauto using (StrictOrder_Transitive x y z) with *. Qed. @@ -114,19 +124,19 @@ Proof. eauto using eq_trans, eq_sym. Qed. Lemma not_neq_eq : forall x y, ~~x==y -> x==y. Proof. -intros x y H. destruct (lt_total x y) as [H'|[H'|H']]; auto; +intros x y H. destruct (P.lt_total x y) as [H'|[H'|H']]; auto; destruct H; intro H; rewrite H in H'; eapply lt_irrefl; eauto. Qed. Lemma not_ge_lt : forall x y, ~y<=x -> x<y. Proof. -intros x y H. destruct (lt_total x y); auto. -destruct H. rewrite le_lteq. intuition. +intros x y H. destruct (P.lt_total x y); auto. +destruct H. rewrite P.le_lteq. intuition. Qed. Lemma not_gt_le : forall x y, ~y<x -> x<=y. Proof. -intros x y H. rewrite le_lteq. generalize (lt_total x y); intuition. +intros x y H. rewrite P.le_lteq. generalize (P.lt_total x y); intuition. Qed. Lemma le_neq_lt : forall x y, x<=y -> ~x==y -> x<y. @@ -138,9 +148,9 @@ End OrderFacts. (** ** [MakeOrderTac] : The functor providing the order tactic. *) -Module MakeOrderTac (Import O:TotalOrder'). - -Include OrderFacts O. +Module MakeOrderTac (Import O:EqLtLe)(P:IsTotalOrder O). +Include OrderFacts O P. +Include EqLtLeNotation O. (** order_eq : replace x by y in all (in)equations hyps thanks to equality EQ (where eq has been hidden in order to avoid @@ -257,37 +267,10 @@ End MakeOrderTac. Module OTF_to_OrderTac (OTF:OrderedTypeFull). Module TO := OTF_to_TotalOrder OTF. - Include !MakeOrderTac TO. + Include !MakeOrderTac OTF TO. End OTF_to_OrderTac. Module OT_to_OrderTac (OT:OrderedType). Module OTF := OT_to_Full OT. Include !OTF_to_OrderTac OTF. End OT_to_OrderTac. - -Module TotalOrderRev (O:TotalOrder) <: TotalOrder. - -Definition t := O.t. -Definition eq := O.eq. -Definition lt := flip O.lt. -Definition le := flip O.le. -Include EqLtLeNotation. - -(* No Instance syntax to avoid saturating the Equivalence tables *) -Definition eq_equiv := O.eq_equiv. - -Instance lt_strorder: StrictOrder lt. -Proof. unfold lt; auto with *. Qed. -Instance lt_compat : Proper (eq==>eq==>iff) lt. -Proof. unfold lt; auto with *. Qed. - -Lemma le_lteq : forall x y, x<=y <-> x<y \/ x==y. -Proof. intros; unfold le, lt, flip. rewrite O.le_lteq; intuition. Qed. - -Lemma lt_total : forall x y, x<y \/ x==y \/ y<x. -Proof. - intros x y; unfold lt, eq, flip. - generalize (O.lt_total x y); intuition. -Qed. - -End TotalOrderRev. |