diff options
Diffstat (limited to 'theories/Structures/OrderedType2.v')
| -rw-r--r-- | theories/Structures/OrderedType2.v | 518 |
1 files changed, 44 insertions, 474 deletions
diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v index 16da2162d..4d62c2716 100644 --- a/theories/Structures/OrderedType2.v +++ b/theories/Structures/OrderedType2.v @@ -8,18 +8,19 @@ (* $Id$ *) -Require Export SetoidList DecidableType2 OrderTac. +Require Export Relations Morphisms Setoid DecidableType2. Set Implicit Arguments. Unset Strict Implicit. (** * Ordered types *) -Definition Cmp (A:Type)(eq lt : relation A) c := - match c with - | Eq => eq - | Lt => lt - | Gt => flip lt - end. +Inductive Cmp {A} (eq lt:relation A)(x y : A) : comparison -> Prop := +| Cmp_eq : eq x y -> Cmp eq lt x y Eq +| Cmp_lt : lt x y -> Cmp eq lt x y Lt +| Cmp_gt : lt y x -> Cmp eq lt x y Gt. + +Hint Constructors Cmp. + Module Type MiniOrderedType. Include Type EqualityType. @@ -29,10 +30,11 @@ Module Type MiniOrderedType. Instance lt_compat : Proper (eq==>eq==>iff) lt. Parameter compare : t -> t -> comparison. - Axiom compare_spec : forall x y, Cmp eq lt (compare x y) x y. + Axiom compare_spec : forall x y, Cmp eq lt x y (compare x y). End MiniOrderedType. + Module Type OrderedType. Include Type MiniOrderedType. @@ -42,492 +44,60 @@ Module Type OrderedType. End OrderedType. + Module MOT_to_OT (Import O : MiniOrderedType) <: OrderedType. Include O. Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}. Proof. intros. - generalize (compare_spec x y); destruct (compare x y); - unfold Cmp, flip; intros. - left; auto. - right. intro H'; rewrite <- H' in H. - apply (StrictOrder_Irreflexive x); auto. - right. intro H'; rewrite <- H' in H. - apply (StrictOrder_Irreflexive x); auto. + assert (H:=compare_spec x y); destruct (compare x y). + left; inversion_clear H; auto. + right; inversion_clear H. intro H'. rewrite H' in *. + apply (StrictOrder_Irreflexive y); auto. + right; inversion_clear H. intro H'. rewrite H' in *. + apply (StrictOrder_Irreflexive y); auto. Defined. End MOT_to_OT. -(** * Ordered types properties *) - -(** Additional properties that can be derived from signature - [OrderedType]. *) - -Module OrderedTypeFacts (Import O: OrderedType). - - Infix "==" := eq (at level 70, no associativity) : order. - Infix "<" := lt : order. - Notation "x <= y" := (~lt y x) : order. - Infix "?=" := compare (at level 70, no associativity) : order. - - Local Open Scope order. - - Ltac elim_compare x y := - generalize (compare_spec x y); destruct (compare x y); - unfold Cmp, flip. - - Module OrderElts : OrderTacSig - with Definition t := t - with Definition eq := eq - with Definition lt := lt. - (* Opaque signature is crucial for ltac to work correctly later *) - Include O. - Definition le x y := x<y \/ x==y. - Lemma lt_total : forall x y, x<y \/ x==y \/ y<x. - Proof. intros; elim_compare x y; intuition. Qed. - Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y. - Proof. unfold le; intuition. Qed. - End OrderElts. - Module OrderTac := MakeOrderTac OrderElts. - - Ltac order := - change eq with OrderElts.eq in *; - change lt with OrderElts.lt in *; - OrderTac.order. - - (** The following lemmas are either re-phrasing of [eq_equiv] and - [lt_strorder] or immediately provable by [order]. Interest: - compatibility, test of order, etc *) - - Definition eq_refl (x:t) : x==x := Equivalence_Reflexive x. - - Definition eq_sym (x y:t) : x==y -> y==x := Equivalence_Symmetric x y. - - Definition eq_trans (x y z:t) : x==y -> y==z -> x==z := - Equivalence_Transitive x y z. - - Definition lt_trans (x y z:t) : x<y -> y<z -> x<z := - StrictOrder_Transitive x y z. - - Definition lt_irrefl (x:t) : ~x<x := StrictOrder_Irreflexive x. - - (** Some more about [compare] *) - - Lemma compare_eq_iff : forall x y, (x ?= y) = Eq <-> x==y. - Proof. - intros; elim_compare x y; intuition; try discriminate; order. - Qed. - - Lemma compare_lt_iff : forall x y, (x ?= y) = Lt <-> x<y. - Proof. - intros; elim_compare x y; intuition; try discriminate; order. - Qed. - - Lemma compare_gt_iff : forall x y, (x ?= y) = Gt <-> y<x. - Proof. - intros; elim_compare x y; intuition; try discriminate; order. - Qed. - - Lemma compare_ge_iff : forall x y, (x ?= y) <> Lt <-> y<=x. - Proof. - intros; rewrite compare_lt_iff; intuition. - Qed. - - Lemma compare_le_iff : forall x y, (x ?= y) <> Gt <-> x<=y. - Proof. - intros; rewrite compare_gt_iff; intuition. - Qed. - - Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order. - - Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare. - Proof. - intros x x' Hxx' y y' Hyy'. - elim_compare x' y'; intros; autorewrite with order; order. - Qed. - - Lemma compare_refl : forall x, (x ?= x) = Eq. - Proof. - intros; elim_compare x x; auto; order. - Qed. - - Lemma compare_antisym : forall x y, (y ?= x) = CompOpp (x ?= y). - Proof. - intros; elim_compare x y; simpl; intros; autorewrite with order; order. - Qed. - - (** For compatibility reasons *) - Definition eq_dec := eq_dec. - - Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}. - Proof. - intros; elim_compare x y; [ right | left | right ]; order. - Defined. - - Definition eqb x y : bool := if eq_dec x y then true else false. - - Lemma if_eq_dec : forall x y (B:Type)(b b':B), - (if eq_dec x y then b else b') = - (match compare x y with Eq => b | _ => b' end). - Proof. - intros; destruct eq_dec; elim_compare x y; auto; order. - Qed. - - Lemma eqb_alt : - forall x y, eqb x y = match compare x y with Eq => true | _ => false end. - Proof. - unfold eqb; intros; apply if_eq_dec. - Qed. - - Instance eqb_compat : Proper (eq==>eq==>Logic.eq) eqb. - Proof. - intros x x' Hxx' y y' Hyy'. - rewrite 2 eqb_alt, Hxx', Hyy'; auto. - Qed. - - -(* Specialization of resuts about lists modulo. *) - -Section ForNotations. - -Notation In:=(InA eq). -Notation Inf:=(lelistA lt). -Notation Sort:=(sort lt). -Notation NoDup:=(NoDupA eq). - -Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. -Proof. intros. rewrite <- H; auto. Qed. - -Lemma ListIn_In : forall l x, List.In x l -> In x l. -Proof. exact (In_InA eq_equiv). Qed. - -Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l. -Proof. exact (InfA_ltA lt_strorder). Qed. - -Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l. -Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed. - -Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x. -Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed. - -Lemma ListIn_Inf : forall l x, (forall y, List.In y l -> lt x y) -> Inf x l. -Proof. exact (@In_InfA t lt). Qed. - -Lemma In_Inf : forall l x, (forall y, In y l -> lt x y) -> Inf x l. -Proof. exact (InA_InfA eq_equiv (ltA:=lt)). Qed. - -Lemma Inf_alt : - forall l x, Sort l -> (Inf x l <-> (forall y, In y l -> lt x y)). -Proof. exact (InfA_alt eq_equiv lt_strorder lt_compat). Qed. - -Lemma Sort_NoDup : forall l, Sort l -> NoDup l. -Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat) . Qed. - -End ForNotations. - -Hint Resolve ListIn_In Sort_NoDup Inf_lt. -Hint Immediate In_eq Inf_lt. - -End OrderedTypeFacts. - - -(** Some tests of [order] : is it at least capable of - proving some basic properties ? *) -Module OrderedTypeTest (O:OrderedType). - Module Import MO := OrderedTypeFacts O. - Local Open Scope order. - Lemma lt_not_eq x y : x<y -> ~x==y. Proof. order. Qed. - Lemma lt_eq x y z : x<y -> y==z -> x<z. Proof. order. Qed. - Lemma eq_lt x y z : x==y -> y<z -> x<z. Proof. order. Qed. - Lemma le_eq x y z : x<=y -> y==z -> x<=z. Proof. order. Qed. - Lemma eq_le x y z : x==y -> y<=z -> x<=z. Proof. order. Qed. - Lemma neq_eq x y z : ~x==y -> y==z -> ~x==z. Proof. order. Qed. - Lemma eq_neq x y z : x==y -> ~y==z -> ~x==z. Proof. order. Qed. - Lemma le_lt_trans x y z : x<=y -> y<z -> x<z. Proof. order. Qed. - Lemma lt_le_trans x y z : x<y -> y<=z -> x<z. Proof. order. Qed. - Lemma le_trans x y z : x<=y -> y<=z -> x<=z. Proof. order. Qed. - Lemma le_antisym x y : x<=y -> y<=x -> x==y. Proof. order. Qed. - Lemma le_neq x y : x<=y -> ~x==y -> x<y. Proof. order. Qed. - Lemma neq_sym x y : ~x==y -> ~y==x. Proof. order. Qed. - Lemma lt_le x y : x<y -> x<=y. Proof. order. Qed. - Lemma gt_not_eq x y : y<x -> ~x==y. Proof. order. Qed. - Lemma eq_not_lt x y : x==y -> ~x<y. Proof. order. Qed. - Lemma eq_not_gt x y : x==y -> ~ y<x. Proof. order. Qed. - Lemma lt_not_gt x y : x<y -> ~ y<x. Proof. order. Qed. -End OrderedTypeTest. +(** * UsualOrderedType + A particular case of [OrderedType] where the equality is + the usual one of Coq. *) -(** * Relations over pairs (TO MIGRATE in some TypeClasses file) *) +Module Type UsualOrderedType. + Include Type UsualDecidableType. -Definition ProdRel {A B}(RA:relation A)(RB:relation B) : relation (A*B) := - fun p p' => RA (fst p) (fst p') /\ RB (snd p) (snd p'). + Parameter Inline lt : t -> t -> Prop. + Instance lt_strorder : StrictOrder lt. + (* The following is useless since eq is Leibniz, but should be there + for subtyping... *) + Instance lt_compat : Proper (eq==>eq==>iff) lt. -Definition FstRel {A B}(R:relation A) : relation (A*B) := - fun p p' => R (fst p) (fst p'). + Parameter compare : t -> t -> comparison. + Axiom compare_spec : forall x y, Cmp eq lt x y (compare x y). -Definition SndRel {A B}(R:relation B) : relation (A*B) := - fun p p' => R (snd p) (snd p'). +End UsualOrderedType. -Generalizable Variables A B RA RB Ri Ro. +(** a [UsualOrderedType] is in particular an [OrderedType]. *) -Instance ProdRel_equiv {A B} `(Equivalence A RA)`(Equivalence B RB) : - Equivalence (ProdRel RA RB). -Proof. firstorder. Qed. +Module UOT_to_OT (U:UsualOrderedType) <: OrderedType := U. -Instance FstRel_equiv {A B} `(Equivalence A RA) : - Equivalence (FstRel RA (B:=B)). -Proof. firstorder. Qed. -Instance SndRel_equiv {A B} `(Equivalence B RB) : - Equivalence (SndRel RB (A:=A)). -Proof. firstorder. Qed. +(** * OrderedType with also a [<=] predicate *) -Instance FstRel_strorder {A B} `(StrictOrder A RA) : - StrictOrder (FstRel RA (B:=B)). -Proof. firstorder. Qed. +Module Type OrderedTypeFull. + Include Type OrderedType. + Parameter Inline le : t -> t -> Prop. + Axiom le_lteq : forall x y, le x y <-> lt x y \/ eq x y. +End OrderedTypeFull. -Instance SndRel_strorder {A B} `(StrictOrder B RB) : - StrictOrder (SndRel RB (A:=A)). -Proof. firstorder. Qed. - -Lemma FstRel_ProdRel {A B}(RA:relation A) : forall p p':A*B, - (FstRel RA) p p' <-> (ProdRel RA (fun _ _ =>True)) p p'. -Proof. firstorder. Qed. - -Lemma SndRel_ProdRel {A B}(RB:relation B) : forall p p':A*B, - (SndRel RB) p p' <-> (ProdRel (fun _ _ =>True) RB) p p'. -Proof. firstorder. Qed. - -Lemma ProdRel_alt {A B}(RA:relation A)(RB:relation B) : forall p p':A*B, - (ProdRel RA RB) p p' <-> relation_conjunction (FstRel RA) (SndRel RB) p p'. -Proof. firstorder. Qed. - -Instance FstRel_compat {A B} (R : relation A)`(Proper _ (Ri==>Ri==>Ro) R) : - Proper (FstRel Ri==>FstRel Ri==>Ro) (FstRel R (B:=B)). -Proof. - intros A B R Ri Ro H (a1,b1) (a1',b1') Hab1 (a2,b2) (a2',b2') Hab2. - unfold FstRel in *; simpl in *. apply H; auto. -Qed. - -Instance SndRel_compat {A B} (R : relation B)`(Proper _ (Ri==>Ri==>Ro) R) : - Proper (SndRel Ri==>SndRel Ri==>Ro) (SndRel R (A:=A)). -Proof. - intros A B R Ri Ro H (a1,b1) (a1',b1') Hab1 (a2,b2) (a2',b2') Hab2. - unfold SndRel in *; simpl in *. apply H; auto. -Qed. - -Instance FstRel_sub {A B} (RA:relation A)(RB:relation B): - subrelation (ProdRel RA RB) (FstRel RA). -Proof. firstorder. Qed. - -Instance SndRel_sub {A B} (RA:relation A)(RB:relation B): - subrelation (ProdRel RA RB) (SndRel RB). -Proof. firstorder. Qed. - -Instance pair_compat { A B } (RA:relation A)(RB : relation B) : - Proper (RA==>RB==>ProdRel RA RB) (@pair A B). -Proof. firstorder. Qed. - - -Hint Unfold ProdRel FstRel SndRel. -Hint Extern 2 (ProdRel _ _ _ _) => split. - - -Module KeyOrderedType(Import O:OrderedType). - Module Import MO:=OrderedTypeFacts(O). - - Section Elt. - Variable elt : Type. - Notation key:=t. - - Definition eqk : relation (key*elt) := FstRel eq. - Definition eqke : relation (key*elt) := ProdRel eq Logic.eq. - Definition ltk : relation (key*elt) := FstRel lt. - - Hint Unfold eqk eqke ltk. - - (* eqke is stricter than eqk *) - - Global Instance eqke_eqk : subrelation eqke eqk. - Proof. unfold eqke, eqk; auto with *. Qed. - - (* eqk, eqke are equalities, ltk is a strict order *) - - Global Instance eqk_equiv : Equivalence eqk. - - Global Instance eqke_equiv : Equivalence eqke. - - Global Instance ltk_strorder : StrictOrder ltk. - - Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk. - Proof. unfold eqk, ltk; auto with *. Qed. - - (* Additionnal facts *) - - Global Instance pair_compat : Proper (eq==>Logic.eq==>eqke) (@pair key elt). - Proof. unfold eqke; auto with *. Qed. - - Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'. - Proof. - intros e e' LT EQ; rewrite EQ in LT. - elim (StrictOrder_Irreflexive _ LT). - Qed. - - Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'. - Proof. - intros e e' LT EQ; rewrite EQ in LT. - elim (StrictOrder_Irreflexive _ LT). - Qed. - - Lemma InA_eqke_eqk : - forall x m, InA eqke x m -> InA eqk x m. - Proof. - unfold eqke, ProdRel; induction 1; intuition. - Qed. - Hint Resolve InA_eqke_eqk. - - Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). - Definition In k m := exists e:elt, MapsTo k e m. - Notation Sort := (sort ltk). - Notation Inf := (lelistA ltk). - - Hint Unfold MapsTo In. - - (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) - - Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. - Proof. - firstorder. - exists x; auto. - induction H. - destruct y; compute in H. - exists e; auto. - destruct IHInA as [e H0]. - exists e; auto. - Qed. - - Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l. - Proof. - unfold In, MapsTo. - setoid_rewrite Exists_exists; setoid_rewrite InA_alt. - firstorder. - exists (snd x), x; auto. - Qed. - - Lemma In_nil : forall k, In k nil <-> False. - Proof. - intros; rewrite In_alt2; apply Exists_nil. - Qed. - - Lemma In_cons : forall k p l, - In k (p::l) <-> eq k (fst p) \/ In k l. - Proof. - intros; rewrite !In_alt2, Exists_cons; intuition. - Qed. - - Global Instance MapsTo_compat : - Proper (eq==>Logic.eq==>equivlistA eqke==>iff) MapsTo. - Proof. - intros x x' Hx e e' He l l' Hl. unfold MapsTo. - rewrite Hx, He, Hl; intuition. - Qed. - - Global Instance In_compat : Proper (eq==>equivlistA eqk==>iff) In. - Proof. - intros x x' Hx l l' Hl. rewrite !In_alt. - setoid_rewrite Hl. setoid_rewrite Hx. intuition. - Qed. - - Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. - Proof. intros l x y e EQ. rewrite <- EQ; auto. Qed. - - Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. - Proof. intros l x y EQ. rewrite <- EQ; auto. Qed. - - Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l. - Proof. intros l x x' H. rewrite H; auto. Qed. - - Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l. - Proof. apply InfA_ltA; auto with *. Qed. - - Hint Immediate Inf_eq. - Hint Resolve Inf_lt. - - Lemma Sort_Inf_In : - forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p. - Proof. apply SortA_InfA_InA; auto with *. Qed. - - Lemma Sort_Inf_NotIn : - forall l k e, Sort l -> Inf (k,e) l -> ~In k l. - Proof. - intros; red; intros. - destruct H1 as [e' H2]. - elim (@ltk_not_eqk (k,e) (k,e')). - eapply Sort_Inf_In; eauto. - red; simpl; auto. - Qed. - - Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l. - Proof. apply SortA_NoDupA; auto with *. Qed. - - Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'. - Proof. - intros; invlist sort; eapply Sort_Inf_In; eauto. - Qed. - - Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) -> - ltk e e' \/ eqk e e'. - Proof. - intros; invlist InA; auto. - left; apply Sort_In_cons_1 with l; auto. - Qed. - - Lemma Sort_In_cons_3 : - forall x l k e, Sort ((k,e)::l) -> In x l -> ~eq x k. - Proof. - intros; invlist sort; red; intros. - eapply Sort_Inf_NotIn; eauto using In_eq. - Qed. - - Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. - Proof. - intros; invlist In; invlist MapsTo. compute in * |- ; intuition. - right; exists x; auto. - Qed. - - Lemma In_inv_2 : forall k k' e e' l, - InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l. - Proof. - intros; invlist InA; intuition. - Qed. - - Lemma In_inv_3 : forall x x' l, - InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l. - Proof. - intros; invlist InA; compute in * |- ; intuition. - Qed. - - End Elt. - - Hint Resolve (fun elt => @Equivalence_Reflexive _ _ (eqk_equiv elt)). - Hint Resolve (fun elt => @Equivalence_Transitive _ _ (eqk_equiv elt)). - Hint Immediate (fun elt => @Equivalence_Symmetric _ _ (eqk_equiv elt)). - Hint Resolve (fun elt => @Equivalence_Reflexive _ _ (eqke_equiv elt)). - Hint Resolve (fun elt => @Equivalence_Transitive _ _ (eqke_equiv elt)). - Hint Immediate (fun elt => @Equivalence_Symmetric _ _ (eqke_equiv elt)). - Hint Resolve (fun elt => @StrictOrder_Transitive _ _ (ltk_strorder elt)). - - Hint Unfold eqk eqke ltk. - Hint Extern 2 (eqke ?a ?b) => split. - Hint Resolve ltk_not_eqk ltk_not_eqke. - Hint Resolve InA_eqke_eqk. - Hint Unfold MapsTo In. - Hint Immediate Inf_eq. - Hint Resolve Inf_lt. - Hint Resolve Sort_Inf_NotIn. - Hint Resolve In_inv_2 In_inv_3. - -End KeyOrderedType. +Module OT_to_Full (O:OrderedType) <: OrderedTypeFull. + Include O. + Definition le x y := lt x y \/ eq x y. + Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y. + Proof. unfold le; split; auto. Qed. +End OT_to_Full. |