diff options
Diffstat (limited to 'theories/Structures')
-rw-r--r-- | theories/Structures/EqualitiesFacts.v | 216 | ||||
-rw-r--r-- | theories/Structures/OrdersEx.v | 67 | ||||
-rw-r--r-- | theories/Structures/OrdersLists.v | 211 |
3 files changed, 250 insertions, 244 deletions
diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v index 11d94c11..8e2b2d08 100644 --- a/theories/Structures/EqualitiesFacts.v +++ b/theories/Structures/EqualitiesFacts.v @@ -8,132 +8,172 @@ Require Import Equalities Bool SetoidList RelationPairs. -(** * Keys and datas used in FMap *) +Set Implicit Arguments. -Module KeyDecidableType(Import D:DecidableType). +(** * Keys and datas used in MMap *) - Section Elt. - Variable elt : Type. - Notation key:=t. +Module KeyDecidableType(D:DecidableType). - Local Open Scope signature_scope. + Local Open Scope signature_scope. + Local Notation key := D.t. - Definition eqk : relation (key*elt) := eq @@1. - Definition eqke : relation (key*elt) := eq * Logic.eq. - Hint Unfold eqk eqke. + Definition eqk {elt} : relation (key*elt) := D.eq @@1. + Definition eqke {elt} : relation (key*elt) := D.eq * Logic.eq. - (* eqke is stricter than eqk *) + Hint Unfold eqk eqke. - Global Instance eqke_eqk : subrelation eqke eqk. - Proof. firstorder. Qed. + (** eqk, eqke are equalities *) - (* eqk, eqke are equalities, ltk is a strict order *) + Instance eqk_equiv {elt} : Equivalence (@eqk elt) := _. - Global Instance eqk_equiv : Equivalence eqk := _. + Instance eqke_equiv {elt} : Equivalence (@eqke elt) := _. - Global Instance eqke_equiv : Equivalence eqke := _. + (** eqke is stricter than eqk *) - (* Additionnal facts *) + Instance eqke_eqk {elt} : subrelation (@eqke elt) (@eqk elt). + Proof. firstorder. 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. + (** Alternative definitions of eqke and 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. + Lemma eqke_def {elt} k k' (e e':elt) : + eqke (k,e) (k',e') = (D.eq k k' /\ e = e'). + Proof. reflexivity. Defined. - Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). - Definition In k m := exists e:elt, MapsTo k e m. + Lemma eqke_def' {elt} (p q:key*elt) : + eqke p q = (D.eq (fst p) (fst q) /\ snd p = snd q). + Proof. reflexivity. Defined. - Hint Unfold MapsTo In. + Lemma eqke_1 {elt} k k' (e e':elt) : eqke (k,e) (k',e') -> D.eq k k'. + Proof. now destruct 1. Qed. - (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) + Lemma eqke_2 {elt} k k' (e e':elt) : eqke (k,e) (k',e') -> e=e'. + Proof. now destruct 1. Qed. - 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. + Lemma eqk_def {elt} k k' (e e':elt) : eqk (k,e) (k',e') = D.eq k k'. + Proof. reflexivity. Defined. + + Lemma eqk_def' {elt} (p q:key*elt) : eqk p q = D.eq (fst p) (fst q). + Proof. reflexivity. Qed. + + Lemma eqk_1 {elt} k k' (e e':elt) : eqk (k,e) (k',e') -> D.eq k k'. + Proof. trivial. Qed. + + Hint Resolve eqke_1 eqke_2 eqk_1. + + (* Additionnal facts *) + + Lemma InA_eqke_eqk {elt} p (m:list (key*elt)) : + InA eqke p m -> InA eqk p m. + Proof. + induction 1; firstorder. + Qed. + Hint Resolve InA_eqke_eqk. + + Lemma InA_eqk_eqke {elt} p (m:list (key*elt)) : + InA eqk p m -> exists q, eqk p q /\ InA eqke q m. + Proof. + induction 1; firstorder. + Qed. + + Lemma InA_eqk {elt} p q (m:list (key*elt)) : + eqk p q -> InA eqk p m -> InA eqk q m. + Proof. + now intros <-. + Qed. + + Definition MapsTo {elt} (k:key)(e:elt):= InA eqke (k,e). + Definition In {elt} k m := exists e:elt, MapsTo k e m. + + Hint Unfold MapsTo In. + + (* Alternative formulations for [In k l] *) + + Lemma In_alt {elt} k (l:list (key*elt)) : + In k l <-> exists e, InA eqk (k,e) l. + Proof. + unfold In, MapsTo. + split; intros (e,H). + - exists e; auto. + - apply InA_eqk_eqke in H. destruct H as ((k',e'),(E,H)). + compute in E. exists e'. now rewrite E. + Qed. + + Lemma In_alt' {elt} (l:list (key*elt)) k e : + In k l <-> InA eqk (k,e) l. + Proof. + rewrite In_alt. firstorder. eapply InA_eqk; eauto. now compute. + Qed. + + Lemma In_alt2 {elt} k (l:list (key*elt)) : + In k l <-> Exists (fun p => D.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. + Qed. + + Lemma In_nil {elt} k : In k (@nil (key*elt)) <-> False. + Proof. + rewrite In_alt2; apply Exists_nil. + Qed. + + Lemma In_cons {elt} k p (l:list (key*elt)) : + In k (p::l) <-> D.eq k (fst p) \/ In k l. + Proof. + rewrite !In_alt2, Exists_cons; intuition. + Qed. + + Instance MapsTo_compat {elt} : + Proper (D.eq==>Logic.eq==>equivlistA eqke==>iff) (@MapsTo elt). + Proof. intros x x' Hx e e' He l l' Hl. unfold MapsTo. rewrite Hx, He, Hl; intuition. - Qed. + Qed. - Global Instance In_compat : Proper (eq==>equivlistA eqk==>iff) In. - Proof. + Instance In_compat {elt} : Proper (D.eq==>equivlistA eqk==>iff) (@In elt). + 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. + 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 MapsTo_eq {elt} (l:list (key*elt)) x y e : + D.eq x y -> MapsTo x e l -> MapsTo y e l. + Proof. now intros <-. 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_eq {elt} (l:list (key*elt)) x y : + D.eq x y -> In x l -> In y l. + Proof. now intros <-. 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 {elt} k k' e (l:list (key*elt)) : + In k ((k',e) :: l) -> D.eq k k' \/ In k l. + Proof. + intros (e',H). red in H. rewrite InA_cons, eqke_def in H. + intuition. right. now exists e'. + 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. + Lemma In_inv_2 {elt} k k' e e' (l:list (key*elt)) : + InA eqk (k, e) ((k', e') :: l) -> ~ D.eq k k' -> InA eqk (k, e) l. + Proof. + rewrite InA_cons, eqk_def. intuition. + Qed. - End Elt. + Lemma In_inv_3 {elt} x x' (l:list (key*elt)) : + InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l. + Proof. + rewrite InA_cons. destruct 1 as [H|H]; trivial. destruct 1. + eauto with *. + Qed. - 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 - +(** * PairDecidableType + From two decidable types, we can build a new DecidableType over their cartesian product. *) diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v index acc7c767..b484257b 100644 --- a/theories/Structures/OrdersEx.v +++ b/theories/Structures/OrdersEx.v @@ -84,3 +84,70 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. 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 MSetPositive and MMapPositive. *) + +Local Open Scope positive. + +Module PositiveOrderedTypeBits <: UsualOrderedType. + Definition t:=positive. + Include HasUsualEq <+ UsualIsEq. + Definition eqb := Pos.eqb. + Definition eqb_eq := Pos.eqb_eq. + Include HasEqBool2Dec. + + 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_antirefl : forall x : positive, ~ bits_lt x x. + Proof. + induction x; simpl; auto. + Qed. + + Lemma bits_lt_trans : + forall x y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z. + Proof. + induction x; destruct y,z; simpl; eauto; intuition. + Qed. + + Instance lt_compat : Proper (eq==>eq==>iff) lt. + Proof. + intros x x' Hx y y' Hy. rewrite Hx, Hy; intuition. + Qed. + + Instance lt_strorder : StrictOrder lt. + Proof. + split; [ exact bits_lt_antirefl | exact bits_lt_trans ]. + Qed. + + Fixpoint compare x y := + match x, y with + | x~1, y~1 => compare x y + | x~1, _ => Gt + | x~0, y~0 => compare x y + | x~0, _ => Lt + | 1, y~1 => Lt + | 1, 1 => Eq + | 1, y~0 => Gt + end. + + Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). + Proof. + unfold eq, lt. + induction x; destruct y; try constructor; simpl; auto. + destruct (IHx y); subst; auto. + destruct (IHx y); subst; auto. + Qed. + +End PositiveOrderedTypeBits. diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v index 059992f5..4d49ac84 100644 --- a/theories/Structures/OrdersLists.v +++ b/theories/Structures/OrdersLists.v @@ -6,51 +6,47 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -Require Export RelationPairs SetoidList Orders. +Require Export RelationPairs SetoidList Orders EqualitiesFacts. Set Implicit Arguments. Unset Strict Implicit. (** * Specialization of results about lists modulo. *) -Module OrderedTypeLists (Import O:OrderedType). +Module OrderedTypeLists (O:OrderedType). -Section ForNotations. - -Notation In:=(InA eq). -Notation Inf:=(lelistA lt). -Notation Sort:=(sort lt). -Notation NoDup:=(NoDupA eq). +Local Notation In:=(InA O.eq). +Local Notation Inf:=(lelistA O.lt). +Local Notation Sort:=(sort O.lt). +Local Notation NoDup:=(NoDupA O.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. +Proof. exact (In_InA O.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_lt : forall l x y, O.lt x y -> Inf y l -> Inf x l. +Proof. exact (InfA_ltA O.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_compat). Qed. +Lemma Inf_eq : forall l x y, O.eq x y -> Inf y l -> Inf x l. +Proof. exact (InfA_eqA O.eq_equiv O.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 Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> O.lt a x. +Proof. exact (SortA_InfA_InA O.eq_equiv O.lt_strorder O.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 ListIn_Inf : forall l x, (forall y, List.In y l -> O.lt x y) -> Inf x l. +Proof. exact (@In_InfA O.t O.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 In_Inf : forall l x, (forall y, In y l -> O.lt x y) -> Inf x l. +Proof. exact (InA_InfA O.eq_equiv (ltA:=O.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. + forall l x, Sort l -> (Inf x l <-> (forall y, In y l -> O.lt x y)). +Proof. exact (InfA_alt O.eq_equiv O.lt_strorder O.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. +Proof. exact (SortA_NoDupA O.eq_equiv O.lt_strorder O.lt_compat) . Qed. Hint Resolve ListIn_In Sort_NoDup Inf_lt. Hint Immediate In_eq Inf_lt. @@ -58,140 +54,66 @@ Hint Immediate In_eq Inf_lt. End OrderedTypeLists. +(** * Results about keys and data as manipulated in MMaps. *) +Module KeyOrderedType(O:OrderedType). + Include KeyDecidableType(O). (* provides eqk, eqke *) + Local Notation key:=O.t. + Local Open Scope signature_scope. -(** * 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. + Definition ltk {elt} : relation (key*elt) := O.lt @@1. - (* eqke is stricter than eqk *) + Hint Unfold ltk. - Global Instance eqke_eqk : subrelation eqke eqk. - Proof. firstorder. Qed. + (* ltk is a strict order *) - (* eqk, eqke are equalities, ltk is a strict order *) + Instance ltk_strorder {elt} : StrictOrder (@ltk elt) := _. - Global Instance eqk_equiv : Equivalence eqk := _. + Instance ltk_compat {elt} : Proper (eqk==>eqk==>iff) (@ltk elt). + Proof. unfold eqk, ltk; auto with *. Qed. - Global Instance eqke_equiv : Equivalence eqke := _. + Instance ltk_compat' {elt} : Proper (eqke==>eqke==>iff) (@ltk elt). + Proof. eapply subrelation_proper; eauto with *. Qed. - Global Instance ltk_strorder : StrictOrder ltk := _. + (* Additionnal facts *) - Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk. - Proof. unfold eqk, ltk; auto with *. Qed. + Instance pair_compat {elt} : Proper (O.eq==>Logic.eq==>eqke) (@pair key elt). + Proof. apply pair_compat. Qed. - (* Additionnal facts *) - - Global Instance pair_compat : Proper (eq==>Logic.eq==>eqke) (@pair key elt). - Proof. apply pair_compat. Qed. + Section Elt. + Variable elt : Type. + Implicit Type p q : key*elt. + Implicit Type l m : list (key*elt). - Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'. + Lemma ltk_not_eqk p q : ltk p q -> ~ eqk p q. Proof. - intros e e' LT EQ; rewrite EQ in LT. + intros LT EQ; rewrite EQ in LT. elim (StrictOrder_Irreflexive _ LT). Qed. - Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'. + Lemma ltk_not_eqke p q : ltk p q -> ~eqke p q. Proof. - intros e e' LT EQ; rewrite EQ in LT. + intros 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 Inf_eq l x x' : eqk x x' -> Inf x' l -> Inf x l. + Proof. now intros <-. 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. + Lemma Inf_lt 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. + Lemma Sort_Inf_In 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. + Lemma Sort_Inf_NotIn l k e : Sort l -> Inf (k,e) l -> ~In k l. Proof. intros; red; intros. destruct H1 as [e' H2]. @@ -200,57 +122,34 @@ Module KeyOrderedType(Import O:OrderedType). repeat red; reflexivity. Qed. - Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l. + Lemma Sort_NoDupA 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'. + Lemma Sort_In_cons_1 l p q : Sort (p::l) -> InA eqk q l -> ltk p q. 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'. + Lemma Sort_In_cons_2 l p q : Sort (p::l) -> InA eqk q (p::l) -> + ltk p q \/ eqk p q. 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. + Lemma Sort_In_cons_3 x l k e : + Sort ((k,e)::l) -> In x l -> ~O.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. |