diff options
Diffstat (limited to 'theories/Structures')
| -rw-r--r-- | theories/Structures/DecidableType.v | 173 | ||||
| -rw-r--r-- | theories/Structures/DecidableType2.v | 164 | ||||
| -rw-r--r-- | theories/Structures/DecidableType2Ex.v | 85 | ||||
| -rw-r--r-- | theories/Structures/DecidableTypeEx.v | 109 | ||||
| -rw-r--r-- | theories/Structures/OrderedType.v | 587 | ||||
| -rw-r--r-- | theories/Structures/OrderedType2.v | 680 | ||||
| -rw-r--r-- | theories/Structures/OrderedType2Alt.v | 297 | ||||
| -rw-r--r-- | theories/Structures/OrderedType2Ex.v | 261 | ||||
| -rw-r--r-- | theories/Structures/OrderedTypeAlt.v | 122 | ||||
| -rw-r--r-- | theories/Structures/OrderedTypeEx.v | 243 |
10 files changed, 2721 insertions, 0 deletions
diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v new file mode 100644 index 0000000000..625f776bfa --- /dev/null +++ b/theories/Structures/DecidableType.v @@ -0,0 +1,173 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* $Id$ *) + +Require Export SetoidList. +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. + +End EqualityType. + +(** * 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. + +(** * 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 *) + + Lemma eqk_refl : forall e, eqk e e. + Proof. auto. Qed. + + Lemma eqke_refl : forall e, eqke e e. + Proof. auto. Qed. + + Lemma eqk_sym : forall e e', eqk e e' -> eqk e' e. + Proof. auto. Qed. + + Lemma eqke_sym : forall e e', eqke e e' -> eqke e' e. + Proof. unfold eqke; intuition. Qed. + + Lemma eqk_trans : forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''. + Proof. eauto. Qed. + + Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''. + Proof. + unfold eqke; intuition; [ eauto | congruence ]. + Qed. + + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. + Hint Immediate eqk_sym eqke_sym. + + 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; apply InA_eqA with p; auto; apply eqk_trans; 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. + + Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. + Proof. + intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto. + Qed. + + Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. + Proof. + destruct 2 as (e,E); exists e; eapply MapsTo_eq; eauto. + 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 Unfold eqk eqke. + Hint Extern 2 (eqke ?a ?b) => split. + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. + Hint Immediate eqk_sym eqke_sym. + Hint Resolve InA_eqke_eqk. + Hint Unfold MapsTo In. + Hint Resolve In_inv_2 In_inv_3. + +End KeyDecidableType. + + + + + diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v new file mode 100644 index 0000000000..0b3ebfa295 --- /dev/null +++ b/theories/Structures/DecidableType2.v @@ -0,0 +1,164 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* $Id$ *) + +Require Export SetoidList2. +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. + Instance eq_equiv : Equivalence eq. + + Hint Resolve (@Equivalence_Reflexive _ _ eq_equiv). + Hint Resolve (@Equivalence_Transitive _ _ eq_equiv). + Hint Immediate (@Equivalence_Symmetric _ _ eq_equiv). +End EqualityType. + +(** * Types with decidable Equalities (but no ordering) *) + +Module Type DecidableType. + Include Type EqualityType. + Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }. +End DecidableType. + +(** * 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'). + + Global Hint Unfold eqk eqke. + Global 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. + + Global Hint Resolve (@Equivalence_Reflexive _ _ eqk_equiv). + Global Hint Resolve (@Equivalence_Transitive _ _ eqk_equiv). + Global Hint Immediate (@Equivalence_Symmetric _ _ eqk_equiv). + Global Hint Resolve (@Equivalence_Reflexive _ _ eqke_equiv). + Global Hint Resolve (@Equivalence_Transitive _ _ eqke_equiv). + Global 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. + Global 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. + + Global 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. + + + + + diff --git a/theories/Structures/DecidableType2Ex.v b/theories/Structures/DecidableType2Ex.v new file mode 100644 index 0000000000..7b9c052ec4 --- /dev/null +++ b/theories/Structures/DecidableType2Ex.v @@ -0,0 +1,85 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* $Id$ *) + +Require Import DecidableType2. +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 eq x y := D1.eq (fst x) (fst y) /\ D2.eq (snd x) (snd y). + + 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. + Defined. + +End PairDecidableType. + +(** Similarly for pairs of UsualDecidableType *) + +Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType. + Definition t := prod D1.t D2.t. + Definition eq := @eq t. + Program Instance eq_equiv : Equivalence eq. + Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }. + Proof. + intros (x1,x2) (y1,y2); + destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2); + unfold eq, D1.eq, D2.eq in *; simpl; + (left; f_equal; auto; fail) || + (right; intro H; injection H; auto). + Defined. + +End PairUsualDecidableType. diff --git a/theories/Structures/DecidableTypeEx.v b/theories/Structures/DecidableTypeEx.v new file mode 100644 index 0000000000..022102f70d --- /dev/null +++ b/theories/Structures/DecidableTypeEx.v @@ -0,0 +1,109 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* $Id$ *) + +Require Import DecidableType OrderedType OrderedTypeEx. +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. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + 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. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + Definition eq_dec := M.eq_dec. +End Make_UDT. + +(** An OrderedType can now directly be seen as a DecidableType *) + +Module OT_as_DT (O:OrderedType) <: DecidableType := O. + +(** (Usual) Decidable Type for [nat], [positive], [N], [Z] *) + +Module Nat_as_DT <: UsualDecidableType := Nat_as_OT. +Module Positive_as_DT <: UsualDecidableType := Positive_as_OT. +Module N_as_DT <: UsualDecidableType := N_as_OT. +Module Z_as_DT <: UsualDecidableType := Z_as_OT. + +(** 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 eq x y := D1.eq (fst x) (fst y) /\ D2.eq (snd x) (snd y). + + Lemma eq_refl : forall x : t, eq x x. + Proof. + intros (x1,x2); red; simpl; auto. + Qed. + + Lemma eq_sym : forall x y : t, eq x y -> eq y x. + Proof. + intros (x1,x2) (y1,y2); unfold eq; simpl; intuition. + Qed. + + Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. + Proof. + 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. + Defined. + +End PairDecidableType. + +(** Similarly for pairs of UsualDecidableType *) + +Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType. + Definition t := prod D1.t D2.t. + Definition eq := @eq t. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }. + Proof. + intros (x1,x2) (y1,y2); + destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2); + unfold eq, D1.eq, D2.eq in *; simpl; + (left; f_equal; auto; fail) || + (right; intro H; injection H; auto). + Defined. + +End PairUsualDecidableType. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v new file mode 100644 index 0000000000..f17eb43a95 --- /dev/null +++ b/theories/Structures/OrderedType.v @@ -0,0 +1,587 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* $Id$ *) + +Require Export SetoidList. +Set Implicit Arguments. +Unset Strict Implicit. + +(** * Ordered types *) + +Inductive Compare (X : Type) (lt eq : X -> X -> Prop) (x y : X) : Type := + | LT : lt x y -> Compare lt eq x y + | EQ : eq x y -> Compare lt eq x y + | GT : lt y x -> Compare lt eq x y. + +Module Type MiniOrderedType. + + Parameter Inline t : Type. + + Parameter Inline eq : t -> t -> Prop. + Parameter Inline lt : 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. + + Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. + Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y. + + Parameter compare : forall x y : t, Compare lt eq x y. + + Hint Immediate eq_sym. + Hint Resolve eq_refl eq_trans lt_not_eq lt_trans. + +End MiniOrderedType. + +Module Type OrderedType. + Include Type MiniOrderedType. + + (** A [eq_dec] can be deduced from [compare] below. But adding this + redundant field allows to see an OrderedType as a DecidableType. *) + Parameter eq_dec : forall x y, { eq x y } + { ~ eq x y }. + +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; elim (compare x y); intro H; [ right | left | right ]; auto. + assert (~ eq y x); auto. + Defined. + +End MOT_to_OT. + +(** * Ordered types properties *) + +(** Additional properties that can be derived from signature + [OrderedType]. *) + +Module OrderedTypeFacts (Import O: OrderedType). + + Lemma lt_antirefl : forall x, ~ lt x x. + Proof. + intros; intro; absurd (eq x x); auto. + Qed. + + Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z. + Proof. + intros; destruct (compare x z); auto. + elim (lt_not_eq H); apply eq_trans with z; auto. + elim (lt_not_eq (lt_trans l H)); auto. + Qed. + + Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z. + Proof. + intros; destruct (compare x z); auto. + elim (lt_not_eq H0); apply eq_trans with x; auto. + elim (lt_not_eq (lt_trans H0 l)); auto. + Qed. + + Lemma le_eq : forall x y z, ~lt x y -> eq y z -> ~lt x z. + Proof. + intros; intro; destruct H; apply lt_eq with z; auto. + Qed. + + Lemma eq_le : forall x y z, eq x y -> ~lt y z -> ~lt x z. + Proof. + intros; intro; destruct H0; apply eq_lt with x; auto. + Qed. + + Lemma neq_eq : forall x y z, ~eq x y -> eq y z -> ~eq x z. + Proof. + intros; intro; destruct H; apply eq_trans with z; auto. + Qed. + + Lemma eq_neq : forall x y z, eq x y -> ~eq y z -> ~eq x z. + Proof. + intros; intro; destruct H0; apply eq_trans with x; auto. + Qed. + + Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq. + + Lemma le_lt_trans : forall x y z, ~lt y x -> lt y z -> lt x z. + Proof. + intros; destruct (compare y x); auto. + elim (H l). + apply eq_lt with y; auto. + apply lt_trans with y; auto. + Qed. + + Lemma lt_le_trans : forall x y z, lt x y -> ~lt z y -> lt x z. + Proof. + intros; destruct (compare z y); auto. + elim (H0 l). + apply lt_eq with y; auto. + apply lt_trans with y; auto. + Qed. + + Lemma le_neq : forall x y, ~lt x y -> ~eq x y -> lt y x. + Proof. + intros; destruct (compare x y); intuition. + Qed. + + Lemma neq_sym : forall x y, ~eq x y -> ~eq y x. + Proof. + intuition. + Qed. + +(* TODO concernant la tactique order: + * propagate_lt n'est sans doute pas complet + * un propagate_le + * exploiter les hypotheses negatives restant a la fin + * faire que ca marche meme quand une hypothese depend d'un eq ou lt. +*) + +Ltac abstraction := match goal with + (* First, some obvious simplifications *) + | H : False |- _ => elim H + | H : lt ?x ?x |- _ => elim (lt_antirefl H) + | H : ~eq ?x ?x |- _ => elim (H (eq_refl x)) + | H : eq ?x ?x |- _ => clear H; abstraction + | H : ~lt ?x ?x |- _ => clear H; abstraction + | |- eq ?x ?x => exact (eq_refl x) + | |- lt ?x ?x => exfalso; abstraction + | |- ~ _ => intro; abstraction + | H1: ~lt ?x ?y, H2: ~eq ?x ?y |- _ => + generalize (le_neq H1 H2); clear H1 H2; intro; abstraction + | H1: ~lt ?x ?y, H2: ~eq ?y ?x |- _ => + generalize (le_neq H1 (neq_sym H2)); clear H1 H2; intro; abstraction + (* Then, we generalize all interesting facts *) + | H : ~eq ?x ?y |- _ => revert H; abstraction + | H : ~lt ?x ?y |- _ => revert H; abstraction + | H : lt ?x ?y |- _ => revert H; abstraction + | H : eq ?x ?y |- _ => revert H; abstraction + | _ => idtac +end. + +Ltac do_eq a b EQ := match goal with + | |- lt ?x ?y -> _ => let H := fresh "H" in + (intro H; + (generalize (eq_lt (eq_sym EQ) H); clear H; intro H) || + (generalize (lt_eq H EQ); clear H; intro H) || + idtac); + do_eq a b EQ + | |- ~lt ?x ?y -> _ => let H := fresh "H" in + (intro H; + (generalize (eq_le (eq_sym EQ) H); clear H; intro H) || + (generalize (le_eq H EQ); clear H; intro H) || + idtac); + do_eq a b EQ + | |- eq ?x ?y -> _ => let H := fresh "H" in + (intro H; + (generalize (eq_trans (eq_sym EQ) H); clear H; intro H) || + (generalize (eq_trans H EQ); clear H; intro H) || + idtac); + do_eq a b EQ + | |- ~eq ?x ?y -> _ => let H := fresh "H" in + (intro H; + (generalize (eq_neq (eq_sym EQ) H); clear H; intro H) || + (generalize (neq_eq H EQ); clear H; intro H) || + idtac); + do_eq a b EQ + | |- lt a ?y => apply eq_lt with b; [exact EQ|] + | |- lt ?y a => apply lt_eq with b; [|exact (eq_sym EQ)] + | |- eq a ?y => apply eq_trans with b; [exact EQ|] + | |- eq ?y a => apply eq_trans with b; [|exact (eq_sym EQ)] + | _ => idtac + end. + +Ltac propagate_eq := abstraction; clear; match goal with + (* the abstraction tactic leaves equality facts in head position...*) + | |- eq ?a ?b -> _ => + let EQ := fresh "EQ" in (intro EQ; do_eq a b EQ; clear EQ); + propagate_eq + | _ => idtac +end. + +Ltac do_lt x y LT := match goal with + (* LT *) + | |- lt x y -> _ => intros _; do_lt x y LT + | |- lt y ?z -> _ => let H := fresh "H" in + (intro H; generalize (lt_trans LT H); intro); do_lt x y LT + | |- lt ?z x -> _ => let H := fresh "H" in + (intro H; generalize (lt_trans H LT); intro); do_lt x y LT + | |- lt _ _ -> _ => intro; do_lt x y LT + (* GE *) + | |- ~lt y x -> _ => intros _; do_lt x y LT + | |- ~lt x ?z -> _ => let H := fresh "H" in + (intro H; generalize (le_lt_trans H LT); intro); do_lt x y LT + | |- ~lt ?z y -> _ => let H := fresh "H" in + (intro H; generalize (lt_le_trans LT H); intro); do_lt x y LT + | |- ~lt _ _ -> _ => intro; do_lt x y LT + | _ => idtac + end. + +Definition hide_lt := lt. + +Ltac propagate_lt := abstraction; match goal with + (* when no [=] remains, the abstraction tactic leaves [<] facts first. *) + | |- lt ?x ?y -> _ => + let LT := fresh "LT" in (intro LT; do_lt x y LT; + change (hide_lt x y) in LT); + propagate_lt + | _ => unfold hide_lt in * +end. + +Ltac order := + intros; + propagate_eq; + propagate_lt; + auto; + propagate_lt; + eauto. + +Ltac false_order := exfalso; order. + + Lemma gt_not_eq : forall x y, lt y x -> ~ eq x y. + Proof. + order. + Qed. + + Lemma eq_not_lt : forall x y : t, eq x y -> ~ lt x y. + Proof. + order. + Qed. + + Hint Resolve gt_not_eq eq_not_lt. + + Lemma eq_not_gt : forall x y : t, eq x y -> ~ lt y x. + Proof. + order. + Qed. + + Lemma lt_not_gt : forall x y : t, lt x y -> ~ lt y x. + Proof. + order. + Qed. + + Hint Resolve eq_not_gt lt_antirefl lt_not_gt. + + Lemma elim_compare_eq : + forall x y : t, + eq x y -> exists H : eq x y, compare x y = EQ _ H. + Proof. + intros; case (compare x y); intros H'; try solve [false_order]. + exists H'; auto. + Qed. + + Lemma elim_compare_lt : + forall x y : t, + lt x y -> exists H : lt x y, compare x y = LT _ H. + Proof. + intros; case (compare x y); intros H'; try solve [false_order]. + exists H'; auto. + Qed. + + Lemma elim_compare_gt : + forall x y : t, + lt y x -> exists H : lt y x, compare x y = GT _ H. + Proof. + intros; case (compare x y); intros H'; try solve [false_order]. + exists H'; auto. + Qed. + + Ltac elim_comp := + match goal with + | |- ?e => match e with + | context ctx [ compare ?a ?b ] => + let H := fresh in + (destruct (compare a b) as [H|H|H]; + try solve [ intros; false_order]) + end + end. + + Ltac elim_comp_eq x y := + elim (elim_compare_eq (x:=x) (y:=y)); + [ intros _1 _2; rewrite _2; clear _1 _2 | auto ]. + + Ltac elim_comp_lt x y := + elim (elim_compare_lt (x:=x) (y:=y)); + [ intros _1 _2; rewrite _2; clear _1 _2 | auto ]. + + Ltac elim_comp_gt x y := + elim (elim_compare_gt (x:=x) (y:=y)); + [ intros _1 _2; rewrite _2; clear _1 _2 | auto ]. + + (** 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); [ left | right | right ]; auto. + Defined. + + Definition eqb x y : bool := if eq_dec x y then true else false. + + Lemma eqb_alt : + forall x y, eqb x y = match compare x y with EQ _ => true | _ => false end. + Proof. + unfold eqb; intros; destruct (eq_dec x y); elim_comp; 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. exact (InA_eqA eq_sym eq_trans). Qed. + +Lemma ListIn_In : forall l x, List.In x l -> In x l. +Proof. exact (In_InA eq_refl). Qed. + +Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l. +Proof. exact (InfA_ltA lt_trans). Qed. + +Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l. +Proof. exact (InfA_eqA eq_lt). 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_refl eq_sym lt_trans lt_eq eq_lt). 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_refl (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_refl eq_sym lt_trans lt_eq eq_lt). Qed. + +Lemma Sort_NoDup : forall l, Sort l -> NoDup l. +Proof. exact (SortA_NoDupA eq_refl eq_sym lt_trans lt_not_eq lt_eq eq_lt) . Qed. + +End ForNotations. + +Hint Resolve ListIn_In Sort_NoDup Inf_lt. +Hint Immediate In_eq Inf_lt. + +End OrderedTypeFacts. + +Module KeyOrderedType(O:OrderedType). + Import O. + Module MO:=OrderedTypeFacts(O). + Import MO. + + 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'). + Definition ltk (p p':key*elt) := lt (fst p) (fst p'). + + Hint Unfold eqk eqke ltk. + 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. + + (* ltk ignore the second components *) + + Lemma ltk_right_r : forall x k e e', ltk x (k,e) -> ltk x (k,e'). + Proof. auto. Qed. + + Lemma ltk_right_l : forall x k e e', ltk (k,e) x -> ltk (k,e') x. + Proof. auto. Qed. + Hint Immediate ltk_right_r ltk_right_l. + + (* eqk, eqke are equalities, ltk is a strict order *) + + Lemma eqk_refl : forall e, eqk e e. + Proof. auto. Qed. + + Lemma eqke_refl : forall e, eqke e e. + Proof. auto. Qed. + + Lemma eqk_sym : forall e e', eqk e e' -> eqk e' e. + Proof. auto. Qed. + + Lemma eqke_sym : forall e e', eqke e e' -> eqke e' e. + Proof. unfold eqke; intuition. Qed. + + Lemma eqk_trans : forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''. + Proof. eauto. Qed. + + Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''. + Proof. + unfold eqke; intuition; [ eauto | congruence ]. + Qed. + + Lemma ltk_trans : forall e e' e'', ltk e e' -> ltk e' e'' -> ltk e e''. + Proof. eauto. Qed. + + Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'. + Proof. unfold eqk, ltk; auto. Qed. + + Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'. + Proof. + unfold eqke, ltk; intuition; simpl in *; subst. + exact (lt_not_eq H H1). + Qed. + + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. + Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke. + Hint Immediate eqk_sym eqke_sym. + + (* Additionnal facts *) + + Lemma eqk_not_ltk : forall x x', eqk x x' -> ~ltk x x'. + Proof. + unfold eqk, ltk; simpl; auto. + Qed. + + Lemma ltk_eqk : forall e e' e'', ltk e e' -> eqk e' e'' -> ltk e e''. + Proof. eauto. Qed. + + Lemma eqk_ltk : forall e e' e'', eqk e e' -> ltk e' e'' -> ltk e e''. + Proof. + intros (k,e) (k',e') (k'',e''). + unfold ltk, eqk; simpl; eauto. + Qed. + Hint Resolve eqk_not_ltk. + Hint Immediate ltk_eqk eqk_ltk. + + 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. + + 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. + exists e; auto. + destruct IHInA as [e H0]. + exists e; auto. + Qed. + + Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. + Proof. + intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto. + Qed. + + Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. + Proof. + destruct 2 as (e,E); exists e; eapply MapsTo_eq; eauto. + Qed. + + Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l. + Proof. exact (InfA_eqA eqk_ltk). Qed. + + Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l. + Proof. exact (InfA_ltA ltk_trans). 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. + exact (SortA_InfA_InA eqk_refl eqk_sym ltk_trans ltk_eqk eqk_ltk). + 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. + exact (SortA_NoDupA eqk_refl eqk_sym ltk_trans ltk_not_eqk ltk_eqk eqk_ltk). + Qed. + + Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'. + Proof. + inversion 1; intros; 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. + inversion_clear 2; 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. + inversion_clear 1; red; intros. + destruct (Sort_Inf_NotIn H0 H1 (In_eq H2 H)). + 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 Unfold eqk eqke ltk. + Hint Extern 2 (eqke ?a ?b) => split. + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. + Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke. + Hint Immediate eqk_sym eqke_sym. + Hint Resolve eqk_not_ltk. + Hint Immediate ltk_eqk eqk_ltk. + 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/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v new file mode 100644 index 0000000000..e1b7f4e22c --- /dev/null +++ b/theories/Structures/OrderedType2.v @@ -0,0 +1,680 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* $Id$ *) + +Require Export SetoidList2 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. + +Module Type MiniOrderedType. + Include Type EqualityType. + + Parameter Inline lt : t -> t -> Prop. + Instance lt_strorder : StrictOrder lt. + 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 MiniOrderedType. + +Module Type OrderedType. + Include Type MiniOrderedType. + + (** A [eq_dec] can be deduced from [compare] below. But adding this + redundant field allows to see an OrderedType as a DecidableType. *) + Parameter eq_dec : forall x y, { eq x y } + { ~ eq x y }. + +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. + 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. + + (** The following lemmas are re-phrasing of eq_equiv and lt_strorder. + Interest: compatibility, simple use (e.g. in tactic 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_antirefl (x:t) : ~x<x := StrictOrder_Irreflexive x. + + Lemma lt_not_eq : forall x y, x<y -> ~x==y. + Proof. + intros x y H H'. rewrite H' in H. + apply lt_antirefl with y; auto. + Qed. + + Lemma lt_eq : forall x y z, x<y -> y==z -> x<z. + Proof. + intros x y z H H'. rewrite <- H'; auto. + Qed. + + Lemma eq_lt : forall x y z, x==y -> y<z -> x<z. + Proof. + intros x y z H H'. rewrite H; auto. + Qed. + + Lemma le_eq : forall x y z, x<=y -> y==z -> x<=z. + Proof. + intros x y z H H' H''. rewrite H' in H; auto. + Qed. + + Lemma eq_le : forall x y z, x==y -> y<=z -> x<=z. + Proof. + intros x y z H H'. rewrite H; auto. + Qed. + + Lemma neq_eq : forall x y z, ~x==y -> y==z -> ~x==z. + Proof. + intros x y z H H'; rewrite <-H'; auto. + Qed. + + Lemma eq_neq : forall x y z, x==y -> ~y==z -> ~x==z. + Proof. + intros x y z H H'; rewrite H; auto. + Qed. + + Hint Resolve eq_trans eq_refl lt_trans. + Hint Immediate eq_sym eq_lt lt_eq le_eq eq_le neq_eq eq_neq. + + Ltac elim_compare x y := + generalize (compare_spec x y); destruct (compare x y); + unfold Cmp, flip. + + Lemma le_lt_trans : forall x y z, x<=y -> y<z -> x<z. + Proof. + intros. elim_compare x y; intro H'. + rewrite H'; auto. + transitivity y; auto. + intuition. + Qed. + + Lemma lt_le_trans : forall x y z, x<y -> y<=z -> x<z. + Proof. + intros. elim_compare y z; intro H'. + rewrite <- H'; auto. + transitivity y; auto. + intuition. + Qed. + + Lemma le_trans : forall x y z, x<=y -> y<=z -> x<=z. + Proof. + intros x y z Hxy Hyz Hzx. + apply Hxy. + eapply le_lt_trans; eauto. + Qed. + + Lemma le_antisym : forall x y, x<=y -> y<=x -> x==y. + Proof. + intros. elim_compare x y; intuition. + Qed. + + Lemma le_neq : forall x y, x<=y -> ~x==y -> x<y. + Proof. + intros. elim_compare x y; intuition. + Qed. + + Lemma neq_sym : forall x y, ~x==y -> ~y==x. + Proof. + intuition. + Qed. + +(** The order tactic *) + +(** This tactic is designed to solve systems of (in)equations + involving eq and lt and ~eq and ~lt (i.e. ge). All others + parts of the goal will be discarded. This tactic is + domain-agnostic : it will only use equivalence+order axioms. + Moreover it doesn't directly use totality of the order + (but uses above lemmas such as le_trans that rely on it). + A typical use of this tactic is transitivity problems. *) + +Definition hide_eq := eq. + +(** order_eq : replace x by y in all (in)equations thanks + to equality EQ (where eq has been hidden in order to avoid + self-rewriting). + + NB: order_saturate_eq could be written in a shorter way thanks + to rewrite, but proof terms would be uglier *) + +Ltac order_eq x y EQ := + let rewr H t := generalize t; clear H; intro H + in + match goal with + | H : x == _ |- _ => rewr H (eq_trans (eq_sym EQ) H); order_eq x y EQ + | H : _ == x |- _ => rewr H (eq_trans H EQ); order_eq x y EQ + | H : ~x == _ |- _ => rewr H (eq_neq (eq_sym EQ) H); order_eq x y EQ + | H : ~_ == x |- _ => rewr H (neq_eq H EQ); order_eq x y EQ + | H : x < ?z |- _ => rewr H (eq_lt (eq_sym EQ) H); order_eq x y EQ + | H : ?z < x |- _ => rewr H (lt_eq H EQ); order_eq x y EQ + | H : x <= ?z |- _ => rewr H (eq_le (eq_sym EQ) H); order_eq x y EQ + | H : ?z <= x |- _ => rewr H (le_eq H EQ); order_eq x y EQ + (* NB: no negation in the goal, see below *) + | |- x == ?z => apply eq_trans with y; [apply EQ| ]; order_eq x y EQ + | |- ?z == x => apply eq_trans with y; [ | apply (eq_sym EQ) ]; + order_eq x y EQ + | |- x < ?z => apply eq_lt with y; [apply EQ| ]; order_eq x y EQ + | |- ?z < x => apply lt_eq with y; [ | apply (eq_sym EQ) ]; + order_eq x y EQ + | _ => clear EQ +end. + +Ltac order := intros; trivial; + match goal with + | |- ~ _ => intro; order + | H : ?A -> False |- _ => change (~A) in H; order + (* First, successful situations *) + | H : ?x < ?x |- _ => elim (lt_antirefl H) + | H : ~ ?x == ?x |- _ => elim (H (Equivalence_Reflexive x)) + | |- ?x == ?x => apply (Equivalence_Reflexive x) + (* Second, useless hyps or goal *) + | H : ?x == ?x |- _ => clear H; order + | H : ?x <= ?x |- _ => clear H; order + | |- ?x < ?x => elimtype False; order + (* We eliminate equalities *) + | H : ?x == ?y |- _ => + change (hide_eq x y) in H; order_eq x y H; order + (* Simultaneous le and ge is eq *) + | H1 : ?x <= ?y, H2 : ?y <= ?x |- _ => + generalize (le_antisym H1 H2); clear H1 H2; intro; order + (* Simultaneous le and ~eq is lt *) + | H1: ?x <= ?y, H2: ~ ?x == ?y |- _ => + generalize (le_neq H1 H2); clear H1 H2; intro; order + | H1: ?x <= ?y, H2: ~ ?y == ?x |- _ => + generalize (le_neq H1 (neq_sym H2)); clear H1 H2; intro; order + (* Transitivity of lt and le *) + | H1 : ?x < ?y, H2 : ?y < ?z |- _ => + match goal with + | H : x < z |- _ => fail 1 + | _ => generalize (lt_trans H1 H2); intro; order + end + | H1 : ?x <= ?y, H2 : ?y < ?z |- _ => + match goal with + | H : x < z |- _ => fail 1 + | _ => generalize (le_lt_trans H1 H2); intro; order + end + | H1 : ?x < ?y, H2 : ?y <= ?z |- _ => + match goal with + | H : x < z |- _ => fail 1 + | _ => generalize (lt_le_trans H1 H2); intro; order + end + | H1 : ?x <= ?y, H2 : ?y <= ?z |- _ => + match goal with + | H : x <= z |- _ => fail 1 + | _ => generalize (le_trans H1 H2); intro; order + end + | _ => auto; fail +end. + +Ltac false_order := elimtype False; order. + + Lemma gt_not_eq : forall x y, lt y x -> ~ eq x y. + Proof. + order. + Qed. + + Lemma eq_not_lt : forall x y : t, eq x y -> ~ lt x y. + Proof. + order. + Qed. + + Hint Resolve gt_not_eq eq_not_lt. + + Lemma eq_not_gt : forall x y : t, eq x y -> ~ lt y x. + Proof. + order. + Qed. + + Lemma lt_not_gt : forall x y : t, lt x y -> ~ lt y x. + Proof. + order. + Qed. + + Hint Resolve eq_not_gt lt_antirefl lt_not_gt. + + 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 ]; auto. + 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. + +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'). + +Definition FstRel {A B}(R:relation A) : relation (A*B) := + fun p p' => R (fst p) (fst p'). + +Definition SndRel {A B}(R:relation B) : relation (A*B) := + fun p p' => R (snd p) (snd p'). + +Instance ProdRel_equiv {A B} `(Equivalence A RA)`(Equivalence B RB) : + Equivalence (ProdRel RA RB). +Proof. firstorder. Qed. + +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. + +Instance FstRel_strorder {A B} `(StrictOrder A RA) : + StrictOrder (FstRel RA (B:=B)). +Proof. firstorder. Qed. + +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. + +(* + (* ltk ignore the second components *) + + Lemma ltk_right_r : forall x k e e', ltk x (k,e) -> ltk x (k,e'). + Proof. auto. Qed. + + Lemma ltk_right_l : forall x k e e', ltk (k,e) x -> ltk (k,e') x. + Proof. auto. Qed. + Hint Immediate ltk_right_r ltk_right_l. +*) + + (* 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 <-> ExistsL (fun p => eq k (fst p)) l. + Proof. + unfold In, MapsTo. + setoid_rewrite ExistsL_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 ExistsL_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, ExistsL_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/Structures/OrderedType2Alt.v b/theories/Structures/OrderedType2Alt.v new file mode 100644 index 0000000000..43b3d05f8a --- /dev/null +++ b/theories/Structures/OrderedType2Alt.v @@ -0,0 +1,297 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* Finite sets library. + * Authors: Pierre Letouzey and Jean-Christophe Filliâtre + * Institution: LRI, CNRS UMR 8623 - Université Paris Sud + * 91405 Orsay, France *) + +(* $Id$ *) + +Require Import OrderedType2. +Set Implicit Arguments. + +(** NB: Instead of [comparison], defined in [Datatypes.v] which is [Eq|Lt|Gt], + we used historically the dependent type [compare] which is + [EQ _ | LT _ | GT _ ] +*) + +Inductive Compare (X : Type) (lt eq : X -> X -> Prop) (x y : X) : Type := + | LT : lt x y -> Compare lt eq x y + | EQ : eq x y -> Compare lt eq x y + | GT : lt y x -> Compare lt eq x y. + +(** * Some alternative (but equivalent) presentations for an Ordered Type + inferface. *) + +(** ** The original interface *) + +Module Type OrderedTypeOrig. + 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 Inline lt : t -> t -> Prop. + Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. + Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y. + + Parameter compare : forall x y : t, Compare lt eq x y. + + Hint Immediate eq_sym. + Hint Resolve eq_refl eq_trans. + +End OrderedTypeOrig. + +(** ** An interface based on compare *) + +Module Type OrderedTypeAlt. + + Parameter t : Type. + + Parameter compare : t -> t -> comparison. + + Infix "?=" := compare (at level 70, no associativity). + + Parameter compare_sym : + forall x y, (y?=x) = CompOpp (x?=y). + Parameter compare_trans : + forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c. + +End OrderedTypeAlt. + +(** ** From OrderedTypeOrig to OrderedType. *) + +Module OrderedType_from_Orig (O:OrderedTypeOrig) <: OrderedType. + + Import O. + Definition t := O.t. + Definition eq := O.eq. + Instance eq_equiv : Equivalence eq. + Proof. + split; red; [ apply eq_refl | apply eq_sym | eapply eq_trans ]. + Qed. + + Definition lt := O.lt. + Instance lt_strorder : StrictOrder lt. + Proof. + split; repeat red; intros. + eapply lt_not_eq; eauto. + eapply lt_trans; eauto. + Qed. + + Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z. + Proof. + intros; destruct (compare x z); auto. + elim (@lt_not_eq x y); eauto. + elim (@lt_not_eq z y); eauto using lt_trans. + Qed. + + Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z. + Proof. + intros; destruct (compare x z); auto. + elim (@lt_not_eq y z); eauto. + elim (@lt_not_eq y x); eauto using lt_trans. + Qed. + + Instance lt_compat : Proper (eq==>eq==>iff) lt. + Proof. + apply proper_sym_impl_iff_2; auto with *. + repeat red; intros. + eapply lt_eq; eauto. eapply eq_lt; eauto. symmetry; auto. + Qed. + + Definition compare x y := + match O.compare x y with + | EQ _ => Eq + | LT _ => Lt + | GT _ => Gt + end. + + Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y. + Proof. + intros; unfold compare; destruct O.compare; auto. + Qed. + + Definition eq_dec : forall x y, { eq x y } + { ~eq x y }. + Proof. + intros; destruct (O.compare x y). + right. apply lt_not_eq; auto. + left; auto. + right. intro. apply (@lt_not_eq y x); auto. + Defined. + +End OrderedType_from_Orig. + +(** ** From OrderedType to OrderedTypeOrig. *) + +Module OrderedType_to_Orig (O:OrderedType) <: OrderedTypeOrig. + + Import O. + Definition t := t. + Definition eq := eq. + Definition lt := lt. + + Lemma eq_refl : Reflexive eq. + Proof. auto. Qed. + Lemma eq_sym : Symmetric eq. + Proof. apply eq_equiv. Qed. + Lemma eq_trans : Transitive eq. + Proof. apply eq_equiv. Qed. + + Lemma lt_not_eq : forall x y, lt x y -> ~eq x y. + Proof. + intros x y L E; rewrite E in L. apply (StrictOrder_Irreflexive y); auto. + Qed. + + Lemma lt_trans : Transitive lt. + Proof. apply lt_strorder. Qed. + + Definition compare : forall x y, Compare lt eq x y. + Proof. + intros. generalize (compare_spec x y); unfold Cmp, flip. + destruct (compare x y); [apply EQ|apply LT|apply GT]; auto. + Defined. + + Definition eq_dec := eq_dec. + +End OrderedType_to_Orig. + + +(** ** From OrderedTypeAlt to OrderedType. *) + +Module OrderedType_from_Alt (O:OrderedTypeAlt) <: OrderedType. + Import O. + + Definition t := t. + + Definition eq x y := (x?=y) = Eq. + Definition lt x y := (x?=y) = Lt. + + Instance eq_equiv : Equivalence eq. + Proof. + split; red. + (* refl *) + unfold eq; intros x. + assert (H:=compare_sym x x). + destruct (x ?= x); simpl in *; auto; discriminate. + (* sym *) + unfold eq; intros x y H. + rewrite compare_sym, H; simpl; auto. + (* trans *) + apply compare_trans. + Qed. + + Instance lt_strorder : StrictOrder lt. + Proof. + split; repeat red; unfold lt; try apply compare_trans. + intros x H. + assert (eq x x) by reflexivity. + unfold eq in *; congruence. + Qed. + + Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z. + Proof. + unfold lt, eq; intros x y z Hxy Hyz. + destruct (compare x z) as [ ]_eqn:Hxz; auto. + rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz. + rewrite (compare_trans Hxz Hyz) in Hxy; discriminate. + rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy. + rewrite (compare_trans Hxy Hxz) in Hyz; discriminate. + Qed. + + Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z. + Proof. + unfold lt, eq; intros x y z Hxy Hyz. + destruct (compare x z) as [ ]_eqn:Hxz; auto. + rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy. + rewrite (compare_trans Hxy Hxz) in Hyz; discriminate. + rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz. + rewrite (compare_trans Hxz Hyz) in Hxy; discriminate. + Qed. + + Instance lt_compat : Proper (eq==>eq==>iff) lt. + Proof. + apply proper_sym_impl_iff_2; auto with *. + repeat red; intros. + eapply lt_eq; eauto. eapply eq_lt; eauto. symmetry; auto. + Qed. + + Definition compare := O.compare. + + Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y. + Proof. + unfold Cmp, flip, eq, lt, compare; intros. + destruct (O.compare x y) as [ ]_eqn:H; auto. + rewrite compare_sym, H; auto. + Qed. + + Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }. + Proof. + intros; unfold eq. + case (x ?= y); [ left | right | right ]; auto; discriminate. + Defined. + +End OrderedType_from_Alt. + +(** From the original presentation to this alternative one. *) + +Module OrderedType_to_Alt (O:OrderedType) <: OrderedTypeAlt. + Import O. + + Definition t := t. + Definition compare := compare. + + Infix "?=" := compare (at level 70, no associativity). + + Lemma compare_sym : + 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. + 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. + rewrite V in U. elim (StrictOrder_Irreflexive x); auto. + rewrite V in U. elim (StrictOrder_Irreflexive x); auto. + rewrite V in U. elim (StrictOrder_Irreflexive y); auto. + Qed. + + 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. + rewrite H0 in H. elim (StrictOrder_Irreflexive y); auto. + rewrite H0 in H. elim (StrictOrder_Irreflexive y); auto. + Qed. + + 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. + rewrite H in H0. elim (StrictOrder_Irreflexive y); auto. + rewrite H in H0. elim (StrictOrder_Irreflexive x); auto. + Qed. + + Lemma compare_trans : + forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c. + Proof. + intros c x y z. + destruct c; unfold compare. + rewrite 3 compare_Eq; eauto. + rewrite 3 compare_Lt. apply StrictOrder_Transitive. + do 3 (rewrite compare_sym, CompOpp_iff, compare_Lt). + intros; apply StrictOrder_Transitive with y; auto. + Qed. + +End OrderedType_to_Alt. diff --git a/theories/Structures/OrderedType2Ex.v b/theories/Structures/OrderedType2Ex.v new file mode 100644 index 0000000000..73bd3810f9 --- /dev/null +++ b/theories/Structures/OrderedType2Ex.v @@ -0,0 +1,261 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* Finite sets library. + * Authors: Pierre Letouzey and Jean-Christophe Filliâtre + * Institution: LRI, CNRS UMR 8623 - Université Paris Sud + * 91405 Orsay, France *) + +(* $Id$ *) + +Require Import OrderedType2 DecidableType2Ex. +Require Import ZArith NArith Ndec Compare_dec. + +(** * 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. + + +(** An OrderedType can now directly be seen as a DecidableType *) + +Module OT_as_DT (O:OrderedType) <: DecidableType := O. + +(** (Usual) Decidable Type for [nat], [positive], [N], [Z] *) + +Module Nat_as_DT <: UsualDecidableType := Nat_as_OT. +Module Positive_as_DT <: UsualDecidableType := Positive_as_OT. +Module N_as_DT <: UsualDecidableType := N_as_OT. +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. + + 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. + + Instance lt_strorder : StrictOrder lt. + Proof. + split. + (* irreflexive *) + intros (x1,x2); compute. destruct 1. + apply (StrictOrder_Irreflexive x1); auto. + apply (StrictOrder_Irreflexive x2); intuition. + (* transitive *) + intros (x1,x2) (y1,y2) (z1,z2); unfold eq, lt; simpl; intuition. + left; etransitivity; eauto. + left; rewrite <- H0; auto. + left; rewrite H; auto. + right; split; eauto. etransitivity; eauto. + Qed. + + Instance lt_compat : Proper (eq==>eq==>iff) lt. + Proof. + intros (x1,x2) (x1',x2') (X1,X2) (y1,y2) (y1',y2') (Y1,Y2). + unfold lt; simpl in *. + rewrite X1,X2,Y1,Y2; intuition. + Qed. + + Definition compare x y := + match O1.compare (fst x) (fst y) with + | Eq => O2.compare (snd x) (snd y) + | Lt => Lt + | Gt => Gt + end. + + Lemma compare_spec : forall x y, Cmp eq lt (compare x y) 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. + 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/OrderedTypeAlt.v b/theories/Structures/OrderedTypeAlt.v new file mode 100644 index 0000000000..23ae4c85a3 --- /dev/null +++ b/theories/Structures/OrderedTypeAlt.v @@ -0,0 +1,122 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) +(* $Id$ *) + +Require Import OrderedType. + +(** * An alternative (but equivalent) presentation for an Ordered Type + inferface. *) + +(** NB: [comparison], defined in [Datatypes.v] is [Eq|Lt|Gt] +whereas [compare], defined in [OrderedType.v] is [EQ _ | LT _ | GT _ ] +*) + +Module Type OrderedTypeAlt. + + Parameter t : Type. + + Parameter compare : t -> t -> comparison. + + Infix "?=" := compare (at level 70, no associativity). + + Parameter compare_sym : + forall x y, (y?=x) = CompOpp (x?=y). + Parameter compare_trans : + forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c. + +End OrderedTypeAlt. + +(** From this new presentation to the original one. *) + +Module OrderedType_from_Alt (O:OrderedTypeAlt) <: OrderedType. + Import O. + + Definition t := t. + + Definition eq x y := (x?=y) = Eq. + Definition lt x y := (x?=y) = Lt. + + Lemma eq_refl : forall x, eq x x. + Proof. + intro x. + unfold eq. + assert (H:=compare_sym x x). + destruct (x ?= x); simpl in *; try discriminate; auto. + Qed. + + Lemma eq_sym : forall x y, eq x y -> eq y x. + Proof. + unfold eq; intros. + rewrite compare_sym. + rewrite H; simpl; auto. + Qed. + + Definition eq_trans := (compare_trans Eq). + + Definition lt_trans := (compare_trans Lt). + + Lemma lt_not_eq : forall x y, lt x y -> ~eq x y. + Proof. + unfold eq, lt; intros. + rewrite H; discriminate. + Qed. + + Definition compare : forall x y, Compare lt eq x y. + Proof. + intros. + case_eq (x ?= y); intros. + apply EQ; auto. + apply LT; auto. + apply GT; red. + rewrite compare_sym; rewrite H; auto. + Defined. + + Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }. + Proof. + intros; unfold eq. + case (x ?= y); [ left | right | right ]; auto; discriminate. + Defined. + +End OrderedType_from_Alt. + +(** From the original presentation to this alternative one. *) + +Module OrderedType_to_Alt (O:OrderedType) <: OrderedTypeAlt. + Import O. + Module MO:=OrderedTypeFacts(O). + Import MO. + + Definition t := t. + + Definition compare x y := match compare x y with + | LT _ => Lt + | EQ _ => Eq + | GT _ => Gt + end. + + Infix "?=" := compare (at level 70, no associativity). + + Lemma compare_sym : + forall x y, (y?=x) = CompOpp (x?=y). + Proof. + intros x y; unfold compare. + destruct O.compare; elim_comp; simpl; auto. + Qed. + + Lemma compare_trans : + forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c. + Proof. + intros c x y z. + destruct c; unfold compare; + do 2 (destruct O.compare; intros; try discriminate); + elim_comp; auto. + Qed. + +End OrderedType_to_Alt. + + diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v new file mode 100644 index 0000000000..a39f336a57 --- /dev/null +++ b/theories/Structures/OrderedTypeEx.v @@ -0,0 +1,243 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* $Id$ *) + +Require Import OrderedType. +Require Import ZArith. +Require Import Omega. +Require Import NArith Ndec. +Require Import Compare_dec. + +(** * Examples of Ordered Type structures. *) + +(** First, a particular case of [OrderedType] where + the equality is the usual one of Coq. *) + +Module Type UsualOrderedType. + Parameter Inline t : Type. + Definition eq := @eq t. + Parameter Inline lt : t -> t -> Prop. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. + Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y. + Parameter compare : forall x y : t, Compare lt eq x y. + Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq 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 eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + + Definition lt := lt. + + Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. + Proof. unfold lt; intros; apply lt_trans with y; auto. Qed. + + Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. + Proof. unfold lt, eq; intros; omega. Qed. + + Definition compare : forall x y : t, Compare lt eq x y. + Proof. + intros x y; destruct (nat_compare x y) as [ | | ]_eqn. + apply EQ. apply nat_compare_eq; assumption. + apply LT. apply nat_compare_Lt_lt; assumption. + apply GT. apply nat_compare_Gt_gt; assumption. + Defined. + + Definition eq_dec := eq_nat_dec. + +End Nat_as_OT. + + +(** [Z] is an ordered type with respect to the usual order on integers. *) + +Open Local Scope Z_scope. + +Module Z_as_OT <: UsualOrderedType. + + Definition t := Z. + Definition eq := @eq Z. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + + Definition lt (x y:Z) := (x<y). + + Lemma lt_trans : forall x y z, x<y -> y<z -> x<z. + Proof. intros; omega. Qed. + + Lemma lt_not_eq : forall x y, x<y -> ~ x=y. + Proof. intros; omega. Qed. + + Definition compare : forall x y, Compare lt eq x y. + Proof. + intros x y; destruct (x ?= y) as [ | | ]_eqn. + apply EQ; apply Zcompare_Eq_eq; assumption. + apply LT; assumption. + apply GT; apply Zgt_lt; assumption. + Defined. + + Definition eq_dec := Z_eq_dec. + +End Z_as_OT. + +(** [positive] is an ordered type with respect to the usual order on natural numbers. *) + +Open Local Scope positive_scope. + +Module Positive_as_OT <: UsualOrderedType. + Definition t:=positive. + Definition eq:=@eq positive. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + + Definition lt p q:= (p ?= q) Eq = Lt. + + Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. + Proof. + unfold lt; intros x y z. + change ((Zpos x < Zpos y)%Z -> (Zpos y < Zpos z)%Z -> (Zpos x < Zpos z)%Z). + omega. + Qed. + + Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. + Proof. + intros; intro. + rewrite H0 in H. + unfold lt in H. + rewrite Pcompare_refl in H; discriminate. + Qed. + + Definition compare : forall x y : t, Compare lt eq x y. + Proof. + intros x y. destruct ((x ?= y) Eq) as [ | | ]_eqn. + apply EQ; apply Pcompare_Eq_eq; assumption. + apply LT; assumption. + apply GT; apply ZC1; assumption. + Defined. + + 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. *) + +Open Local Scope positive_scope. + +Module N_as_OT <: UsualOrderedType. + Definition t:=N. + Definition eq:=@eq N. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + + Definition lt:=Nlt. + Definition lt_trans := Nlt_trans. + Definition lt_not_eq := Nlt_not_eq. + + Definition compare : forall x y : t, Compare lt eq x y. + Proof. + intros x y. destruct (x ?= y)%N as [ | | ]_eqn. + apply EQ; apply Ncompare_Eq_eq; assumption. + apply LT; assumption. + apply GT. apply Ngt_Nlt; assumption. + Defined. + + Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }. + Proof. + intros. unfold eq. decide equality. apply Positive_as_OT.eq_dec. + Defined. + +End N_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. + Module MO1:=OrderedTypeFacts(O1). + Module MO2:=OrderedTypeFacts(O2). + + Definition t := prod O1.t O2.t. + + Definition eq x y := O1.eq (fst x) (fst y) /\ O2.eq (snd x) (snd y). + + Definition lt x y := + O1.lt (fst x) (fst y) \/ + (O1.eq (fst x) (fst y) /\ O2.lt (snd x) (snd y)). + + Lemma eq_refl : forall x : t, eq x x. + Proof. + intros (x1,x2); red; simpl; auto. + Qed. + + Lemma eq_sym : forall x y : t, eq x y -> eq y x. + Proof. + intros (x1,x2) (y1,y2); unfold eq; simpl; intuition. + Qed. + + Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. + Proof. + intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto. + Qed. + + Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. + Proof. + intros (x1,x2) (y1,y2) (z1,z2); unfold eq, lt; simpl; intuition. + left; eauto. + left; eapply MO1.lt_eq; eauto. + left; eapply MO1.eq_lt; eauto. + right; split; eauto. + Qed. + + Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. + Proof. + intros (x1,x2) (y1,y2); unfold eq, lt; simpl; intuition. + apply (O1.lt_not_eq H0 H1). + apply (O2.lt_not_eq H3 H2). + Qed. + + Definition compare : forall x y : t, Compare lt eq x y. + intros (x1,x2) (y1,y2). + destruct (O1.compare x1 y1). + apply LT; unfold lt; auto. + destruct (O2.compare x2 y2). + apply LT; unfold lt; auto. + apply EQ; unfold eq; auto. + apply GT; unfold lt; auto. + apply GT; unfold lt; auto. + Defined. + + Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}. + Proof. + intros; elim (compare x y); intro H; [ right | left | right ]; auto. + auto using lt_not_eq. + assert (~ eq y x); auto using lt_not_eq, eq_sym. + Defined. + +End PairOrderedType. + |