Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Export SetoidList.
Require Equalities.

Set Implicit Arguments.
Unset Strict Implicit.

NB: This file is here only for compatibility with earlier version of FSets and FMap. Please use Structures/Equalities.v directly now.

Types with Equalities, and nothing more (for subtyping purpose)

Module Type EqualityType := Equalities.EqualityTypeOrig.

Types with decidable Equalities (but no ordering)

Module Type DecidableType := Equalities.DecidableTypeOrig.

Additional notions about keys and datas used in FMap

Module KeyDecidableType(D:DecidableType).
 Import D.

 Section Elt.
 Variable elt : Type.
 Notation key:=t.

  Definition eqk (p p':key*elt) := eq (fst p) (fst p').
  Definition eqke (p p':key*elt) :=
          eq (fst p) (fst p') /\ (snd p) = (snd p').

  Hint Unfold eqk eqke : core.
  Hint Extern 2 (eqke ?a ?b) => split : core.

   (* eqke is stricter than eqk *)

   Lemma eqke_eqk : forall x x', eqke x x' -> eqk x x'.elt:Type
forall x x' : key * elt, eqke x x' -> eqk x x'
   Proof.elt:Type
forall x x' : key * elt, eqke x x' -> eqk x x'
     unfold eqk, eqke; intuition.
   Qed.

  (* eqk, eqke are equalities *)

  Lemma eqk_refl : forall e, eqk e e.elt:Type
forall e : key * elt, eqk e e
  Proof.elt:Type
forall e : key * elt, eqk e e auto. Qed.

  Lemma eqke_refl : forall e, eqke e e.elt:Type
forall e : key * elt, eqke e e
  Proof.elt:Type
forall e : key * elt, eqke e e auto. Qed.

  Lemma eqk_sym : forall e e', eqk e e' -> eqk e' e.elt:Type
forall e e' : key * elt, eqk e e' -> eqk e' e
  Proof.elt:Type
forall e e' : key * elt, eqk e e' -> eqk e' e auto. Qed.

  Lemma eqke_sym : forall e e', eqke e e' -> eqke e' e.elt:Type
forall e e' : key * elt, eqke e e' -> eqke e' e
  Proof.elt:Type
forall e e' : key * elt, eqke e e' -> eqke e' e unfold eqke; intuition. Qed.

  Lemma eqk_trans : forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''.elt:Type
forall e e' e'' : key * elt,
eqk e e' -> eqk e' e'' -> eqk e e''
  Proof.elt:Type
forall e e' e'' : key * elt,
eqk e e' -> eqk e' e'' -> eqk e e'' eauto. Qed.

  Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''.elt:Type
forall e e' e'' : key * elt,
eqke e e' -> eqke e' e'' -> eqke e e''
  Proof.elt:Type
forall e e' e'' : key * elt,
eqke e e' -> eqke e' e'' -> eqke e e''
    unfold eqke; intuition; [ eauto | congruence ].
  Qed.

  Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core.
  Hint Immediate eqk_sym eqke_sym : core.

  Instance eqk_equiv : Equivalence eqk.elt:Type
Equivalence eqk
  Proof.elt:Type
Equivalence eqk split; eauto. Qed.

  Instance eqke_equiv : Equivalence eqke.elt:Type
Equivalence eqke
  Proof.elt:Type
Equivalence eqke split; eauto. Qed.

  Lemma InA_eqke_eqk :
     forall x m, InA eqke x m -> InA eqk x m.elt:Type
forall (x : key * elt) (m : list (key * elt)),
InA eqke x m -> InA eqk x m
  Proof.elt:Type
forall (x : key * elt) (m : list (key * elt)),
InA eqke x m -> InA eqk x m
    unfold eqke; induction 1; intuition. 
  Qed.
  Hint Resolve InA_eqke_eqk : core.

  Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.elt:Type
forall (p q : key * elt) (m : list (key * elt)),
eqk p q -> InA eqk p m -> InA eqk q m
  Proof.elt:Type
forall (p q : key * elt) (m : list (key * elt)),
eqk p q -> InA eqk p m -> InA eqk q m
   intros; apply InA_eqA with p; auto using eqk_equiv.
  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 : core.

  (* 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.elt:Type
forall (k : key) (l : list (key * elt)),
In k l <-> (exists e : elt, InA eqk (k, e) l)
  Proof.elt:Type
forall (k : key) (l : list (key * elt)),
In k l <-> (exists e : elt, InA eqk (k, e) l)
  firstorder.elt:Type
k:key
l:list (key * elt)
x:elt
H:MapsTo k x l
exists e : elt, InA eqk (k, e) l
elt:Type
k:key
l:list (key * elt)
x:elt
H:InA eqk (k, x) l
In k l
  exists x; auto.elt:Type
k:key
l:list (key * elt)
x:elt
H:InA eqk (k, x) l
In k l
  induction H.elt:Type
k:key
x:elt
y:(key * elt)%type
l:list (key * elt)
H:eqk (k, x) y
In k (y :: l)
elt:Type
k:key
x:elt
y:(key * elt)%type
l:list (key * elt)
H:InA eqk (k, x) l
IHInA:In k l
In k (y :: l)
  destruct y.elt:Type
k:key
x:elt
t0:key
e:elt
l:list (key * elt)
H:eqk (k, x) (t0, e)
In k ((t0, e) :: l)
elt:Type
k:key
x:elt
y:(key * elt)%type
l:list (key * elt)
H:InA eqk (k, x) l
IHInA:In k l
In k (y :: l)
  exists e; auto.elt:Type
k:key
x:elt
y:(key * elt)%type
l:list (key * elt)
H:InA eqk (k, x) l
IHInA:In k l
In k (y :: l)
  destruct IHInA as [e H0].elt:Type
k:key
x:elt
y:(key * elt)%type
l:list (key * elt)
H:InA eqk (k, x) l
e:elt
H0:MapsTo k e l
In k (y :: l)
  exists e; auto.
  Qed.

  Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.elt:Type
forall (l : list (key * elt)) (x y : key) (e : elt),
eq x y -> MapsTo x e l -> MapsTo y e l
  Proof.elt:Type
forall (l : list (key * elt)) (x y : key) (e : elt),
eq x y -> MapsTo x e l -> MapsTo y e l
    intros; unfold MapsTo in *; apply InA_eqA with (x,e); auto using eqke_equiv.
  Qed.

  Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.elt:Type
forall (l : list (key * elt)) (x y : key),
eq x y -> In x l -> In y l
  Proof.elt:Type
forall (l : list (key * elt)) (x y : key),
eq x y -> In x l -> In y l
  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.elt:Type
forall (k k' : key) (e : elt) (l : list (key * elt)),
In k ((k', e) :: l) -> eq k k' \/ In k l
  Proof.elt:Type
forall (k k' : key) (e : elt) (l : list (key * elt)),
In k ((k', e) :: l) -> eq k k' \/ In k l
    inversion 1.elt:Type
k, k':key
e:elt
l:list (key * elt)
H:In k ((k', e) :: l)
x:elt
H0:MapsTo k x ((k', e) :: l)
eq k k' \/ In k l
    inversion_clear H0; eauto.elt:Type
k, k':key
e:elt
l:list (key * elt)
H:In k ((k', e) :: l)
x:elt
H1:eqke (k, x) (k', e)
eq k k' \/ In k l
    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.elt:Type
forall (k k' : key) (e e' : elt)
  (l : list (key * elt)),
InA eqk (k, e) ((k', e') :: l) ->
~ eq k k' -> InA eqk (k, e) l
  Proof.elt:Type
forall (k k' : key) (e e' : elt)
  (l : list (key * elt)),
InA eqk (k, e) ((k', e') :: l) ->
~ eq k k' -> InA eqk (k, e) l
   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.elt:Type
forall (x x' : key * elt) (l : list (key * elt)),
InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l
  Proof.elt:Type
forall (x x' : key * elt) (l : list (key * elt)),
InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l
   inversion_clear 1; compute in H0; intuition.
  Qed.

 End Elt.

 Hint Unfold eqk eqke : core.
 Hint Extern 2 (eqke ?a ?b) => split : core.
 Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core.
 Hint Immediate eqk_sym eqke_sym : core.
 Hint Resolve InA_eqke_eqk : core.
 Hint Unfold MapsTo In : core.
 Hint Resolve In_inv_2 In_inv_3 : core.

End KeyDecidableType.