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 Import Equalities Bool SetoidList RelationPairs.

Set Implicit Arguments.

Keys and datas used in the future MMaps

Module KeyDecidableType(D:DecidableType).

 Local Open Scope signature_scope.
 Notation key := D.t.

 Definition eqk {elt} : relation (key*elt) := D.eq @@1.
 Definition eqke {elt} : relation (key*elt) := D.eq * Logic.eq.

 Hint Unfold eqk eqke : core.

eqk, eqke are equalities

 Instance eqk_equiv {elt} : Equivalence (@eqk elt) := _.

 Instance eqke_equiv {elt} : Equivalence (@eqke elt) := _.

eqke is stricter than eqk

 Instance eqke_eqk {elt} : subrelation (@eqke elt) (@eqk elt).elt:Type
subrelation eqke eqk
 Proof.elt:Type
subrelation eqke eqk firstorder. Qed.

Alternative definitions of eqke and eqk

 Lemma eqke_def {elt} k k' (e e':elt) :
  eqke (k,e) (k',e') = (D.eq k k' /\ e = e').elt:Type
k, k':key
e, e':elt
eqke (k, e) (k', e') = (D.eq k k' /\ e = e')
 Proof.elt:Type
k, k':key
e, e':elt
eqke (k, e) (k', e') = (D.eq k k' /\ e = e') reflexivity. Defined.

 Lemma eqke_def' {elt} (p q:key*elt) :
  eqke p q = (D.eq (fst p) (fst q) /\ snd p = snd q).elt:Type
p, q:(key * elt)%type
eqke p q = (D.eq (fst p) (fst q) /\ snd p = snd q)
 Proof.elt:Type
p, q:(key * elt)%type
eqke p q = (D.eq (fst p) (fst q) /\ snd p = snd q) reflexivity. Defined.

 Lemma eqke_1 {elt} k k' (e e':elt) : eqke (k,e) (k',e') -> D.eq k k'.elt:Type
k, k':key
e, e':elt
eqke (k, e) (k', e') -> D.eq k k'
 Proof.elt:Type
k, k':key
e, e':elt
eqke (k, e) (k', e') -> D.eq k k' now destruct 1. Qed.

 Lemma eqke_2 {elt} k k' (e e':elt) : eqke (k,e) (k',e') -> e=e'.elt:Type
k, k':key
e, e':elt
eqke (k, e) (k', e') -> e = e'
 Proof.elt:Type
k, k':key
e, e':elt
eqke (k, e) (k', e') -> e = e' now destruct 1. Qed.

 Lemma eqk_def {elt} k k' (e e':elt) : eqk (k,e) (k',e') = D.eq k k'.elt:Type
k, k':key
e, e':elt
eqk (k, e) (k', e') = D.eq k k'
 Proof.elt:Type
k, k':key
e, e':elt
eqk (k, e) (k', e') = D.eq k k' reflexivity. Defined.

 Lemma eqk_def' {elt} (p q:key*elt) : eqk p q = D.eq (fst p) (fst q).elt:Type
p, q:(key * elt)%type
eqk p q = D.eq (fst p) (fst q)
 Proof.elt:Type
p, q:(key * elt)%type
eqk p q = D.eq (fst p) (fst q) reflexivity. Qed.

 Lemma eqk_1 {elt} k k' (e e':elt) : eqk (k,e) (k',e') -> D.eq k k'.elt:Type
k, k':key
e, e':elt
eqk (k, e) (k', e') -> D.eq k k'
 Proof.elt:Type
k, k':key
e, e':elt
eqk (k, e) (k', e') -> D.eq k k' trivial. Qed.

 Hint Resolve eqke_1 eqke_2 eqk_1 : core.

 (* Additional facts *)

 Lemma InA_eqke_eqk {elt} p (m:list (key*elt)) :
   InA eqke p m -> InA eqk p m.elt:Type
p:(key * elt)%type
m:list (key * elt)
InA eqke p m -> InA eqk p m
 Proof.elt:Type
p:(key * elt)%type
m:list (key * elt)
InA eqke p m -> InA eqk p m
  induction 1; firstorder.
 Qed.
 Hint Resolve InA_eqke_eqk : core.

 Lemma InA_eqk_eqke {elt} p (m:list (key*elt)) :
  InA eqk p m -> exists q, eqk p q /\ InA eqke q m.elt:Type
p:(key * elt)%type
m:list (key * elt)
InA eqk p m ->
exists q : key * elt, eqk p q /\ InA eqke q m
 Proof.elt:Type
p:(key * elt)%type
m:list (key * elt)
InA eqk p m ->
exists q : key * elt, eqk p q /\ InA eqke q m
  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.elt:Type
p, q:(key * elt)%type
m:list (key * elt)
eqk p q -> InA eqk p m -> InA eqk q m
 Proof.elt:Type
p, q:(key * elt)%type
m:list (key * elt)
eqk p q -> InA eqk p m -> InA eqk q m
  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 : core.

 (* 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.elt:Type
k:key
l:list (key * elt)
In k l <-> (exists e : elt, InA eqk (k, e) l)
 Proof.elt:Type
k:key
l:list (key * elt)
In k l <-> (exists e : elt, InA eqk (k, e) l)
  unfold In, MapsTo.elt:Type
k:key
l:list (key * elt)
(exists e : elt, InA eqke (k, e) l) <->
(exists e : elt, InA eqk (k, e) l)
  split; intros (e,H).elt:Type
k:key
l:list (key * elt)
e:elt
H:InA eqke (k, e) l
exists e0 : elt, InA eqk (k, e0) l
elt:Type
k:key
l:list (key * elt)
e:elt
H:InA eqk (k, e) l
exists e0 : elt, InA eqke (k, e0) l
  -elt:Type
k:key
l:list (key * elt)
e:elt
H:InA eqke (k, e) l
exists e0 : elt, InA eqk (k, e0) l exists e; auto.
  -elt:Type
k:key
l:list (key * elt)
e:elt
H:InA eqk (k, e) l
exists e0 : elt, InA eqke (k, e0) l apply InA_eqk_eqke in H.elt:Type
k:key
l:list (key * elt)
e:elt
H:exists q : key * elt, eqk (k, e) q /\ InA eqke q l
exists e0 : elt, InA eqke (k, e0) l destruct H as ((k',e'),(E,H)).elt:Type
k:key
l:list (key * elt)
e:elt
k':key
e':elt
E:eqk (k, e) (k', e')
H:InA eqke (k', e') l
exists e0 : elt, InA eqke (k, e0) l
    compute in E.elt:Type
k:key
l:list (key * elt)
e:elt
k':key
e':elt
E:D.eq k k'
H:InA eqke (k', e') l
exists e0 : elt, InA eqke (k, e0) l exists e'.elt:Type
k:key
l:list (key * elt)
e:elt
k':key
e':elt
E:D.eq k k'
H:InA eqke (k', e') l
InA eqke (k, e') l now rewrite E.
 Qed.

 Lemma In_alt' {elt} (l:list (key*elt)) k e :
   In k l <-> InA eqk (k,e) l.elt:Type
l:list (key * elt)
k:key
e:elt
In k l <-> InA eqk (k, e) l
 Proof.elt:Type
l:list (key * elt)
k:key
e:elt
In k l <-> InA eqk (k, e) l
  rewrite In_alt.elt:Type
l:list (key * elt)
k:key
e:elt
(exists e0 : elt, InA eqk (k, e0) l) <->
InA eqk (k, e) l firstorder.elt:Type
l:list (key * elt)
k:key
e, x:elt
H:InA eqk (k, x) l
InA eqk (k, e) l eapply InA_eqk; eauto.elt:Type
l:list (key * elt)
k:key
e, x:elt
H:InA eqk (k, x) l
eqk (k, x) (k, e) now compute.
 Qed.

 Lemma In_alt2 {elt} k (l:list (key*elt)) :
   In k l <-> Exists (fun p => D.eq k (fst p)) l.elt:Type
k:key
l:list (key * elt)
In k l <->
Exists (fun p : key * elt => D.eq k (fst p)) l
 Proof.elt:Type
k:key
l:list (key * elt)
In k l <->
Exists (fun p : key * elt => D.eq k (fst p)) l
  unfold In, MapsTo.elt:Type
k:key
l:list (key * elt)
(exists e : elt, InA eqke (k, e) l) <->
Exists (fun p : key * elt => D.eq k (fst p)) l
  setoid_rewrite Exists_exists; setoid_rewrite InA_alt.elt:Type
k:key
l:list (key * elt)
(exists (e : elt) (y : key * elt),
   eqke (k, e) y /\ List.In y l) <->
(exists x : key * elt, List.In x l /\ D.eq k (fst x))
  firstorder.elt:Type
k:key
l:list (key * elt)
x:(key * elt)%type
H:List.In x l
H0:D.eq k (fst x)
exists (e : elt) (y : key * elt),
  eqke (k, e) y /\ List.In y l
  exists (snd x), x; auto.
 Qed.

 Lemma In_nil {elt} k : In k (@nil (key*elt)) <-> False.elt:Type
k:key
In k nil <-> False
 Proof.elt:Type
k:key
In k nil <-> False
  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.elt:Type
k:key
p:(key * elt)%type
l:list (key * elt)
In k (p :: l) <-> D.eq k (fst p) \/ In k l
 Proof.elt:Type
k:key
p:(key * elt)%type
l:list (key * elt)
In k (p :: l) <-> D.eq k (fst p) \/ In k l
  rewrite !In_alt2, Exists_cons; intuition.
 Qed.

 Instance MapsTo_compat {elt} :
   Proper (D.eq==>Logic.eq==>equivlistA eqke==>iff) (@MapsTo elt).elt:Type
Proper (D.eq ==> eq ==> equivlistA eqke ==> iff)
  MapsTo
 Proof.elt:Type
Proper (D.eq ==> eq ==> equivlistA eqke ==> iff)
  MapsTo
  intros x x' Hx e e' He l l' Hl.elt:Type
x, x':key
Hx:D.eq x x'
e, e':elt
He:e = e'
l, l':list (key * elt)
Hl:equivlistA eqke l l'
MapsTo x e l <-> MapsTo x' e' l' unfold MapsTo.elt:Type
x, x':key
Hx:D.eq x x'
e, e':elt
He:e = e'
l, l':list (key * elt)
Hl:equivlistA eqke l l'
InA eqke (x, e) l <-> InA eqke (x', e') l'
  rewrite Hx, He, Hl; intuition.
 Qed.

 Instance In_compat {elt} : Proper (D.eq==>equivlistA eqk==>iff) (@In elt).elt:Type
Proper (D.eq ==> equivlistA eqk ==> iff) In
 Proof.elt:Type
Proper (D.eq ==> equivlistA eqk ==> iff) In
  intros x x' Hx l l' Hl.elt:Type
x, x':key
Hx:D.eq x x'
l, l':list (key * elt)
Hl:equivlistA eqk l l'
In x l <-> In x' l' rewrite !In_alt.elt:Type
x, x':key
Hx:D.eq x x'
l, l':list (key * elt)
Hl:equivlistA eqk l l'
(exists e : elt, InA eqk (x, e) l) <->
(exists e : elt, InA eqk (x', e) l')
  setoid_rewrite Hl.elt:Type
x, x':key
Hx:D.eq x x'
l, l':list (key * elt)
Hl:equivlistA eqk l l'
(exists e : elt, InA eqk (x, e) l') <->
(exists e : elt, InA eqk (x', e) l') setoid_rewrite Hx.elt:Type
x, x':key
Hx:D.eq x x'
l, l':list (key * elt)
Hl:equivlistA eqk l l'
(exists e : elt, InA eqk (x', e) l') <->
(exists e : elt, InA eqk (x', e) l') intuition.
 Qed.

 Lemma MapsTo_eq {elt} (l:list (key*elt)) x y e :
   D.eq x y -> MapsTo x e l -> MapsTo y e l.elt:Type
l:list (key * elt)
x, y:key
e:elt
D.eq x y -> MapsTo x e l -> MapsTo y e l
 Proof.elt:Type
l:list (key * elt)
x, y:key
e:elt
D.eq x y -> MapsTo x e l -> MapsTo y e l now intros <-. Qed.

 Lemma In_eq {elt} (l:list (key*elt)) x y :
   D.eq x y -> In x l -> In y l.elt:Type
l:list (key * elt)
x, y:key
D.eq x y -> In x l -> In y l
 Proof.elt:Type
l:list (key * elt)
x, y:key
D.eq x y -> In x l -> In y l now intros <-. Qed.

 Lemma In_inv {elt} k k' e (l:list (key*elt)) :
   In k ((k',e) :: l) -> D.eq k k' \/ In k l.elt:Type
k, k':key
e:elt
l:list (key * elt)
In k ((k', e) :: l) -> D.eq k k' \/ In k l
 Proof.elt:Type
k, k':key
e:elt
l:list (key * elt)
In k ((k', e) :: l) -> D.eq k k' \/ In k l
  intros (e',H).elt:Type
k, k':key
e:elt
l:list (key * elt)
e':elt
H:MapsTo k e' ((k', e) :: l)
D.eq k k' \/ In k l red in H.elt:Type
k, k':key
e:elt
l:list (key * elt)
e':elt
H:InA eqke (k, e') ((k', e) :: l)
D.eq k k' \/ In k l rewrite InA_cons, eqke_def in H.elt:Type
k, k':key
e:elt
l:list (key * elt)
e':elt
H:D.eq k k' /\ e' = e \/ InA eqke (k, e') l
D.eq k k' \/ In k l
  intuition.elt:Type
k, k':key
e:elt
l:list (key * elt)
e':elt
H0:InA eqke (k, e') l
D.eq k k' \/ In k l right.elt:Type
k, k':key
e:elt
l:list (key * elt)
e':elt
H0:InA eqke (k, e') l
In k l now exists e'.
 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.elt:Type
k, k':key
e, e':elt
l:list (key * elt)
InA eqk (k, e) ((k', e') :: l) ->
~ D.eq k k' -> InA eqk (k, e) l
 Proof.elt:Type
k, k':key
e, e':elt
l:list (key * elt)
InA eqk (k, e) ((k', e') :: l) ->
~ D.eq k k' -> InA eqk (k, e) l
  rewrite InA_cons, eqk_def.elt:Type
k, k':key
e, e':elt
l:list (key * elt)
D.eq k k' \/ InA eqk (k, e) l ->
~ D.eq k k' -> InA eqk (k, e) l intuition.
 Qed.

 Lemma In_inv_3 {elt} x x' (l:list (key*elt)) :
   InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.elt:Type
x, x':(key * elt)%type
l:list (key * elt)
InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l
 Proof.elt:Type
x, x':(key * elt)%type
l:list (key * elt)
InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l
  rewrite InA_cons.elt:Type
x, x':(key * elt)%type
l:list (key * elt)
eqke x x' \/ InA eqke x l ->
~ eqk x x' -> InA eqke x l destruct 1 as [H|H]; trivial.elt:Type
x, x':(key * elt)%type
l:list (key * elt)
H:eqke x x'
~ eqk x x' -> InA eqke x l destruct 1.elt:Type
x, x':(key * elt)%type
l:list (key * elt)
H:eqke x x'
eqk x x'
  eauto with *.
 Qed.

 Hint Extern 2 (eqke ?a ?b) => split : core.
 Hint Resolve InA_eqke_eqk : core.
 Hint Resolve In_inv_2 In_inv_3 : core.

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 }.forall x y : D1.t * D2.t, {eq x y} + {~ eq x y}
 Proof.forall x y : D1.t * D2.t, {eq x y} + {~ eq x y}
 intros (x1,x2) (y1,y2); unfold eq; simpl.x1:D1.t
x2:D2.t
y1:D1.t
y2:D2.t
{(D1.eq * D2.eq)%signature (x1, x2) (y1, y2)} +
{~ (D1.eq * D2.eq)%signature (x1, x2) (y1, y2)}
 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.
 Instance eq_equiv : Equivalence eq := _.
 Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.forall x y : t, {eq x y} + {~ eq x y}
 Proof.forall x y : t, {eq x y} + {~ eq x y}
 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; intros [=]; auto).
 Defined.

End PairUsualDecidableType.

And also for pairs of UsualDecidableTypeFull

Module PairUsualDecidableTypeFull (D1 D2:UsualDecidableTypeFull)
  <: UsualDecidableTypeFull.

 Module M := PairUsualDecidableType D1 D2.
 Include Backport_DT (M).
 Include HasEqDec2Bool.

End PairUsualDecidableTypeFull.