|
(************************************************************************)
(* * 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.
Local 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).
Proof. 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').
Proof. reflexivity. Defined.
Lemma eqke_def' {elt} (p q:key*elt) :
eqke p q = (D.eq (fst p) (fst q) /\ snd p = snd q).
Proof. reflexivity. Defined.
Lemma eqke_1 {elt} k k' (e e':elt) : eqke (k,e) (k',e') -> D.eq k k'.
Proof. now destruct 1. Qed.
Lemma eqke_2 {elt} k k' (e e':elt) : eqke (k,e) (k',e') -> e=e'.
Proof. now destruct 1. Qed.
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 : core.
(* Additional 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 : core.
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 : 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.
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 {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.
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 {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_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 {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_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.
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 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 }.
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.
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; 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.
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
