diff options
Diffstat (limited to 'theories')
40 files changed, 3196 insertions, 1643 deletions
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index 6f8a5f127..0f2595b26 100644 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v @@ -52,4 +52,4 @@ Qed. Require Export Wf_nat. -Require Export Min. +Require Export Min Max.
\ No newline at end of file diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index 62250fc33..3d7fe9fc2 100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -8,127 +8,34 @@ (*i $Id$ i*) -Require Import Le Plus. +(** THIS FILE IS DEPRECATED. Use [MinMax] instead. *) -Open Local Scope nat_scope. +Require Export MinMax. +Local Open Scope nat_scope. Implicit Types m n p : nat. -(** * Maximum of two natural numbers *) - -Fixpoint max n m : nat := - match n, m with - | O, _ => m - | S n', O => n - | S n', S m' => S (max n' m') - end. - -(** * Inductive characterization of [max] *) - -Lemma max_case_strong : forall n m (P:nat -> Type), - (m<=n -> P n) -> (n<=m -> P m) -> P (max n m). -Proof. - induction n; destruct m; simpl in *; auto with arith. - intros P H1 H2; apply IHn; intro; [apply H1|apply H2]; auto with arith. -Qed. - -(** Propositional characterization of [max] *) - -Lemma max_spec : forall n m, m <= n /\ max n m = n \/ n <= m /\ max n m = m. -Proof. - intros n m; apply max_case_strong; auto. -Qed. - -(** * [max n m] is equal to [n] or [m] *) - -Lemma max_dec : forall n m, {max n m = n} + {max n m = m}. -Proof. - induction n; destruct m; simpl; auto. - destruct (IHn m) as [-> | ->]; auto. -Defined. - -(** [max n m] is equal to [n] or [m], alternative formulation *) - -Lemma max_case : forall n m (P:nat -> Type), P n -> P m -> P (max n m). -Proof. - intros n m; destruct (max_dec n m) as [-> | ->]; auto. -Defined. - -(** * Compatibility properties of [max] *) - -Lemma succ_max_distr : forall n m, S (max n m) = max (S n) (S m). -Proof. - auto. -Qed. - -Lemma plus_max_distr_l : forall n m p, max (p + n) (p + m) = p + max n m. -Proof. - induction p; simpl; auto. -Qed. - -Lemma plus_max_distr_r : forall n m p, max (n + p) (m + p) = max n m + p. -Proof. - intros n m p; repeat rewrite (plus_comm _ p). - apply plus_max_distr_l. -Qed. - -(** * Semi-lattice algebraic properties of [max] *) - -Lemma max_idempotent : forall n, max n n = n. -Proof. - intros; apply max_case; auto. -Qed. - -Lemma max_assoc : forall m n p : nat, max m (max n p) = max (max m n) p. -Proof. - induction m; destruct n; destruct p; trivial. - simpl; auto. -Qed. - -Lemma max_comm : forall n m, max n m = max m n. -Proof. - induction n; destruct m; simpl; auto. -Qed. - -(** * Least-upper bound properties of [max] *) - -Lemma max_l : forall n m, m <= n -> max n m = n. -Proof. - induction n; destruct m; simpl; auto with arith. -Qed. - -Lemma max_r : forall n m, n <= m -> max n m = m. -Proof. - induction n; destruct m; simpl; auto with arith. -Qed. - -Lemma le_max_l : forall n m, n <= max n m. -Proof. - induction n; simpl; auto with arith. - destruct m; simpl; auto with arith. -Qed. - -Lemma le_max_r : forall n m, m <= max n m. -Proof. - induction n; simpl; auto with arith. - induction m; simpl; auto with arith. -Qed. -Hint Resolve max_r max_l le_max_l le_max_r: arith v62. - -Lemma max_lub_l : forall n m p, max n m <= p -> n <= p. -Proof. -intros n m p; eapply le_trans. apply le_max_l. -Qed. - -Lemma max_lub_r : forall n m p, max n m <= p -> m <= p. -Proof. -intros n m p; eapply le_trans. apply le_max_r. -Qed. - -Lemma max_lub : forall n m p, n <= p -> m <= p -> max n m <= p. -Proof. - intros n m p; apply max_case; auto. -Qed. +Notation max := MinMax.max (only parsing). + +Definition max_0_l := max_0_l. +Definition max_0_r := max_0_r. +Definition succ_max_distr := succ_max_distr. +Definition plus_max_distr_l := plus_max_distr_l. +Definition plus_max_distr_r := plus_max_distr_r. +Definition max_case_strong := max_case_strong. +Definition max_spec := max_spec. +Definition max_dec := max_dec. +Definition max_case := max_case. +Definition max_idempotent := max_id. +Definition max_assoc := max_assoc. +Definition max_comm := max_comm. +Definition max_l := max_l. +Definition max_r := max_r. +Definition le_max_l := le_max_l. +Definition le_max_r := le_max_r. +Definition max_lub_l := max_lub_l. +Definition max_lub_r := max_lub_r. +Definition max_lub := max_lub. (* begin hide *) (* Compatibility *) diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index 62948093f..c52fc0dd0 100644 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -8,111 +8,37 @@ (*i $Id$ i*) -Require Import Le. +(** THIS FILE IS DEPRECATED. Use [MinMax] instead. *) -Open Local Scope nat_scope. +Require Export MinMax. +Open Local Scope nat_scope. Implicit Types m n p : nat. -(** * minimum of two natural numbers *) - -Fixpoint min n m : nat := - match n, m with - | O, _ => 0 - | S n', O => 0 - | S n', S m' => S (min n' m') - end. - -(** * Simplifications of [min] *) - -Lemma min_0_l : forall n : nat, min 0 n = 0. -Proof. - trivial. -Qed. - -Lemma min_0_r : forall n : nat, min n 0 = 0. -Proof. - destruct n; trivial. -Qed. - -Lemma min_SS : forall n m, S (min n m) = min (S n) (S m). -Proof. - auto with arith. -Qed. - -(** * [min n m] is equal to [n] or [m] *) - -Lemma min_dec : forall n m, {min n m = n} + {min n m = m}. -Proof. - induction n; induction m; simpl in |- *; auto with arith. - elim (IHn m); intro H; elim H; auto. -Qed. - -Lemma min_case : forall n m (P:nat -> Type), P n -> P m -> P (min n m). -Proof. - induction n; simpl in |- *; auto with arith. - induction m; intros; simpl in |- *; auto with arith. - pattern (min n m) in |- *; apply IHn; auto with arith. -Qed. - -(** * Semi-lattice algebraic properties of [min] *) - -Lemma min_idempotent : forall n, min n n = n. -Proof. - induction n; simpl; [|rewrite IHn]; trivial. -Qed. - -Lemma min_assoc : forall m n p : nat, min m (min n p) = min (min m n) p. -Proof. - induction m; destruct n; destruct p; trivial. - simpl. - auto using (IHm n p). -Qed. - -Lemma min_comm : forall n m, min n m = min m n. -Proof. - induction n; induction m; simpl in |- *; auto with arith. -Qed. - -(** * Least-upper bound properties of [min] *) - -Lemma min_l : forall n m, n <= m -> min n m = n. -Proof. - induction n; induction m; simpl in |- *; auto with arith. -Qed. - -Lemma min_r : forall n m, m <= n -> min n m = m. -Proof. - induction n; induction m; simpl in |- *; auto with arith. -Qed. - -Lemma le_min_l : forall n m, min n m <= n. -Proof. - induction n; intros; simpl in |- *; auto with arith. - elim m; intros; simpl in |- *; auto with arith. -Qed. - -Lemma le_min_r : forall n m, min n m <= m. -Proof. - induction n; simpl in |- *; auto with arith. - induction m; simpl in |- *; auto with arith. -Qed. -Hint Resolve min_l min_r le_min_l le_min_r: arith v62. - -Lemma min_glb_l : forall n m p, p <= min n m -> p <= n. -Proof. -intros; eapply le_trans; [eassumption|apply le_min_l]. -Qed. - -Lemma min_glb_r : forall n m p, p <= min n m -> p <= m. -Proof. -intros; eapply le_trans; [eassumption|apply le_min_r]. -Qed. - -Lemma min_glb : forall n m p, p <= n -> p <= m -> p <= min n m. -Proof. - intros n m p; apply min_case; auto. -Qed. - +Notation min := MinMax.min (only parsing). + +Definition min_0_l := min_0_l. +Definition min_0_r := min_0_r. +Definition succ_min_distr := succ_min_distr. +Definition plus_min_distr_l := plus_min_distr_l. +Definition plus_min_distr_r := plus_min_distr_r. +Definition min_case_strong := min_case_strong. +Definition min_spec := min_spec. +Definition min_dec := min_dec. +Definition min_case := min_case. +Definition min_idempotent := min_id. +Definition min_assoc := min_assoc. +Definition min_comm := min_comm. +Definition min_l := min_l. +Definition min_r := min_r. +Definition le_min_l := le_min_l. +Definition le_min_r := le_min_r. +Definition min_glb_l := min_glb_l. +Definition min_glb_r := min_glb_r. +Definition min_glb := min_glb. + +(* begin hide *) +(* Compatibility *) Notation min_case2 := min_case (only parsing). - +Notation min_SS := succ_min_distr (only parsing). +(* end hide *)
\ No newline at end of file diff --git a/theories/Arith/MinMax.v b/theories/Arith/MinMax.v new file mode 100644 index 000000000..784e10455 --- /dev/null +++ b/theories/Arith/MinMax.v @@ -0,0 +1,211 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import OrderedType2 NatOrderedType GenericMinMax. + +(** * Maximum and Minimum of two natural numbers *) + +Fixpoint max n m : nat := + match n, m with + | O, _ => m + | S n', O => n + | S n', S m' => S (max n' m') + end. + +Fixpoint min n m : nat := + match n, m with + | O, _ => 0 + | S n', O => 0 + | S n', S m' => S (min n' m') + end. + +(** These functions implement indeed a maximum and a minimum *) + +Lemma max_spec : forall x y, + (x<y /\ max x y = y) \/ (y<=x /\ max x y = x). +Proof. + induction x; destruct y; simpl; auto with arith. + destruct (IHx y); intuition. +Qed. + +Lemma min_spec : forall x y, + (x<y /\ min x y = x) \/ (y<=x /\ min x y = y). +Proof. + induction x; destruct y; simpl; auto with arith. + destruct (IHx y); intuition. +Qed. + +Module NatHasMinMax <: HasMinMax Nat_as_OT. + Definition max := max. + Definition min := min. + Definition max_spec := max_spec. + Definition min_spec := min_spec. +End NatHasMinMax. + +(** We obtain hence all the generic properties of max and min. *) + +Module Import NatMinMaxProps := MinMaxProperties Nat_as_OT NatHasMinMax. + +(** For some generic properties, we can have nicer statements here, + since underlying equality is Leibniz. *) + +Lemma max_case_strong : forall n m (P:nat -> Type), + (m<=n -> P n) -> (n<=m -> P m) -> P (max n m). +Proof. intros; apply max_case_strong; auto. congruence. Defined. + +Lemma max_case : forall n m (P:nat -> Type), + P n -> P m -> P (max n m). +Proof. intros. apply max_case_strong; auto. Defined. + +Lemma max_monotone: forall f, + (Proper (le ==> le) f) -> + forall x y, max (f x) (f y) = f (max x y). +Proof. intros; apply max_monotone; auto. congruence. Qed. + +Lemma min_case_strong : forall n m (P:nat -> Type), + (m<=n -> P m) -> (n<=m -> P n) -> P (min n m). +Proof. intros; apply min_case_strong; auto. congruence. Defined. + +Lemma min_case : forall n m (P:nat -> Type), + P n -> P m -> P (min n m). +Proof. intros. apply min_case_strong; auto. Defined. + +Lemma min_monotone: forall f, + (Proper (le ==> le) f) -> + forall x y, min (f x) (f y) = f (min x y). +Proof. intros; apply min_monotone; auto. congruence. Qed. + +Lemma max_min_antimonotone : forall f, + Proper (le==>ge) f -> + forall x y, max (f x) (f y) == f (min x y). +Proof. + intros. apply max_min_antimonotone. congruence. + intros z z' Hz; red; unfold ge in *; auto. +Qed. + +Lemma min_max_antimonotone : forall f, + Proper (le==>ge) f -> + forall x y, min (f x) (f y) == f (max x y). +Proof. + intros. apply min_max_antimonotone. congruence. + intros z z' Hz; red; unfold ge in *; auto. +Qed. + +(** For the other generic properties, we make aliases, + since otherwise SearchAbout misses some of them + (bad interaction with an Include). + See GenericMinMax (or SearchAbout) for the statements. *) + +Definition max_spec_le := max_spec_le. +Definition max_dec := max_dec. +Definition max_unicity := max_unicity. +Definition max_unicity_ext := max_unicity_ext. +Definition max_id := max_id. +Notation max_idempotent := max_id (only parsing). +Definition max_assoc := max_assoc. +Definition max_comm := max_comm. +Definition max_l := max_l. +Definition max_r := max_r. +Definition le_max_l := le_max_l. +Definition le_max_r := le_max_r. +Definition max_le := max_le. +Definition max_le_iff := max_le_iff. +Definition max_lt_iff := max_lt_iff. +Definition max_lub_l := max_lub_l. +Definition max_lub_r := max_lub_r. +Definition max_lub := max_lub. +Definition max_lub_iff := max_lub_iff. +Definition max_lub_lt := max_lub_lt. +Definition max_lub_lt_iff := max_lub_lt_iff. +Definition max_le_compat_l := max_le_compat_l. +Definition max_le_compat_r := max_le_compat_r. +Definition max_le_compat := max_le_compat. + +Definition min_spec_le := min_spec_le. +Definition min_dec := min_dec. +Definition min_unicity := min_unicity. +Definition min_unicity_ext := min_unicity_ext. +Definition min_id := min_id. +Notation min_idempotent := min_id (only parsing). +Definition min_assoc := min_assoc. +Definition min_comm := min_comm. +Definition min_l := min_l. +Definition min_r := min_r. +Definition le_min_l := le_min_l. +Definition le_min_r := le_min_r. +Definition min_le := min_le. +Definition min_le_iff := min_le_iff. +Definition min_lt_iff := min_lt_iff. +Definition min_glb_l := min_glb_l. +Definition min_glb_r := min_glb_r. +Definition min_glb := min_glb. +Definition min_glb_iff := min_glb_iff. +Definition min_glb_lt := min_glb_lt. +Definition min_glb_lt_iff := min_glb_lt_iff. +Definition min_le_compat_l := min_le_compat_l. +Definition min_le_compat_r := min_le_compat_r. +Definition min_le_compat := min_le_compat. + +Definition min_max_absorption := min_max_absorption. +Definition max_min_absorption := max_min_absorption. +Definition max_min_distr := max_min_distr. +Definition min_max_distr := min_max_distr. +Definition max_min_modular := max_min_modular. +Definition min_max_modular := min_max_modular. +Definition max_min_disassoc := max_min_disassoc. + + +(** * Properties specific to the [nat] domain *) + +(** Simplifications *) + +Lemma max_0_l : forall n, max 0 n = n. +Proof. reflexivity. Qed. + +Lemma max_0_r : forall n, max n 0 = n. +Proof. destruct n; auto. Qed. + +Lemma min_0_l : forall n, min 0 n = 0. +Proof. reflexivity. Qed. + +Lemma min_0_r : forall n, min n 0 = 0. +Proof. destruct n; auto. Qed. + +(** Compatibilities (consequences of monotonicity) *) + +Lemma succ_max_distr : forall n m, S (max n m) = max (S n) (S m). +Proof. auto. Qed. + +Lemma succ_min_distr : forall n m, S (min n m) = min (S n) (S m). +Proof. auto. Qed. + +Lemma plus_max_distr_l : forall n m p, max (p + n) (p + m) = p + max n m. +Proof. +intros. apply max_monotone. repeat red; auto with arith. +Qed. + +Lemma plus_max_distr_r : forall n m p, max (n + p) (m + p) = max n m + p. +Proof. +intros. apply max_monotone with (f:=fun x => x + p). +repeat red; auto with arith. +Qed. + +Lemma plus_min_distr_l : forall n m p, min (p + n) (p + m) = p + min n m. +Proof. +intros. apply min_monotone. repeat red; auto with arith. +Qed. + +Lemma plus_min_distr_r : forall n m p, min (n + p) (m + p) = min n m + p. +Proof. +intros. apply min_monotone with (f:=fun x => x + p). +repeat red; auto with arith. +Qed. + +Hint Resolve + max_l max_r le_max_l le_max_r + min_l min_r le_min_l le_min_r : arith v62. diff --git a/theories/Arith/NatOrderedType.v b/theories/Arith/NatOrderedType.v new file mode 100644 index 000000000..c4e71632c --- /dev/null +++ b/theories/Arith/NatOrderedType.v @@ -0,0 +1,69 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import Peano_dec Compare_dec + DecidableType2 OrderedType2 OrderedType2Facts. + + +(** * DecidableType structure for Peano numbers *) + +Module Nat_as_MiniDT <: MiniDecidableType. + Definition t := nat. + Definition eq_dec := eq_nat_dec. +End Nat_as_MiniDT. + +Module Nat_as_DT <: UsualDecidableType := Make_UDT Nat_as_MiniDT. + +(** Note that [Nat_as_DT] can also be seen as a [DecidableType] + and a [DecidableTypeOrig]. *) + + + +(** * OrderedType structure for Peano numbers *) + +Module Nat_as_OT <: OrderedTypeFull. + Include Nat_as_DT. + Definition lt := lt. + Definition le := le. + Definition compare := nat_compare. + + Instance lt_strorder : StrictOrder lt. + Proof. split; [ exact Lt.lt_irrefl | exact Lt.lt_trans ]. Qed. + + Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) lt. + Proof. repeat red; intros; subst; auto. Qed. + + Lemma le_lteq : forall x y, x <= y <-> x < y \/ x=y. + Proof. intuition; subst; auto using Lt.le_lt_or_eq. Qed. + + Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y). + Proof. + intros; unfold compare. + destruct (nat_compare x y) as [ ]_eqn; constructor. + apply nat_compare_eq; auto. + apply nat_compare_Lt_lt; auto. + apply nat_compare_Gt_gt; auto. + Qed. + +End Nat_as_OT. + +(* Note that [Nat_as_OT] can also be seen as a [UsualOrderedType] + and a [OrderedType] (and also as a [DecidableType]). *) + + + +(** * An [order] tactic for Peano numbers *) + +Module NatOrder := OTF_to_OrderTac Nat_as_OT. +Ltac nat_order := + change (@eq nat) with NatOrder.OrderElts.eq in *; + NatOrder.order. + +(** Note that [nat_order] is domain-agnostic: it will not prove + [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *) + diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v new file mode 100644 index 000000000..c0e0bd61c --- /dev/null +++ b/theories/Classes/RelationPairs.v @@ -0,0 +1,125 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(** * Relations over pairs *) + + +Require Import Relations Morphisms. + +(* NB: This should be system-wide someday, but for that we need to + fix the simpl tactic, since "simpl fst" would be refused for + the moment. *) + +Implicit Arguments fst [[A] [B]]. +Implicit Arguments snd [[A] [B]]. +Implicit Arguments pair [[A] [B]]. + +(* /NB *) + + +(* NB: is signature_scope the right one for that ? *) + +Arguments Scope relation_conjunction + [type_scope signature_scope signature_scope]. +Arguments Scope relation_equivalence + [type_scope signature_scope signature_scope]. +Arguments Scope subrelation [type_scope signature_scope signature_scope]. +Arguments Scope Reflexive [type_scope signature_scope]. +Arguments Scope Irreflexive [type_scope signature_scope]. +Arguments Scope Symmetric [type_scope signature_scope]. +Arguments Scope Transitive [type_scope signature_scope]. +Arguments Scope PER [type_scope signature_scope]. +Arguments Scope Equivalence [type_scope signature_scope]. +Arguments Scope StrictOrder [type_scope signature_scope]. + +Generalizable Variables A B RA RB Ri Ro. + +(** Any function from [A] to [B] allow to obtain a relation over [A] + out of a relation over [B]. *) + +Definition RelCompFun {A B}(R:relation B)(f:A->B) : relation A := + fun a a' => R (f a) (f a'). + +Infix "@@" := RelCompFun (at level 30, right associativity) : signature_scope. + + +(** We define a product relation over [A*B]: each components should + satisfy the corresponding initial relation. *) + +Definition RelProd {A B}(RA:relation A)(RB:relation B) : relation (A*B) := + relation_conjunction (RA @@ fst) (RB @@ snd). + +Infix "*" := RelProd : signature_scope. + + +Instance RelCompFun_Reflexive {A B}(R:relation B)(f:A->B) + `(Reflexive _ R) : Reflexive (R@@f). +Proof. firstorder. Qed. + +Instance RelCompFun_Symmetric {A B}(R:relation B)(f:A->B) + `(Symmetric _ R) : Symmetric (R@@f). +Proof. firstorder. Qed. + +Instance RelCompFun_Transitive {A B}(R:relation B)(f:A->B) + `(Transitive _ R) : Transitive (R@@f). +Proof. firstorder. Qed. + +Instance RelCompFun_Irreflexive {A B}(R:relation B)(f:A->B) + `(Irreflexive _ R) : Irreflexive (R@@f). +Proof. firstorder. Qed. + +Instance RelCompFun_Equivalence {A B}(R:relation B)(f:A->B) + `(Equivalence _ R) : Equivalence (R@@f). + +Instance RelCompFun_StrictOrder {A B}(R:relation B)(f:A->B) + `(StrictOrder _ R) : StrictOrder (R@@f). + +Instance RelProd_Reflexive {A B}(RA:relation A)(RB:relation B) + `(Reflexive _ RA, Reflexive _ RB) : Reflexive (RA*RB). +Proof. firstorder. Qed. + +Instance RelProd_Symmetric {A B}(RA:relation A)(RB:relation B) + `(Symmetric _ RA, Symmetric _ RB) : Symmetric (RA*RB). +Proof. firstorder. Qed. + +Instance RelProd_Transitive {A B}(RA:relation A)(RB:relation B) + `(Transitive _ RA, Transitive _ RB) : Transitive (RA*RB). +Proof. firstorder. Qed. + +Instance RelProd_Equivalence {A B}(RA:relation A)(RB:relation B) + `(Equivalence _ RA, Equivalence _ RB) : Equivalence (RA*RB). + +Lemma FstRel_ProdRel {A B}(RA:relation A) : + relation_equivalence (RA @@ fst) (RA*(fun _ _ : B => True)). +Proof. firstorder. Qed. + +Lemma SndRel_ProdRel {A B}(RB:relation B) : + relation_equivalence (RB @@ snd) ((fun _ _ : A =>True) * RB). +Proof. firstorder. Qed. + +Instance FstRel_sub {A B} (RA:relation A)(RB:relation B): + subrelation (RA*RB) (RA @@ fst). +Proof. firstorder. Qed. + +Instance SndRel_sub {A B} (RA:relation A)(RB:relation B): + subrelation (RA*RB) (RB @@ snd). +Proof. firstorder. Qed. + +Instance pair_compat { A B } (RA:relation A)(RB : relation B) : + Proper (RA==>RB==> RA*RB) pair. +Proof. firstorder. Qed. + + +Instance RelCompFun_compat {A B}(f:A->B)(R : relation B) + `(Proper _ (Ri==>Ri==>Ro) R) : + Proper (Ri@@f==>Ri@@f==>Ro) (R@@f)%signature. +Proof. unfold RelCompFun; firstorder. Qed. + +Hint Unfold RelProd RelCompFun. +Hint Extern 2 (RelProd _ _ _ _) => split. + diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v index 487b4fc32..f6d5ae1ac 100644 --- a/theories/FSets/FSetCompat.v +++ b/theories/FSets/FSetCompat.v @@ -209,11 +209,10 @@ Module Backport_Sets Qed. Definition compare : forall s s', Compare lt eq s s'. Proof. - intros s s'. generalize (M.compare_spec s s'). - destruct (M.compare s s'); simpl; intros. - constructor 2; auto. - constructor 1; auto. - constructor 3; auto. + intros s s'. + assert (H := M.compare_spec s s'). + destruct (M.compare s s'); [ apply EQ | apply LT | apply GT ]; + inversion H; auto. Defined. End Backport_Sets. @@ -407,7 +406,7 @@ Module Update_Sets | GT _ => Gt end. - Lemma compare_spec : forall s s', Cmp eq lt (compare s s') s s'. + Lemma compare_spec : forall s s', Cmp eq lt s s' (compare s s'). Proof. intros; unfold compare; destruct M.compare; auto. Qed. End Update_Sets. diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index bd1472330..b750edfc0 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -291,35 +291,23 @@ End BoolSpec. (** * [E.eq] and [Equal] are setoid equalities *) -Definition E_ST : Equivalence E.eq. +Instance E_ST : Equivalence E.eq. Proof. constructor ; red; [apply E.eq_refl|apply E.eq_sym|apply E.eq_trans]. Qed. -Definition Equal_ST : Equivalence Equal. +Instance Equal_ST : Equivalence Equal. Proof. constructor ; red; [apply eq_refl | apply eq_sym | apply eq_trans]. Qed. -Add Relation elt E.eq - reflexivity proved by E.eq_refl - symmetry proved by E.eq_sym - transitivity proved by E.eq_trans - as EltSetoid. - -Add Relation t Equal - reflexivity proved by eq_refl - symmetry proved by eq_sym - transitivity proved by eq_trans - as EqualSetoid. - -Add Morphism In with signature E.eq ==> Equal ==> iff as In_m. +Instance In_m : Proper (E.eq ==> Equal ==> iff) In. Proof. unfold Equal; intros x y H s s' H0. rewrite (In_eq_iff s H); auto. Qed. -Add Morphism is_empty : is_empty_m. +Instance is_empty_m : Proper (Equal==> Logic.eq) is_empty. Proof. unfold Equal; intros s s' H. generalize (is_empty_iff s)(is_empty_iff s'). @@ -336,12 +324,12 @@ destruct H1 as (_,H1). exact (H1 (refl_equal true) _ Ha). Qed. -Add Morphism Empty with signature Equal ==> iff as Empty_m. +Instance Empty_m : Proper (Equal ==> iff) Empty. Proof. -intros; do 2 rewrite is_empty_iff; rewrite H; intuition. +repeat red; intros; do 2 rewrite is_empty_iff; rewrite H; intuition. Qed. -Add Morphism mem : mem_m. +Instance mem_m : Proper (E.eq ==> Equal ==> Logic.eq) mem. Proof. unfold Equal; intros x y H s s' H0. generalize (H0 x); clear H0; rewrite (In_eq_iff s' H). @@ -349,7 +337,7 @@ generalize (mem_iff s x)(mem_iff s' y). destruct (mem x s); destruct (mem y s'); intuition. Qed. -Add Morphism singleton : singleton_m. +Instance singleton_m : Proper (E.eq ==> Equal) singleton. Proof. unfold Equal; intros x y H a. do 2 rewrite singleton_iff; split; intros. @@ -357,42 +345,42 @@ apply E.eq_trans with x; auto. apply E.eq_trans with y; auto. Qed. -Add Morphism add : add_m. +Instance add_m : Proper (E.eq==>Equal==>Equal) add. Proof. unfold Equal; intros x y H s s' H0 a. do 2 rewrite add_iff; rewrite H; rewrite H0; intuition. Qed. -Add Morphism remove : remove_m. +Instance remove_m : Proper (E.eq==>Equal==>Equal) remove. Proof. unfold Equal; intros x y H s s' H0 a. do 2 rewrite remove_iff; rewrite H; rewrite H0; intuition. Qed. -Add Morphism union : union_m. +Instance union_m : Proper (Equal==>Equal==>Equal) union. Proof. unfold Equal; intros s s' H s'' s''' H0 a. do 2 rewrite union_iff; rewrite H; rewrite H0; intuition. Qed. -Add Morphism inter : inter_m. +Instance inter_m : Proper (Equal==>Equal==>Equal) inter. Proof. unfold Equal; intros s s' H s'' s''' H0 a. do 2 rewrite inter_iff; rewrite H; rewrite H0; intuition. Qed. -Add Morphism diff : diff_m. +Instance diff_m : Proper (Equal==>Equal==>Equal) diff. Proof. unfold Equal; intros s s' H s'' s''' H0 a. do 2 rewrite diff_iff; rewrite H; rewrite H0; intuition. Qed. -Add Morphism Subset with signature Equal ==> Equal ==> iff as Subset_m. +Instance Subset_m : Proper (Equal==>Equal==>iff) Subset. Proof. unfold Equal, Subset; firstorder. Qed. -Add Morphism subset : subset_m. +Instance subset_m : Proper (Equal ==> Equal ==> Logic.eq) subset. Proof. intros s s' H s'' s''' H0. generalize (subset_iff s s'') (subset_iff s' s'''). @@ -401,7 +389,7 @@ rewrite H in H1; rewrite H0 in H1; intuition. rewrite H in H1; rewrite H0 in H1; intuition. Qed. -Add Morphism equal : equal_m. +Instance equal_m : Proper (Equal ==> Equal ==> Logic.eq) equal. Proof. intros s s' H s'' s''' H0. generalize (equal_iff s s'') (equal_iff s' s'''). diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index 70be28f87..408461a25 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -570,7 +570,7 @@ Fixpoint isok s := (** * Correctness proofs *) (* Module Proofs. *) - Module MX := OrderedTypeFacts X. + Module Import MX := OrderedTypeFacts X. Hint Resolve MX.lt_trans. (** * Automation and dedicated tactics *) @@ -631,7 +631,7 @@ Lemma ltb_tree_iff : forall x s, lt_tree x s <-> ltb_tree x s = true. Proof. induction s as [|l IHl y r IHr h]; simpl. unfold lt_tree; intuition_in. - MX.elim_compare x y; intros. + elim_compare x y. split; intros; try discriminate. assert (X.lt y x) by auto. order. split; intros; try discriminate. assert (X.lt y x) by auto. order. rewrite !andb_true_iff, <-IHl, <-IHr. @@ -642,7 +642,7 @@ Lemma gtb_tree_iff : forall x s, gt_tree x s <-> gtb_tree x s = true. Proof. induction s as [|l IHl y r IHr h]; simpl. unfold gt_tree; intuition_in. - MX.elim_compare x y; intros. + elim_compare x y. split; intros; try discriminate. assert (X.lt x y) by auto. order. rewrite !andb_true_iff, <-IHl, <-IHr. unfold gt_tree; intuition_in; order. @@ -753,7 +753,7 @@ Functional Scheme union_ind := Induction for union Sort Prop. Ltac induct s x := induction s as [|l IHl x' r IHr h]; simpl; intros; - [|MX.elim_compare x x'; intros; inv]. + [|elim_compare x x'; intros; inv]. (** * Notations and helper lemma about pairs and triples *) @@ -794,7 +794,7 @@ Qed. Lemma mem_spec : forall s x `{Ok s}, mem x s = true <-> InT x s. Proof. split. - induct s x; auto; discriminate. + induct s x; auto; try discriminate. induct s x; intuition_in; order. Qed. @@ -1098,7 +1098,7 @@ Proof. assert (~X.lt x' x). apply min_elt_spec2 with s; auto. rewrite H; auto using min_elt_spec1. - MX.elim_compare x x'; intuition. + elim_compare x x'; intuition. Qed. @@ -1274,7 +1274,7 @@ Proof. intuition_in. factornode _x0 _x1 _x2 _x3 as s2; destruct_split; inv. rewrite join_spec, IHt0, IHt1, split_spec1, split_spec2; auto with *. - MX.elim_compare y x1; intuition_in. + elim_compare y x1; intuition_in. Qed. Instance union_ok s1 s2 `(Ok s1, Ok s2) : Ok (union s1 s2). @@ -1316,7 +1316,8 @@ Proof. apply Hl; auto. constructor. apply Hr; auto. - apply MX.In_Inf; intros. + eapply InA_InfA; eauto with *. + intros. destruct (elements_spec1' r acc y0); intuition. intros. inversion_clear H. @@ -1333,7 +1334,7 @@ Hint Resolve elements_spec2. Lemma elements_spec2w : forall s `(Ok s), NoDupA X.eq (elements s). Proof. - auto. + intros. eapply SortA_NoDupA; eauto with *. Qed. Lemma elements_aux_cardinal : @@ -1586,7 +1587,7 @@ Proof. specialize (IHl2 H). specialize (IHr2 H). inv. - MX.elim_compare x1 x2; intros. + elim_compare x1 x2. rewrite H1 by auto; clear H1 IHl2 IHr2. unfold Subset. intuition_in. @@ -1617,7 +1618,7 @@ Proof. specialize (IHl2 H). specialize (IHr2 H). inv. - MX.elim_compare x1 x2; intros. + elim_compare x1 x2. rewrite H1 by auto; clear H1 IHl2 IHr2. unfold Subset. intuition_in. @@ -1645,7 +1646,7 @@ Proof. unfold Subset; intuition_in; try discriminate. assert (H': InT x1 Leaf) by auto; inversion H'. inv. - MX.elim_compare x1 x2; intros. + elim_compare x1 x2. rewrite <-andb_lazy_alt, andb_true_iff, IHl1, IHr1 by auto. clear IHl1 IHr1. @@ -1751,12 +1752,14 @@ Hint Unfold flip. (** Correctness of this comparison *) -Definition LCmp := Cmp L.eq L.lt. +Definition LCmp c x y := Cmp L.eq L.lt x y c. + +Hint Unfold LCmp. Lemma compare_end_Cmp : forall e2, LCmp (compare_end e2) nil (flatten_e e2). Proof. - destruct e2; simpl; auto. reflexivity. + destruct e2; simpl; constructor; auto. reflexivity. Qed. Lemma compare_more_Cmp : forall x1 cont x2 r2 e2 l, @@ -1764,8 +1767,7 @@ Lemma compare_more_Cmp : forall x1 cont x2 r2 e2 l, LCmp (compare_more x1 cont (More x2 r2 e2)) (x1::l) (flatten_e (More x2 r2 e2)). Proof. - simpl; intros; MX.elim_compare x1 x2; simpl; auto. - intros; apply L.cons_Cmp; auto. + simpl; intros; elim_compare x1 x2; simpl; auto. Qed. Lemma compare_cont_Cmp : forall s1 cont e2 l, @@ -1793,11 +1795,10 @@ Proof. Qed. Lemma compare_spec : forall s1 s2 `{Ok s1, Ok s2}, - Cmp eq lt (compare s1 s2) s1 s2. + Cmp eq lt s1 s2 (compare s1 s2). Proof. intros. - generalize (compare_Cmp s1 s2). - destruct (compare s1 s2); unfold LCmp, Cmp, flip; auto. + destruct (compare_Cmp s1 s2); constructor. rewrite eq_Leq; auto. intros; exists s1, s2; repeat split; auto. intros; exists s2, s1; repeat split; auto. @@ -1810,10 +1811,10 @@ Lemma equal_spec : forall s1 s2 `{Ok s1, Ok s2}, equal s1 s2 = true <-> eq s1 s2. Proof. unfold equal; intros s1 s2 B1 B2. -generalize (@compare_spec s1 s2 B1 B2). -destruct (compare s1 s2); simpl; split; intros E; auto; try discriminate. -rewrite E in H. elim (StrictOrder_Irreflexive s2); auto. -rewrite E in H. elim (StrictOrder_Irreflexive s2); auto. +destruct (@compare_spec s1 s2 B1 B2) as [H|H|H]; + split; intros H'; auto; try discriminate. +rewrite H' in H. elim (StrictOrder_Irreflexive s2); auto. +rewrite H' in H. elim (StrictOrder_Irreflexive s2); auto. Qed. End MakeRaw. diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v index 24eb77e62..49f436a01 100644 --- a/theories/MSets/MSetEqProperties.v +++ b/theories/MSets/MSetEqProperties.v @@ -858,8 +858,7 @@ intros. rewrite <- (fold_equal _ _ _ _ fc ft 0 _ _ H). rewrite <- (fold_equal _ _ _ _ gc gt 0 _ _ H). rewrite <- (fold_equal _ _ _ _ fgc fgt 0 _ _ H); auto. -intros; do 3 (rewrite (fold_add _ _ _);auto). -rewrite H0;simpl;omega. +intros; do 3 (rewrite fold_add; auto with *). do 3 rewrite fold_empty;auto. Qed. diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index 831ea0179..a011eb32e 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -29,7 +29,8 @@ [RawSets] via the use of a subset type (see (W)Raw2Sets below). *) -Require Export Bool OrderedType2 DecidableType2. +Require Export Bool SetoidList RelationClasses Morphisms + RelationPairs DecidableType2 OrderedType2 OrderedType2Facts. Set Implicit Arguments. Unset Strict Implicit. @@ -226,7 +227,7 @@ Module Type SetsOn (E : OrderedType). Variable s s': t. Variable x y : elt. - Parameter compare_spec : Cmp eq lt (compare s s') s s'. + Parameter compare_spec : Cmp eq lt s s' (compare s s'). (** Additional specification of [elements] *) Parameter elements_spec2 : sort E.lt (elements s). @@ -569,7 +570,7 @@ Module Type RawSets (E : OrderedType). Variable x y : elt. (** Specification of [compare] *) - Parameter compare_spec : forall `{Ok s, Ok s'}, Cmp eq lt (compare s s') s s'. + Parameter compare_spec : forall `{Ok s, Ok s'}, Cmp eq lt s s' (compare s s'). (** Additional specification of [elements] *) Parameter elements_spec2 : forall `{Ok s}, sort E.lt (elements s). @@ -604,11 +605,6 @@ Module Raw2SetsOn (O:OrderedType)(M:RawSets O) <: SetsOn O. (** Specification of [lt] *) Instance lt_strorder : StrictOrder lt. - Proof. - unfold lt; split; repeat red. - intros s; eapply StrictOrder_Irreflexive; eauto. - intros s s' s''; eapply StrictOrder_Transitive; eauto. - Qed. Instance lt_compat : Proper (eq==>eq==>iff) lt. Proof. @@ -623,10 +619,10 @@ Module Raw2SetsOn (O:OrderedType)(M:RawSets O) <: SetsOn O. Variable s s' s'' : t. Variable x y : elt. - Lemma compare_spec : Cmp eq lt (compare s s') s s'. + Lemma compare_spec : Cmp eq lt s s' (compare s s'). Proof. - generalize (@M.compare_spec s s' _ _). - unfold compare; destruct M.compare; auto. + assert (H:=@M.compare_spec s s' _ _). + unfold compare; destruct M.compare; inversion_clear H; auto. Qed. (** Additional specification of [elements] *) @@ -752,7 +748,7 @@ Module MakeSetOrdering (O:OrderedType)(Import M:IN O). left; split; auto. rewrite <- (EQ' x); auto. (* 2) Pre / Lex *) - elim_compare x x'; intros Hxx'. + elim_compare x x'. (* 2a) x=x' --> Pre *) destruct Lex' as (y & INy & LT & Be). exists y; split. @@ -781,16 +777,17 @@ Module MakeSetOrdering (O:OrderedType)(Import M:IN O). rewrite <- (EQ' y); auto. intros z Hz LTz; apply Be; auto. rewrite (EQ' z); auto; order. (* 4) Lex / Lex *) - elim_compare x x'; intros Hxx'. + elim_compare x x'. (* 4a) x=x' --> impossible *) destruct Lex as (y & INy & LT & Be). - rewrite Hxx' in LT; specialize (Be x' IN' LT); order. + setoid_replace x with x' in LT; auto. + specialize (Be x' IN' LT); order. (* 4b) x<x' --> Lex *) exists x; split. intros z Hz. rewrite <- (EQ' z) by order; auto. right; split; auto. destruct Lex as (y & INy & LT & Be). - elim_compare y x'; intros Hyx'. + elim_compare y x'. (* 4ba *) destruct Lex' as (y' & Iny' & LT' & Be'). exists y'; repeat split; auto. order. @@ -802,7 +799,7 @@ Module MakeSetOrdering (O:OrderedType)(Import M:IN O). rewrite <- (EQ' y); auto. intros z Hz LTz. apply Be; auto. rewrite (EQ' z); auto; order. (* 4bc*) - specialize (Be x' IN' Hyx'); order. + assert (O.lt x' x) by auto. order. (* 4c) x>x' --> Lex *) exists x'; split. intros z Hz. rewrite (EQ z) by order; auto. @@ -879,8 +876,8 @@ End MakeSetOrdering. Module MakeListOrdering (O:OrderedType). Module MO:=OrderedTypeFacts O. - Notation t := (list O.t). - Notation In := (InA O.eq). + Local Notation t := (list O.t). + Local Notation In := (InA O.eq). Definition eq s s' := forall x, In x s <-> In x s'. @@ -944,9 +941,9 @@ Module MakeListOrdering (O:OrderedType). Hint Resolve eq_cons. Lemma cons_Cmp : forall c x1 x2 l1 l2, O.eq x1 x2 -> - Cmp eq lt c l1 l2 -> Cmp eq lt c (x1::l1) (x2::l2). + Cmp eq lt l1 l2 c -> Cmp eq lt (x1::l1) (x2::l2) c. Proof. - destruct c; simpl; unfold flip; auto. + destruct c; simpl; inversion_clear 2; auto. Qed. Hint Resolve cons_Cmp. diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v index 471b43e24..28205e3f6 100644 --- a/theories/MSets/MSetList.v +++ b/theories/MSets/MSetList.v @@ -13,7 +13,7 @@ (** This file proposes an implementation of the non-dependant interface [MSetInterface.S] using strictly ordered list. *) -Require Export MSetInterface. +Require Export MSetInterface OrderedType2Facts OrderedType2Lists. Set Implicit Arguments. Unset Strict Implicit. @@ -206,6 +206,7 @@ End Ops. Module MakeRaw (X: OrderedType) <: RawSets X. Module Import MX := OrderedTypeFacts X. + Module Import ML := OrderedTypeLists X. Include Ops X. @@ -291,7 +292,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Proof. induction s; intros; inv; simpl. intuition. discriminate. inv. - elim_compare x a; intros; rewrite InA_cons; intuition; try order. + elim_compare x a; rewrite InA_cons; intuition; try order. discriminate. sort_inf_in. order. rewrite <- IHs; auto. @@ -303,7 +304,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Proof. simple induction s; simpl. intuition. - intros; elim_compare x a; intros; inv; intuition. + intros; elim_compare x a; inv; intuition. Qed. Hint Resolve add_inf. @@ -311,7 +312,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Proof. simple induction s; simpl. intuition. - intros; elim_compare x a; intros; inv; auto. + intros; elim_compare x a; inv; auto. Qed. Lemma add_spec : @@ -320,7 +321,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Proof. induction s; simpl; intros. intuition. inv; auto. - elim_compare x a; intros; inv; rewrite !InA_cons, ?IHs; intuition. + elim_compare x a; inv; rewrite !InA_cons, ?IHs; intuition. left; order. Qed. @@ -329,7 +330,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Proof. induction s; simpl. intuition. - intros; elim_compare x a; intros; inv; auto. + intros; elim_compare x a; inv; auto. apply Inf_lt with a; auto. Qed. Hint Resolve remove_inf. @@ -338,7 +339,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Proof. induction s; simpl. intuition. - intros; elim_compare x a; intros; inv; auto. + intros; elim_compare x a; inv; auto. Qed. Lemma remove_spec : @@ -347,7 +348,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Proof. induction s; simpl; intros. intuition; inv; auto. - elim_compare x a; intros; inv; rewrite !InA_cons, ?IHs; intuition; + elim_compare x a; inv; rewrite !InA_cons, ?IHs; intuition; try sort_inf_in; try order. Qed. @@ -454,7 +455,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. split; intros H. discriminate. assert (In x' nil) by (rewrite H; auto). inv. split; intros H. discriminate. assert (In x nil) by (rewrite <-H; auto). inv. inv. - elim_compare x x'; intros C; try discriminate. + elim_compare x x' as C; try discriminate. (* x=x' *) rewrite IH; auto. split; intros E y; specialize (E y). @@ -479,7 +480,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. split; try red; intros; auto. split; intros H. discriminate. assert (In x nil) by (apply H; auto). inv. split; try red; intros; auto. inv. - inv. elim_compare x x'; intros C. + inv. elim_compare x x' as C. (* x=x' *) rewrite IH; auto. split; intros S y; specialize (S y). @@ -750,51 +751,6 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Instance In_compat : Proper (X.eq==>eq==> iff) In. Proof. repeat red; intros; rewrite H, H0; auto. Qed. -(* - Module IN <: IN X. - Definition t := t. - Definition In := In. - Instance In_compat : Proper (X.eq==>eq==>iff) In. - Proof. - intros x x' Ex s s' Es. subst. rewrite Ex; intuition. - Qed. - Definition Equal := Equal. - Definition Empty := Empty. - End IN. - Include MakeSetOrdering X IN. - - Lemma Ok_Above_Add : forall x s, Ok (x::s) -> Above x s /\ Add x s (x::s). - Proof. - intros. - inver Ok. - split. - intros y Hy. eapply Sort_Inf_In; eauto. - red. intuition. inver In; auto. rewrite <- H2; left; auto. - right; auto. - Qed. - - Lemma compare_spec : - forall (s s' : t) (Hs : Ok s) (Hs' : Ok s'), Cmp eq lt (compare s s') s s'. - Proof. - induction s as [|x s IH]; intros [|x' s'] Hs Hs'; simpl; intuition. - destruct (Ok_Above_Add Hs'). - eapply lt_empty_l; eauto. intros y Hy. inver InA. - destruct (Ok_Above_Add Hs). - eapply lt_empty_l; eauto. intros y Hy. inver InA. - destruct (Ok_Above_Add Hs); destruct (Ok_Above_Add Hs'). - inver Ok. unfold Ok in IH. specialize (IH s'). - elim_compare x x'; intros. - destruct (compare s s'); unfold Cmp, flip in IH; auto. - intro y; split; intros; inver InA; try (left; order). - right; rewrite <- IH; auto. - right; rewrite IH; auto. - eapply (@lt_add_eq x x'); eauto. - eapply (@lt_add_eq x' x); eauto. - eapply (@lt_add_lt x x'); eauto. - eapply (@lt_add_lt x' x); eauto. - Qed. -*) - Module L := MakeListOrdering X. Definition eq := L.eq. Definition eq_equiv := L.eq_equiv. @@ -834,24 +790,20 @@ Module MakeRaw (X: OrderedType) <: RawSets X. split; auto. transitivity s4; auto. Qed. - Lemma compare_spec_aux : forall s s', Cmp eq L.lt (compare s s') s s'. + Lemma compare_spec_aux : forall s s', Cmp eq L.lt s s' (compare s s'). Proof. induction s as [|x s IH]; intros [|x' s']; simpl; intuition. - red; auto. - elim_compare x x'; intros; auto. - specialize (IH s'). - destruct (compare s s'); unfold Cmp, flip, eq in IH; auto. - apply L.eq_cons; auto. + elim_compare x x'; auto. Qed. Lemma compare_spec : forall s s', Ok s -> Ok s' -> - Cmp eq lt (compare s s') s s'. + Cmp eq lt s s' (compare s s'). Proof. intros s s' Hs Hs'. generalize (compare_spec_aux s s'). - destruct (compare s s'); unfold Cmp, flip in *; auto. - exists s, s'; repeat split; auto using @ok. - exists s', s; repeat split; auto using @ok. + destruct (compare s s'); inversion_clear 1; auto. + apply Cmp_lt. exists s, s'; repeat split; auto using @ok. + apply Cmp_gt. exists s', s; repeat split; auto using @ok. Qed. End MakeRaw. diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v index ab9c69afb..59fbcf49d 100644 --- a/theories/MSets/MSetProperties.v +++ b/theories/MSets/MSetProperties.v @@ -17,7 +17,7 @@ [Equal s s'] instead of [equal s s'=true], etc. *) Require Export MSetInterface. -Require Import DecidableTypeEx MSetFacts MSetDecide. +Require Import DecidableTypeEx OrderedType2Lists MSetFacts MSetDecide. Set Implicit Arguments. Unset Strict Implicit. @@ -762,7 +762,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). rewrite (cardinal_2 (s:=remove x s') (s':=s') (x:=x)); eauto with set. Qed. - Add Morphism cardinal : cardinal_m. + Instance cardinal_m : Proper (Equal==>Logic.eq) cardinal. Proof. exact Equal_cardinal. Qed. @@ -908,7 +908,8 @@ Module Properties := WProperties. invalid for Weak Sets. *) Module OrdProperties (M:Sets). - Module ME:=OrderedTypeFacts(M.E). + Module Import ME:=OrderedTypeFacts(M.E). + Module Import ML:=OrderedTypeLists(M.E). Module Import P := Properties M. Import FM. Import M.E. @@ -934,13 +935,13 @@ Module OrdProperties (M:Sets). Lemma gtb_1 : forall x y, gtb x y = true <-> E.lt y x. Proof. - intros; rewrite <- ME.compare_gt_iff. unfold gtb. + intros; rewrite <- compare_gt_iff. unfold gtb. destruct E.compare; intuition; try discriminate. Qed. Lemma leb_1 : forall x y, leb x y = true <-> ~E.lt y x. Proof. - intros; rewrite <- ME.compare_gt_iff. unfold leb, gtb. + intros; rewrite <- compare_gt_iff. unfold leb, gtb. destruct E.compare; intuition; try discriminate. Qed. @@ -963,9 +964,9 @@ Module OrdProperties (M:Sets). intros. rewrite gtb_1 in H. assert (~E.lt y x). - unfold gtb in *; ME.elim_compare x y; intuition; - try discriminate; ME.order. - ME.order. + unfold gtb in *; elim_compare x y; intuition; + try discriminate; order. + order. Qed. Lemma elements_Add : forall s s' x, ~In x s -> Add x s s' -> @@ -977,29 +978,29 @@ Module OrdProperties (M:Sets). apply (@filter_sort _ E.eq); auto with *; eauto with *. constructor; auto. apply (@filter_sort _ E.eq); auto with *; eauto with *. - rewrite ME.Inf_alt by (apply (@filter_sort _ E.eq); eauto with *). + rewrite Inf_alt by (apply (@filter_sort _ E.eq); eauto with *). intros. rewrite filter_InA in H1; auto with *; destruct H1. rewrite leb_1 in H2. rewrite <- elements_iff in H1. assert (~E.eq x y). contradict H; rewrite H; auto. - ME.order. + order. intros. rewrite filter_InA in H1; auto with *; destruct H1. rewrite gtb_1 in H3. inversion_clear H2. - ME.order. + order. rewrite filter_InA in H4; auto with *; destruct H4. rewrite leb_1 in H4. - ME.order. + order. red; intros a. rewrite InA_app_iff, InA_cons, !filter_InA, <-!elements_iff, leb_1, gtb_1, (H0 a) by (auto with *). intuition. - ME.elim_compare a x; intuition. + elim_compare a x; intuition. right; right; split; auto. - ME.order. + order. Qed. Definition Above x s := forall y, In y s -> E.lt y x. @@ -1056,7 +1057,7 @@ Module OrdProperties (M:Sets). inversion H0; auto. red; intros. rewrite remove_iff in H0; destruct H0. - generalize (@max_elt_spec2 s e y H H0); ME.order. + generalize (@max_elt_spec2 s e y H H0); order. assert (H0:=max_elt_spec3 H). rewrite cardinal_Empty in H0; rewrite H0 in Heqn; inversion Heqn. @@ -1077,7 +1078,7 @@ Module OrdProperties (M:Sets). inversion H0; auto. red; intros. rewrite remove_iff in H0; destruct H0. - generalize (@min_elt_spec2 s e y H H0); ME.order. + generalize (@min_elt_spec2 s e y H H0); order. assert (H0:=min_elt_spec3 H). rewrite cardinal_Empty in H0; auto; rewrite H0 in Heqn; inversion Heqn. diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index e02f2817c..813956332 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -140,6 +140,14 @@ Definition Nmax (n n' : N) := match Ncompare n n' with | Gt => n end. +(** Decidability of equality. *) + +Definition N_eq_dec : forall n m : N, { n = m } + { n <> m }. +Proof. + decide equality. + apply positive_eq_dec. +Defined. + (** convenient induction principles *) Lemma N_ind_double : diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index 0a1cd9ab4..20cfb43a3 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -751,6 +751,13 @@ Proof. destruct (Pcompare_not_Eq p q) as (_,H'); elim H'; auto. Qed. +Lemma Pcompare_eq_iff : forall p q:positive, (p ?= q) Eq = Eq <-> p = q. +Proof. + split. + apply Pcompare_Eq_eq. + intros; subst; apply Pcompare_refl. +Qed. + Lemma Pcompare_Gt_Lt : forall p q:positive, (p ?= q) Gt = Lt -> (p ?= q) Eq = Lt. Proof. diff --git a/theories/NArith/NOrderedType.v b/theories/NArith/NOrderedType.v new file mode 100644 index 000000000..8f69cd656 --- /dev/null +++ b/theories/NArith/NOrderedType.v @@ -0,0 +1,72 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import BinNat + DecidableType2 OrderedType2 OrderedType2Facts. + +Local Open Scope N_scope. + +(** * DecidableType structure for [N] binary natural numbers *) + +Module N_as_MiniDT <: MiniDecidableType. + Definition t := N. + Definition eq_dec := N_eq_dec. +End N_as_MiniDT. + +Module N_as_DT <: UsualDecidableType := Make_UDT N_as_MiniDT. + +(** Note that [N_as_DT] can also be seen as a [DecidableType] + and a [DecidableTypeOrig]. *) + + + +(** * OrderedType structure for [N] numbers *) + +Module N_as_OT <: OrderedTypeFull. + Include N_as_DT. + Definition lt := Nlt. + Definition le := Nle. + Definition compare := Ncompare. + + Instance lt_strorder : StrictOrder Nlt. + Proof. split; [ exact Nlt_irrefl | exact Nlt_trans ]. Qed. + + Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) Nlt. + Proof. repeat red; intros; subst; auto. Qed. + + Lemma le_lteq : forall x y, x <= y <-> x < y \/ x=y. + Proof. + unfold Nle, Nlt; intros. rewrite <- Ncompare_eq_correct. + destruct (x ?= y); intuition; discriminate. + Qed. + + Lemma compare_spec : forall x y, Cmp eq lt x y (Ncompare x y). + Proof. + intros. + destruct (Ncompare x y) as [ ]_eqn; constructor; auto. + apply Ncompare_Eq_eq; auto. + apply Ngt_Nlt; auto. + Qed. + +End N_as_OT. + +(* Note that [N_as_OT] can also be seen as a [UsualOrderedType] + and a [OrderedType] (and also as a [DecidableType]). *) + + + +(** * An [order] tactic for [N] numbers *) + +Module NOrder := OTF_to_OrderTac N_as_OT. +Ltac n_order := + change (@eq N) with NOrder.OrderElts.eq in *; + NOrder.order. + +(** Note that [n_order] is domain-agnostic: it will not prove + [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *) + diff --git a/theories/NArith/Nminmax.v b/theories/NArith/Nminmax.v new file mode 100644 index 000000000..86e6b609f --- /dev/null +++ b/theories/NArith/Nminmax.v @@ -0,0 +1,226 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import OrderedType2 BinNat Nnat NOrderedType GenericMinMax. + +(** * Maximum and Minimum of two [N] numbers *) + +Local Open Scope N_scope. + +(** The functions [Nmax] and [Nmin] implement indeed + a maximum and a minimum *) + +Lemma Nmax_spec : forall x y, + (x<y /\ Nmax x y = y) \/ (y<=x /\ Nmax x y = x). +Proof. + unfold Nlt, Nle, Nmax. intros. + generalize (Ncompare_eq_correct x y). + rewrite <- (Ncompare_antisym x y). + destruct (x ?= y); simpl; auto; right; intuition; discriminate. +Qed. + +Lemma Nmin_spec : forall x y, + (x<y /\ Nmin x y = x) \/ (y<=x /\ Nmin x y = y). +Proof. + unfold Nlt, Nle, Nmin. intros. + generalize (Ncompare_eq_correct x y). + rewrite <- (Ncompare_antisym x y). + destruct (x ?= y); simpl; auto; right; intuition; discriminate. +Qed. + +Module NHasMinMax <: HasMinMax N_as_OT. + Definition max := Nmax. + Definition min := Nmin. + Definition max_spec := Nmax_spec. + Definition min_spec := Nmin_spec. +End NHasMinMax. + +(** We obtain hence all the generic properties of max and min. *) + +Module Import NMinMaxProps := MinMaxProperties N_as_OT NHasMinMax. + +(** For some generic properties, we can have nicer statements here, + since underlying equality is Leibniz. *) + +Lemma Nmax_case_strong : forall n m (P:N -> Type), + (m<=n -> P n) -> (n<=m -> P m) -> P (Nmax n m). +Proof. intros; apply max_case_strong; auto. congruence. Defined. + +Lemma Nmax_case : forall n m (P:N -> Type), + P n -> P m -> P (Nmax n m). +Proof. intros. apply Nmax_case_strong; auto. Defined. + +Lemma Nmax_monotone: forall f, + (Proper (Nle ==> Nle) f) -> + forall x y, Nmax (f x) (f y) = f (Nmax x y). +Proof. intros; apply max_monotone; auto. congruence. Qed. + +Lemma Nmin_case_strong : forall n m (P:N -> Type), + (m<=n -> P m) -> (n<=m -> P n) -> P (Nmin n m). +Proof. intros; apply min_case_strong; auto. congruence. Defined. + +Lemma Nmin_case : forall n m (P:N -> Type), + P n -> P m -> P (Nmin n m). +Proof. intros. apply Nmin_case_strong; auto. Defined. + +Lemma Nmin_monotone: forall f, + (Proper (Nle ==> Nle) f) -> + forall x y, Nmin (f x) (f y) = f (Nmin x y). +Proof. intros; apply min_monotone; auto. congruence. Qed. + +Lemma Nmax_min_antimonotone : forall f, + Proper (Nle==>Nge) f -> + forall x y, Nmax (f x) (f y) == f (Nmin x y). +Proof. + intros f H. apply max_min_antimonotone. congruence. + intros x x' Hx. red. specialize (H _ _ Hx). clear Hx. + unfold Nle, Nge in *; contradict H. rewrite <- Ncompare_antisym, H; auto. +Qed. + +Lemma Nmin_max_antimonotone : forall f, + Proper (Nle==>Nge) f -> + forall x y, Nmin (f x) (f y) == f (Nmax x y). +Proof. + intros f H. apply min_max_antimonotone. congruence. + intros z z' Hz; red. specialize (H _ _ Hz). clear Hz. + unfold Nle, Nge in *. contradict H. rewrite <- Ncompare_antisym, H; auto. +Qed. + +(** For the other generic properties, we make aliases, + since otherwise SearchAbout misses some of them + (bad interaction with an Include). + See GenericMinMax (or SearchAbout) for the statements. *) + +Definition Nmax_spec_le := max_spec_le. +Definition Nmax_dec := max_dec. +Definition Nmax_unicity := max_unicity. +Definition Nmax_unicity_ext := max_unicity_ext. +Definition Nmax_id := max_id. +Notation Nmax_idempotent := Nmax_id (only parsing). +Definition Nmax_assoc := max_assoc. +Definition Nmax_comm := max_comm. +Definition Nmax_l := max_l. +Definition Nmax_r := max_r. +Definition Nle_max_l := le_max_l. +Definition Nle_max_r := le_max_r. +Definition Nmax_le := max_le. +Definition Nmax_le_iff := max_le_iff. +Definition Nmax_lt_iff := max_lt_iff. +Definition Nmax_lub_l := max_lub_l. +Definition Nmax_lub_r := max_lub_r. +Definition Nmax_lub := max_lub. +Definition Nmax_lub_iff := max_lub_iff. +Definition Nmax_lub_lt := max_lub_lt. +Definition Nmax_lub_lt_iff := max_lub_lt_iff. +Definition Nmax_le_compat_l := max_le_compat_l. +Definition Nmax_le_compat_r := max_le_compat_r. +Definition Nmax_le_compat := max_le_compat. + +Definition Nmin_spec_le := min_spec_le. +Definition Nmin_dec := min_dec. +Definition Nmin_unicity := min_unicity. +Definition Nmin_unicity_ext := min_unicity_ext. +Definition Nmin_id := min_id. +Notation Nmin_idempotent := Nmin_id (only parsing). +Definition Nmin_assoc := min_assoc. +Definition Nmin_comm := min_comm. +Definition Nmin_l := min_l. +Definition Nmin_r := min_r. +Definition Nle_min_l := le_min_l. +Definition Nle_min_r := le_min_r. +Definition Nmin_le := min_le. +Definition Nmin_le_iff := min_le_iff. +Definition Nmin_lt_iff := min_lt_iff. +Definition Nmin_glb_l := min_glb_l. +Definition Nmin_glb_r := min_glb_r. +Definition Nmin_glb := min_glb. +Definition Nmin_glb_iff := min_glb_iff. +Definition Nmin_glb_lt := min_glb_lt. +Definition Nmin_glb_lt_iff := min_glb_lt_iff. +Definition Nmin_le_compat_l := min_le_compat_l. +Definition Nmin_le_compat_r := min_le_compat_r. +Definition Nmin_le_compat := min_le_compat. + +Definition Nmin_max_absorption := min_max_absorption. +Definition Nmax_min_absorption := max_min_absorption. +Definition Nmax_min_distr := max_min_distr. +Definition Nmin_max_distr := min_max_distr. +Definition Nmax_min_modular := max_min_modular. +Definition Nmin_max_modular := min_max_modular. +Definition Nmax_min_disassoc := max_min_disassoc. + + + +(** * Properties specific to the [positive] domain *) + +(** Simplifications *) + +Lemma Nmax_0_l : forall n, Nmax 0 n = n. +Proof. + intros. unfold Nmax. rewrite <- Ncompare_antisym. generalize (Ncompare_0 n). + destruct (n ?= 0); intuition. +Qed. + +Lemma Nmax_0_r : forall n, Nmax n 0 = n. +Proof. intros. rewrite max_comm. apply Nmax_0_l. Qed. + +Lemma Nmin_0_l : forall n, Nmin 0 n = 0. +Proof. + intros. unfold Nmin. rewrite <- Ncompare_antisym. generalize (Ncompare_0 n). + destruct (n ?= 0); intuition. +Qed. + +Lemma Nmin_0_r : forall n, Nmin n 0 = 0. +Proof. intros. rewrite min_comm. apply Nmin_0_l. Qed. + +(** Compatibilities (consequences of monotonicity) *) + +Lemma Nsucc_max_distr : + forall n m, Nsucc (Nmax n m) = Nmax (Nsucc n) (Nsucc m). +Proof. + intros. symmetry. apply Nmax_monotone. + intros x x'. unfold Nle. + rewrite 2 nat_of_Ncompare, 2 nat_of_Nsucc. + simpl; auto. +Qed. + +Lemma Nsucc_min_distr : forall n m, Nsucc (Nmin n m) = Nmin (Nsucc n) (Nsucc m). +Proof. + intros. symmetry. apply Nmin_monotone. + intros x x'. unfold Nle. + rewrite 2 nat_of_Ncompare, 2 nat_of_Nsucc. + simpl; auto. +Qed. + +Lemma Nplus_max_distr_l : forall n m p, Nmax (p + n) (p + m) = p + Nmax n m. +Proof. + intros. apply Nmax_monotone. + intros x x'. unfold Nle. + rewrite 2 nat_of_Ncompare, 2 nat_of_Nplus. + rewrite <- 2 Compare_dec.nat_compare_le. auto with arith. +Qed. + +Lemma Nplus_max_distr_r : forall n m p, Nmax (n + p) (m + p) = Nmax n m + p. +Proof. + intros. rewrite (Nplus_comm n p), (Nplus_comm m p), (Nplus_comm _ p). + apply Nplus_max_distr_l. +Qed. + +Lemma Nplus_min_distr_l : forall n m p, Nmin (p + n) (p + m) = p + Nmin n m. +Proof. + intros. apply Nmin_monotone. + intros x x'. unfold Nle. + rewrite 2 nat_of_Ncompare, 2 nat_of_Nplus. + rewrite <- 2 Compare_dec.nat_compare_le. auto with arith. +Qed. + +Lemma Nplus_min_distr_r : forall n m p, Nmin (n + p) (m + p) = Nmin n m + p. +Proof. + intros. rewrite (Nplus_comm n p), (Nplus_comm m p), (Nplus_comm _ p). + apply Nplus_min_distr_l. +Qed. diff --git a/theories/NArith/POrderedType.v b/theories/NArith/POrderedType.v new file mode 100644 index 000000000..2f89b0e68 --- /dev/null +++ b/theories/NArith/POrderedType.v @@ -0,0 +1,73 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import BinPos + DecidableType2 OrderedType2 OrderedType2Facts. + +Local Open Scope positive_scope. + +(** * DecidableType structure for [positive] numbers *) + +Module Positive_as_MiniDT <: MiniDecidableType. + Definition t := positive. + Definition eq_dec := positive_eq_dec. +End Positive_as_MiniDT. + +Module Positive_as_DT <: UsualDecidableType := Make_UDT Positive_as_MiniDT. + +(** Note that [Positive_as_DT] can also be seen as a [DecidableType] + and a [DecidableTypeOrig]. *) + + + +(** * OrderedType structure for [positive] numbers *) + +Module Positive_as_OT <: OrderedTypeFull. + Include Positive_as_DT. + Definition lt := Plt. + Definition le := Ple. + Definition compare p q := Pcompare p q Eq. + + Instance lt_strorder : StrictOrder Plt. + Proof. split; [ exact Plt_irrefl | exact Plt_trans ]. Qed. + + Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) Plt. + Proof. repeat red; intros; subst; auto. Qed. + + Lemma le_lteq : forall x y, x <= y <-> x < y \/ x=y. + Proof. + unfold Ple, Plt. intros. + rewrite <- Pcompare_eq_iff. + destruct (Pcompare x y Eq); intuition; discriminate. + Qed. + + Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y). + Proof. + intros; unfold compare. + destruct (Pcompare x y Eq) as [ ]_eqn; constructor. + apply Pcompare_Eq_eq; auto. + auto. + apply ZC1; auto. + Qed. + +End Positive_as_OT. + +(* Note that [Positive_as_OT] can also be seen as a [UsualOrderedType] + and a [OrderedType] (and also as a [DecidableType]). *) + + + +(** * An [order] tactic for positive numbers *) + +Module PositiveOrder := OTF_to_OrderTac Positive_as_OT. +Ltac p_order := + change (@eq positive) with PositiveOrder.OrderElts.eq in *; + PositiveOrder.order. + +(** Note that [p_order] is domain-agnostic: it will not prove + [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *) diff --git a/theories/NArith/Pminmax.v b/theories/NArith/Pminmax.v new file mode 100644 index 000000000..18008d18d --- /dev/null +++ b/theories/NArith/Pminmax.v @@ -0,0 +1,225 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import OrderedType2 BinPos Pnat POrderedType GenericMinMax. + +(** * Maximum and Minimum of two positive numbers *) + +Local Open Scope positive_scope. + +(** The functions [Pmax] and [Pmin] implement indeed + a maximum and a minimum *) + +Lemma Pmax_spec : forall x y, + (x<y /\ Pmax x y = y) \/ (y<=x /\ Pmax x y = x). +Proof. + unfold Plt, Ple, Pmax. intros. + generalize (Pcompare_eq_iff x y). rewrite (ZC4 y x). + destruct ((x ?= y) Eq); simpl; auto; right; intuition; discriminate. +Qed. + +Lemma Pmin_spec : forall x y, + (x<y /\ Pmin x y = x) \/ (y<=x /\ Pmin x y = y). +Proof. + unfold Plt, Ple, Pmin. intros. + generalize (Pcompare_eq_iff x y). rewrite (ZC4 y x). + destruct ((x ?= y) Eq); simpl; auto; right; intuition; discriminate. +Qed. + +Module PositiveHasMinMax <: HasMinMax Positive_as_OT. + Definition max := Pmax. + Definition min := Pmin. + Definition max_spec := Pmax_spec. + Definition min_spec := Pmin_spec. +End PositiveHasMinMax. + +(** We obtain hence all the generic properties of max and min. *) + +Module Import NatMinMaxProps := + MinMaxProperties Positive_as_OT PositiveHasMinMax. + + +(** For some generic properties, we can have nicer statements here, + since underlying equality is Leibniz. *) + +Lemma Pmax_case_strong : forall n m (P:positive -> Type), + (m<=n -> P n) -> (n<=m -> P m) -> P (Pmax n m). +Proof. intros; apply max_case_strong; auto. congruence. Defined. + +Lemma Pmax_case : forall n m (P:positive -> Type), + P n -> P m -> P (Pmax n m). +Proof. intros. apply Pmax_case_strong; auto. Defined. + +Lemma Pmax_monotone: forall f, + (Proper (Ple ==> Ple) f) -> + forall x y, Pmax (f x) (f y) = f (Pmax x y). +Proof. intros; apply max_monotone; auto. congruence. Qed. + +Lemma Pmin_case_strong : forall n m (P:positive -> Type), + (m<=n -> P m) -> (n<=m -> P n) -> P (Pmin n m). +Proof. intros; apply min_case_strong; auto. congruence. Defined. + +Lemma Pmin_case : forall n m (P:positive -> Type), + P n -> P m -> P (Pmin n m). +Proof. intros. apply Pmin_case_strong; auto. Defined. + +Lemma Pmin_monotone: forall f, + (Proper (Ple ==> Ple) f) -> + forall x y, Pmin (f x) (f y) = f (Pmin x y). +Proof. intros; apply min_monotone; auto. congruence. Qed. + +Lemma Pmax_min_antimonotone : forall f, + Proper (Ple==>Pge) f -> + forall x y, Pmax (f x) (f y) == f (Pmin x y). +Proof. + intros f H. apply max_min_antimonotone. congruence. + intros z z' Hz; red. specialize (H _ _ Hz). clear Hz. + unfold Ple, Pge in *. contradict H. rewrite ZC4, H; auto. +Qed. + +Lemma Pmin_max_antimonotone : forall f, + Proper (Ple==>Pge) f -> + forall x y, Pmin (f x) (f y) == f (Pmax x y). +Proof. + intros f H. apply min_max_antimonotone. congruence. + intros z z' Hz; red. specialize (H _ _ Hz). clear Hz. + unfold Ple, Pge in *. contradict H. rewrite ZC4, H; auto. +Qed. + +(** For the other generic properties, we make aliases, + since otherwise SearchAbout misses some of them + (bad interaction with an Include). + See GenericMinMax (or SearchAbout) for the statements. *) + +Definition Pmax_spec_le := max_spec_le. +Definition Pmax_dec := max_dec. +Definition Pmax_unicity := max_unicity. +Definition Pmax_unicity_ext := max_unicity_ext. +Definition Pmax_id := max_id. +Notation Pmax_idempotent := Pmax_id (only parsing). +Definition Pmax_assoc := max_assoc. +Definition Pmax_comm := max_comm. +Definition Pmax_l := max_l. +Definition Pmax_r := max_r. +Definition Ple_max_l := le_max_l. +Definition Ple_max_r := le_max_r. +Definition Pmax_le := max_le. +Definition Pmax_le_iff := max_le_iff. +Definition Pmax_lt_iff := max_lt_iff. +Definition Pmax_lub_l := max_lub_l. +Definition Pmax_lub_r := max_lub_r. +Definition Pmax_lub := max_lub. +Definition Pmax_lub_iff := max_lub_iff. +Definition Pmax_lub_lt := max_lub_lt. +Definition Pmax_lub_lt_iff := max_lub_lt_iff. +Definition Pmax_le_compat_l := max_le_compat_l. +Definition Pmax_le_compat_r := max_le_compat_r. +Definition Pmax_le_compat := max_le_compat. + +Definition Pmin_spec_le := min_spec_le. +Definition Pmin_dec := min_dec. +Definition Pmin_unicity := min_unicity. +Definition Pmin_unicity_ext := min_unicity_ext. +Definition Pmin_id := min_id. +Notation Pmin_idempotent := Pmin_id (only parsing). +Definition Pmin_assoc := min_assoc. +Definition Pmin_comm := min_comm. +Definition Pmin_l := min_l. +Definition Pmin_r := min_r. +Definition Ple_min_l := le_min_l. +Definition Ple_min_r := le_min_r. +Definition Pmin_le := min_le. +Definition Pmin_le_iff := min_le_iff. +Definition Pmin_lt_iff := min_lt_iff. +Definition Pmin_glb_l := min_glb_l. +Definition Pmin_glb_r := min_glb_r. +Definition Pmin_glb := min_glb. +Definition Pmin_glb_iff := min_glb_iff. +Definition Pmin_glb_lt := min_glb_lt. +Definition Pmin_glb_lt_iff := min_glb_lt_iff. +Definition Pmin_le_compat_l := min_le_compat_l. +Definition Pmin_le_compat_r := min_le_compat_r. +Definition Pmin_le_compat := min_le_compat. + +Definition Pmin_max_absorption := min_max_absorption. +Definition Pmax_min_absorption := max_min_absorption. +Definition Pmax_min_distr := max_min_distr. +Definition Pmin_max_distr := min_max_distr. +Definition Pmax_min_modular := max_min_modular. +Definition Pmin_max_modular := min_max_modular. +Definition Pmax_min_disassoc := max_min_disassoc. + + +(** * Properties specific to the [positive] domain *) + +(** Simplifications *) + +Lemma Pmax_1_l : forall n, Pmax 1 n = n. +Proof. + intros. unfold Pmax. rewrite ZC4. generalize (Pcompare_1 n). + destruct (n ?= 1); intuition. +Qed. + +Lemma Pmax_1_r : forall n, Pmax n 1 = n. +Proof. intros. rewrite max_comm. apply Pmax_1_l. Qed. + +Lemma Pmin_1_l : forall n, Pmin 1 n = 1. +Proof. + intros. unfold Pmin. rewrite ZC4. generalize (Pcompare_1 n). + destruct (n ?= 1); intuition. +Qed. + +Lemma Pmin_1_r : forall n, Pmin n 1 = 1. +Proof. intros. rewrite min_comm. apply Pmin_1_l. Qed. + +(** Compatibilities (consequences of monotonicity) *) + +Lemma Psucc_max_distr : + forall n m, Psucc (Pmax n m) = Pmax (Psucc n) (Psucc m). +Proof. + intros. symmetry. apply Pmax_monotone. + intros x x'. unfold Ple. + rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_succ_morphism. + simpl; auto. +Qed. + +Lemma Psucc_min_distr : forall n m, Psucc (Pmin n m) = Pmin (Psucc n) (Psucc m). +Proof. + intros. symmetry. apply Pmin_monotone. + intros x x'. unfold Ple. + rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_succ_morphism. + simpl; auto. +Qed. + +Lemma Pplus_max_distr_l : forall n m p, Pmax (p + n) (p + m) = p + Pmax n m. +Proof. + intros. apply Pmax_monotone. + intros x x'. unfold Ple. + rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_plus_morphism. + rewrite <- 2 Compare_dec.nat_compare_le. auto with arith. +Qed. + +Lemma Pplus_max_distr_r : forall n m p, Pmax (n + p) (m + p) = Pmax n m + p. +Proof. + intros. rewrite (Pplus_comm n p), (Pplus_comm m p), (Pplus_comm _ p). + apply Pplus_max_distr_l. +Qed. + +Lemma Pplus_min_distr_l : forall n m p, Pmin (p + n) (p + m) = p + Pmin n m. +Proof. + intros. apply Pmin_monotone. + intros x x'. unfold Ple. + rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_plus_morphism. + rewrite <- 2 Compare_dec.nat_compare_le. auto with arith. +Qed. + +Lemma Pplus_min_distr_r : forall n m p, Pmin (n + p) (m + p) = Pmin n m + p. +Proof. + intros. rewrite (Pplus_comm n p), (Pplus_comm m p), (Pplus_comm _ p). + apply Pplus_min_distr_l. +Qed. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index c87c9df9e..70830ad80 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -10,7 +10,7 @@ Require Export ZArith. Require Export ZArithRing. -Require Export Setoid Bool. +Require Export Morphisms Setoid Bool. (** * Definition of [Q] and basic properties *) @@ -101,7 +101,7 @@ Qed. Theorem Qeq_trans : forall x y z, x == y -> y == z -> x == z. Proof. -unfold Qeq in |- *; intros. +unfold Qeq; intros. apply Zmult_reg_l with (QDen y). auto with qarith. transitivity (Qnum x * QDen y * QDen z)%Z; try ring. @@ -110,6 +110,15 @@ transitivity (Qnum y * QDen z * QDen x)%Z; try ring. rewrite H0; ring. Qed. +Hint Resolve Qeq_refl : qarith. +Hint Resolve Qeq_sym : qarith. +Hint Resolve Qeq_trans : qarith. + +(** In a word, [Qeq] is a setoid equality. *) + +Instance Q_Setoid : Equivalence Qeq. +Proof. split; red; eauto with qarith. Qed. + (** Furthermore, this equality is decidable: *) Theorem Qeq_dec : forall x y, {x==y} + {~ x==y}. @@ -155,18 +164,6 @@ Proof. intros; rewrite <- Qle_bool_iff; auto. Qed. -(** We now consider [Q] seen as a setoid. *) - -Add Relation Q Qeq - reflexivity proved by Qeq_refl - symmetry proved by Qeq_sym - transitivity proved by Qeq_trans -as Q_Setoid. - -Hint Resolve Qeq_refl : qarith. -Hint Resolve Qeq_sym : qarith. -Hint Resolve Qeq_trans : qarith. - Theorem Qnot_eq_sym : forall x y, ~x == y -> ~y == x. Proof. auto with qarith. @@ -218,7 +215,7 @@ Qed. (** * Setoid compatibility results *) -Add Morphism Qplus : Qplus_comp. +Instance Qplus_comp : Proper (Qeq==>Qeq==>Qeq) Qplus. Proof. unfold Qeq, Qplus; simpl. Open Scope Z_scope. @@ -232,24 +229,23 @@ Proof. Close Scope Z_scope. Qed. -Add Morphism Qopp : Qopp_comp. +Instance Qopp_comp : Proper (Qeq==>Qeq) Qopp. Proof. unfold Qeq, Qopp; simpl. Open Scope Z_scope. - intros. + intros x y H; simpl. replace (- Qnum x * ' Qden y) with (- (Qnum x * ' Qden y)) by ring. - rewrite H in |- *; ring. + rewrite H; ring. Close Scope Z_scope. Qed. -Add Morphism Qminus : Qminus_comp. +Instance Qminus_comp : Proper (Qeq==>Qeq==>Qeq) Qminus. Proof. - intros. - unfold Qminus. - rewrite H; rewrite H0; auto with qarith. + intros x x' Hx y y' Hy. + unfold Qminus. rewrite Hx, Hy; auto with qarith. Qed. -Add Morphism Qmult : Qmult_comp. +Instance Qmult_comp : Proper (Qeq==>Qeq==>Qeq) Qmult. Proof. unfold Qeq; simpl. Open Scope Z_scope. @@ -263,7 +259,7 @@ Proof. Close Scope Z_scope. Qed. -Add Morphism Qinv : Qinv_comp. +Instance Qinv_comp : Proper (Qeq==>Qeq) Qinv. Proof. unfold Qeq, Qinv; simpl. Open Scope Z_scope. @@ -281,83 +277,49 @@ Proof. Close Scope Z_scope. Qed. -Add Morphism Qdiv : Qdiv_comp. +Instance Qdiv_comp : Proper (Qeq==>Qeq==>Qeq) Qdiv. Proof. - intros; unfold Qdiv. - rewrite H; rewrite H0; auto with qarith. + intros x x' Hx y y' Hy; unfold Qdiv. + rewrite Hx, Hy; auto with qarith. Qed. -Add Morphism Qle with signature Qeq ==> Qeq ==> iff as Qle_comp. +Instance Qcompare_comp : Proper (Qeq==>Qeq==>eq) Qcompare. Proof. - cut (forall x1 x2, x1==x2 -> forall x3 x4, x3==x4 -> x1<=x3 -> x2<=x4). - split; apply H; assumption || (apply Qeq_sym ; assumption). - - unfold Qeq, Qle; simpl. + unfold Qeq, Qcompare. Open Scope Z_scope. - intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0 H1; simpl in *. - apply Zmult_le_reg_r with ('p2). - unfold Zgt; auto. - replace (q1 * 's2 * 'p2) with (q1 * 'p2 * 's2) by ring. - rewrite <- H. - apply Zmult_le_reg_r with ('r2). - unfold Zgt; auto. - replace (s1 * 'q2 * 'p2 * 'r2) with (s1 * 'r2 * 'q2 * 'p2) by ring. - rewrite <- H0. - replace (p1 * 'q2 * 's2 * 'r2) with ('q2 * 's2 * (p1 * 'r2)) by ring. - replace (r1 * 's2 * 'q2 * 'p2) with ('q2 * 's2 * (r1 * 'p2)) by ring. - auto with zarith. + intros (p1,p2) (q1,q2) H (r1,r2) (s1,s2) H'; simpl in *. + rewrite <- (Zcompare_mult_compat (q2*s2) (p1*'r2)). + rewrite <- (Zcompare_mult_compat (p2*r2) (q1*'s2)). + change ('(q2*s2)) with ('q2 * 's2). + change ('(p2*r2)) with ('p2 * 'r2). + replace ('q2 * 's2 * (p1*'r2)) with ((p1*'q2)*'r2*'s2) by ring. + rewrite H. + replace ('q2 * 's2 * (r1*'p2)) with ((r1*'s2)*'q2*'p2) by ring. + rewrite H'. + f_equal; ring. Close Scope Z_scope. Qed. -Add Morphism Qlt with signature Qeq ==> Qeq ==> iff as Qlt_comp. +Instance Qle_comp : Proper (Qeq==>Qeq==>iff) Qle. Proof. - cut (forall x1 x2, x1==x2 -> forall x3 x4, x3==x4 -> x1<x3 -> x2<x4). - split; apply H; assumption || (apply Qeq_sym ; assumption). - - unfold Qeq, Qlt; simpl. - Open Scope Z_scope. - intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0 H1; simpl in *. - apply Zgt_lt. - generalize (Zlt_gt _ _ H1); clear H1; intro H1. - apply Zmult_gt_reg_r with ('p2); auto with zarith. - replace (q1 * 's2 * 'p2) with (q1 * 'p2 * 's2) by ring. - rewrite <- H. - apply Zmult_gt_reg_r with ('r2); auto with zarith. - replace (s1 * 'q2 * 'p2 * 'r2) with (s1 * 'r2 * 'q2 * 'p2) by ring. - rewrite <- H0. - replace (p1 * 'q2 * 's2 * 'r2) with ('q2 * 's2 * (p1 * 'r2)) by ring. - replace (r1 * 's2 * 'q2 * 'p2) with ('q2 * 's2 * (r1 * 'p2)) by ring. - apply Zlt_gt. - apply Zmult_gt_0_lt_compat_l; auto with zarith. - Close Scope Z_scope. + intros p q H r s H'. rewrite 2 Qle_alt, H, H'; auto with *. Qed. -Add Morphism Qeq_bool with signature Qeq ==> Qeq ==> (@eq bool) as Qeqb_comp. +Instance Qlt_compat : Proper (Qeq==>Qeq==>iff) Qlt. Proof. - intros; apply eq_true_iff_eq. - rewrite 2 Qeq_bool_iff, H, H0; split; auto with qarith. + intros p q H r s H'. rewrite 2 Qlt_alt, H, H'; auto with *. Qed. -Add Morphism Qle_bool with signature Qeq ==> Qeq ==> (@eq bool) as Qleb_comp. +Instance Qeqb_comp : Proper (Qeq==>Qeq==>eq) Qeq_bool. Proof. - intros; apply eq_true_iff_eq. - rewrite 2 Qle_bool_iff, H, H0. - split; auto with qarith. + intros p q H r s H'; apply eq_true_iff_eq. + rewrite 2 Qeq_bool_iff, H, H'; split; auto with qarith. Qed. -Lemma Qcompare_egal_dec: forall n m p q : Q, - (n<m -> p<q) -> (n==m -> p==q) -> (n>m -> p>q) -> ((n?=m) = (p?=q)). +Instance Qleb_comp : Proper (Qeq==>Qeq==>eq) Qle_bool. Proof. - intros. - do 2 rewrite Qeq_alt in H0. - unfold Qeq, Qlt, Qcompare in *. - apply Zcompare_egal_dec; auto. - omega. -Qed. - -Add Morphism Qcompare : Qcompare_comp. -Proof. - intros; apply Qcompare_egal_dec; rewrite H; rewrite H0; auto. + intros p q H r s H'; apply eq_true_iff_eq. + rewrite 2 Qle_bool_iff, H, H'; split; auto with qarith. Qed. @@ -554,6 +516,11 @@ Qed. Hint Resolve Qle_trans : qarith. +Lemma Qlt_irrefl : forall x, ~x<x. +Proof. + unfold Qlt. auto with zarith. +Qed. + Lemma Qlt_not_eq : forall x y, x<y -> ~ x==y. Proof. unfold Qlt, Qeq; auto with zarith. @@ -561,6 +528,13 @@ Qed. (** Large = strict or equal *) +Lemma Qle_lteq : forall x y, x<=y <-> x<y \/ x==y. +Proof. + intros. + rewrite Qeq_alt, Qle_alt, Qlt_alt. + destruct (x ?= y); intuition; discriminate. +Qed. + Lemma Qlt_le_weak : forall x y, x<y -> x<=y. Proof. unfold Qle, Qlt; auto with zarith. @@ -835,9 +809,9 @@ Qed. Definition Qpower_positive (q:Q)(p:positive) : Q := pow_pos Qmult q p. -Add Morphism Qpower_positive with signature Qeq ==> eq ==> Qeq as Qpower_positive_comp. +Instance Qpower_positive_comp : Proper (Qeq==>eq==>Qeq) Qpower_positive. Proof. -intros x1 x2 Hx y. +intros x x' Hx y y' Hy. rewrite <-Hy; clear y' Hy. unfold Qpower_positive. induction y; simpl; try rewrite IHy; @@ -854,8 +828,8 @@ Definition Qpower (q:Q) (z:Z) := Notation " q ^ z " := (Qpower q z) : Q_scope. -Add Morphism Qpower with signature Qeq ==> eq ==> Qeq as Qpower_comp. +Instance Qpower_comp : Proper (Qeq==>eq==>Qeq) Qpower. Proof. -intros x1 x2 Hx [|y|y]; try reflexivity; -simpl; rewrite Hx; reflexivity. +intros x x' Hx y y' Hy. rewrite <- Hy; clear y' Hy. +destruct y; simpl; rewrite ?Hx; auto with *. Qed. diff --git a/theories/QArith/QOrderedType.v b/theories/QArith/QOrderedType.v new file mode 100644 index 000000000..3d83eac38 --- /dev/null +++ b/theories/QArith/QOrderedType.v @@ -0,0 +1,68 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import QArith_base + DecidableType2 OrderedType2 OrderedType2Facts. + +Local Open Scope Q_scope. + +(** * DecidableType structure for rational numbers *) + +Module Q_as_DT <: DecidableType. + Definition t := Q. + Definition eq := Qeq. + Instance eq_equiv : Equivalence Qeq. + Definition eq_dec := Qeq_dec. + + (** The next fields are not mandatory, but allow [Q_as_DT] to be + also a [DecidableTypeOrig]. *) + Definition eq_refl := Qeq_refl. + Definition eq_sym := Qeq_sym. + Definition eq_trans := eq_trans. +End Q_as_DT. + + +(** * OrderedType structure for rational numbers *) + +Module Q_as_OT <: OrderedTypeFull. + Include Q_as_DT. + Definition lt := Qlt. + Definition le := Qle. + Definition compare := Qcompare. + + Instance lt_strorder : StrictOrder Qlt. + Proof. split; [ exact Qlt_irrefl | exact Qlt_trans ]. Qed. + + Instance lt_compat : Proper (Qeq==>Qeq==>iff) Qlt. + Proof. auto with *. Qed. + + Definition le_lteq := Qle_lteq. + + Lemma Qcompare_antisym : forall x y, CompOpp (x ?= y) = (y ?= x). + Proof. + unfold "?=". intros. apply Zcompare_antisym. + Qed. + + Lemma compare_spec : forall x y, Cmp Qeq Qlt x y (Qcompare x y). + Proof. + intros. + destruct (x ?= y) as [ ]_eqn:H; constructor; auto. + rewrite Qeq_alt; auto. + rewrite Qlt_alt, <- Qcompare_antisym, H; auto. + Qed. + +End Q_as_OT. + + +(** * An [order] tactic for [Q] numbers *) + +Module QOrder := OTF_to_OrderTac Q_as_OT. +Ltac q_order := QOrder.order. + +(** Note that [q_order] is domain-agnostic: it will not prove + [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x==y]. *) diff --git a/theories/QArith/Qminmax.v b/theories/QArith/Qminmax.v new file mode 100644 index 000000000..e9d2f79ab --- /dev/null +++ b/theories/QArith/Qminmax.v @@ -0,0 +1,130 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import QArith_base OrderedType2 QOrderedType GenericMinMax. + +(** * Maximum and Minimum of two rational numbers *) + +Local Open Scope Q_scope. + +(** [Qmin] and [Qmax] are obtained the usual way from [Qcompare]. *) + +Definition Qmax := gmax Qcompare. +Definition Qmin := gmin Qcompare. + +Module QHasMinMax <: HasMinMax Q_as_OT. + Module QMM := GenericMinMax Q_as_OT. + Definition max := Qmax. + Definition min := Qmin. + Definition max_spec := QMM.max_spec. + Definition min_spec := QMM.min_spec. +End QHasMinMax. + +(** We obtain hence all the generic properties of max and min. *) + +Module Import QMinMaxProps := MinMaxProperties Q_as_OT QHasMinMax. + +Definition Qmax_case_strong := max_case_strong. +Definition Qmax_case := max_case. +Definition Qmax_monotone := max_monotone. +Definition Qmax_spec := max_spec. +Definition Qmax_spec_le := max_spec_le. +Definition Qmax_dec := max_dec. +Definition Qmax_unicity := max_unicity. +Definition Qmax_unicity_ext := max_unicity_ext. +Definition Qmax_id := max_id. +Notation Qmax_idempotent := Qmax_id (only parsing). +Definition Qmax_assoc := max_assoc. +Definition Qmax_comm := max_comm. +Definition Qmax_l := max_l. +Definition Qmax_r := max_r. +Definition Nle_max_l := le_max_l. +Definition Nle_max_r := le_max_r. +Definition Qmax_le := max_le. +Definition Qmax_le_iff := max_le_iff. +Definition Qmax_lt_iff := max_lt_iff. +Definition Qmax_lub_l := max_lub_l. +Definition Qmax_lub_r := max_lub_r. +Definition Qmax_lub := max_lub. +Definition Qmax_lub_iff := max_lub_iff. +Definition Qmax_lub_lt := max_lub_lt. +Definition Qmax_lub_lt_iff := max_lub_lt_iff. +Definition Qmax_le_compat_l := max_le_compat_l. +Definition Qmax_le_compat_r := max_le_compat_r. +Definition Qmax_le_compat := max_le_compat. + +Definition Qmin_case_strong := min_case_strong. +Definition Qmin_case := min_case. +Definition Qmin_monotone := min_monotone. +Definition Qmin_spec := min_spec. +Definition Qmin_spec_le := min_spec_le. +Definition Qmin_dec := min_dec. +Definition Qmin_unicity := min_unicity. +Definition Qmin_unicity_ext := min_unicity_ext. +Definition Qmin_id := min_id. +Notation Qmin_idempotent := Qmin_id (only parsing). +Definition Qmin_assoc := min_assoc. +Definition Qmin_comm := min_comm. +Definition Qmin_l := min_l. +Definition Qmin_r := min_r. +Definition Nle_min_l := le_min_l. +Definition Nle_min_r := le_min_r. +Definition Qmin_le := min_le. +Definition Qmin_le_iff := min_le_iff. +Definition Qmin_lt_iff := min_lt_iff. +Definition Qmin_glb_l := min_glb_l. +Definition Qmin_glb_r := min_glb_r. +Definition Qmin_glb := min_glb. +Definition Qmin_glb_iff := min_glb_iff. +Definition Qmin_glb_lt := min_glb_lt. +Definition Qmin_glb_lt_iff := min_glb_lt_iff. +Definition Qmin_le_compat_l := min_le_compat_l. +Definition Qmin_le_compat_r := min_le_compat_r. +Definition Qmin_le_compat := min_le_compat. + +Definition Qmin_max_absorption := min_max_absorption. +Definition Qmax_min_absorption := max_min_absorption. +Definition Qmax_min_distr := max_min_distr. +Definition Qmin_max_distr := min_max_distr. +Definition Qmax_min_modular := max_min_modular. +Definition Qmin_max_modular := min_max_modular. +Definition Qmax_min_disassoc := max_min_disassoc. +Definition Qmax_min_antimonotone := max_min_antimonotone. +Definition Qmin_max_antimonotone := min_max_antimonotone. + + + +(** * Properties specific to the [Q] domain *) + +(** Compatibilities (consequences of monotonicity) *) + +Lemma Qplus_max_distr_l : forall n m p, Qmax (p + n) (p + m) == p + Qmax n m. +Proof. + intros. apply Qmax_monotone. + intros x x' Hx; rewrite Hx; auto with qarith. + intros x x' Hx. apply Qplus_le_compat; q_order. +Qed. + +Lemma Qplus_max_distr_r : forall n m p, Qmax (n + p) (m + p) == Qmax n m + p. +Proof. + intros. rewrite (Qplus_comm n p), (Qplus_comm m p), (Qplus_comm _ p). + apply Qplus_max_distr_l. +Qed. + +Lemma Qplus_min_distr_l : forall n m p, Qmin (p + n) (p + m) == p + Qmin n m. +Proof. + intros. apply Qmin_monotone. + intros x x' Hx; rewrite Hx; auto with qarith. + intros x x' Hx. apply Qplus_le_compat; q_order. +Qed. + +Lemma Qplus_min_distr_r : forall n m p, Qmin (n + p) (m + p) == Qmin n m + p. +Proof. + intros. rewrite (Qplus_comm n p), (Qplus_comm m p), (Qplus_comm _ p). + apply Qplus_min_distr_l. +Qed. diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v index 5b0fb21ef..de7a20d4c 100644 --- a/theories/Structures/DecidableType.v +++ b/theories/Structures/DecidableType.v @@ -9,44 +9,19 @@ (* $Id$ *) Require Export SetoidList. +Require DecidableType2. (* No Import here, this is on purpose. *) + Set Implicit Arguments. Unset Strict Implicit. -(** * Types with Equalities, and nothing more (for subtyping purpose) *) - -Module Type EqualityType. - - Parameter Inline t : Type. - Parameter Inline eq : t -> t -> Prop. - - Axiom eq_refl : forall x : t, eq x x. - Axiom eq_sym : forall x y : t, eq x y -> eq y x. - Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. - - Hint Immediate eq_sym. - Hint Resolve eq_refl eq_trans. +(** * Types with Equalities, and nothing more (for subtyping purpose) *) -End EqualityType. +Module Type EqualityType := DecidableType2.EqualityTypeOrig. (** * Types with decidable Equalities (but no ordering) *) -Module Type DecidableType. - - Parameter Inline t : Type. - - Parameter Inline eq : t -> t -> Prop. - - Axiom eq_refl : forall x : t, eq x x. - Axiom eq_sym : forall x y : t, eq x y -> eq y x. - Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. - - Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }. - - Hint Immediate eq_sym. - Hint Resolve eq_refl eq_trans. - -End DecidableType. +Module Type DecidableType := DecidableType2.DecidableTypeOrig. (** * Additional notions about keys and datas used in FMap *) diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v index b1cd5bfa5..7b329dd5e 100644 --- a/theories/Structures/DecidableType2.v +++ b/theories/Structures/DecidableType2.v @@ -8,8 +8,7 @@ (* $Id$ *) -Require Export SetoidList. -Require DecidableType. (* No Import here, this is on purpose *) +Require Export RelationClasses. Set Implicit Arguments. Unset Strict Implicit. @@ -33,152 +32,88 @@ Module Type DecidableType. Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }. End DecidableType. +(** * Old versions of [DecidableType], with reflexivity, symmetry, + transitivity as three separate axioms. *) + +Module Type EqualityTypeOrig. + Parameter Inline t : Type. + Parameter Inline eq : t -> t -> Prop. + + Axiom eq_refl : forall x : t, eq x x. + Axiom eq_sym : forall x y : t, eq x y -> eq y x. + Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. + + Hint Immediate eq_sym. + Hint Resolve eq_refl eq_trans. +End EqualityTypeOrig. + +Module Type DecidableTypeOrig. + Include Type EqualityTypeOrig. + Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }. +End DecidableTypeOrig. + (** * Compatibility wrapper from/to the old version of [DecidableType] *) -Module Type DecidableTypeOrig := DecidableType.DecidableType. +(** Interestingly, a module can be at the same time a [DecidableType] + and a [DecidableTypeOrig]. For the sake of compatibility, + this will be the case of all [DecidableType] modules provided here. +*) -Module Backport_DT (E:DecidableType) <: DecidableTypeOrig. +Module Backport_ET (E:EqualityType) <: EqualityTypeOrig. Include E. Definition eq_refl := @Equivalence_Reflexive _ _ eq_equiv. Definition eq_sym := @Equivalence_Symmetric _ _ eq_equiv. Definition eq_trans := @Equivalence_Transitive _ _ eq_equiv. -End Backport_DT. +End Backport_ET. -Module Update_DT (E:DecidableTypeOrig) <: DecidableType. +Module Update_ET (E:EqualityTypeOrig) <: EqualityType. Include E. Instance eq_equiv : Equivalence eq. Proof. exact (Build_Equivalence _ _ eq_refl eq_sym eq_trans). Qed. +End Update_ET. + +Module Backport_DT (E:DecidableType) <: DecidableTypeOrig. + Include Backport_ET E. + Definition eq_dec := E.eq_dec. +End Backport_DT. + +Module Update_DT (E:DecidableTypeOrig) <: DecidableType. + Include Update_ET E. + Definition eq_dec := E.eq_dec. End Update_DT. +(** * UsualDecidableType + + A particular case of [DecidableType] where the equality is + the usual one of Coq. *) -(** * Additional notions about keys and datas used in FMap *) - -Module KeyDecidableType(D:DecidableType). - Import D. - - Section Elt. - Variable elt : Type. - Notation key:=t. - - Definition eqk (p p':key*elt) := eq (fst p) (fst p'). - Definition eqke (p p':key*elt) := - eq (fst p) (fst p') /\ (snd p) = (snd p'). - - Hint Unfold eqk eqke. - Hint Extern 2 (eqke ?a ?b) => split. - - (* eqke is stricter than eqk *) - - Lemma eqke_eqk : forall x x', eqke x x' -> eqk x x'. - Proof. - unfold eqk, eqke; intuition. - Qed. - - (* eqk, eqke are equalities *) - - Instance eqk_equiv : Equivalence eqk. - Proof. - constructor; eauto. - Qed. - - Instance eqke_equiv : Equivalence eqke. - Proof. - constructor. auto. - red; unfold eqke; intuition. - red; unfold eqke; intuition; [ eauto | congruence ]. - Qed. - - Hint Resolve (@Equivalence_Reflexive _ _ eqk_equiv). - Hint Resolve (@Equivalence_Transitive _ _ eqk_equiv). - Hint Immediate (@Equivalence_Symmetric _ _ eqk_equiv). - Hint Resolve (@Equivalence_Reflexive _ _ eqke_equiv). - Hint Resolve (@Equivalence_Transitive _ _ eqke_equiv). - Hint Immediate (@Equivalence_Symmetric _ _ eqke_equiv). - - Lemma InA_eqke_eqk : - forall x m, InA eqke x m -> InA eqk x m. - Proof. - unfold eqke; induction 1; intuition. - Qed. - Hint Resolve InA_eqke_eqk. - - Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. - Proof. - intros. rewrite <- H; auto. - Qed. - - Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). - Definition In k m := exists e:elt, MapsTo k e m. - - Hint Unfold MapsTo In. - - (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) - - Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. - Proof. - firstorder. - exists x; auto. - induction H. - destruct y. - exists e; auto. - destruct IHInA as [e H0]. - exists e; auto. - Qed. - - Global Instance MapsTo_compat : - Proper (eq==>Logic.eq==>Logic.eq==>iff) MapsTo. - Proof. - intros x x' Hxx' e e' Hee' l l' Hll'; subst. - unfold MapsTo. - assert (EQN : eqke (x,e') (x',e')) by (compute;auto). - rewrite EQN; intuition. - Qed. - - Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. - Proof. - intros; rewrite <- H; auto. - Qed. - - Global Instance In_compat : Proper (eq==>Logic.eq==>iff) In. - Proof. - intros x x' Hxx' l l' Hll'; subst l. - unfold In. - split; intros (e,He); exists e. - rewrite <- Hxx'; auto. - rewrite Hxx'; auto. - Qed. - - Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. - Proof. - intros; rewrite <- H; auto. - Qed. - - Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. - Proof. - inversion 1. - inversion_clear H0; eauto. - destruct H1; simpl in *; intuition. - Qed. - - Lemma In_inv_2 : forall k k' e e' l, - InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l. - Proof. - inversion_clear 1; compute in H0; intuition. - Qed. - - Lemma In_inv_3 : forall x x' l, - InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l. - Proof. - inversion_clear 1; compute in H0; intuition. - Qed. - - End Elt. - - Hint Resolve In_inv_2 In_inv_3. - -End KeyDecidableType. +Module Type UsualDecidableType. + Parameter Inline t : Type. + Definition eq := @eq t. + Program Instance eq_equiv : Equivalence eq. + Parameter eq_dec : forall x y, { eq x y }+{~eq x y }. +End UsualDecidableType. +(** a [UsualDecidableType] is in particular an [DecidableType]. *) +Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U. +(** an shortcut for easily building a UsualDecidableType *) + +Module Type MiniDecidableType. + Parameter Inline t : Type. + Parameter eq_dec : forall x y:t, { x=y }+{ x<>y }. +End MiniDecidableType. + +Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType. + Definition t:=M.t. + Definition eq := @eq M.t. + Program Instance eq_equiv : Equivalence eq. + Definition eq_dec := M.eq_dec. + (* For building DecidableTypeOrig at the same time: *) + Definition eq_refl := @Equivalence_Reflexive _ _ eq_equiv. + Definition eq_sym := @Equivalence_Symmetric _ _ eq_equiv. + Definition eq_trans := @Equivalence_Transitive _ _ eq_equiv. +End Make_UDT. diff --git a/theories/Structures/DecidableType2Ex.v b/theories/Structures/DecidableType2Ex.v index 7b9c052ec..2ce2b5662 100644 --- a/theories/Structures/DecidableType2Ex.v +++ b/theories/Structures/DecidableType2Ex.v @@ -8,61 +8,29 @@ (* $Id$ *) -Require Import DecidableType2. +Require Import DecidableType2 Morphisms RelationPairs. Set Implicit Arguments. Unset Strict Implicit. (** * Examples of Decidable Type structures. *) -(** A particular case of [DecidableType] where - the equality is the usual one of Coq. *) - -Module Type UsualDecidableType. - Parameter Inline t : Type. - Definition eq := @eq t. - Program Instance eq_equiv : Equivalence eq. - Parameter eq_dec : forall x y, { eq x y }+{~eq x y }. -End UsualDecidableType. - -(** a [UsualDecidableType] is in particular an [DecidableType]. *) - -Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U. - -(** an shortcut for easily building a UsualDecidableType *) - -Module Type MiniDecidableType. - Parameter Inline t : Type. - Parameter eq_dec : forall x y:t, { x=y }+{ x<>y }. -End MiniDecidableType. - -Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType. - Definition t:=M.t. - Definition eq := @eq t. - Program Instance eq_equiv : Equivalence eq. - Definition eq_dec := M.eq_dec. -End Make_UDT. (** From two decidable types, we can build a new DecidableType over their cartesian product. *) Module PairDecidableType(D1 D2:DecidableType) <: DecidableType. - Definition t := prod D1.t D2.t. + Definition t := (D1.t * D2.t)%type. - Definition eq x y := D1.eq (fst x) (fst y) /\ D2.eq (snd x) (snd y). + Definition eq := (D1.eq * D2.eq)%signature. Instance eq_equiv : Equivalence eq. - Proof. - constructor. - intros (x1,x2); red; simpl; auto. - intros (x1,x2) (y1,y2); unfold eq; simpl; intuition. - intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto. - Qed. Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }. Proof. intros (x1,x2) (y1,y2); unfold eq; simpl. - destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2); intuition. + destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2); + compute; intuition. Defined. End PairDecidableType. @@ -70,7 +38,7 @@ End PairDecidableType. (** Similarly for pairs of UsualDecidableType *) Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType. - Definition t := prod D1.t D2.t. + Definition t := (D1.t * D2.t)%type. Definition eq := @eq t. Program Instance eq_equiv : Equivalence eq. Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }. diff --git a/theories/Structures/DecidableType2Facts.v b/theories/Structures/DecidableType2Facts.v new file mode 100644 index 000000000..5a5caaab8 --- /dev/null +++ b/theories/Structures/DecidableType2Facts.v @@ -0,0 +1,141 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +Require Import DecidableType2 SetoidList. + + +(** * Keys and datas used in FMap *) + +Module KeyDecidableType(D:DecidableType). + Import D. + + Section Elt. + Variable elt : Type. + Notation key:=t. + + Definition eqk (p p':key*elt) := eq (fst p) (fst p'). + Definition eqke (p p':key*elt) := + eq (fst p) (fst p') /\ (snd p) = (snd p'). + + Hint Unfold eqk eqke. + Hint Extern 2 (eqke ?a ?b) => split. + + (* eqke is stricter than eqk *) + + Lemma eqke_eqk : forall x x', eqke x x' -> eqk x x'. + Proof. + unfold eqk, eqke; intuition. + Qed. + + (* eqk, eqke are equalities *) + + Instance eqk_equiv : Equivalence eqk. + Proof. + constructor; eauto. + Qed. + + Instance eqke_equiv : Equivalence eqke. + Proof. + constructor. auto. + red; unfold eqke; intuition. + red; unfold eqke; intuition; [ eauto | congruence ]. + Qed. + + Hint Resolve (@Equivalence_Reflexive _ _ eqk_equiv). + Hint Resolve (@Equivalence_Transitive _ _ eqk_equiv). + Hint Immediate (@Equivalence_Symmetric _ _ eqk_equiv). + Hint Resolve (@Equivalence_Reflexive _ _ eqke_equiv). + Hint Resolve (@Equivalence_Transitive _ _ eqke_equiv). + Hint Immediate (@Equivalence_Symmetric _ _ eqke_equiv). + + Lemma InA_eqke_eqk : + forall x m, InA eqke x m -> InA eqk x m. + Proof. + unfold eqke; induction 1; intuition. + Qed. + Hint Resolve InA_eqke_eqk. + + Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. + Proof. + intros. rewrite <- H; auto. + Qed. + + Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). + Definition In k m := exists e:elt, MapsTo k e m. + + Hint Unfold MapsTo In. + + (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) + + Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. + Proof. + firstorder. + exists x; auto. + induction H. + destruct y. + exists e; auto. + destruct IHInA as [e H0]. + exists e; auto. + Qed. + + Global Instance MapsTo_compat : + Proper (eq==>Logic.eq==>Logic.eq==>iff) MapsTo. + Proof. + intros x x' Hxx' e e' Hee' l l' Hll'; subst. + unfold MapsTo. + assert (EQN : eqke (x,e') (x',e')) by (compute;auto). + rewrite EQN; intuition. + Qed. + + Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. + Proof. + intros; rewrite <- H; auto. + Qed. + + Global Instance In_compat : Proper (eq==>Logic.eq==>iff) In. + Proof. + intros x x' Hxx' l l' Hll'; subst l. + unfold In. + split; intros (e,He); exists e. + rewrite <- Hxx'; auto. + rewrite Hxx'; auto. + Qed. + + Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. + Proof. + intros; rewrite <- H; auto. + Qed. + + Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. + Proof. + inversion 1. + inversion_clear H0; eauto. + destruct H1; simpl in *; intuition. + Qed. + + Lemma In_inv_2 : forall k k' e e' l, + InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l. + Proof. + inversion_clear 1; compute in H0; intuition. + Qed. + + Lemma In_inv_3 : forall x x' l, + InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l. + Proof. + inversion_clear 1; compute in H0; intuition. + Qed. + + End Elt. + + Hint Resolve In_inv_2 In_inv_3. + (* TODO: (re-)populate with more hints after failed attempt of Global Hint *) + +End KeyDecidableType. + + + diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v new file mode 100644 index 000000000..ed9c035a1 --- /dev/null +++ b/theories/Structures/GenericMinMax.v @@ -0,0 +1,507 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +Require Import OrderedType2 OrderedType2Facts Setoid Morphisms Basics. + +(** * A Generic construction of min and max based on OrderedType *) + +(** ** First, an interface for types with [max] and/or [min] *) + +Module Type HasMax (Import O:OrderedTypeFull). + Parameter Inline max : t -> t -> t. + Parameter max_spec : forall x y, + (lt x y /\ eq (max x y) y) \/ (le y x /\ eq (max x y) x). +End HasMax. + +Module Type HasMin (Import O:OrderedTypeFull). + Parameter Inline min : t -> t -> t. + Parameter min_spec : forall x y, + (lt x y /\ eq (min x y) x) \/ (le y x /\ eq (min x y) y). +End HasMin. + +Module Type HasMinMax (Import O:OrderedTypeFull). + Include Type HasMax O. + Include Type HasMin O. +End HasMinMax. + + +(** ** Any [OrderedTypeFull] can be equipped by [max] and [min] + based on the compare function. *) + +Definition gmax {A} (cmp : A->A->comparison) x y := + match cmp x y with Lt => y | _ => x end. +Definition gmin {A} (cmp : A->A->comparison) x y := + match cmp x y with Gt => y | _ => x end. + +Module GenericMinMax (Import O:OrderedTypeFull) <: HasMinMax O. + + Definition max := gmax O.compare. + Definition min := gmin O.compare. + + Lemma max_spec : forall x y, + (lt x y /\ eq (max x y) y) \/ (le y x /\ eq (max x y) x). + Proof. + intros. rewrite le_lteq. unfold max, gmax. + destruct (compare_spec x y); auto. + Qed. + + Lemma min_spec : forall x y, + (lt x y /\ eq (min x y) x) \/ (le y x /\ eq (min x y) y). + Proof. + intros. rewrite le_lteq. unfold min, gmin. + destruct (compare_spec x y); auto. + Qed. + +End GenericMinMax. + + +(** ** Consequences of the minimalist interface: facts about [max]. *) + +Module MaxProperties (Import O:OrderedTypeFull)(Import M:HasMax O). + Module Import OF := OrderedTypeFullFacts O. + Infix "<" := lt. + Infix "==" := eq (at level 70). + Infix "<=" := le. + +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 (compare_spec x y); intuition; order. +Qed. + +(** An alias to the [max_spec] of the interface. *) + +Lemma max_spec : forall n m, + (n < m /\ max n m == m) \/ (m <= n /\ max n m == n). +Proof. exact max_spec. 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, + (n <= m /\ max n m == m) \/ (m <= n /\ max n m == n). +Proof. + intros. destruct (max_spec n m); [left|right]; intuition; order. +Qed. + +(** Another 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. +Proof. + intros. assert (Hm := max_spec n m). + destruct (compare_spec 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)) -> + (forall n m, f n m == max n m). +Proof. + intros. apply max_unicity; auto. +Qed. + +(** Induction principles for [max]. *) + +Lemma max_case_strong : forall 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. +assert (H:=compare_spec n m). assert (H':=max_spec n m). +destruct (compare n m). +apply (Compat m), Hr; inversion_clear H; intuition; order. +apply (Compat m), Hr; inversion_clear H; intuition; order. +apply (Compat n), Hl; inversion_clear H; intuition; order. +Qed. + +Lemma max_case : forall 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}. +Proof. + intros n m. apply max_case; auto. + intros x y H [E|E]; [left|right]; order. +Defined. + +(** [max] commutes with monotone functions. *) + +Lemma max_monotone: forall 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. + destruct (M.max_spec x y) as [(H,E)|(H,E)]; rewrite E; + destruct (M.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. +Qed. + +(** *** Semi-lattice algebraic properties of [max] *) + +Lemma max_id : forall n, max n n == n. +Proof. + intros. destruct (M.max_spec n n); intuition. +Qed. + +Lemma max_assoc : forall m n p, max m (max n p) == max (max m n) p. +Proof. + intros. + destruct (M.max_spec n p) as [(H,Eq)|(H,Eq)]; rewrite Eq; auto. + destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; auto. + destruct (max_spec m p); intuition; order. + destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; auto. + destruct (max_spec m p); intuition; order. +Qed. + +Lemma max_comm : forall n m, max n m == max m n. +Proof. + intros. + destruct (M.max_spec n m) as [(H,Eq)|(H,Eq)]; rewrite Eq; auto. + destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; auto. + order. + destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; auto. + order. +Qed. + +(** *** Least-upper bound properties of [max] *) + +Lemma max_l : forall n m, m <= n -> max n m == n. +Proof. + intros. destruct (M.max_spec n m); intuition; order. +Qed. + +Lemma max_r : forall n m, n <= m -> max n m == m. +Proof. + intros. destruct (M.max_spec n m); intuition; order. +Qed. + +Lemma le_max_l : forall n m, n <= max n m. +Proof. + intros; destruct (M.max_spec n m); intuition; order. +Qed. + +Lemma le_max_r : forall n m, m <= max n m. +Proof. + intros; destruct (M.max_spec n m); intuition; order. +Qed. + +Lemma max_le : forall n m p, p <= max n m -> p <= n \/ p <= m. +Proof. + intros n m p H; destruct (M.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 (M.max_spec n m); intuition; order. +Qed. + +Lemma max_lt_iff : forall n m p, p < max n m <-> p < n \/ p < m. +Proof. + intros. destruct (M.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 (M.max_spec n m); intuition; order. +Qed. + +Lemma max_lub_r : forall n m p, max n m <= p -> m <= p. +Proof. + intros; destruct (M.max_spec n m); intuition; order. +Qed. + +Lemma max_lub : forall n m p, n <= p -> m <= p -> max n m <= p. +Proof. + intros; destruct (M.max_spec n m); intuition; order. +Qed. + +Lemma max_lub_iff : forall n m p, max n m <= p <-> n <= p /\ m <= p. +Proof. + intros; destruct (M.max_spec n m); intuition; order. +Qed. + +Lemma max_lub_lt : forall n m p, n < p -> m < p -> max n m < p. +Proof. + intros; destruct (M.max_spec n m); intuition; order. +Qed. + +Lemma max_lub_lt_iff : forall n m p, max n m < p <-> n < p /\ m < p. +Proof. + intros; destruct (M.max_spec n m); intuition; order. +Qed. + +Lemma max_le_compat_l : forall n m p, n <= m -> max p n <= max p m. +Proof. + intros. + destruct (M.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_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 : forall n m p q, n <= m -> p <= q -> + max n p <= max m q. +Proof. + intros n m p q Hnm Hpq. + assert (LE := max_le_compat_l _ _ m Hpq). + assert (LE' := max_le_compat_r _ _ p Hnm). + order. +Qed. + +End MaxProperties. + + +(** ** Properties concernant [min], then both [min] and [max]. + + To avoid duplication of code, we exploit that [min] can be + seen as a [max] of the reversed order. +*) + +Module MinMaxProperties (Import O:OrderedTypeFull)(Import M:HasMinMax O). + Include MaxProperties O M. + + Module ORev := OrderedTypeRev O. + Module MRev <: HasMax ORev. + Definition max x y := M.min y x. + Definition max_spec x y := M.min_spec y x. + End MRev. + Module MPRev := MaxProperties ORev MRev. + +Instance min_compat : Proper (eq==>eq==>eq) min. +Proof. intros x x' Hx y y' Hy. apply MPRev.max_compat; assumption. Qed. + +Lemma min_spec : forall n m, + (n < m /\ min n m == n) \/ (m <= n /\ min n m == m). +Proof. exact min_spec. 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_case_strong : forall n m (P:O.t -> Type), + (forall x y, x == y -> P x -> P y) -> + (m<=n -> P m) -> (n<=m -> P n) -> P (min n m). +Proof. intros. apply (MPRev.max_case_strong m n P); auto. Qed. + +Lemma min_case : forall 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}. +Proof. + intros. destruct (MPRev.max_dec m n); [right|left]; assumption. +Defined. + +Lemma min_monotone: forall 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_monotone; auto. compute in *; eauto. +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_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_comm : forall n m, min n m == min m n. +Proof. intros. exact (MPRev.max_comm m n). Qed. + +Lemma min_l : forall n m, n <= m -> min n m == n. +Proof. intros n m. exact (MPRev.max_r m n). Qed. + +Lemma min_r : forall n m, m <= n -> min n m == m. +Proof. intros n m. exact (MPRev.max_l m n). Qed. + +Lemma le_min_r : forall n m, min n m <= m. +Proof. intros. exact (MPRev.le_max_l m n). Qed. + +Lemma le_min_l : forall n m, min n m <= n. +Proof. intros. exact (MPRev.le_max_r m n). 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_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_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_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_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 : forall n m p, p <= n -> p <= m -> p <= min n m. +Proof. intros. apply MPRev.max_lub; auto. 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_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_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_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_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 : forall n m p q, n <= m -> p <= q -> + min n p <= min m q. +Proof. intros. apply MPRev.max_le_compat; auto. Qed. + + +(** *** Combined properties of min and max *) + +Lemma min_max_absorption : forall n m, max n (min n m) == n. +Proof. + intros. + destruct (M.min_spec n m) as [(C,E)|(C,E)]; rewrite E. + apply max_l. OF.order. + destruct (M.max_spec n m); intuition; OF.order. +Qed. + +Lemma max_min_absorption : forall n m, min n (max n m) == n. +Proof. + intros. + destruct (M.max_spec n m) as [(C,E)|(C,E)]; rewrite E. + destruct (M.min_spec n m) as [(C',E')|(C',E')]; auto. OF.order. + apply min_l; auto. OF.order. +Qed. + +(** Distributivity *) + +Lemma max_min_distr : forall n m p, + max n (min m p) == min (max n m) (max n p). +Proof. + intros. symmetry. apply min_monotone. + eauto with *. + repeat red; intros. apply max_le_compat_l; auto. +Qed. + +Lemma min_max_distr : forall n m p, + min n (max m p) == max (min n m) (min n p). +Proof. + intros. symmetry. apply max_monotone. + eauto with *. + repeat red; intros. apply min_le_compat_l; auto. +Qed. + +(** Modularity *) + +Lemma max_min_modular : forall n m p, + max n (min m (max n p)) == min (max n m) (max n p). +Proof. + intros. rewrite <- max_min_distr. + destruct (max_spec n p) as [(C,E)|(C,E)]; rewrite E; auto. + destruct (min_spec m n) as [(C',E')|(C',E')]; rewrite E'. + rewrite 2 max_l; try OF.order. rewrite min_le_iff; auto. + rewrite 2 max_l; try OF.order. rewrite min_le_iff; auto. +Qed. + +Lemma min_max_modular : forall n m p, + min n (max m (min n p)) == max (min n m) (min n p). +Proof. + intros. rewrite <- min_max_distr. + destruct (min_spec n p) as [(C,E)|(C,E)]; rewrite E; auto. + destruct (max_spec m n) as [(C',E')|(C',E')]; rewrite E'. + rewrite 2 min_l; try OF.order. rewrite max_le_iff; right; OF.order. + rewrite 2 min_l; try OF.order. rewrite max_le_iff; auto. +Qed. + +(** Disassociativity *) + +Lemma max_min_disassoc : forall n m p, + min n (max m p) <= max (min n m) p. +Proof. + intros. rewrite min_max_distr. + auto using max_le_compat_l, le_min_r. +Qed. + +(** Anti-monotonicity swaps the role of [min] and [max] *) + +Lemma max_min_antimonotone : forall 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. + destruct (M.min_spec x y) as [(H,E)|(H,E)]; rewrite E; + destruct (M.max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. + assert (f y <= f x) by (apply Lef; OF.order). OF.order. + assert (f x <= f y) by (apply Lef; OF.order). OF.order. +Qed. + + +Lemma min_max_antimonotone : forall 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. + destruct (M.max_spec x y) as [(H,E)|(H,E)]; rewrite E; + destruct (M.min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. + assert (f y <= f x) by (apply Lef; OF.order). OF.order. + assert (f x <= f y) by (apply Lef; OF.order). OF.order. +Qed. + +End MinMaxProperties. + + + +(** Some Remaining questions... + +--> Compare with a type-classes version ? + +--> Is max_unicity and max_unicity_ext really convenient to express + that any possible definition of max will in fact be equivalent ? + +--> Is it possible to avoid copy-paste about min even more ? + +--> Can this modular approach be used for more complex things, + in particular div/mod ? + How can we share common parts between nat and Z in this case ? + How to handle different choices (Zdiv vs. ZOdiv) ? + +*) diff --git a/theories/Structures/OrderTac.v b/theories/Structures/OrderTac.v index 31c9324f8..8a3635686 100644 --- a/theories/Structures/OrderTac.v +++ b/theories/Structures/OrderTac.v @@ -27,7 +27,7 @@ Set Implicit Arguments. a strict order [lt] total and compatible with [eq], and a larger order [le] synonym of [lt\/eq]. *) -Module Type OrderTacSig. +Module Type OrderSig. Parameter Inline t : Type. Parameters eq lt le : t -> t -> Prop. @@ -37,7 +37,7 @@ Instance lt_compat : Proper (eq==>eq==>iff) lt. Parameter lt_total : forall x y, lt x y \/ eq x y \/ lt y x. Parameter le_lteq : forall x y, le x y <-> lt x y \/ eq x y. -End OrderTacSig. +End OrderSig. (** NB : we should _not_ use "Inline" for these predicates, otherwise the ltac matching will not work properly later. *) @@ -60,7 +60,7 @@ Infix "+" := trans_ord : order. (** ** [MakeOrderTac] : The functor providing the order tactic. *) -Module MakeOrderTac(Import O:OrderTacSig). +Module MakeOrderTac(Import O:OrderSig). Local Open Scope order. @@ -249,7 +249,8 @@ end. (** The complete tactic. *) -Ltac order := intros; order_prepare; order_loop; fail. +Ltac order := + intros; order_prepare; order_loop; fail "Order tactic unsuccessful". End MakeOrderTac. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index a8e1ebdd6..f0d4163c3 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -103,7 +103,7 @@ 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 : OrderTacSig + Module OrderElts : OrderSig with Definition t := t with Definition eq := eq with Definition lt := lt. diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v index 16da2162d..4d62c2716 100644 --- a/theories/Structures/OrderedType2.v +++ b/theories/Structures/OrderedType2.v @@ -8,18 +8,19 @@ (* $Id$ *) -Require Export SetoidList DecidableType2 OrderTac. +Require Export Relations Morphisms Setoid DecidableType2. Set Implicit Arguments. Unset Strict Implicit. (** * Ordered types *) -Definition Cmp (A:Type)(eq lt : relation A) c := - match c with - | Eq => eq - | Lt => lt - | Gt => flip lt - end. +Inductive Cmp {A} (eq lt:relation A)(x y : A) : comparison -> Prop := +| Cmp_eq : eq x y -> Cmp eq lt x y Eq +| Cmp_lt : lt x y -> Cmp eq lt x y Lt +| Cmp_gt : lt y x -> Cmp eq lt x y Gt. + +Hint Constructors Cmp. + Module Type MiniOrderedType. Include Type EqualityType. @@ -29,10 +30,11 @@ Module Type MiniOrderedType. Instance lt_compat : Proper (eq==>eq==>iff) lt. Parameter compare : t -> t -> comparison. - Axiom compare_spec : forall x y, Cmp eq lt (compare x y) x y. + Axiom compare_spec : forall x y, Cmp eq lt x y (compare x y). End MiniOrderedType. + Module Type OrderedType. Include Type MiniOrderedType. @@ -42,492 +44,60 @@ Module Type OrderedType. End OrderedType. + Module MOT_to_OT (Import O : MiniOrderedType) <: OrderedType. Include O. Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}. Proof. intros. - generalize (compare_spec x y); destruct (compare x y); - unfold Cmp, flip; intros. - left; auto. - right. intro H'; rewrite <- H' in H. - apply (StrictOrder_Irreflexive x); auto. - right. intro H'; rewrite <- H' in H. - apply (StrictOrder_Irreflexive x); auto. + assert (H:=compare_spec x y); destruct (compare x y). + left; inversion_clear H; auto. + right; inversion_clear H. intro H'. rewrite H' in *. + apply (StrictOrder_Irreflexive y); auto. + right; inversion_clear H. intro H'. rewrite H' in *. + apply (StrictOrder_Irreflexive y); auto. Defined. End MOT_to_OT. -(** * Ordered types properties *) - -(** Additional properties that can be derived from signature - [OrderedType]. *) - -Module OrderedTypeFacts (Import O: OrderedType). - - Infix "==" := eq (at level 70, no associativity) : order. - Infix "<" := lt : order. - Notation "x <= y" := (~lt y x) : order. - Infix "?=" := compare (at level 70, no associativity) : order. - - Local Open Scope order. - - Ltac elim_compare x y := - generalize (compare_spec x y); destruct (compare x y); - unfold Cmp, flip. - - Module OrderElts : OrderTacSig - with Definition t := t - with Definition eq := eq - with Definition lt := lt. - (* Opaque signature is crucial for ltac to work correctly later *) - Include O. - Definition le x y := x<y \/ x==y. - Lemma lt_total : forall x y, x<y \/ x==y \/ y<x. - Proof. intros; elim_compare x y; intuition. Qed. - 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. - - Ltac order := - change eq with OrderElts.eq in *; - change lt with OrderElts.lt in *; - OrderTac.order. - - (** The following lemmas are either re-phrasing of [eq_equiv] and - [lt_strorder] or immediately provable by [order]. Interest: - compatibility, test of order, etc *) - - Definition eq_refl (x:t) : x==x := Equivalence_Reflexive x. - - Definition eq_sym (x y:t) : x==y -> y==x := Equivalence_Symmetric x y. - - Definition eq_trans (x y z:t) : x==y -> y==z -> x==z := - Equivalence_Transitive x y z. - - Definition lt_trans (x y z:t) : x<y -> y<z -> x<z := - StrictOrder_Transitive x y z. - - 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'; intros; 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; intros; autorewrite with order; order. - Qed. - - (** For compatibility reasons *) - Definition eq_dec := eq_dec. - - Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}. - Proof. - intros; elim_compare x y; [ right | left | right ]; order. - Defined. - - Definition eqb x y : bool := if eq_dec x y then true else false. - - Lemma if_eq_dec : forall x y (B:Type)(b b':B), - (if eq_dec x y then b else b') = - (match compare x y with Eq => b | _ => b' end). - Proof. - intros; destruct eq_dec; elim_compare x y; auto; order. - Qed. - - Lemma eqb_alt : - forall x y, eqb x y = match compare x y with Eq => true | _ => false end. - Proof. - unfold eqb; intros; apply if_eq_dec. - Qed. - - Instance eqb_compat : Proper (eq==>eq==>Logic.eq) eqb. - Proof. - intros x x' Hxx' y y' Hyy'. - rewrite 2 eqb_alt, Hxx', Hyy'; auto. - Qed. - - -(* Specialization of resuts about lists modulo. *) - -Section ForNotations. - -Notation In:=(InA eq). -Notation Inf:=(lelistA lt). -Notation Sort:=(sort lt). -Notation NoDup:=(NoDupA eq). - -Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. -Proof. intros. rewrite <- H; auto. Qed. - -Lemma ListIn_In : forall l x, List.In x l -> In x l. -Proof. exact (In_InA eq_equiv). Qed. - -Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l. -Proof. exact (InfA_ltA lt_strorder). Qed. - -Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l. -Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed. - -Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x. -Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed. - -Lemma ListIn_Inf : forall l x, (forall y, List.In y l -> lt x y) -> Inf x l. -Proof. exact (@In_InfA t lt). Qed. - -Lemma In_Inf : forall l x, (forall y, In y l -> lt x y) -> Inf x l. -Proof. exact (InA_InfA eq_equiv (ltA:=lt)). Qed. - -Lemma Inf_alt : - forall l x, Sort l -> (Inf x l <-> (forall y, In y l -> lt x y)). -Proof. exact (InfA_alt eq_equiv lt_strorder lt_compat). Qed. - -Lemma Sort_NoDup : forall l, Sort l -> NoDup l. -Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat) . Qed. - -End ForNotations. - -Hint Resolve ListIn_In Sort_NoDup Inf_lt. -Hint Immediate In_eq Inf_lt. - -End OrderedTypeFacts. - - -(** Some tests of [order] : is it at least capable of - proving some basic properties ? *) -Module OrderedTypeTest (O:OrderedType). - Module Import MO := OrderedTypeFacts O. - Local Open Scope order. - Lemma lt_not_eq x y : x<y -> ~x==y. Proof. order. Qed. - Lemma lt_eq x y z : x<y -> y==z -> x<z. Proof. order. Qed. - Lemma eq_lt x y z : x==y -> y<z -> x<z. Proof. order. Qed. - Lemma le_eq x y z : x<=y -> y==z -> x<=z. Proof. order. Qed. - Lemma eq_le x y z : x==y -> y<=z -> x<=z. Proof. order. Qed. - Lemma neq_eq x y z : ~x==y -> y==z -> ~x==z. Proof. order. Qed. - Lemma eq_neq x y z : x==y -> ~y==z -> ~x==z. Proof. order. Qed. - Lemma le_lt_trans x y z : x<=y -> y<z -> x<z. Proof. order. Qed. - Lemma lt_le_trans x y z : x<y -> y<=z -> x<z. Proof. order. Qed. - Lemma le_trans x y z : x<=y -> y<=z -> x<=z. Proof. order. Qed. - Lemma le_antisym x y : x<=y -> y<=x -> x==y. Proof. order. Qed. - Lemma le_neq x y : x<=y -> ~x==y -> x<y. Proof. order. Qed. - Lemma neq_sym x y : ~x==y -> ~y==x. Proof. order. Qed. - Lemma lt_le x y : x<y -> x<=y. Proof. order. Qed. - Lemma gt_not_eq x y : y<x -> ~x==y. Proof. order. Qed. - Lemma eq_not_lt x y : x==y -> ~x<y. Proof. order. Qed. - Lemma eq_not_gt x y : x==y -> ~ y<x. Proof. order. Qed. - Lemma lt_not_gt x y : x<y -> ~ y<x. Proof. order. Qed. -End OrderedTypeTest. +(** * UsualOrderedType + A particular case of [OrderedType] where the equality is + the usual one of Coq. *) -(** * Relations over pairs (TO MIGRATE in some TypeClasses file) *) +Module Type UsualOrderedType. + Include Type UsualDecidableType. -Definition ProdRel {A B}(RA:relation A)(RB:relation B) : relation (A*B) := - fun p p' => RA (fst p) (fst p') /\ RB (snd p) (snd p'). + Parameter Inline lt : t -> t -> Prop. + Instance lt_strorder : StrictOrder lt. + (* The following is useless since eq is Leibniz, but should be there + for subtyping... *) + Instance lt_compat : Proper (eq==>eq==>iff) lt. -Definition FstRel {A B}(R:relation A) : relation (A*B) := - fun p p' => R (fst p) (fst p'). + Parameter compare : t -> t -> comparison. + Axiom compare_spec : forall x y, Cmp eq lt x y (compare x y). -Definition SndRel {A B}(R:relation B) : relation (A*B) := - fun p p' => R (snd p) (snd p'). +End UsualOrderedType. -Generalizable Variables A B RA RB Ri Ro. +(** a [UsualOrderedType] is in particular an [OrderedType]. *) -Instance ProdRel_equiv {A B} `(Equivalence A RA)`(Equivalence B RB) : - Equivalence (ProdRel RA RB). -Proof. firstorder. Qed. +Module UOT_to_OT (U:UsualOrderedType) <: OrderedType := U. -Instance FstRel_equiv {A B} `(Equivalence A RA) : - Equivalence (FstRel RA (B:=B)). -Proof. firstorder. Qed. -Instance SndRel_equiv {A B} `(Equivalence B RB) : - Equivalence (SndRel RB (A:=A)). -Proof. firstorder. Qed. +(** * OrderedType with also a [<=] predicate *) -Instance FstRel_strorder {A B} `(StrictOrder A RA) : - StrictOrder (FstRel RA (B:=B)). -Proof. firstorder. Qed. +Module Type OrderedTypeFull. + Include Type OrderedType. + Parameter Inline le : t -> t -> Prop. + Axiom le_lteq : forall x y, le x y <-> lt x y \/ eq x y. +End OrderedTypeFull. -Instance SndRel_strorder {A B} `(StrictOrder B RB) : - StrictOrder (SndRel RB (A:=A)). -Proof. firstorder. Qed. - -Lemma FstRel_ProdRel {A B}(RA:relation A) : forall p p':A*B, - (FstRel RA) p p' <-> (ProdRel RA (fun _ _ =>True)) p p'. -Proof. firstorder. Qed. - -Lemma SndRel_ProdRel {A B}(RB:relation B) : forall p p':A*B, - (SndRel RB) p p' <-> (ProdRel (fun _ _ =>True) RB) p p'. -Proof. firstorder. Qed. - -Lemma ProdRel_alt {A B}(RA:relation A)(RB:relation B) : forall p p':A*B, - (ProdRel RA RB) p p' <-> relation_conjunction (FstRel RA) (SndRel RB) p p'. -Proof. firstorder. Qed. - -Instance FstRel_compat {A B} (R : relation A)`(Proper _ (Ri==>Ri==>Ro) R) : - Proper (FstRel Ri==>FstRel Ri==>Ro) (FstRel R (B:=B)). -Proof. - intros A B R Ri Ro H (a1,b1) (a1',b1') Hab1 (a2,b2) (a2',b2') Hab2. - unfold FstRel in *; simpl in *. apply H; auto. -Qed. - -Instance SndRel_compat {A B} (R : relation B)`(Proper _ (Ri==>Ri==>Ro) R) : - Proper (SndRel Ri==>SndRel Ri==>Ro) (SndRel R (A:=A)). -Proof. - intros A B R Ri Ro H (a1,b1) (a1',b1') Hab1 (a2,b2) (a2',b2') Hab2. - unfold SndRel in *; simpl in *. apply H; auto. -Qed. - -Instance FstRel_sub {A B} (RA:relation A)(RB:relation B): - subrelation (ProdRel RA RB) (FstRel RA). -Proof. firstorder. Qed. - -Instance SndRel_sub {A B} (RA:relation A)(RB:relation B): - subrelation (ProdRel RA RB) (SndRel RB). -Proof. firstorder. Qed. - -Instance pair_compat { A B } (RA:relation A)(RB : relation B) : - Proper (RA==>RB==>ProdRel RA RB) (@pair A B). -Proof. firstorder. Qed. - - -Hint Unfold ProdRel FstRel SndRel. -Hint Extern 2 (ProdRel _ _ _ _) => split. - - -Module KeyOrderedType(Import O:OrderedType). - Module Import MO:=OrderedTypeFacts(O). - - Section Elt. - Variable elt : Type. - Notation key:=t. - - Definition eqk : relation (key*elt) := FstRel eq. - Definition eqke : relation (key*elt) := ProdRel eq Logic.eq. - Definition ltk : relation (key*elt) := FstRel lt. - - Hint Unfold eqk eqke ltk. - - (* eqke is stricter than eqk *) - - Global Instance eqke_eqk : subrelation eqke eqk. - Proof. unfold eqke, eqk; auto with *. Qed. - - (* eqk, eqke are equalities, ltk is a strict order *) - - Global Instance eqk_equiv : Equivalence eqk. - - Global Instance eqke_equiv : Equivalence eqke. - - Global Instance ltk_strorder : StrictOrder ltk. - - Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk. - Proof. unfold eqk, ltk; auto with *. Qed. - - (* Additionnal facts *) - - Global Instance pair_compat : Proper (eq==>Logic.eq==>eqke) (@pair key elt). - Proof. unfold eqke; auto with *. Qed. - - Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'. - Proof. - intros e e' LT EQ; rewrite EQ in LT. - elim (StrictOrder_Irreflexive _ LT). - Qed. - - Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'. - Proof. - intros e e' LT EQ; rewrite EQ in LT. - elim (StrictOrder_Irreflexive _ LT). - Qed. - - Lemma InA_eqke_eqk : - forall x m, InA eqke x m -> InA eqk x m. - Proof. - unfold eqke, ProdRel; induction 1; intuition. - Qed. - Hint Resolve InA_eqke_eqk. - - Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). - Definition In k m := exists e:elt, MapsTo k e m. - Notation Sort := (sort ltk). - Notation Inf := (lelistA ltk). - - Hint Unfold MapsTo In. - - (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) - - Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. - Proof. - firstorder. - exists x; auto. - induction H. - destruct y; compute in H. - exists e; auto. - destruct IHInA as [e H0]. - exists e; auto. - Qed. - - Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l. - Proof. - unfold In, MapsTo. - setoid_rewrite Exists_exists; setoid_rewrite InA_alt. - firstorder. - exists (snd x), x; auto. - Qed. - - Lemma In_nil : forall k, In k nil <-> False. - Proof. - intros; rewrite In_alt2; apply Exists_nil. - Qed. - - Lemma In_cons : forall k p l, - In k (p::l) <-> eq k (fst p) \/ In k l. - Proof. - intros; rewrite !In_alt2, Exists_cons; intuition. - Qed. - - Global Instance MapsTo_compat : - Proper (eq==>Logic.eq==>equivlistA eqke==>iff) MapsTo. - Proof. - intros x x' Hx e e' He l l' Hl. unfold MapsTo. - rewrite Hx, He, Hl; intuition. - Qed. - - Global Instance In_compat : Proper (eq==>equivlistA eqk==>iff) In. - Proof. - intros x x' Hx l l' Hl. rewrite !In_alt. - setoid_rewrite Hl. setoid_rewrite Hx. intuition. - Qed. - - Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. - Proof. intros l x y e EQ. rewrite <- EQ; auto. Qed. - - Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. - Proof. intros l x y EQ. rewrite <- EQ; auto. Qed. - - Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l. - Proof. intros l x x' H. rewrite H; auto. Qed. - - Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l. - Proof. apply InfA_ltA; auto with *. Qed. - - Hint Immediate Inf_eq. - Hint Resolve Inf_lt. - - Lemma Sort_Inf_In : - forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p. - Proof. apply SortA_InfA_InA; auto with *. Qed. - - Lemma Sort_Inf_NotIn : - forall l k e, Sort l -> Inf (k,e) l -> ~In k l. - Proof. - intros; red; intros. - destruct H1 as [e' H2]. - elim (@ltk_not_eqk (k,e) (k,e')). - eapply Sort_Inf_In; eauto. - red; simpl; auto. - Qed. - - Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l. - Proof. apply SortA_NoDupA; auto with *. Qed. - - Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'. - Proof. - intros; invlist sort; eapply Sort_Inf_In; eauto. - Qed. - - Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) -> - ltk e e' \/ eqk e e'. - Proof. - intros; invlist InA; auto. - left; apply Sort_In_cons_1 with l; auto. - Qed. - - Lemma Sort_In_cons_3 : - forall x l k e, Sort ((k,e)::l) -> In x l -> ~eq x k. - Proof. - intros; invlist sort; red; intros. - eapply Sort_Inf_NotIn; eauto using In_eq. - Qed. - - Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. - Proof. - intros; invlist In; invlist MapsTo. compute in * |- ; intuition. - right; exists x; auto. - Qed. - - Lemma In_inv_2 : forall k k' e e' l, - InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l. - Proof. - intros; invlist InA; intuition. - Qed. - - Lemma In_inv_3 : forall x x' l, - InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l. - Proof. - intros; invlist InA; compute in * |- ; intuition. - Qed. - - End Elt. - - Hint Resolve (fun elt => @Equivalence_Reflexive _ _ (eqk_equiv elt)). - Hint Resolve (fun elt => @Equivalence_Transitive _ _ (eqk_equiv elt)). - Hint Immediate (fun elt => @Equivalence_Symmetric _ _ (eqk_equiv elt)). - Hint Resolve (fun elt => @Equivalence_Reflexive _ _ (eqke_equiv elt)). - Hint Resolve (fun elt => @Equivalence_Transitive _ _ (eqke_equiv elt)). - Hint Immediate (fun elt => @Equivalence_Symmetric _ _ (eqke_equiv elt)). - Hint Resolve (fun elt => @StrictOrder_Transitive _ _ (ltk_strorder elt)). - - Hint Unfold eqk eqke ltk. - Hint Extern 2 (eqke ?a ?b) => split. - Hint Resolve ltk_not_eqk ltk_not_eqke. - Hint Resolve InA_eqke_eqk. - Hint Unfold MapsTo In. - Hint Immediate Inf_eq. - Hint Resolve Inf_lt. - Hint Resolve Sort_Inf_NotIn. - Hint Resolve In_inv_2 In_inv_3. - -End KeyOrderedType. +Module OT_to_Full (O:OrderedType) <: OrderedTypeFull. + Include O. + Definition le x y := lt x y \/ eq x y. + Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y. + Proof. unfold le; split; auto. Qed. +End OT_to_Full. diff --git a/theories/Structures/OrderedType2Alt.v b/theories/Structures/OrderedType2Alt.v index 6c2fb0d3f..4e14f5128 100644 --- a/theories/Structures/OrderedType2Alt.v +++ b/theories/Structures/OrderedType2Alt.v @@ -76,7 +76,7 @@ Module Update_OT (O:OrderedTypeOrig) <: OrderedType. | GT _ => Gt end. - Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y. + Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y). Proof. intros; unfold compare; destruct O.compare; auto. Qed. @@ -101,8 +101,9 @@ Module Backport_OT (O:OrderedType) <: OrderedTypeOrig. Definition compare : forall x y, Compare lt eq x y. Proof. - intros. generalize (O.compare_spec x y); unfold Cmp, flip. - destruct (O.compare x y); [apply EQ|apply LT|apply GT]; auto. + intros. assert (H:=O.compare_spec x y). + destruct (O.compare x y); [apply EQ|apply LT|apply GT]; + inversion H; auto. Defined. End Backport_OT. @@ -168,10 +169,11 @@ Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType. Definition compare := O.compare. - Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y. + Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y). Proof. - unfold Cmp, flip, eq, lt, compare; intros. + unfold eq, lt, compare; intros. destruct (O.compare x y) as [ ]_eqn:H; auto. + apply Cmp_gt. rewrite compare_sym, H; auto. Qed. @@ -196,8 +198,8 @@ Module OT_to_Alt (Import O:OrderedType) <: OrderedTypeAlt. forall x y, (y?=x) = CompOpp (x?=y). Proof. intros x y; unfold compare. - generalize (compare_spec x y) (compare_spec y x); unfold Cmp, flip. - destruct (O.compare x y); destruct (O.compare y x); intros U V; auto. + destruct (compare_spec x y) as [U|U|U]; + destruct (compare_spec y x) as [V|V|V]; auto. rewrite U in V. elim (StrictOrder_Irreflexive y); auto. rewrite U in V. elim (StrictOrder_Irreflexive y); auto. rewrite V in U. elim (StrictOrder_Irreflexive x); auto. @@ -209,8 +211,8 @@ Module OT_to_Alt (Import O:OrderedType) <: OrderedTypeAlt. Lemma compare_Eq : forall x y, compare x y = Eq <-> eq x y. Proof. unfold compare. - intros x y; generalize (compare_spec x y). - destruct (O.compare x y); intuition; try discriminate. + intros x y; destruct (compare_spec x y); intuition; + try discriminate. rewrite H0 in H. elim (StrictOrder_Irreflexive y); auto. rewrite H0 in H. elim (StrictOrder_Irreflexive y); auto. Qed. @@ -218,8 +220,8 @@ Module OT_to_Alt (Import O:OrderedType) <: OrderedTypeAlt. Lemma compare_Lt : forall x y, compare x y = Lt <-> lt x y. Proof. unfold compare. - intros x y; generalize (compare_spec x y); unfold Cmp, flip. - destruct (O.compare x y); intuition; try discriminate. + intros x y; destruct (compare_spec x y); intuition; + try discriminate. rewrite H in H0. elim (StrictOrder_Irreflexive y); auto. rewrite H in H0. elim (StrictOrder_Irreflexive x); auto. Qed. diff --git a/theories/Structures/OrderedType2Ex.v b/theories/Structures/OrderedType2Ex.v index 73bd3810f..801c18723 100644 --- a/theories/Structures/OrderedType2Ex.v +++ b/theories/Structures/OrderedType2Ex.v @@ -13,174 +13,18 @@ (* $Id$ *) -Require Import OrderedType2 DecidableType2Ex. -Require Import ZArith NArith Ndec Compare_dec. +Require Import OrderedType2 NatOrderedType POrderedType NOrderedType + ZOrderedType DecidableType2Ex RelationPairs. (** * Examples of Ordered Type structures. *) -(** First, a particular case of [OrderedType] where - the equality is the usual one of Coq. *) -Module Type UsualOrderedType. - Include Type UsualDecidableType. - - Parameter Inline lt : t -> t -> Prop. - Instance lt_strorder : StrictOrder lt. - (* The following is useless since eq is Leibniz, but should be there - for subtyping... *) - Instance lt_compat : Proper (eq==>eq==>iff) lt. - - Parameter compare : t -> t -> comparison. - Axiom compare_spec : forall x y, Cmp eq lt (compare x y) x y. - -End UsualOrderedType. - -(** a [UsualOrderedType] is in particular an [OrderedType]. *) - -Module UOT_to_OT (U:UsualOrderedType) <: OrderedType := U. - -(** [nat] is an ordered type with respect to the usual order on natural numbers. *) - -Module Nat_as_OT <: UsualOrderedType. - - Definition t := nat. - Definition eq := @eq nat. - Definition lt := lt. - Definition compare := nat_compare. - Definition eq_dec := eq_nat_dec. - - Program Instance eq_equiv : Equivalence eq. - - Instance lt_strorder : StrictOrder lt. - Proof. - constructor; [exact lt_irrefl|exact lt_trans]. - Qed. - - Instance lt_compat : Proper (eq==>eq==>iff) lt. - Proof. - unfold eq in *; repeat red; intros; subst; auto. - Qed. - - Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y. - Proof. - intros. - unfold Cmp, flip, lt, eq. destruct (compare x y) as [ ]_eqn:H. - apply nat_compare_eq; auto. - apply nat_compare_Lt_lt; auto. - apply nat_compare_Gt_gt; auto. - Qed. - -End Nat_as_OT. - - -(** [Z] is an ordered type with respect to the usual order on integers. *) - -Module Z_as_OT <: UsualOrderedType. - - Definition t := Z. - Definition eq := @eq Z. - Definition lt := Zlt. - Definition compare := Zcompare. - Definition eq_dec := Z_eq_dec. - - Program Instance eq_equiv : Equivalence eq. - - Instance lt_strorder : StrictOrder lt. - Proof. - constructor; [exact Zlt_irrefl | exact Zlt_trans]. - Qed. - - Instance lt_compat : Proper (eq==>eq==>iff) lt. - Proof. - unfold eq in *; repeat red; intros; subst; auto. - Qed. - - Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y. - Proof. - intros. - unfold Cmp, flip, lt, eq. destruct (compare x y) as [ ]_eqn:H. - apply Zcompare_Eq_eq; auto. - auto. - apply Zgt_lt; auto. - Qed. - -End Z_as_OT. - -(** [positive] is an ordered type with respect to the usual order - on natural numbers. *) - -Module Positive_as_OT <: UsualOrderedType. - Definition t:=positive. - Definition eq:=@eq positive. - Definition lt:=Plt. - Definition compare x y := Pcompare x y Eq. - - Program Instance eq_equiv : Equivalence eq. - - Instance lt_strorder : StrictOrder lt. - Proof. - constructor; [exact Plt_irrefl | exact Plt_trans]. - Qed. - - Instance lt_compat : Proper (eq==>eq==>iff) lt. - Proof. - unfold eq in *; repeat red; intros; subst; auto. - Qed. - - Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y. - Proof. - intros. - unfold Cmp, flip, lt, eq. destruct (compare x y) as [ ]_eqn:H. - apply Pcompare_Eq_eq; auto. - auto. - apply ZC1; auto. - Qed. - - Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }. - Proof. - intros; unfold eq; decide equality. - Defined. - -End Positive_as_OT. - - -(** [N] is an ordered type with respect to the usual order - on natural numbers. *) - -Module N_as_OT <: UsualOrderedType. - Definition t:=N. - Definition eq:=@eq N. - Definition lt:=Nlt. - Definition compare:=Ncompare. - - Program Instance eq_equiv : Equivalence eq. - - Instance lt_strorder : StrictOrder lt. - Proof. - constructor; [exact Nlt_irrefl | exact Nlt_trans]. - Qed. - - Instance lt_compat : Proper (eq==>eq==>iff) lt. - Proof. - unfold eq in *; repeat red; intros; subst; auto. - Qed. - - Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y. - Proof. - intros. - unfold Cmp, flip, lt, eq. destruct (compare x y) as [ ]_eqn:H. - apply Ncompare_Eq_eq; auto. - auto. - apply Ngt_Nlt; auto. - Qed. - - 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. - -End N_as_OT. +(** Ordered Type for [nat], [Positive], [N], [Z] with the usual order. *) +Module Nat_as_OT := NatOrderedType.Nat_as_OT. +Module Positive_as_OT := POrderedType.Positive_as_OT. +Module N_as_OT := NOrderedType.N_as_OT. +Module Z_as_OT := ZOrderedType.Z_as_OT. (** An OrderedType can now directly be seen as a DecidableType *) @@ -195,21 +39,14 @@ Module Z_as_DT <: UsualDecidableType := Z_as_OT. - (** From two ordered types, we can build a new OrderedType over their cartesian product, using the lexicographic order. *) Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. + Include PairDecidableType O1 O2. - Definition t := prod O1.t O2.t. - - Definition eq := ProdRel O1.eq O2.eq. - - Definition lt x y := - O1.lt (fst x) (fst y) \/ - (O1.eq (fst x) (fst y) /\ O2.lt (snd x) (snd y)). - - Instance eq_equiv : Equivalence eq. + Definition lt := + (relation_disjunction (O1.lt @@ fst) (O1.eq * O2.lt))%signature. Instance lt_strorder : StrictOrder lt. Proof. @@ -219,7 +56,7 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. apply (StrictOrder_Irreflexive x1); auto. apply (StrictOrder_Irreflexive x2); intuition. (* transitive *) - intros (x1,x2) (y1,y2) (z1,z2); unfold eq, lt; simpl; intuition. + intros (x1,x2) (y1,y2) (z1,z2). compute. intuition. left; etransitivity; eauto. left; rewrite <- H0; auto. left; rewrite H; auto. @@ -228,8 +65,8 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. Instance lt_compat : Proper (eq==>eq==>iff) lt. Proof. + compute. intros (x1,x2) (x1',x2') (X1,X2) (y1,y2) (y1',y2') (Y1,Y2). - unfold lt; simpl in *. rewrite X1,X2,Y1,Y2; intuition. Qed. @@ -240,22 +77,12 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. | Gt => Gt end. - Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y. + Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y). Proof. - intros (x1,x2) (y1,y2); unfold Cmp, flip, compare, eq, lt; simpl. - generalize (O1.compare_spec x1 y1); destruct (O1.compare x1 y1); intros; auto. - generalize (O2.compare_spec x2 y2); destruct (O2.compare x2 y2); intros; auto. + intros (x1,x2) (y1,y2); unfold compare; simpl. + destruct (O1.compare_spec x1 y1); try (constructor; compute; auto). + destruct (O2.compare_spec x2 y2); constructor; compute; auto. Qed. - Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}. - Proof. - intros; generalize (compare_spec x y); destruct (compare x y). - left; auto. - right. intros E; rewrite E in *. - apply (StrictOrder_Irreflexive y); auto. - right. intros E; rewrite E in *. - apply (StrictOrder_Irreflexive y); auto. - Defined. - End PairOrderedType. diff --git a/theories/Structures/OrderedType2Facts.v b/theories/Structures/OrderedType2Facts.v new file mode 100644 index 000000000..382b6366d --- /dev/null +++ b/theories/Structures/OrderedType2Facts.v @@ -0,0 +1,264 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +Require Import Basics OrderTac. +Require Export OrderedType2. + + +Set Implicit Arguments. +Unset Strict Implicit. + + +(** * Properties of ordered types *) + +(** First, an OrderdType (with [<=]) is enough for building an [order] + tactic. *) + +Module OTF_to_OrderSig (O : OrderedTypeFull) : + OrderSig with Definition t := O.t + with Definition eq := O.eq + with Definition lt := O.lt + with Definition le := O.le. + Include O. + Lemma lt_total : forall x y, O.lt x y \/ O.eq x y \/ O.lt y x. + Proof. intros; destruct (O.compare_spec x y); auto. Qed. +End OTF_to_OrderSig. + + +Module OTF_to_OrderTac (O:OrderedTypeFull). + Module OrderElts := OTF_to_OrderSig O. + Module OrderTac := MakeOrderTac OrderElts. + Ltac order := + change O.eq with OrderElts.eq in *; + change O.lt with OrderElts.lt in *; + change O.le with OrderElts.le in *; + OrderTac.order. +End OTF_to_OrderTac. + + +(** This allows to prove a few properties of [<=] *) + +Module OrderedTypeFullFacts (Import O:OrderedTypeFull). + + Module Order := OTF_to_OrderTac O. + Ltac order := Order.order. + + Instance le_compat : Proper (eq==>eq==>iff) le. + Proof. repeat red; intuition; order. Qed. + + Instance le_preorder : PreOrder le. + Proof. split; red; order. Qed. + + Instance le_order : PartialOrder eq le. + Proof. compute; intuition; order. Qed. + + Instance le_antisym : Antisymmetric _ eq le. + Proof. apply partial_order_antisym; auto with *. Qed. + + Lemma le_not_gt_iff : forall x y, le x y <-> ~lt y x. + Proof. split; order. Qed. + + Lemma lt_not_ge_iff : forall x y, lt x y <-> ~le y x. + Proof. split; order. Qed. + + Lemma le_or_gt : forall x y, le x y \/ lt y x. + Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); auto. Qed. + + Lemma lt_or_ge : forall x y, lt x y \/ le y x. + Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); auto. Qed. + + Lemma eq_is_le_ge : forall x y, eq x y <-> le x y /\ le y x. + Proof. intuition; order. Qed. + +End OrderedTypeFullFacts. + + +(** * Properties of OrderedType *) + +Module OrderedTypeFacts (Import O: OrderedType). + Module O' := OT_to_Full O. + Module Order := OTF_to_OrderTac O'. + Ltac order := Order.order. + + Infix "==" := eq (at level 70, no associativity) : order. + Infix "<" := lt : order. + Notation "x <= y" := (~lt y x) : order. + Infix "?=" := compare (at level 70, no associativity) : order. + + Local Open Scope order. + + Tactic Notation "elim_compare" constr(x) constr(y) := + destruct (compare_spec x y). + + Tactic Notation "elim_compare" constr(x) constr(y) "as" ident(h) := + destruct (compare_spec x y) as [h|h|h]. + + (** The following lemmas are either re-phrasing of [eq_equiv] and + [lt_strorder] or immediately provable by [order]. Interest: + compatibility, test of order, etc *) + + Definition eq_refl (x:t) : x==x := Equivalence_Reflexive x. + + Definition eq_sym (x y:t) : x==y -> y==x := Equivalence_Symmetric x y. + + Definition eq_trans (x y z:t) : x==y -> y==z -> x==z := + Equivalence_Transitive x y z. + + Definition lt_trans (x y z:t) : x<y -> y<z -> x<z := + StrictOrder_Transitive x y z. + + 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; autorewrite with order; order. + Qed. + + (** For compatibility reasons *) + Definition eq_dec := eq_dec. + + Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}. + Proof. + intros; assert (H:=compare_spec x y); destruct (compare x y); + [ right | left | right ]; inversion_clear H; order. + Defined. + + Definition eqb x y : bool := if eq_dec x y then true else false. + + Lemma if_eq_dec : forall x y (B:Type)(b b':B), + (if eq_dec x y then b else b') = + (match compare x y with Eq => b | _ => b' end). + Proof. + intros; destruct eq_dec; elim_compare x y; auto; order. + Qed. + + Lemma eqb_alt : + forall x y, eqb x y = match compare x y with Eq => true | _ => false end. + Proof. + unfold eqb; intros; apply if_eq_dec. + Qed. + + Instance eqb_compat : Proper (eq==>eq==>Logic.eq) eqb. + Proof. + intros x x' Hxx' y y' Hyy'. + rewrite 2 eqb_alt, Hxx', Hyy'; auto. + Qed. + +End OrderedTypeFacts. + + + + + + +(** * Tests of the order tactic + + Is it at least capable of proving some basic properties ? *) + +Module OrderedTypeTest (O:OrderedType). + Module Import MO := OrderedTypeFacts O. + Local Open Scope order. + Lemma lt_not_eq x y : x<y -> ~x==y. Proof. order. Qed. + Lemma lt_eq x y z : x<y -> y==z -> x<z. Proof. order. Qed. + Lemma eq_lt x y z : x==y -> y<z -> x<z. Proof. order. Qed. + Lemma le_eq x y z : x<=y -> y==z -> x<=z. Proof. order. Qed. + Lemma eq_le x y z : x==y -> y<=z -> x<=z. Proof. order. Qed. + Lemma neq_eq x y z : ~x==y -> y==z -> ~x==z. Proof. order. Qed. + Lemma eq_neq x y z : x==y -> ~y==z -> ~x==z. Proof. order. Qed. + Lemma le_lt_trans x y z : x<=y -> y<z -> x<z. Proof. order. Qed. + Lemma lt_le_trans x y z : x<y -> y<=z -> x<z. Proof. order. Qed. + Lemma le_trans x y z : x<=y -> y<=z -> x<=z. Proof. order. Qed. + Lemma le_antisym x y : x<=y -> y<=x -> x==y. Proof. order. Qed. + Lemma le_neq x y : x<=y -> ~x==y -> x<y. Proof. order. Qed. + Lemma neq_sym x y : ~x==y -> ~y==x. Proof. order. Qed. + Lemma lt_le x y : x<y -> x<=y. Proof. order. Qed. + Lemma gt_not_eq x y : y<x -> ~x==y. Proof. order. Qed. + Lemma eq_not_lt x y : x==y -> ~x<y. Proof. order. Qed. + Lemma eq_not_gt x y : x==y -> ~ y<x. Proof. order. Qed. + Lemma lt_not_gt x y : x<y -> ~ y<x. Proof. order. Qed. + Lemma eq_is_nlt_ngt x y : x==y <-> ~x<y /\ ~y<x. + Proof. intuition; order. Qed. +End OrderedTypeTest. + + + +(** * Reversed OrderedTypeFull. + + we can switch the orientation of the order. This is used for + example when deriving properties of [min] out of the ones of [max] + (see [GenericMinMax]). +*) + +Module OrderedTypeRev (O:OrderedTypeFull) <: OrderedTypeFull. + +Definition t := O.t. +Definition eq := O.eq. +Instance eq_equiv : Equivalence eq. +Definition eq_dec := O.eq_dec. + +Definition lt := flip O.lt. +Definition le := flip O.le. + +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, le x y <-> lt x y \/ eq x y. +Proof. intros; unfold le, lt, flip. rewrite O.le_lteq; intuition. Qed. + +Definition compare := flip O.compare. + +Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y). +Proof. +intros; unfold compare, eq, lt, flip. +destruct (O.compare_spec y x); auto. +Qed. + +End OrderedTypeRev. + diff --git a/theories/Structures/OrderedType2Lists.v b/theories/Structures/OrderedType2Lists.v new file mode 100644 index 000000000..4aa07dfdc --- /dev/null +++ b/theories/Structures/OrderedType2Lists.v @@ -0,0 +1,264 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +Require Export RelationPairs SetoidList OrderedType2. + +Set Implicit Arguments. +Unset Strict Implicit. + +(** * Specialization of results about lists modulo. *) + +Module OrderedTypeLists (Import O:OrderedType). + +Section ForNotations. + +Notation In:=(InA eq). +Notation Inf:=(lelistA lt). +Notation Sort:=(sort lt). +Notation NoDup:=(NoDupA eq). + +Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. +Proof. intros. rewrite <- H; auto. Qed. + +Lemma ListIn_In : forall l x, List.In x l -> In x l. +Proof. exact (In_InA eq_equiv). Qed. + +Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l. +Proof. exact (InfA_ltA lt_strorder). Qed. + +Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l. +Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed. + +Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x. +Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed. + +Lemma ListIn_Inf : forall l x, (forall y, List.In y l -> lt x y) -> Inf x l. +Proof. exact (@In_InfA t lt). Qed. + +Lemma In_Inf : forall l x, (forall y, In y l -> lt x y) -> Inf x l. +Proof. exact (InA_InfA eq_equiv (ltA:=lt)). Qed. + +Lemma Inf_alt : + forall l x, Sort l -> (Inf x l <-> (forall y, In y l -> lt x y)). +Proof. exact (InfA_alt eq_equiv lt_strorder lt_compat). Qed. + +Lemma Sort_NoDup : forall l, Sort l -> NoDup l. +Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat) . Qed. + +End ForNotations. + +Hint Resolve ListIn_In Sort_NoDup Inf_lt. +Hint Immediate In_eq Inf_lt. + +End OrderedTypeLists. + + + + + +(** * Results about keys and data as manipulated in FMaps. *) + + +Module KeyOrderedType(Import O:OrderedType). + Module Import MO:=OrderedTypeLists(O). + + Section Elt. + Variable elt : Type. + Notation key:=t. + + Local Open Scope signature_scope. + + Definition eqk : relation (key*elt) := eq @@ fst. + Definition eqke : relation (key*elt) := eq * Logic.eq. + Definition ltk : relation (key*elt) := lt @@ fst. + + Hint Unfold eqk eqke ltk. + + (* eqke is stricter than eqk *) + + Global Instance eqke_eqk : subrelation eqke eqk. + Proof. firstorder. Qed. + + (* eqk, eqke are equalities, ltk is a strict order *) + + Global Instance eqk_equiv : Equivalence eqk. + + Global Instance eqke_equiv : Equivalence eqke. + + Global Instance ltk_strorder : StrictOrder ltk. + + Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk. + Proof. unfold eqk, ltk; auto with *. Qed. + + (* Additionnal facts *) + + Global Instance pair_compat : Proper (eq==>Logic.eq==>eqke) (@pair key elt). + Proof. apply pair_compat. Qed. + + Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'. + Proof. + intros e e' LT EQ; rewrite EQ in LT. + elim (StrictOrder_Irreflexive _ LT). + Qed. + + Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'. + Proof. + intros e e' LT EQ; rewrite EQ in LT. + elim (StrictOrder_Irreflexive _ LT). + Qed. + + Lemma InA_eqke_eqk : + forall x m, InA eqke x m -> InA eqk x m. + Proof. + unfold eqke, RelProd; induction 1; firstorder. + Qed. + Hint Resolve InA_eqke_eqk. + + Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). + Definition In k m := exists e:elt, MapsTo k e m. + Notation Sort := (sort ltk). + Notation Inf := (lelistA ltk). + + Hint Unfold MapsTo In. + + (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) + + Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. + Proof. + firstorder. + exists x; auto. + induction H. + destruct y; compute in H. + exists e; left; auto. + destruct IHInA as [e H0]. + exists e; auto. + Qed. + + Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l. + Proof. + unfold In, MapsTo. + setoid_rewrite Exists_exists; setoid_rewrite InA_alt. + firstorder. + exists (snd x), x; auto. + Qed. + + Lemma In_nil : forall k, In k nil <-> False. + Proof. + intros; rewrite In_alt2; apply Exists_nil. + Qed. + + Lemma In_cons : forall k p l, + In k (p::l) <-> eq k (fst p) \/ In k l. + Proof. + intros; rewrite !In_alt2, Exists_cons; intuition. + Qed. + + Global Instance MapsTo_compat : + Proper (eq==>Logic.eq==>equivlistA eqke==>iff) MapsTo. + Proof. + intros x x' Hx e e' He l l' Hl. unfold MapsTo. + rewrite Hx, He, Hl; intuition. + Qed. + + Global Instance In_compat : Proper (eq==>equivlistA eqk==>iff) In. + Proof. + intros x x' Hx l l' Hl. rewrite !In_alt. + setoid_rewrite Hl. setoid_rewrite Hx. intuition. + Qed. + + Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. + Proof. intros l x y e EQ. rewrite <- EQ; auto. Qed. + + Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. + Proof. intros l x y EQ. rewrite <- EQ; auto. Qed. + + Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l. + Proof. intros l x x' H. rewrite H; auto. Qed. + + Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l. + Proof. apply InfA_ltA; auto with *. Qed. + + Hint Immediate Inf_eq. + Hint Resolve Inf_lt. + + Lemma Sort_Inf_In : + forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p. + Proof. apply SortA_InfA_InA; auto with *. Qed. + + Lemma Sort_Inf_NotIn : + forall l k e, Sort l -> Inf (k,e) l -> ~In k l. + Proof. + intros; red; intros. + destruct H1 as [e' H2]. + elim (@ltk_not_eqk (k,e) (k,e')). + eapply Sort_Inf_In; eauto. + red; simpl; auto. + Qed. + + Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l. + Proof. apply SortA_NoDupA; auto with *. Qed. + + Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'. + Proof. + intros; invlist sort; eapply Sort_Inf_In; eauto. + Qed. + + Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) -> + ltk e e' \/ eqk e e'. + Proof. + intros; invlist InA; auto. + left; apply Sort_In_cons_1 with l; auto. + Qed. + + Lemma Sort_In_cons_3 : + forall x l k e, Sort ((k,e)::l) -> In x l -> ~eq x k. + Proof. + intros; invlist sort; red; intros. + eapply Sort_Inf_NotIn; eauto using In_eq. + Qed. + + Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. + Proof. + intros; invlist In; invlist MapsTo. compute in * |- ; intuition. + right; exists x; auto. + Qed. + + Lemma In_inv_2 : forall k k' e e' l, + InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l. + Proof. + intros; invlist InA; intuition. + Qed. + + Lemma In_inv_3 : forall x x' l, + InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l. + Proof. + intros; invlist InA; compute in * |- ; intuition. + Qed. + + End Elt. + + Hint Resolve (fun elt => @Equivalence_Reflexive _ _ (eqk_equiv elt)). + Hint Resolve (fun elt => @Equivalence_Transitive _ _ (eqk_equiv elt)). + Hint Immediate (fun elt => @Equivalence_Symmetric _ _ (eqk_equiv elt)). + Hint Resolve (fun elt => @Equivalence_Reflexive _ _ (eqke_equiv elt)). + Hint Resolve (fun elt => @Equivalence_Transitive _ _ (eqke_equiv elt)). + Hint Immediate (fun elt => @Equivalence_Symmetric _ _ (eqke_equiv elt)). + Hint Resolve (fun elt => @StrictOrder_Transitive _ _ (ltk_strorder elt)). + + Hint Unfold eqk eqke ltk. + Hint Extern 2 (eqke ?a ?b) => split. + Hint Resolve ltk_not_eqk ltk_not_eqke. + Hint Resolve InA_eqke_eqk. + Hint Unfold MapsTo In. + Hint Immediate Inf_eq. + Hint Resolve Inf_lt. + Hint Resolve Sort_Inf_NotIn. + Hint Resolve In_inv_2 In_inv_3. + +End KeyOrderedType. + diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v index 956221cb3..cd866c375 100644 --- a/theories/ZArith/ZArith_base.v +++ b/theories/ZArith/ZArith_base.v @@ -18,9 +18,9 @@ Require Export BinInt. Require Export Zcompare. Require Export Zorder. Require Export Zeven. +Require Export Zminmax. Require Export Zmin. Require Export Zmax. -Require Export Zminmax. Require Export Zabs. Require Export Znat. Require Export auxiliary. diff --git a/theories/ZArith/ZOrderedType.v b/theories/ZArith/ZOrderedType.v new file mode 100644 index 000000000..6e30e0bf8 --- /dev/null +++ b/theories/ZArith/ZOrderedType.v @@ -0,0 +1,73 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import BinInt Zcompare Zorder ZArith_dec + DecidableType2 OrderedType2 OrderedType2Facts. + +Local Open Scope Z_scope. + +(** * DecidableType structure for binary integers *) + +Module Z_as_MiniDT <: MiniDecidableType. + Definition t := Z. + Definition eq_dec := Z_eq_dec. +End Z_as_MiniDT. + +Module Z_as_DT <: UsualDecidableType := Make_UDT Z_as_MiniDT. + +(** Note that [Z_as_DT] can also be seen as a [DecidableType] + and a [DecidableTypeOrig]. *) + + + +(** * OrderedType structure for binary integers *) + +Module Z_as_OT <: OrderedTypeFull. + Include Z_as_DT. + Definition lt := Zlt. + Definition le := Zle. + Definition compare := Zcompare. + + Instance lt_strorder : StrictOrder Zlt. + Proof. split; [ exact Zlt_irrefl | exact Zlt_trans ]. Qed. + + Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) Zlt. + Proof. repeat red; intros; subst; auto. Qed. + + Lemma le_lteq : forall x y, x <= y <-> x < y \/ x=y. + Proof. + unfold le, lt, Zle, Zlt. intros. + rewrite <- Zcompare_Eq_iff_eq. + destruct (x ?= y); intuition; discriminate. + Qed. + + Lemma compare_spec : forall x y, Cmp eq lt x y (Zcompare x y). + Proof. + intros; unfold compare. + destruct (Zcompare x y) as [ ]_eqn; constructor; auto. + apply Zcompare_Eq_eq; auto. + apply Zgt_lt; auto. + Qed. + +End Z_as_OT. + +(* Note that [Z_as_OT] can also be seen as a [UsualOrderedType] + and a [OrderedType] (and also as a [DecidableType]). *) + + + +(** * An [order] tactic for integers *) + +Module ZOrder := OTF_to_OrderTac Z_as_OT. +Ltac z_order := + change (@eq Z) with ZOrder.OrderElts.eq in *; + ZOrder.order. + +(** Note that [z_order] is domain-agnostic: it will not prove + [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *) + diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v index dd46e885d..e6582a775 100644 --- a/theories/ZArith/Zmax.v +++ b/theories/ZArith/Zmax.v @@ -7,190 +7,100 @@ (************************************************************************) (*i $Id$ i*) -Require Import Arith_base. -Require Import BinInt. -Require Import Zcompare. -Require Import Zorder. +(** THIS FILE IS DEPRECATED. Use [Zminmax] instead. *) + +Require Export BinInt Zorder Zminmax. Open Local Scope Z_scope. -(******************************************) -(** Maximum of two binary integer numbers *) +(** [Zmax] is now [Zminmax.Zmax]. Code that do things like + [unfold Zmin.Zmin] will have to be adapted, and neither + a [Definition] or a [Notation] here can help much. *) -Definition Zmax m n := - match m ?= n with - | Eq | Gt => m - | Lt => n - end. (** * Characterization of maximum on binary integer numbers *) -Lemma Zmax_case : forall (n m:Z) (P:Z -> Type), P n -> P m -> P (Zmax n m). -Proof. - intros n m P H1 H2; unfold Zmax in |- *; case (n ?= m); auto with arith. -Qed. +Definition Zmax_case := Zmax_case. +Definition Zmax_case_strong := Zmax_case_strong. -Lemma Zmax_case_strong : forall (n m:Z) (P:Z -> Type), - (m<=n -> P n) -> (n<=m -> P m) -> P (Zmax n m). +Lemma Zmax_spec : forall x y, + x >= y /\ Zmax x y = x \/ x < y /\ Zmax x y = y. Proof. - intros n m P H1 H2; unfold Zmax, Zle, Zge in *. - rewrite <- (Zcompare_antisym n m) in H1. - destruct (n ?= m); (apply H1|| apply H2); discriminate. + intros x y. rewrite Zge_iff_le. destruct (Zmax_spec x y); auto. Qed. -Lemma Zmax_spec : forall x y:Z, - x >= y /\ Zmax x y = x \/ - x < y /\ Zmax x y = y. -Proof. - intros; unfold Zmax, Zlt, Zge. - destruct (Zcompare x y); [ left | right | left ]; split; auto; discriminate. -Qed. +Lemma Zmax_left : forall n m, n>=m -> Zmax n m = n. +Proof. intros x y. rewrite Zge_iff_le. apply Zmax_l. Qed. -Lemma Zmax_left : forall n m:Z, n>=m -> Zmax n m = n. -Proof. - intros n m; unfold Zmax, Zge; destruct (n ?= m); auto. - intro H; elim H; auto. -Qed. - -Lemma Zmax_right : forall n m:Z, n<=m -> Zmax n m = m. -Proof. - intros n m; unfold Zmax, Zle. - generalize (Zcompare_Eq_eq n m). - destruct (n ?= m); auto. - intros _ H; elim H; auto. -Qed. +Definition Zmax_right : forall n m, n<=m -> Zmax n m = m := Zmax_r. (** * Least upper bound properties of max *) -Lemma Zle_max_l : forall n m:Z, n <= Zmax n m. -Proof. - intros; apply Zmax_case_strong; auto with zarith. -Qed. +Definition Zle_max_l : forall n m, n <= Zmax n m := Zle_max_l. +Definition Zle_max_r : forall n m, m <= Zmax n m := Zle_max_r. -(* begin hide *) -Notation Zmax1 := Zle_max_l (only parsing). -(* end hide *) +Definition Zmax_lub : forall n m p, n <= p -> m <= p -> Zmax n m <= p + := Zmax_lub. -Lemma Zle_max_r : forall n m:Z, m <= Zmax n m. -Proof. - intros; apply Zmax_case_strong; auto with zarith. -Qed. - -(* begin hide *) -Notation Zmax2 := Zle_max_r (only parsing). -(* end hide *) - -Lemma Zmax_lub : forall n m p:Z, n <= p -> m <= p -> Zmax n m <= p. -Proof. - intros; apply Zmax_case; assumption. -Qed. +Definition Zmax_lub_lt : forall n m p:Z, n < p -> m < p -> Zmax n m < p + := Zmax_lub_lt. -Lemma Zmax_lub_lt : forall n m p:Z, n < p -> m < p -> Zmax n m < p. -Proof. - intros; apply Zmax_case; assumption. -Qed. (** * Compatibility with order *) -Lemma Zle_max_compat_r : forall n m p, n <= m -> Zmax n p <= Zmax m p. -Proof. - intros; do 2 (apply Zmax_case_strong; intro); eauto using Zle_trans, Zle_refl. -Qed. - -Lemma Zle_max_compat_l : forall n m p, n <= m -> Zmax p n <= Zmax p m. -Proof. - intros; do 2 (apply Zmax_case_strong; intro); eauto using Zle_trans, Zle_refl. -Qed. +Definition Zle_max_compat_r : forall n m p, n <= m -> Zmax n p <= Zmax m p + := Zmax_le_compat_r. -(** * Semi-lattice properties of max *) +Definition Zle_max_compat_l : forall n m p, n <= m -> Zmax p n <= Zmax p m + := Zmax_le_compat_l. -Lemma Zmax_idempotent : forall n:Z, Zmax n n = n. -Proof. - intros; apply Zmax_case; auto. -Qed. -Lemma Zmax_comm : forall n m:Z, Zmax n m = Zmax m n. -Proof. - intros; do 2 apply Zmax_case_strong; intros; - apply Zle_antisym; auto with zarith. -Qed. +(** * Semi-lattice properties of max *) -Lemma Zmax_assoc : forall n m p:Z, Zmax n (Zmax m p) = Zmax (Zmax n m) p. -Proof. - intros n m p; repeat apply Zmax_case_strong; intros; - reflexivity || (try apply Zle_antisym); eauto with zarith. -Qed. +Definition Zmax_idempotent : forall n, Zmax n n = n := Zmax_id. +Definition Zmax_comm : forall n m, Zmax n m = Zmax m n := Zmax_comm. +Definition Zmax_assoc : forall n m p, Zmax n (Zmax m p) = Zmax (Zmax n m) p + := Zmax_assoc. (** * Additional properties of max *) -Lemma Zmax_irreducible_dec : forall n m:Z, {Zmax n m = n} + {Zmax n m = m}. -Proof. - intros; apply Zmax_case; auto. -Qed. +Lemma Zmax_irreducible_dec : forall n m, {Zmax n m = n} + {Zmax n m = m}. +Proof. exact Zmax_dec. Qed. + +Definition Zmax_le_prime : forall n m p, p <= Zmax n m -> p <= n \/ p <= m + := Zmax_le. -Lemma Zmax_le_prime : forall n m p:Z, p <= Zmax n m -> p <= n \/ p <= m. -Proof. - intros n m p; apply Zmax_case; auto. -Qed. (** * Operations preserving max *) -Lemma Zsucc_max_distr : - forall n m:Z, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m). -Proof. - intros n m; unfold Zmax in |- *; rewrite (Zcompare_succ_compat n m); - elim_compare n m; intros E; rewrite E; auto with arith. -Qed. +Definition Zsucc_max_distr : + forall n m:Z, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m) + := Zsucc_max_distr. -Lemma Zplus_max_distr_l : forall n m p:Z, Zmax (p + n) (p + m) = p + Zmax n m. -Proof. - intros n m p; unfold Zmax. - rewrite (Zcompare_plus_compat n m p). - destruct (n ?= m); trivial. -Qed. +Definition Zplus_max_distr_l : forall n m p:Z, Zmax (p + n) (p + m) = p + Zmax n m + := Zplus_max_distr_l. -Lemma Zplus_max_distr_r : forall n m p:Z, Zmax (n + p) (m + p) = Zmax n m + p. -Proof. - intros n m p; repeat rewrite (Zplus_comm _ p); apply Zplus_max_distr_l. -Qed. +Definition Zplus_max_distr_r : forall n m p:Z, Zmax (n + p) (m + p) = Zmax n m + p + := Zplus_max_distr_r. (** * Maximum and Zpos *) -Lemma Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q). -Proof. - intros; unfold Zmax, Pmax; simpl; generalize (Pcompare_Eq_eq p q). - destruct Pcompare; auto. - intro H; rewrite H; auto. -Qed. +Definition Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q) + := Zpos_max. -Lemma Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p. -Proof. - intros; unfold Zmax; simpl; destruct p; simpl; auto. -Qed. +Definition Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p + := Zpos_max_1. (** * Characterization of Pminus in term of Zminus and Zmax *) -Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q). -Proof. - intros. - case_eq (Pcompare p q Eq). - intros H; rewrite (Pcompare_Eq_eq _ _ H). - rewrite Zminus_diag. - unfold Zmax; simpl. - unfold Pminus; rewrite Pminus_mask_diag; auto. - intros; rewrite Pminus_Lt; auto. - destruct (Zmax_spec 1 (Zpos p - Zpos q)) as [(H1,H2)|(H1,H2)]; auto. - exfalso; clear H2. - assert (H1':=Zlt_trans 0 1 _ Zlt_0_1 H1). - generalize (Zlt_0_minus_lt _ _ H1'). - unfold Zlt; simpl. - rewrite (ZC2 _ _ H); intro; discriminate. - intros; simpl; rewrite H. - symmetry; apply Zpos_max_1. -Qed. +Definition Zpos_minus : + forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q) + := Zpos_minus. (* begin hide *) (* Compatibility *) +Notation Zmax1 := Zle_max_l (only parsing). +Notation Zmax2 := Zle_max_r (only parsing). Notation Zmax_irreducible_inf := Zmax_irreducible_dec (only parsing). Notation Zmax_le_prime_inf := Zmax_le_prime (only parsing). (* end hide *) diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index de83af137..0278b604b 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -1,4 +1,3 @@ -(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -8,157 +7,84 @@ (************************************************************************) (*i $Id$ i*) -(** Initial version from Pierre Crégut (CNET, Lannion, France), 1996. - Further extensions by the Coq development team, with suggestions - from Russell O'Connor (Radbout U., Nijmegen, The Netherlands). - *) +(** THIS FILE IS DEPRECATED. Use [Zminmax] instead. *) -Require Import Arith_base. -Require Import BinInt. -Require Import Zcompare. -Require Import Zorder. +Require Import BinInt Zorder Zminmax. Open Local Scope Z_scope. -(**************************************) -(** Minimum on binary integer numbers *) +(** [Zmin] is now [Zminmax.Zmin]. Code that do things like + [unfold Zmin.Zmin] will have to be adapted, and neither + a [Definition] or a [Notation] here can help much. *) -Unboxed Definition Zmin (n m:Z) := - match n ?= m with - | Eq | Lt => n - | Gt => m - end. (** * Characterization of the minimum on binary integer numbers *) -Lemma Zmin_case_strong : forall (n m:Z) (P:Z -> Type), - (n<=m -> P n) -> (m<=n -> P m) -> P (Zmin n m). -Proof. - intros n m P H1 H2; unfold Zmin, Zle, Zge in *. - rewrite <- (Zcompare_antisym n m) in H2. - destruct (n ?= m); (apply H1|| apply H2); discriminate. -Qed. - -Lemma Zmin_case : forall (n m:Z) (P:Z -> Type), P n -> P m -> P (Zmin n m). -Proof. - intros n m P H1 H2; unfold Zmin in |- *; case (n ?= m); auto with arith. -Qed. +Definition Zmin_case := Zmin_case. +Definition Zmin_case_strong := Zmin_case_strong. -Lemma Zmin_spec : forall x y:Z, - x <= y /\ Zmin x y = x \/ - x > y /\ Zmin x y = y. +Lemma Zmin_spec : forall x y, + x <= y /\ Zmin x y = x \/ x > y /\ Zmin x y = y. Proof. - intros; unfold Zmin, Zle, Zgt. - destruct (Zcompare x y); [ left | left | right ]; split; auto; discriminate. + intros x y. rewrite Zgt_iff_lt, Zmin_comm. destruct (Zmin_spec y x); auto. Qed. (** * Greatest lower bound properties of min *) -Lemma Zle_min_l : forall n m:Z, Zmin n m <= n. -Proof. - intros n m; unfold Zmin in |- *; elim_compare n m; intros E; rewrite E; - [ apply Zle_refl - | apply Zle_refl - | apply Zlt_le_weak; apply Zgt_lt; exact E ]. -Qed. - -Lemma Zle_min_r : forall n m:Z, Zmin n m <= m. -Proof. - intros n m; unfold Zmin in |- *; elim_compare n m; intros E; rewrite E; - [ unfold Zle in |- *; rewrite E; discriminate - | unfold Zle in |- *; rewrite E; discriminate - | apply Zle_refl ]. -Qed. - -Lemma Zmin_glb : forall n m p:Z, p <= n -> p <= m -> p <= Zmin n m. -Proof. - intros; apply Zmin_case; assumption. -Qed. +Definition Zle_min_l : forall n m, Zmin n m <= n := Zle_min_l. +Definition Zle_min_r : forall n m, Zmin n m <= m := Zle_min_r. -Lemma Zmin_glb_lt : forall n m p:Z, p < n -> p < m -> p < Zmin n m. -Proof. - intros; apply Zmin_case; assumption. -Qed. +Definition Zmin_glb : forall n m p, p <= n -> p <= m -> p <= Zmin n m + := Zmin_glb. +Definition Zmin_glb_lt : forall n m p, p < n -> p < m -> p < Zmin n m + := Zmin_glb_lt. (** * Compatibility with order *) -Lemma Zle_min_compat_r : forall n m p, n <= m -> Zmin n p <= Zmin m p. -Proof. - intros; do 2 (apply Zmin_case_strong; intro); eauto using Zle_trans, Zle_refl. -Qed. - -Lemma Zle_min_compat_l : forall n m p, n <= m -> Zmin p n <= Zmin p m. -Proof. - intros; do 2 (apply Zmin_case_strong; intro); eauto using Zle_trans, Zle_refl. -Qed. +Definition Zle_min_compat_r : forall n m p, n <= m -> Zmin n p <= Zmin m p + := Zmin_le_compat_r. +Definition Zle_min_compat_l : forall n m p, n <= m -> Zmin p n <= Zmin p m + := Zmin_le_compat_l. (** * Semi-lattice properties of min *) -Lemma Zmin_idempotent : forall n:Z, Zmin n n = n. -Proof. - unfold Zmin in |- *; intros; elim (n ?= n); auto. -Qed. - +Definition Zmin_idempotent : forall n, Zmin n n = n := Zmin_id. Notation Zmin_n_n := Zmin_idempotent (only parsing). - -Lemma Zmin_comm : forall n m:Z, Zmin n m = Zmin m n. -Proof. - intros n m; unfold Zmin. - rewrite <- (Zcompare_antisym n m). - assert (H:=Zcompare_Eq_eq n m). - destruct (n ?= m); simpl; auto. -Qed. - -Lemma Zmin_assoc : forall n m p:Z, Zmin n (Zmin m p) = Zmin (Zmin n m) p. -Proof. - intros n m p; repeat apply Zmin_case_strong; intros; - reflexivity || (try apply Zle_antisym); eauto with zarith. -Qed. +Definition Zmin_comm : forall n m, Zmin n m = Zmin m n := Zmin_comm. +Definition Zmin_assoc : forall n m p, Zmin n (Zmin m p) = Zmin (Zmin n m) p + := Zmin_assoc. (** * Additional properties of min *) -Lemma Zmin_irreducible_inf : forall n m:Z, {Zmin n m = n} + {Zmin n m = m}. -Proof. - unfold Zmin in |- *; intros; elim (n ?= m); auto. -Qed. +Lemma Zmin_irreducible_inf : forall n m, {Zmin n m = n} + {Zmin n m = m}. +Proof. exact Zmin_dec. Qed. -Lemma Zmin_irreducible : forall n m:Z, Zmin n m = n \/ Zmin n m = m. -Proof. - intros n m; destruct (Zmin_irreducible_inf n m); [left|right]; trivial. -Qed. +Lemma Zmin_irreducible : forall n m, Zmin n m = n \/ Zmin n m = m. +Proof. intros; destruct (Zmin_dec n m); auto. Qed. Notation Zmin_or := Zmin_irreducible (only parsing). -Lemma Zmin_le_prime_inf : forall n m p:Z, Zmin n m <= p -> {n <= p} + {m <= p}. -Proof. - intros n m p; apply Zmin_case; auto. -Qed. +Lemma Zmin_le_prime_inf : forall n m p, Zmin n m <= p -> {n <= p} + {m <= p}. +Proof. intros n m p; apply Zmin_case; auto. Qed. (** * Operations preserving min *) -Lemma Zsucc_min_distr : - forall n m:Z, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m). -Proof. - intros n m; unfold Zmin in |- *; rewrite (Zcompare_succ_compat n m); - elim_compare n m; intros E; rewrite E; auto with arith. -Qed. +Definition Zsucc_min_distr : + forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m) + := Zsucc_min_distr. Notation Zmin_SS := Zsucc_min_distr (only parsing). -Lemma Zplus_min_distr_r : forall n m p:Z, Zmin (n + p) (m + p) = Zmin n m + p. -Proof. - intros x y n; unfold Zmin in |- *. - rewrite (Zplus_comm x n); rewrite (Zplus_comm y n); - rewrite (Zcompare_plus_compat x y n). - case (x ?= y); apply Zplus_comm. -Qed. +Definition Zplus_min_distr_r : + forall n m p, Zmin (n + p) (m + p) = Zmin n m + p + := Zplus_min_distr_r. Notation Zmin_plus := Zplus_min_distr_r (only parsing). (** * Minimum and Zpos *) -Lemma Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q). -Proof. - intros; unfold Zmin, Pmin; simpl; destruct Pcompare; auto. -Qed. +Definition Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q) + := Zpos_min. + + diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v index 83dceb84b..5fa90487b 100644 --- a/theories/ZArith/Zminmax.v +++ b/theories/ZArith/Zminmax.v @@ -5,72 +5,294 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) -Require Import Zmin Zmax. -Require Import BinInt Zorder. +Require Import OrderedType2 BinInt Zcompare Zorder ZOrderedType + GenericMinMax. -Open Local Scope Z_scope. +(** * Maximum and Minimum of two [Z] numbers *) -(** Lattice properties of min and max on Z *) +Local Open Scope Z_scope. -(** Absorption *) +Unboxed Definition Zmax (n m:Z) := + match n ?= m with + | Eq | Gt => n + | Lt => m + end. -Lemma Zmin_max_absorption_r_r : forall n m, Zmax n (Zmin n m) = n. +Unboxed Definition Zmin (n m:Z) := + match n ?= m with + | Eq | Lt => n + | Gt => m + end. + +(** The functions [Zmax] and [Zmin] implement indeed + a maximum and a minimum *) + +Lemma Zmax_spec : forall x y, + (x<y /\ Zmax x y = y) \/ (y<=x /\ Zmax x y = x). Proof. - intros; apply Zmin_case_strong; intro; apply Zmax_case_strong; intro; - reflexivity || apply Zle_antisym; trivial. + unfold Zlt, Zle, Zmax. intros. + generalize (Zcompare_Eq_eq x y). + rewrite <- (Zcompare_antisym x y). + destruct (x ?= y); simpl; auto; right; intuition; discriminate. Qed. -Lemma Zmax_min_absorption_r_r : forall n m, Zmin n (Zmax n m) = n. +Lemma Zmin_spec : forall x y, + (x<y /\ Zmin x y = x) \/ (y<=x /\ Zmin x y = y). Proof. - intros; apply Zmax_case_strong; intro; apply Zmin_case_strong; intro; - reflexivity || apply Zle_antisym; trivial. + unfold Zlt, Zle, Zmin. intros. + generalize (Zcompare_Eq_eq x y). + rewrite <- (Zcompare_antisym x y). + destruct (x ?= y); simpl; auto; right; intuition; discriminate. Qed. -(** Distributivity *) +Module ZHasMinMax <: HasMinMax Z_as_OT. + Definition max := Zmax. + Definition min := Zmin. + Definition max_spec := Zmax_spec. + Definition min_spec := Zmin_spec. +End ZHasMinMax. + +(** We obtain hence all the generic properties of max and min. *) + +Module Import ZMinMaxProps := MinMaxProperties Z_as_OT ZHasMinMax. + +(** For some generic properties, we can have nicer statements here, + since underlying equality is Leibniz. *) + +Lemma Zmax_case_strong : forall n m (P:Z -> Type), + (m<=n -> P n) -> (n<=m -> P m) -> P (Zmax n m). +Proof. intros; apply max_case_strong; auto. congruence. Defined. + +Lemma Zmax_case : forall n m (P:Z -> Type), + P n -> P m -> P (Zmax n m). +Proof. intros. apply Zmax_case_strong; auto. Defined. + +Lemma Zmax_monotone: forall f, + (Proper (Zle ==> Zle) f) -> + forall x y, Zmax (f x) (f y) = f (Zmax x y). +Proof. intros; apply max_monotone; auto. congruence. Qed. + +Lemma Zmin_case_strong : forall n m (P:Z -> Type), + (m<=n -> P m) -> (n<=m -> P n) -> P (Zmin n m). +Proof. intros; apply min_case_strong; auto. congruence. Defined. -Lemma Zmax_min_distr_r : - forall n m p, Zmax n (Zmin m p) = Zmin (Zmax n m) (Zmax n p). +Lemma Zmin_case : forall n m (P:Z -> Type), + P n -> P m -> P (Zmin n m). +Proof. intros. apply Zmin_case_strong; auto. Defined. + +Lemma Zmin_monotone: forall f, + (Proper (Zle ==> Zle) f) -> + forall x y, Zmin (f x) (f y) = f (Zmin x y). +Proof. intros; apply min_monotone; auto. congruence. Qed. + +Lemma Zmax_min_antimonotone : forall f, + Proper (Zle==>Zge) f -> + forall x y, Zmax (f x) (f y) == f (Zmin x y). Proof. - intros. - repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; - reflexivity || - apply Zle_antisym; (assumption || eapply Zle_trans; eassumption). + intros. apply max_min_antimonotone. congruence. + intros z z' Hz; red. apply Zge_le. auto. Qed. -Lemma Zmin_max_distr_r : - forall n m p, Zmin n (Zmax m p) = Zmax (Zmin n m) (Zmin n p). +Lemma Zmin_max_antimonotone : forall f, + Proper (Zle==>Zge) f -> + forall x y, Zmin (f x) (f y) == f (Zmax x y). Proof. - intros. - repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; - reflexivity || - apply Zle_antisym; (assumption || eapply Zle_trans; eassumption). + intros. apply min_max_antimonotone. congruence. + intros z z' Hz; red. apply Zge_le. auto. Qed. -(** Modularity *) +(** For the other generic properties, we make aliases, + since otherwise SearchAbout misses some of them + (bad interaction with an Include). + See GenericMinMax (or SearchAbout) for the statements. *) + +Definition Zmax_spec_le := max_spec_le. +Definition Zmax_dec := max_dec. +Definition Zmax_unicity := max_unicity. +Definition Zmax_unicity_ext := max_unicity_ext. +Definition Zmax_id := max_id. +Notation Zmax_idempotent := Zmax_id (only parsing). +Definition Zmax_assoc := max_assoc. +Definition Zmax_comm := max_comm. +Definition Zmax_l := max_l. +Definition Zmax_r := max_r. +Definition Zle_max_l := le_max_l. +Definition Zle_max_r := le_max_r. +Definition Zmax_le := max_le. +Definition Zmax_le_iff := max_le_iff. +Definition Zmax_lt_iff := max_lt_iff. +Definition Zmax_lub_l := max_lub_l. +Definition Zmax_lub_r := max_lub_r. +Definition Zmax_lub := max_lub. +Definition Zmax_lub_iff := max_lub_iff. +Definition Zmax_lub_lt := max_lub_lt. +Definition Zmax_lub_lt_iff := max_lub_lt_iff. +Definition Zmax_le_compat_l := max_le_compat_l. +Definition Zmax_le_compat_r := max_le_compat_r. +Definition Zmax_le_compat := max_le_compat. + +Definition Zmin_spec_le := min_spec_le. +Definition Zmin_dec := min_dec. +Definition Zmin_unicity := min_unicity. +Definition Zmin_unicity_ext := min_unicity_ext. +Definition Zmin_id := min_id. +Notation Zmin_idempotent := Zmin_id (only parsing). +Definition Zmin_assoc := min_assoc. +Definition Zmin_comm := min_comm. +Definition Zmin_l := min_l. +Definition Zmin_r := min_r. +Definition Zle_min_l := le_min_l. +Definition Zle_min_r := le_min_r. +Definition Zmin_le := min_le. +Definition Zmin_le_iff := min_le_iff. +Definition Zmin_lt_iff := min_lt_iff. +Definition Zmin_glb_l := min_glb_l. +Definition Zmin_glb_r := min_glb_r. +Definition Zmin_glb := min_glb. +Definition Zmin_glb_iff := min_glb_iff. +Definition Zmin_glb_lt := min_glb_lt. +Definition Zmin_glb_lt_iff := min_glb_lt_iff. +Definition Zmin_le_compat_l := min_le_compat_l. +Definition Zmin_le_compat_r := min_le_compat_r. +Definition Zmin_le_compat := min_le_compat. + +Definition Zmin_max_absorption := min_max_absorption. +Definition Zmax_min_absorption := max_min_absorption. +Definition Zmax_min_distr := max_min_distr. +Definition Zmin_max_distr := min_max_distr. +Definition Zmax_min_modular := max_min_modular. +Definition Zmin_max_modular := min_max_modular. +Definition Zmax_min_disassoc := max_min_disassoc. + + +(** * Properties specific to the [Z] domain *) + +(** Compatibilities (consequences of monotonicity) *) + +Lemma Zplus_max_distr_l : forall n m p, Zmax (p + n) (p + m) = p + Zmax n m. +Proof. + intros. apply Zmax_monotone. + intros x y. apply Zplus_le_compat_l. +Qed. + +Lemma Zplus_max_distr_r : forall n m p, Zmax (n + p) (m + p) = Zmax n m + p. +Proof. + intros. rewrite (Zplus_comm n p), (Zplus_comm m p), (Zplus_comm _ p). + apply Zplus_max_distr_l. +Qed. + +Lemma Zplus_min_distr_l : forall n m p, Zmin (p + n) (p + m) = p + Zmin n m. +Proof. + intros. apply Zmin_monotone. + intros x y. apply Zplus_le_compat_l. +Qed. + +Lemma Zplus_min_distr_r : forall n m p, Zmin (n + p) (m + p) = Zmin n m + p. +Proof. + intros. rewrite (Zplus_comm n p), (Zplus_comm m p), (Zplus_comm _ p). + apply Zplus_min_distr_l. +Qed. + +Lemma Zsucc_max_distr : forall n m, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m). +Proof. + unfold Zsucc. intros. symmetry. apply Zplus_max_distr_r. +Qed. + +Lemma Zsucc_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m). +Proof. + unfold Zsucc. intros. symmetry. apply Zplus_min_distr_r. +Qed. -Lemma Zmax_min_modular_r : - forall n m p, Zmax n (Zmin m (Zmax n p)) = Zmin (Zmax n m) (Zmax n p). +Lemma Zpred_max_distr : forall n m, Zpred (Zmax n m) = Zmax (Zpred n) (Zpred m). Proof. - intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; - reflexivity || - apply Zle_antisym; (assumption || eapply Zle_trans; eassumption). + unfold Zpred. intros. symmetry. apply Zplus_max_distr_r. Qed. -Lemma Zmin_max_modular_r : - forall n m p, Zmin n (Zmax m (Zmin n p)) = Zmax (Zmin n m) (Zmin n p). +Lemma Zpred_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m). Proof. - intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; - reflexivity || - apply Zle_antisym; (assumption || eapply Zle_trans; eassumption). + unfold Zpred. intros. symmetry. apply Zplus_min_distr_r. Qed. -(** Disassociativity *) +(** Anti-monotonicity swaps the role of [min] and [max] *) -Lemma max_min_disassoc : forall n m p, Zmin n (Zmax m p) <= Zmax (Zmin n m) p. +Lemma Zopp_max_distr : forall n m : Z, -(Zmax n m) = Zmin (- n) (- m). Proof. - intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; - apply Zle_refl || (assumption || eapply Zle_trans; eassumption). + intros. symmetry. apply Zmin_max_antimonotone. + intros x x'. rewrite Zge_iff_le; red; rewrite <- Zcompare_opp; auto. Qed. +Lemma Zopp_min_distr : forall n m : Z, - (Zmin n m) = Zmax (- n) (- m). +Proof. + intros. symmetry. apply Zmax_min_antimonotone. + intros x x'. rewrite Zge_iff_le; red; rewrite <- Zcompare_opp; auto. +Qed. + +Lemma Zminus_max_distr_l : forall n m p, Zmax (p - n) (p - m) = p - Zmin n m. +Proof. + unfold Zminus. intros. rewrite Zopp_min_distr. apply Zplus_max_distr_l. +Qed. + +Lemma Zminus_max_distr_r : forall n m p, Zmax (n - p) (m - p) = Zmax n m - p. +Proof. + unfold Zminus. intros. apply Zplus_max_distr_r. +Qed. + +Lemma Zminus_min_distr_l : forall n m p, Zmin (p - n) (p - m) = p - Zmax n m. +Proof. + unfold Zminus. intros. rewrite Zopp_max_distr. apply Zplus_min_distr_l. +Qed. + +Lemma Zminus_min_distr_r : forall n m p, Zmin (n - p) (m - p) = Zmin n m - p. +Proof. + unfold Zminus. intros. apply Zplus_min_distr_r. +Qed. + +(** Compatibility with [Zpos] *) + +Lemma Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q). +Proof. + intros; unfold Zmax, Pmax; simpl; generalize (Pcompare_Eq_eq p q). + destruct Pcompare; auto. + intro H; rewrite H; auto. +Qed. + +Lemma Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q). +Proof. + intros; unfold Zmin, Pmin; simpl; generalize (Pcompare_Eq_eq p q). + destruct Pcompare; auto. +Qed. + +Lemma Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p. +Proof. + intros; unfold Zmax; simpl; destruct p; simpl; auto. +Qed. + +Lemma Zpos_min_1 : forall p, Zmin 1 (Zpos p) = 1. +Proof. + intros; unfold Zmax; simpl; destruct p; simpl; auto. +Qed. + + +(** * Characterization of Pminus in term of Zminus and Zmax *) + +Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q). +Proof. + intros; simpl. destruct (Pcompare p q Eq) as [ ]_eqn:H. + rewrite (Pcompare_Eq_eq _ _ H). + unfold Pminus; rewrite Pminus_mask_diag; reflexivity. + rewrite Pminus_Lt; auto. + symmetry. apply Zpos_max_1. +Qed. + + +(*begin hide*) +(* Compatibility with names of the old Zminmax file *) +Notation Zmin_max_absorption_r_r := Zmin_max_absorption (only parsing). +Notation Zmax_min_absorption_r_r := Zmax_min_absorption (only parsing). +Notation Zmax_min_distr_r := Zmax_min_distr (only parsing). +Notation Zmin_max_distr_r := Zmin_max_distr (only parsing). +Notation Zmax_min_modular_r := Zmax_min_modular (only parsing). +Notation Zmin_max_modular_r := Zmin_max_modular (only parsing). +Notation max_min_disassoc := Zmax_min_disassoc (only parsing). +(*end hide*)
\ No newline at end of file diff --git a/theories/theories.itarget b/theories/theories.itarget index 44c6feee7..f33cb8208 100644 --- a/theories/theories.itarget +++ b/theories/theories.itarget @@ -19,6 +19,8 @@ Arith/Mult.vo Arith/Peano_dec.vo Arith/Plus.vo Arith/Wf_nat.vo +Arith/NatOrderedType.vo +Arith/MinMax.vo Bool/BoolEq.vo Bool/Bool.vo @@ -81,8 +83,11 @@ Structures/DecidableTypeEx.vo Structures/OrderedType2Alt.vo Structures/OrderedType2Ex.vo Structures/OrderedType2.vo +Structures/OrderedType2Facts.vo +Structures/OrderedType2Lists.vo Structures/DecidableType2.vo Structures/DecidableType2Ex.vo +Structures/DecidableType2Facts.vo Structures/OrderTac.vo Init/Datatypes.vo @@ -140,6 +145,10 @@ NArith/Ndigits.vo NArith/Ndist.vo NArith/Nnat.vo NArith/Pnat.vo +NArith/POrderedType.vo +NArith/Pminmax.vo +NArith/NOrderedType.vo +NArith/Nminmax.vo Numbers/BigNumPrelude.vo Numbers/Cyclic/Abstract/CyclicAxioms.vo @@ -363,3 +372,4 @@ ZArith/Zpower.vo ZArith/Zpow_facts.vo ZArith/Zsqrt.vo ZArith/Zwf.vo +ZArith/ZOrderedType.vo
\ No newline at end of file |