From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- theories/Structures/DecidableType.v | 156 ++++++++ theories/Structures/DecidableTypeEx.v | 96 +++++ theories/Structures/Equalities.v | 218 +++++++++++ theories/Structures/EqualitiesFacts.v | 185 ++++++++++ theories/Structures/GenericMinMax.v | 656 ++++++++++++++++++++++++++++++++++ theories/Structures/OrderedType.v | 485 +++++++++++++++++++++++++ theories/Structures/OrderedTypeAlt.v | 122 +++++++ theories/Structures/OrderedTypeEx.v | 333 +++++++++++++++++ theories/Structures/Orders.v | 333 +++++++++++++++++ theories/Structures/OrdersAlt.v | 242 +++++++++++++ theories/Structures/OrdersEx.v | 88 +++++ theories/Structures/OrdersFacts.v | 234 ++++++++++++ theories/Structures/OrdersLists.v | 256 +++++++++++++ theories/Structures/OrdersTac.v | 293 +++++++++++++++ theories/Structures/vo.itarget | 14 + 15 files changed, 3711 insertions(+) create mode 100644 theories/Structures/DecidableType.v create mode 100644 theories/Structures/DecidableTypeEx.v create mode 100644 theories/Structures/Equalities.v create mode 100644 theories/Structures/EqualitiesFacts.v create mode 100644 theories/Structures/GenericMinMax.v create mode 100644 theories/Structures/OrderedType.v create mode 100644 theories/Structures/OrderedTypeAlt.v create mode 100644 theories/Structures/OrderedTypeEx.v create mode 100644 theories/Structures/Orders.v create mode 100644 theories/Structures/OrdersAlt.v create mode 100644 theories/Structures/OrdersEx.v create mode 100644 theories/Structures/OrdersFacts.v create mode 100644 theories/Structures/OrdersLists.v create mode 100644 theories/Structures/OrdersTac.v create mode 100644 theories/Structures/vo.itarget (limited to 'theories/Structures') diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v new file mode 100644 index 00000000..2c72e30b --- /dev/null +++ b/theories/Structures/DecidableType.v @@ -0,0 +1,156 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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. + + Global Instance eqk_equiv : Equivalence eqk. + Proof. split; eauto. Qed. + + Global Instance eqke_equiv : Equivalence eqke. + Proof. split; eauto. Qed. + + 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 with *. + 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 with *. + 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/DecidableTypeEx.v b/theories/Structures/DecidableTypeEx.v new file mode 100644 index 00000000..4407ead4 --- /dev/null +++ b/theories/Structures/DecidableTypeEx.v @@ -0,0 +1,96 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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/Equalities.v b/theories/Structures/Equalities.v new file mode 100644 index 00000000..487b1d0c --- /dev/null +++ b/theories/Structures/Equalities.v @@ -0,0 +1,218 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* t -> Prop. +End HasEq. + +Module Type Eq := Typ <+ HasEq. + +Module Type EqNotation (Import E:Eq). + Infix "==" := eq (at level 70, no associativity). + Notation "x ~= y" := (~eq x y) (at level 70, no associativity). +End EqNotation. + +Module Type Eq' := Eq <+ EqNotation. + +(** * Specification of the equality via the [Equivalence] type class *) + +Module Type IsEq (Import E:Eq). + Declare Instance eq_equiv : Equivalence eq. +End IsEq. + +(** * Earlier specification of equality by three separate lemmas. *) + +Module Type IsEqOrig (Import E:Eq'). + Axiom eq_refl : forall x : t, x==x. + Axiom eq_sym : forall x y : t, x==y -> y==x. + Axiom eq_trans : forall x y z : t, x==y -> y==z -> x==z. + Hint Immediate eq_sym. + Hint Resolve eq_refl eq_trans. +End IsEqOrig. + +(** * Types with decidable equality *) + +Module Type HasEqDec (Import E:Eq'). + Parameter eq_dec : forall x y : t, { x==y } + { ~ x==y }. +End HasEqDec. + +(** * Boolean Equality *) + +(** Having [eq_dec] is the same as having a boolean equality plus + a correctness proof. *) + +Module Type HasEqBool (Import E:Eq'). + Parameter Inline eqb : t -> t -> bool. + Parameter eqb_eq : forall x y, eqb x y = true <-> x==y. +End HasEqBool. + +(** From these basic blocks, we can build many combinations + of static standalone module types. *) + +Module Type EqualityType := Eq <+ IsEq. + +Module Type EqualityTypeOrig := Eq <+ IsEqOrig. + +Module Type EqualityTypeBoth <: EqualityType <: EqualityTypeOrig + := Eq <+ IsEq <+ IsEqOrig. + +Module Type DecidableType <: EqualityType + := Eq <+ IsEq <+ HasEqDec. + +Module Type DecidableTypeOrig <: EqualityTypeOrig + := Eq <+ IsEqOrig <+ HasEqDec. + +Module Type DecidableTypeBoth <: DecidableType <: DecidableTypeOrig + := EqualityTypeBoth <+ HasEqDec. + +Module Type BooleanEqualityType <: EqualityType + := Eq <+ IsEq <+ HasEqBool. + +Module Type BooleanDecidableType <: DecidableType <: BooleanEqualityType + := Eq <+ IsEq <+ HasEqDec <+ HasEqBool. + +Module Type DecidableTypeFull <: DecidableTypeBoth <: BooleanDecidableType + := Eq <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool. + +(** Same, with notation for [eq] *) + +Module Type EqualityType' := EqualityType <+ EqNotation. +Module Type EqualityTypeOrig' := EqualityTypeOrig <+ EqNotation. +Module Type EqualityTypeBoth' := EqualityTypeBoth <+ EqNotation. +Module Type DecidableType' := DecidableType <+ EqNotation. +Module Type DecidableTypeOrig' := DecidableTypeOrig <+ EqNotation. +Module Type DecidableTypeBoth' := DecidableTypeBoth <+ EqNotation. +Module Type BooleanEqualityType' := BooleanEqualityType <+ EqNotation. +Module Type BooleanDecidableType' := BooleanDecidableType <+ EqNotation. +Module Type DecidableTypeFull' := DecidableTypeFull <+ EqNotation. + +(** * Compatibility wrapper from/to the old version of + [EqualityType] and [DecidableType] *) + +Module BackportEq (E:Eq)(F:IsEq E) <: IsEqOrig E. + Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv. + Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv. + Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv. +End BackportEq. + +Module UpdateEq (E:Eq)(F:IsEqOrig E) <: IsEq E. + Instance eq_equiv : Equivalence E.eq. + Proof. exact (Build_Equivalence _ _ F.eq_refl F.eq_sym F.eq_trans). Qed. +End UpdateEq. + +Module Backport_ET (E:EqualityType) <: EqualityTypeBoth + := E <+ BackportEq. + +Module Update_ET (E:EqualityTypeOrig) <: EqualityTypeBoth + := E <+ UpdateEq. + +Module Backport_DT (E:DecidableType) <: DecidableTypeBoth + := E <+ BackportEq. + +Module Update_DT (E:DecidableTypeOrig) <: DecidableTypeBoth + := E <+ UpdateEq. + + +(** * Having [eq_dec] is equivalent to having [eqb] and its spec. *) + +Module HasEqDec2Bool (E:Eq)(F:HasEqDec E) <: HasEqBool E. + Definition eqb x y := if F.eq_dec x y then true else false. + Lemma eqb_eq : forall x y, eqb x y = true <-> E.eq x y. + Proof. + intros x y. unfold eqb. destruct F.eq_dec as [EQ|NEQ]. + auto with *. + split. discriminate. intro EQ; elim NEQ; auto. + Qed. +End HasEqDec2Bool. + +Module HasEqBool2Dec (E:Eq)(F:HasEqBool E) <: HasEqDec E. + Lemma eq_dec : forall x y, {E.eq x y}+{~E.eq x y}. + Proof. + intros x y. assert (H:=F.eqb_eq x y). + destruct (F.eqb x y); [left|right]. + apply -> H; auto. + intro EQ. apply H in EQ. discriminate. + Defined. +End HasEqBool2Dec. + +Module Dec2Bool (E:DecidableType) <: BooleanDecidableType + := E <+ HasEqDec2Bool. + +Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType + := E <+ HasEqBool2Dec. + + + +(** * UsualDecidableType + + A particular case of [DecidableType] where the equality is + the usual one of Coq. *) + +Module Type HasUsualEq (Import T:Typ) <: HasEq T. + Definition eq := @Logic.eq t. +End HasUsualEq. + +Module Type UsualEq <: Eq := Typ <+ HasUsualEq. + +Module Type UsualIsEq (E:UsualEq) <: IsEq E. + (* No Instance syntax to avoid saturating the Equivalence tables *) + Lemma eq_equiv : Equivalence E.eq. + Proof. exact eq_equivalence. Qed. +End UsualIsEq. + +Module Type UsualIsEqOrig (E:UsualEq) <: IsEqOrig E. + Definition eq_refl := @Logic.eq_refl E.t. + Definition eq_sym := @Logic.eq_sym E.t. + Definition eq_trans := @Logic.eq_trans E.t. +End UsualIsEqOrig. + +Module Type UsualEqualityType <: EqualityType + := UsualEq <+ UsualIsEq. + +Module Type UsualDecidableType <: DecidableType + := UsualEq <+ UsualIsEq <+ HasEqDec. + +Module Type UsualDecidableTypeOrig <: DecidableTypeOrig + := UsualEq <+ UsualIsEqOrig <+ HasEqDec. + +Module Type UsualDecidableTypeBoth <: DecidableTypeBoth + := UsualEq <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqDec. + +Module Type UsualBoolEq := UsualEq <+ HasEqBool. + +Module Type UsualDecidableTypeFull <: DecidableTypeFull + := UsualEq <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqDec <+ HasEqBool. + + +(** Some shortcuts for easily building a [UsualDecidableType] *) + +Module Type MiniDecidableType. + Include Typ. + Parameter eq_dec : forall x y : t, {x=y}+{~x=y}. +End MiniDecidableType. + +Module Make_UDT (M:MiniDecidableType) <: UsualDecidableTypeBoth + := M <+ HasUsualEq <+ UsualIsEq <+ UsualIsEqOrig. + +Module Make_UDTF (M:UsualBoolEq) <: UsualDecidableTypeFull + := M <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqBool2Dec. diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v new file mode 100644 index 00000000..d9b1d76f --- /dev/null +++ b/theories/Structures/EqualitiesFacts.v @@ -0,0 +1,185 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* E.eq ==> Logic.eq) eqb. +Proof. +intros x x' Exx' y y' Eyy'. +apply eq_true_iff_eq. +rewrite 2 eqb_eq, Exx', Eyy'; auto with *. +Qed. + +End BoolEqualityFacts. + + +(** * Keys and datas used in FMap *) +Module KeyDecidableType(Import D:DecidableType). + + Section Elt. + Variable elt : Type. + Notation key:=t. + + Local Open Scope signature_scope. + + Definition eqk : relation (key*elt) := eq @@1. + Definition eqke : relation (key*elt) := eq * Logic.eq. + Hint Unfold eqk eqke. + + (* 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. + + (* Additionnal facts *) + + 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. + + 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; 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 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 Unfold eqk eqke. + Hint Extern 2 (eqke ?a ?b) => split. + Hint Resolve InA_eqke_eqk. + Hint Unfold MapsTo In. + Hint Resolve In_inv_2 In_inv_3. + +End KeyDecidableType. + + +(** * PairDecidableType + + From two decidable types, we can build a new DecidableType + over their cartesian product. *) + +Module PairDecidableType(D1 D2:DecidableType) <: DecidableType. + + Definition t := (D1.t * D2.t)%type. + + Definition eq := (D1.eq * D2.eq)%signature. + + Instance eq_equiv : Equivalence eq. + + 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); + compute; intuition. + Defined. + +End PairDecidableType. + +(** Similarly for pairs of UsualDecidableType *) + +Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType. + 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 }. + 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/GenericMinMax.v b/theories/Structures/GenericMinMax.v new file mode 100644 index 00000000..68f20189 --- /dev/null +++ b/theories/Structures/GenericMinMax.v @@ -0,0 +1,656 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* t -> t. + Parameter max_l : forall x y, y<=x -> max x y == x. + Parameter max_r : forall x y, x<=y -> max x y == y. +End HasMax. + +Module Type HasMin (Import E:EqLe'). + Parameter Inline min : t -> t -> t. + Parameter min_l : forall x y, x<=y -> min x y == x. + Parameter min_r : forall x y, y<=x -> min x y == y. +End HasMin. + +Module Type HasMinMax (E:EqLe) := HasMax E <+ HasMin E. + + +(** ** 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 ge_not_lt : forall x y, y<=x -> x False. + Proof. + intros x y H H'. + apply (StrictOrder_Irreflexive x). + rewrite le_lteq in *; destruct H as [H|H]. + transitivity y; auto. + rewrite H in H'; auto. + Qed. + + Lemma max_l : forall x y, y<=x -> max x y == x. + Proof. + intros. unfold max, gmax. case compare_spec; auto with relations. + intros; elim (ge_not_lt x y); auto. + Qed. + + Lemma max_r : forall x y, x<=y -> max x y == y. + Proof. + intros. unfold max, gmax. case compare_spec; auto with relations. + intros; elim (ge_not_lt y x); auto. + Qed. + + Lemma min_l : forall x y, x<=y -> min x y == x. + Proof. + intros. unfold min, gmin. case compare_spec; auto with relations. + intros; elim (ge_not_lt y x); auto. + Qed. + + Lemma min_r : forall x y, y<=x -> min x y == y. + Proof. + intros. unfold min, gmin. case compare_spec; auto with relations. + intros; elim (ge_not_lt x y); auto. + Qed. + +End GenericMinMax. + + +(** ** Consequences of the minimalist interface: facts about [max]. *) + +Module MaxLogicalProperties (Import O:TotalOrder')(Import M:HasMax O). + Module Import T := !MakeOrderTac O. + +(** An alternative caracterisation of [max], equivalent to + [max_l /\ max_r] *) + +Lemma max_spec : forall n m, + (n < m /\ max n m == m) \/ (m <= n /\ max n m == n). +Proof. + intros n m. + destruct (lt_total n m); [left|right]. + split; auto. apply max_r. rewrite le_lteq; auto. + assert (m <= n) by (rewrite le_lteq; intuition). + split; auto. apply max_l; auto. +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. + +Instance : Proper (eq==>eq==>iff) le. +Proof. repeat red. intuition order. Qed. + +Instance max_compat : Proper (eq==>eq==>eq) max. +Proof. +intros x x' Hx y y' Hy. +assert (H1 := max_spec x y). assert (H2 := max_spec x' y'). +set (m := max x y) in *; set (m' := max x' y') in *; clearbody m m'. +rewrite <- Hx, <- Hy in *. +destruct (lt_total x y); intuition order. +Qed. + + +(** A function satisfying the same specification is equal to [max]. *) + +Lemma max_unicity : forall n m p, + ((n < m /\ p == m) \/ (m <= n /\ p == n)) -> p == max n m. +Proof. + intros. assert (Hm := max_spec n m). + destruct (lt_total n m); intuition; order. +Qed. + +Lemma max_unicity_ext : forall f, + (forall n m, (n < m /\ f n m == m) \/ (m <= n /\ f n m == n)) -> + (forall n m, f n m == max n m). +Proof. + intros. apply max_unicity; auto. +Qed. + +(** [max] commutes with monotone functions. *) + +Lemma max_mono: 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 (max_spec x y) as [(H,E)|(H,E)]; rewrite E; + destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. + assert (f x <= f y) by (apply Lef; order). order. + assert (f y <= f x) by (apply Lef; order). order. +Qed. + +(** *** Semi-lattice algebraic properties of [max] *) + +Lemma max_id : forall n, max n n == n. +Proof. + intros. destruct (max_spec n n); intuition. +Qed. + +Notation max_idempotent := max_id (only parsing). + +Lemma max_assoc : forall m n p, max m (max n p) == max (max m n) p. +Proof. + intros. + destruct (max_spec n p) as [(H,Eq)|(H,Eq)]; rewrite Eq. + destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'. + destruct (max_spec m p); intuition; order. order. + destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'. order. + destruct (max_spec m p); intuition; order. +Qed. + +Lemma max_comm : forall n m, max n m == max m n. +Proof. + intros. + destruct (max_spec n m) as [(H,Eq)|(H,Eq)]; rewrite Eq. + destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order. + destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order. +Qed. + +(** *** Least-upper bound properties of [max] *) + +Lemma le_max_l : forall n m, n <= max n m. +Proof. + intros; destruct (max_spec n m); intuition; order. +Qed. + +Lemma le_max_r : forall n m, m <= max n m. +Proof. + intros; destruct (max_spec n m); intuition; order. +Qed. + +Lemma max_l_iff : forall n m, max n m == n <-> m <= n. +Proof. + split. intro H; rewrite <- H. apply le_max_r. apply max_l. +Qed. + +Lemma max_r_iff : forall n m, max n m == m <-> n <= m. +Proof. + split. intro H; rewrite <- H. apply le_max_l. apply max_r. +Qed. + +Lemma max_le : forall n m p, p <= max n m -> p <= n \/ p <= m. +Proof. + intros n m p H; destruct (max_spec n m); + [right|left]; intuition; order. +Qed. + +Lemma max_le_iff : forall n m p, p <= max n m <-> p <= n \/ p <= m. +Proof. + intros. split. apply max_le. + destruct (max_spec n m); intuition; order. +Qed. + +Lemma max_lt_iff : forall n m p, p < max n m <-> p < n \/ p < m. +Proof. + intros. destruct (max_spec n m); intuition; + order || (right; order) || (left; order). +Qed. + +Lemma max_lub_l : forall n m p, max n m <= p -> n <= p. +Proof. + intros; destruct (max_spec n m); intuition; order. +Qed. + +Lemma max_lub_r : forall n m p, max n m <= p -> m <= p. +Proof. + intros; destruct (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 (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 (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 (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 (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 (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 MaxLogicalProperties. + + +(** ** Properties concernant [min], then both [min] and [max]. + + To avoid too much code duplication, we exploit that [min] can be + seen as a [max] of the reversed order. +*) + +Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O). + Include MaxLogicalProperties O M. + Import T. + + Module ORev := TotalOrderRev O. + Module MRev <: HasMax ORev. + Definition max x y := M.min y x. + Definition max_l x y := M.min_r y x. + Definition max_r x y := M.min_l y x. + End MRev. + Module MPRev := MaxLogicalProperties ORev MRev. + +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. intros. exact (MPRev.max_spec m n). 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_mono: 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_mono; 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. + +Notation min_idempotent := min_id (only parsing). + +Lemma min_assoc : forall m n p, min m (min n p) == min (min m n) p. +Proof. intros. symmetry; apply MPRev.max_assoc. Qed. + +Lemma min_comm : forall n m, min n m == min m n. +Proof. intros. exact (MPRev.max_comm 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_l_iff : forall n m, min n m == n <-> n <= m. +Proof. intros n m. exact (MPRev.max_r_iff m n). Qed. + +Lemma min_r_iff : forall n m, min n m == m <-> m <= n. +Proof. intros n m. exact (MPRev.max_l_iff m n). Qed. + +Lemma min_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 (min_spec n m) as [(C,E)|(C,E)]; rewrite E. + apply max_l. order. + destruct (max_spec n m); intuition; order. +Qed. + +Lemma max_min_absorption : forall n m, min n (max n m) == n. +Proof. + intros. + destruct (max_spec n m) as [(C,E)|(C,E)]; rewrite E. + destruct (min_spec n m) as [(C',E')|(C',E')]; auto. order. + apply min_l; auto. order. +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_mono. + 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_mono. + 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 with *. + destruct (min_spec m n) as [(C',E')|(C',E')]; rewrite E'. + rewrite 2 max_l; try order. rewrite min_le_iff; auto. + rewrite 2 max_l; try order. rewrite min_le_iff; auto. +Qed. + +Lemma min_max_modular : forall n m p, + 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 with *. + destruct (max_spec m n) as [(C',E')|(C',E')]; rewrite E'. + rewrite 2 min_l; try order. rewrite max_le_iff; right; order. + rewrite 2 min_l; try order. rewrite max_le_iff; auto. +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_antimono : 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 (min_spec x y) as [(H,E)|(H,E)]; rewrite E; + destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. + assert (f y <= f x) by (apply Lef; order). order. + assert (f x <= f y) by (apply Lef; order). order. +Qed. + +Lemma min_max_antimono : forall f, + 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 (max_spec x y) as [(H,E)|(H,E)]; rewrite E; + destruct (min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. + assert (f y <= f x) by (apply Lef; order). order. + assert (f x <= f y) by (apply Lef; order). order. +Qed. + +End MinMaxLogicalProperties. + + +(** ** Properties requiring a decidable order *) + +Module MinMaxDecProperties (Import O:OrderedTypeFull')(Import M:HasMinMax O). + +(** 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. +destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT]. +assert (n<=m) by (rewrite le_lteq; auto). +apply (Compat m), Hr; auto. symmetry; apply max_r; auto. +assert (n<=m) by (rewrite le_lteq; auto). +apply (Compat m), Hr; auto. symmetry; apply max_r; auto. +assert (m<=n) by (rewrite le_lteq; auto). +apply (Compat n), Hl; auto. symmetry; apply max_l; auto. +Defined. + +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 with relations. + intros x y H [E|E]; [left|right]; rewrite <-H; auto. +Defined. + +(** Idem for [min] *) + +Lemma min_case_strong : forall n m (P:O.t -> Type), + (forall x y, x == y -> P x -> P y) -> + (n<=m -> P n) -> (m<=n -> P m) -> P (min n m). +Proof. +intros n m P Compat Hl Hr. +destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT]. +assert (n<=m) by (rewrite le_lteq; auto). +apply (Compat n), Hl; auto. symmetry; apply min_l; auto. +assert (n<=m) by (rewrite le_lteq; auto). +apply (Compat n), Hl; auto. symmetry; apply min_l; auto. +assert (m<=n) by (rewrite le_lteq; auto). +apply (Compat m), Hr; auto. symmetry; apply min_r; auto. +Defined. + +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. apply min_case; auto with relations. + intros x y H [E|E]; [left|right]; rewrite <- E; auto with relations. +Defined. + +End MinMaxDecProperties. + +Module MinMaxProperties (Import O:OrderedTypeFull')(Import M:HasMinMax O). + Module OT := OTF_to_TotalOrder O. + Include MinMaxLogicalProperties OT M. + Include MinMaxDecProperties O M. + Definition max_l := max_l. + Definition max_r := max_r. + Definition min_l := min_l. + Definition min_r := min_r. + Notation max_monotone := max_mono. + Notation min_monotone := min_mono. + Notation max_min_antimonotone := max_min_antimono. + Notation min_max_antimonotone := min_max_antimono. +End MinMaxProperties. + + +(** ** When the equality is Leibniz, we can skip a few [Proper] precondition. *) + +Module UsualMinMaxLogicalProperties + (Import O:UsualTotalOrder')(Import M:HasMinMax O). + + Include MinMaxLogicalProperties O M. + + 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_mono; auto. congruence. Qed. + + 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_mono; auto. congruence. Qed. + + Lemma min_max_antimonotone : forall f, Proper (le ==> inverse le) f -> + forall x y, min (f x) (f y) = f (max x y). + Proof. intros; apply min_max_antimono; auto. congruence. Qed. + + Lemma max_min_antimonotone : forall f, Proper (le ==> inverse le) f -> + forall x y, max (f x) (f y) = f (min x y). + Proof. intros; apply max_min_antimono; auto. congruence. Qed. + +End UsualMinMaxLogicalProperties. + + +Module UsualMinMaxDecProperties + (Import O:UsualOrderedTypeFull')(Import M:HasMinMax O). + + Module P := MinMaxDecProperties O M. + + Lemma max_case_strong : forall n m (P:t -> Type), + (m<=n -> P n) -> (n<=m -> P m) -> P (max n m). + Proof. intros; apply P.max_case_strong; auto. congruence. Defined. + + Lemma max_case : forall n m (P:t -> Type), + P n -> P m -> P (max n m). + Proof. intros; apply max_case_strong; auto. Defined. + + Lemma max_dec : forall n m, {max n m = n} + {max n m = m}. + Proof. exact P.max_dec. Defined. + + Lemma min_case_strong : forall n m (P:O.t -> Type), + (n<=m -> P n) -> (m<=n -> P m) -> P (min n m). + Proof. intros; apply P.min_case_strong; auto. congruence. Defined. + + Lemma min_case : forall n m (P:O.t -> Type), + P n -> P m -> P (min n m). + Proof. intros. apply min_case_strong; auto. Defined. + + Lemma min_dec : forall n m, {min n m = n} + {min n m = m}. + Proof. exact P.min_dec. Defined. + +End UsualMinMaxDecProperties. + +Module UsualMinMaxProperties + (Import O:UsualOrderedTypeFull')(Import M:HasMinMax O). + Module OT := OTF_to_TotalOrder O. + Include UsualMinMaxLogicalProperties OT M. + Include UsualMinMaxDecProperties O M. + Definition max_l := max_l. + Definition max_r := max_r. + Definition min_l := min_l. + Definition min_r := min_r. +End UsualMinMaxProperties. + + +(** From [TotalOrder] and [HasMax] and [HasEqDec], we can prove + that the order is decidable and build an [OrderedTypeFull]. *) + +Module TOMaxEqDec_to_Compare + (Import O:TotalOrder')(Import M:HasMax O)(Import E:HasEqDec O) <: HasCompare O. + + Definition compare x y := + if eq_dec x y then Eq + else if eq_dec (M.max x y) y then Lt else Gt. + + Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). + Proof. + intros; unfold compare; repeat destruct eq_dec; auto; constructor. + destruct (lt_total x y); auto. + absurd (x==y); auto. transitivity (max x y); auto. + symmetry. apply max_l. rewrite le_lteq; intuition. + destruct (lt_total y x); auto. + absurd (max x y == y); auto. apply max_r; rewrite le_lteq; intuition. + Qed. + +End TOMaxEqDec_to_Compare. + +Module TOMaxEqDec_to_OTF (O:TotalOrder)(M:HasMax O)(E:HasEqDec O) + <: OrderedTypeFull + := O <+ E <+ TOMaxEqDec_to_Compare O M E. + + + +(** TODO: 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 ? + +*) diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v new file mode 100644 index 00000000..72fbe796 --- /dev/null +++ b/theories/Structures/OrderedType.v @@ -0,0 +1,485 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 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). + + Instance eq_equiv : Equivalence eq. + Proof. split; [ exact eq_refl | exact eq_sym | exact eq_trans ]. Qed. + + Lemma lt_antirefl : forall x, ~ lt x x. + Proof. + intros; intro; absurd (eq x x); auto. + Qed. + + Instance lt_strorder : StrictOrder lt. + Proof. split; [ exact lt_antirefl | exact lt_trans]. 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. + + Instance lt_compat : Proper (eq==>eq==>iff) lt. + Proof. + apply proper_sym_impl_iff_2; auto with *. + intros x x' Hx y y' Hy H. + apply eq_lt with x; auto. + apply lt_eq with y; auto. + Qed. + + Lemma lt_total : forall x y, lt x y \/ eq x y \/ lt y x. + Proof. intros; destruct (compare x y); auto. Qed. + + Module OrderElts <: Orders.TotalOrder. + Definition t := t. + Definition eq := eq. + Definition lt := lt. + Definition le x y := lt x y \/ eq x y. + Definition eq_equiv := eq_equiv. + Definition lt_strorder := lt_strorder. + Definition lt_compat := lt_compat. + Definition lt_total := lt_total. + Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y. + Proof. unfold le; intuition. Qed. + End OrderElts. + Module OrderTac := !MakeOrderTac OrderElts. + Ltac order := OrderTac.order. + + Lemma le_eq x y z : ~lt x y -> eq y z -> ~lt x z. Proof. order. Qed. + Lemma eq_le x y z : eq x y -> ~lt y z -> ~lt x z. Proof. order. Qed. + Lemma neq_eq x y z : ~eq x y -> eq y z -> ~eq x z. Proof. order. Qed. + Lemma eq_neq x y z : eq x y -> ~eq y z -> ~eq x z. Proof. order. Qed. + Lemma le_lt_trans x y z : ~lt y x -> lt y z -> lt x z. Proof. order. Qed. + Lemma lt_le_trans x y z : lt x y -> ~lt z y -> lt x z. Proof. order. Qed. + Lemma le_neq x y : ~lt x y -> ~eq x y -> lt y x. Proof. order. Qed. + Lemma le_trans x y z : ~lt y x -> ~lt z y -> ~lt z x. Proof. order. Qed. + Lemma le_antisym x y : ~lt y x -> ~lt x y -> eq x y. Proof. order. Qed. + Lemma neq_sym x y : ~eq x y -> ~eq y x. Proof. order. Qed. + Lemma lt_le x y : lt x y -> ~lt y x. Proof. order. Qed. + Lemma gt_not_eq x y : lt y x -> ~ eq x y. Proof. order. Qed. + Lemma eq_not_lt x y : eq x y -> ~ lt x y. Proof. order. Qed. + Lemma eq_not_gt x y : eq x y -> ~ lt y x. Proof. order. Qed. + Lemma lt_not_gt x y : lt x y -> ~ lt y x. Proof. order. Qed. + + Hint Resolve gt_not_eq eq_not_lt. + Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq. + 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 (exfalso; 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 (exfalso; 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 (exfalso; 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 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_equiv). 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. + +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. + + Global Instance eqk_equiv : Equivalence eqk. + Proof. split; eauto. Qed. + + Global Instance eqke_equiv : Equivalence eqke. + Proof. split; eauto. Qed. + + Global Instance ltk_strorder : StrictOrder ltk. + Proof. + split; eauto. + intros (x,e); compute; apply (StrictOrder_Irreflexive x). + Qed. + + Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk. + Proof. + intros (x,e) (x',e') Hxx' (y,f) (y',f') Hyy'; compute. + compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto. + Qed. + + Global Instance ltk_compat' : Proper (eqke==>eqke==>iff) ltk. + Proof. + intros (x,e) (x',e') (Hxx',_) (y,f) (y',f') (Hyy',_); compute. + compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto. + Qed. + + (* 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 with *. + 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_equiv ltk_strorder ltk_compat). Qed. + + Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l. + Proof. exact (InfA_ltA ltk_strorder). 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_equiv ltk_strorder ltk_compat). + 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_equiv ltk_strorder ltk_compat). + 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/OrderedTypeAlt.v b/theories/Structures/OrderedTypeAlt.v new file mode 100644 index 00000000..23ae4c85 --- /dev/null +++ b/theories/Structures/OrderedTypeAlt.v @@ -0,0 +1,122 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 00000000..b4dbceba --- /dev/null +++ b/theories/Structures/OrderedTypeEx.v @@ -0,0 +1,333 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 x ~ 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. + + +(** Even if [positive] can be seen as an ordered type with respect to the + usual order (see above), we can also use a lexicographic order over bits + (lower bits are considered first). This is more natural when using + [positive] as indexes for sets or maps (see FSetPositive and FMapPositive. *) + +Module PositiveOrderedTypeBits <: UsualOrderedType. + Definition t:=positive. + Definition eq:=@eq positive. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + + Fixpoint bits_lt (p q:positive) : Prop := + match p, q with + | xH, xI _ => True + | xH, _ => False + | xO p, xO q => bits_lt p q + | xO _, _ => True + | xI p, xI q => bits_lt p q + | xI _, _ => False + end. + + Definition lt:=bits_lt. + + Lemma bits_lt_trans : + forall x y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z. + Proof. + induction x. + induction y; destruct z; simpl; eauto; intuition. + induction y; destruct z; simpl; eauto; intuition. + induction y; destruct z; simpl; eauto; intuition. + Qed. + + Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. + Proof. + exact bits_lt_trans. + Qed. + + Lemma bits_lt_antirefl : forall x : positive, ~ bits_lt x x. + Proof. + induction x; simpl; auto. + Qed. + + Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. + Proof. + intros; intro. + rewrite <- H0 in H; clear H0 y. + unfold lt in H. + exact (bits_lt_antirefl x H). + Qed. + + Definition compare : forall x y : t, Compare lt eq x y. + Proof. + induction x; destruct y. + (* I I *) + destruct (IHx y). + apply LT; auto. + apply EQ; rewrite e; red; auto. + apply GT; auto. + (* I O *) + apply GT; simpl; auto. + (* I H *) + apply GT; simpl; auto. + (* O I *) + apply LT; simpl; auto. + (* O O *) + destruct (IHx y). + apply LT; auto. + apply EQ; rewrite e; red; auto. + apply GT; auto. + (* O H *) + apply LT; simpl; auto. + (* H I *) + apply LT; simpl; auto. + (* H O *) + apply GT; simpl; auto. + (* H H *) + apply EQ; red; auto. + Qed. + + Lemma eq_dec (x y: positive): {x = y} + {x <> y}. + Proof. + intros. case_eq ((x ?= y) Eq); intros. + left. apply Pcompare_Eq_eq; auto. + right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate. + right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate. + Qed. + +End PositiveOrderedTypeBits. diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v new file mode 100644 index 00000000..bddd461a --- /dev/null +++ b/theories/Structures/Orders.v @@ -0,0 +1,333 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* t -> Prop. +End HasLt. + +Module Type HasLe (Import T:Typ). + Parameter Inline le : t -> t -> Prop. +End HasLe. + +Module Type EqLt := Typ <+ HasEq <+ HasLt. +Module Type EqLe := Typ <+ HasEq <+ HasLe. +Module Type EqLtLe := Typ <+ HasEq <+ HasLt <+ HasLe. + +(** Versions with nice notations *) + +Module Type LtNotation (E:EqLt). + Infix "<" := E.lt. + Notation "x > y" := (y= y" := (y<=x) (only parsing). + Notation "x <= y <= z" := (x<=y /\ y<=z). +End LeNotation. + +Module Type LtLeNotation (E:EqLtLe). + Include LtNotation E <+ LeNotation E. + Notation "x <= y < z" := (x<=y /\ yeq==>iff) lt. +End IsStrOrder. + +Module Type LeIsLtEq (Import E:EqLtLe'). + Axiom le_lteq : forall x y, x<=y <-> x t -> comparison. + Axiom compare_spec : forall x y, CompSpec eq lt x y (compare x y). +End HasCompare. + +Module Type StrOrder := EqualityType <+ HasLt <+ IsStrOrder. +Module Type DecStrOrder := StrOrder <+ HasCompare. +Module Type OrderedType <: DecidableType := DecStrOrder <+ HasEqDec. +Module Type OrderedTypeFull := OrderedType <+ HasLe <+ LeIsLtEq. + +Module Type StrOrder' := StrOrder <+ EqLtNotation. +Module Type DecStrOrder' := DecStrOrder <+ EqLtNotation. +Module Type OrderedType' := OrderedType <+ EqLtNotation. +Module Type OrderedTypeFull' := OrderedTypeFull <+ EqLtLeNotation. + +(** NB: in [OrderedType], an [eq_dec] could be deduced from [compare]. + But adding this redundant field allows to see an [OrderedType] as a + [DecidableType]. *) + +(** * Versions with [eq] being the usual Leibniz equality of Coq *) + +Module Type UsualStrOrder := UsualEqualityType <+ HasLt <+ IsStrOrder. +Module Type UsualDecStrOrder := UsualStrOrder <+ HasCompare. +Module Type UsualOrderedType <: UsualDecidableType <: OrderedType + := UsualDecStrOrder <+ HasEqDec. +Module Type UsualOrderedTypeFull := UsualOrderedType <+ HasLe <+ LeIsLtEq. + +(** NB: in [UsualOrderedType], the field [lt_compat] is + useless since [eq] is [Leibniz], but it should be + there for subtyping. *) + +Module Type UsualStrOrder' := UsualStrOrder <+ LtNotation. +Module Type UsualDecStrOrder' := UsualDecStrOrder <+ LtNotation. +Module Type UsualOrderedType' := UsualOrderedType <+ LtNotation. +Module Type UsualOrderedTypeFull' := UsualOrderedTypeFull <+ LtLeNotation. + +(** * Purely logical versions *) + +Module Type LtIsTotal (Import E:EqLt'). + Axiom lt_total : forall x y, x true | _ => false end. + + Lemma eqb_eq : forall x y, eqb x y = true <-> x==y. + Proof. + unfold eqb. intros x y. + destruct (compare_spec x y) as [H|H|H]; split; auto; try discriminate. + intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H). + intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H). + Qed. + +End Compare2EqBool. + +Module DSO_to_OT (O:DecStrOrder) <: OrderedType := + O <+ Compare2EqBool <+ HasEqBool2Dec. + +(** From [OrderedType] To [OrderedTypeFull] (adding [<=]) *) + +Module OT_to_Full (O:OrderedType') <: OrderedTypeFull. + Include O. + Definition le x y := x x-> Sortclass. +Hint Unfold is_true. + +Module Type HasLeBool (Import T:Typ). + Parameter Inline leb : t -> t -> bool. +End HasLeBool. + +Module Type HasLtBool (Import T:Typ). + Parameter Inline ltb : t -> t -> bool. +End HasLtBool. + +Module Type LeBool := Typ <+ HasLeBool. +Module Type LtBool := Typ <+ HasLtBool. + +Module Type LeBoolNotation (E:LeBool). + Infix "<=?" := E.leb (at level 35). +End LeBoolNotation. + +Module Type LtBoolNotation (E:LtBool). + Infix " Y.le x y. +End LeBool_Le. + +Module Type LtBool_Lt (T:Typ)(X:HasLtBool T)(Y:HasLt T). + Parameter ltb_lt : forall x y, X.ltb x y = true <-> Y.lt x y. +End LtBool_Lt. + +Module Type LeBoolIsTotal (Import X:LeBool'). + Axiom leb_total : forall x y, (x <=? y) = true \/ (y <=? x) = true. +End LeBoolIsTotal. + +Module Type TotalLeBool := LeBool <+ LeBoolIsTotal. +Module Type TotalLeBool' := LeBool' <+ LeBoolIsTotal. + +Module Type LeBoolIsTransitive (Import X:LeBool'). + Axiom leb_trans : Transitive X.leb. +End LeBoolIsTransitive. + +Module Type TotalTransitiveLeBool := TotalLeBool <+ LeBoolIsTransitive. +Module Type TotalTransitiveLeBool' := TotalLeBool' <+ LeBoolIsTransitive. + + +(** * From [OrderedTypeFull] to [TotalTransitiveLeBool] *) + +Module OTF_to_TTLB (Import O : OrderedTypeFull') <: TotalTransitiveLeBool. + + Definition leb x y := + match compare x y with Gt => false | _ => true end. + + Lemma leb_le : forall x y, leb x y <-> x <= y. + Proof. + intros. unfold leb. rewrite le_lteq. + destruct (compare_spec x y) as [EQ|LT|GT]; split; auto. + discriminate. + intros LE. elim (StrictOrder_Irreflexive x). + destruct LE as [LT|EQ]. now transitivity y. now rewrite <- EQ in GT. + Qed. + + Lemma leb_total : forall x y, leb x y \/ leb y x. + Proof. + intros. rewrite 2 leb_le. rewrite 2 le_lteq. + destruct (compare_spec x y); intuition. + Qed. + + Lemma leb_trans : Transitive leb. + Proof. + intros x y z. rewrite !leb_le, !le_lteq. + intros [Hxy|Hxy] [Hyz|Hyz]. + left; transitivity y; auto. + left; rewrite <- Hyz; auto. + left; rewrite Hxy; auto. + right; transitivity y; auto. + Qed. + + Definition t := t. + +End OTF_to_TTLB. + + +(** * From [TotalTransitiveLeBool] to [OrderedTypeFull] + + [le] is [leb ... = true]. + [eq] is [le /\ swap le]. + [lt] is [le /\ ~swap le]. +*) + +Local Open Scope bool_scope. + +Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull. + + Definition t := t. + + Definition le x y : Prop := x <=? y. + Definition eq x y : Prop := le x y /\ le y x. + Definition lt x y : Prop := le x y /\ ~le y x. + + Definition compare x y := + if x <=? y then (if y <=? x then Eq else Lt) else Gt. + + Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). + Proof. + intros. unfold compare. + case_eq (x <=? y). + case_eq (y <=? x). + constructor. split; auto. + constructor. split; congruence. + constructor. destruct (leb_total x y); split; congruence. + Qed. + + Definition eqb x y := (x <=? y) && (y <=? x). + + Lemma eqb_eq : forall x y, eqb x y <-> eq x y. + Proof. + intros. unfold eq, eqb, le. + case leb; simpl; intuition; discriminate. + Qed. + + Include HasEqBool2Dec. + + Instance eq_equiv : Equivalence eq. + Proof. + split. + intros x; unfold eq, le. destruct (leb_total x x); auto. + intros x y; unfold eq, le. intuition. + intros x y z; unfold eq, le. intuition; apply leb_trans with y; auto. + Qed. + + Instance lt_strorder : StrictOrder lt. + Proof. + split. + intros x. unfold lt; red; intuition. + intros x y z; unfold lt, le. intuition. + apply leb_trans with y; auto. + absurd (z <=? y); auto. + apply leb_trans with x; auto. + Qed. + + Instance lt_compat : Proper (eq ==> eq ==> iff) lt. + Proof. + apply proper_sym_impl_iff_2; auto with *. + intros x x' Hx y y' Hy' H. unfold eq, lt, le in *. + intuition. + apply leb_trans with x; auto. + apply leb_trans with y; auto. + absurd (y <=? x); auto. + apply leb_trans with x'; auto. + apply leb_trans with y'; auto. + Qed. + + Definition le_lteq : forall x y, le x y <-> lt x y \/ eq x y. + Proof. + intros. + unfold lt, eq, le. + split; [ | intuition ]. + intros LE. + case_eq (y <=? x); [right|left]; intuition; try discriminate. + Qed. + +End TTLB_to_OTF. diff --git a/theories/Structures/OrdersAlt.v b/theories/Structures/OrdersAlt.v new file mode 100644 index 00000000..d86b02a1 --- /dev/null +++ b/theories/Structures/OrdersAlt.v @@ -0,0 +1,242 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 Update_OT (O:OrderedTypeOrig) <: OrderedType. + + Include Update_DT O. (* Provides : t eq eq_equiv eq_dec *) + + Definition lt := O.lt. + + Instance lt_strorder : StrictOrder lt. + Proof. + split. + intros x Hx. apply (O.lt_not_eq Hx); auto with *. + exact O.lt_trans. + Qed. + + Instance lt_compat : Proper (eq==>eq==>iff) lt. + Proof. + apply proper_sym_impl_iff_2; auto with *. + intros x x' Hx y y' Hy H. + assert (H0 : lt x' y). + destruct (O.compare x' y) as [H'|H'|H']; auto. + elim (O.lt_not_eq H). transitivity x'; auto with *. + elim (O.lt_not_eq (O.lt_trans H H')); auto. + destruct (O.compare x' y') as [H'|H'|H']; auto. + elim (O.lt_not_eq H). + transitivity x'; auto with *. transitivity y'; auto with *. + elim (O.lt_not_eq (O.lt_trans H' H0)); auto with *. + Qed. + + Definition compare x y := + match O.compare x y with + | EQ _ => Eq + | LT _ => Lt + | GT _ => Gt + end. + + Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). + Proof. + intros; unfold compare; destruct O.compare; auto. + Qed. + +End Update_OT. + +(** ** From OrderedType to OrderedTypeOrig. *) + +Module Backport_OT (O:OrderedType) <: OrderedTypeOrig. + + Include Backport_DT O. (* Provides : t eq eq_refl eq_sym eq_trans eq_dec *) + + Definition lt := O.lt. + + 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 O.lt_strorder. Qed. + + Definition compare : forall x y, Compare lt eq x y. + Proof. + intros x y; destruct (CompSpec2Type (O.compare_spec x y)); + [apply EQ|apply LT|apply GT]; auto. + Defined. + +End Backport_OT. + + +(** ** From OrderedTypeAlt to OrderedType. *) + +Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType. + + 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, CompSpec eq lt x y (compare x y). + Proof. + unfold eq, lt, compare; intros. + destruct (O.compare x y) as [ ]_eqn:H; auto. + apply CompGt. + 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 OT_from_Alt. + +(** From the original presentation to this alternative one. *) + +Module OT_to_Alt (Import O:OrderedType) <: OrderedTypeAlt. + + 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. + 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. + 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; 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. + + Lemma compare_Lt : forall x y, compare x y = Lt <-> lt x y. + Proof. + unfold compare. + 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. + + Lemma compare_Gt : forall x y, compare x y = Gt <-> lt y x. + Proof. + intros x y. rewrite compare_sym, CompOpp_iff. apply compare_Lt. + 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 ?compare_Eq, ?compare_Lt, ?compare_Gt; + transitivity y; auto. + Qed. + +End OT_to_Alt. diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v new file mode 100644 index 00000000..56f1d5de --- /dev/null +++ b/theories/Structures/OrdersEx.v @@ -0,0 +1,88 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* eq==>iff) lt. + Proof. + compute. + intros (x1,x2) (x1',x2') (X1,X2) (y1,y2) (y1',y2') (Y1,Y2). + 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, CompSpec eq lt x y (compare x y). + Proof. + 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 with relations. + Qed. + +End PairOrderedType. + diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v new file mode 100644 index 00000000..a28b7977 --- /dev/null +++ b/theories/Structures/OrdersFacts.v @@ -0,0 +1,234 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* eq==>iff) le. + Proof. repeat red; iorder. Qed. + + Instance le_preorder : PreOrder le. + Proof. split; red; order. Qed. + + Instance le_order : PartialOrder eq le. + Proof. compute; iorder. Qed. + + Instance le_antisym : Antisymmetric _ eq le. + Proof. apply partial_order_antisym; auto with *. Qed. + + Lemma le_not_gt_iff : forall x y, x<=y <-> ~y ~y<=x. + Proof. iorder. Qed. + + Lemma le_or_gt : forall x y, x<=y \/ y x<=y /\ y<=x. + Proof. iorder. Qed. + +End OrderedTypeFullFacts. + + +(** * Properties of [OrderedType] *) + +Module OrderedTypeFacts (Import O: OrderedType'). + + Module OrderTac := OT_to_OrderTac O. + Ltac order := OrderTac.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 x 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 Lt <-> y<=x. + Proof. + intros; rewrite compare_lt_iff; intuition. + Qed. + + Lemma compare_le_iff : forall x y, (x ?= y) <> Gt <-> x<=y. + Proof. + intros; rewrite compare_gt_iff; intuition. + Qed. + + Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order. + + Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare. + Proof. + intros x x' Hxx' y y' Hyy'. + elim_compare x' y'; autorewrite with order; order. + Qed. + + Lemma compare_refl : forall x, (x ?= x) = Eq. + Proof. + intros; elim_compare x x; auto; order. + Qed. + + Lemma compare_antisym : forall x y, (y ?= x) = CompOpp (x ?= y). + Proof. + intros; elim_compare x y; simpl; autorewrite with order; order. + Qed. + + (** For compatibility reasons *) + Definition eq_dec := eq_dec. + + Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}. + Proof. + intros x y; destruct (CompSpec2Type (compare_spec 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. + +End OrderedTypeFacts. + + + + + + +(** * Tests of the order tactic + + Is it at least capable of proving some basic properties ? *) + +Module OrderedTypeTest (Import O:OrderedType'). + Module Import MO := OrderedTypeFacts O. + Local Open Scope order. + Lemma lt_not_eq x y : x ~x==y. Proof. order. Qed. + Lemma lt_eq x y z : x y==z -> x y x 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 x y<=z -> x 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==x. Proof. order. Qed. + Lemma lt_le x y : x x<=y. Proof. order. Qed. + Lemma gt_not_eq x y : y ~x==y. Proof. order. Qed. + Lemma eq_not_lt x y : x==y -> ~x ~ y ~ y ~xeq==>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, CompSpec eq lt x y (compare x y). +Proof. +intros; unfold compare, eq, lt, flip. +destruct (O.compare_spec y x); auto with relations. +Qed. + +End OrderedTypeRev. + diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v new file mode 100644 index 00000000..2ed07026 --- /dev/null +++ b/theories/Structures/OrdersLists.v @@ -0,0 +1,256 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 @@1. + Definition eqke : relation (key*elt) := eq * Logic.eq. + Definition ltk : relation (key*elt) := lt @@1. + + 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. + repeat red; reflexivity. + 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 with relations. + left; apply Sort_In_cons_1 with l; auto with relations. + 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 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/OrdersTac.v b/theories/Structures/OrdersTac.v new file mode 100644 index 00000000..66a672c9 --- /dev/null +++ b/theories/Structures/OrdersTac.v @@ -0,0 +1,293 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* le y z -> le x z]. +*) + +Inductive ord := OEQ | OLT | OLE. +Definition trans_ord o o' := + match o, o' with + | OEQ, _ => o' + | _, OEQ => o + | OLE, OLE => OLE + | _, _ => OLT + end. +Local Infix "+" := trans_ord. + + +(** ** The requirements of the tactic : [TotalOrder]. + + [TotalOrder] contains an equivalence [eq], + a strict order [lt] total and compatible with [eq], and + a larger order [le] synonym for [lt\/eq]. +*) + +(** ** Properties that will be used by the [order] tactic *) + +Module OrderFacts(Import O:TotalOrder'). + +(** Reflexivity rules *) + +Lemma eq_refl : forall x, x==x. +Proof. reflexivity. Qed. + +Lemma le_refl : forall x, x<=x. +Proof. intros; rewrite le_lteq; right; reflexivity. Qed. + +Lemma lt_irrefl : forall x, ~ x y==x. +Proof. auto with *. Qed. + +Lemma le_antisym : forall x y, x<=y -> y<=x -> x==y. +Proof. + intros x y; rewrite 2 le_lteq. intuition. + elim (StrictOrder_Irreflexive x); transitivity y; auto. +Qed. + +Lemma neq_sym : forall x y, ~x==y -> ~y==x. +Proof. auto using eq_sym. Qed. + +(** Transitivity rules : first, a generic formulation, then instances*) + +Ltac subst_eqns := + match goal with + | H : _==_ |- _ => (rewrite H || rewrite <- H); clear H; subst_eqns + | _ => idtac + end. + +Definition interp_ord o := + match o with OEQ => O.eq | OLT => O.lt | OLE => O.le end. +Local Notation "#" := interp_ord. + +Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z. +Proof. +destruct o, o'; simpl; intros x y z; rewrite ?le_lteq; intuition; + subst_eqns; eauto using (StrictOrder_Transitive x y z) with *. +Qed. + +Definition eq_trans x y z : x==y -> y==z -> x==z := @trans OEQ OEQ x y z. +Definition le_trans x y z : x<=y -> y<=z -> x<=z := @trans OLE OLE x y z. +Definition lt_trans x y z : x y x y x y<=z -> x y x y==z -> x y<=z -> x<=z := @trans OEQ OLE x y z. +Definition le_eq x y z : x<=y -> y==z -> x<=z := @trans OLE OEQ x y z. + +Lemma eq_neq : forall x y z, x==y -> ~y==z -> ~x==z. +Proof. eauto using eq_trans, eq_sym. Qed. + +Lemma neq_eq : forall x y z, ~x==y -> y==z -> ~x==z. +Proof. eauto using eq_trans, eq_sym. Qed. + +(** (double) negation rules *) + +Lemma not_neq_eq : forall x y, ~~x==y -> x==y. +Proof. +intros x y H. destruct (lt_total x y) as [H'|[H'|H']]; auto; + destruct H; intro H; rewrite H in H'; eapply lt_irrefl; eauto. +Qed. + +Lemma not_ge_lt : forall x y, ~y<=x -> x x<=y. +Proof. +intros x y H. rewrite le_lteq. generalize (lt_total x y); intuition. +Qed. + +Lemma le_neq_lt : forall x y, x<=y -> ~x==y -> x