Library framework.maps
A simple definition of maps as association lists with unique keys.
Require Import List.
Import ListNotations.
Require Import Recdef.
Require Import Omega.
Ltac inv H := (inversion H; subst; clear H).
Definition map (K:Type) (V:Type) := list (K×V)%type.
Section Maps.
Context {K:Type}.
Context {V:Type}.
Variable Kdec : ∀ (k1 k2:K), {k1 = k2} + {k1 ≠ k2}.
Operations
Definition empty : map K V := [].
Fixpoint get (m: map K V) (k:K) : option V :=
match m with
| (k',v')::m' ⇒ if Kdec k k' then Some v' else get m' k
| [] ⇒ None
end.
Fixpoint remove (m: map K V) (k:K) : map K V :=
match m with
| (k',v')::m' ⇒ if Kdec k k' then (remove m' k) else (k',v')::(remove m' k)
| [] ⇒ []
end.
Definition set (m: map K V) (k:K) (v:V) : map K V := (k,v)::(remove m k).
Definition keys (m:map K V) : list K :=
List.map (@fst K V) m.
values must be defined carefully to avoid including values from shadowed entries.
Function values (m:map K V) {measure length m} : list V :=
match m with
| (k,v)::m' ⇒ v::values(remove m' k)
| [] ⇒ []
end.
intros.
clear. induction m'.
simpl. omega.
destruct a. simpl in ×. destruct (Kdec k k0). omega. simpl; omega.
Defined.
match m with
| (k,v)::m' ⇒ v::values(remove m' k)
| [] ⇒ []
end.
intros.
clear. induction m'.
simpl. omega.
destruct a. simpl in ×. destruct (Kdec k k0). omega. simpl; omega.
Defined.
Basic properties
Lemma get_remove_same: ∀ m k, get (remove m k) k = None.
Proof.
induction m; intros.
auto.
simpl. destruct a. destruct (Kdec k k0). subst. auto.
simpl. destruct (Kdec k k0). subst; exfalso; apply n; auto. auto.
Qed.
Lemma get_remove_other: ∀ m k k', k ≠ k' → get (remove m k) k' = get m k'.
Proof.
induction m; intros.
auto.
simpl. destruct a.
destruct (Kdec k k0). subst. destruct (Kdec k' k0). subst. exfalso; apply H; auto. auto.
destruct (Kdec k' k0). subst. simpl. destruct (Kdec k0 k0). auto. exfalso; apply n0; auto.
simpl. destruct (Kdec k' k0). subst. exfalso; apply n0; auto. auto.
Qed.
Lemma get_set_same: ∀ m k v, get (set m k v) k = Some v.
Proof.
intros. simpl. destruct (Kdec k k); auto. exfalso; apply n; auto.
Qed.
Lemma get_set_other: ∀ m k v k', k' ≠ k → get (set m k v) k' = get m k'.
Proof.
intros. simpl. destruct (Kdec k' k). subst k'; exfalso; apply H; auto. apply get_remove_other; auto.
Qed.
Lemma get_empty: ∀ k, get empty k = None.
Proof.
intros. auto.
Qed.
Lemma in_keys: ∀ m k, In k (keys m) → ∃ v, get m k = Some v.
Proof.
induction m; intros.
inversion H.
inversion H; simpl.
destruct a; subst.
∃ v. simpl. destruct (Kdec k0 k0). auto. exfalso; apply n; auto.
destruct a. destruct (Kdec k k0). subst. ∃ v. auto.
apply IHm; auto.
Qed.
Lemma keys_in: ∀ m k v, get m k = Some v → In k (keys m).
Proof.
induction m; intros.
inv H.
simpl in H. destruct a. destruct (Kdec k k0). subst k0. simpl. auto.
simpl. right. eauto.
Qed.
Lemma not_in_keys: ∀ m k, ¬ In k (keys m) → get m k = None.
Proof.
intros.
destruct (get m k) eqn:?.
exfalso. apply H. eapply keys_in; eauto.
auto.
Qed.
Lemma not_keys_in : ∀ m k, get m k = None → ¬ In k (keys m).
Proof.
intros.
intro X. apply in_keys in X. destruct X as [v P].
rewrite H in P; inv P.
Qed.
Lemma values_in: ∀ m k v, get m k = Some v → In v (values m).
Proof.
intros.
functional induction (values m) using values_ind.
inv H.
destruct (Kdec k k0).
inv H1. left; auto.
right. apply IHl. rewrite get_remove_other; eauto.
inv H.
Qed.
Lemma in_values : ∀ m v, In v (values m) → ∃ k, get m k = Some v.
Proof.
intros m v.
functional induction (values m) using values_ind; intros.
inv H.
∃ k; simpl. destruct (Kdec k k); auto. exfalso; apply n; auto.
destruct (IHl H0) as [k0 P].
∃ k0. simpl.
destruct (Kdec k0 k); subst.
rewrite get_remove_same in P. inv P.
erewrite <- get_remove_other; eauto.
inv H.
Qed.
Useful derived properties
Lemma in_keys_set: ∀ m k k' v, In k' (keys (set m k v)) → k' = k ∨ In k' (keys m).
Proof.
intros. apply in_keys in H. destruct H as [v0 P].
destruct (Kdec k' k). left; auto. right.
rewrite get_set_other in P; auto.
eapply keys_in. eauto.
Qed.
Lemma set_in_keys: ∀ m k k' v, k' = k ∨ In k' (keys m) → In k' (keys (set m k v)).
Proof.
intros.
destruct H; subst.
eapply keys_in. eapply get_set_same; eauto.
apply in_keys in H. destruct H as [v' P].
destruct (Kdec k' k); subst.
eapply keys_in. eapply get_set_same; eauto.
eapply keys_in. erewrite get_set_other; eauto.
Qed.
Lemma in_keys_remove : ∀ m k k', In k (keys (remove m k')) → k ≠ k' ∧ In k (keys m).
Proof.
intros. apply in_keys in H. destruct H as [v P].
destruct (Kdec k' k).
subst. rewrite get_remove_same in P. inv P.
split; auto. erewrite get_remove_other in P; auto. eapply keys_in; eauto.
Qed.
Lemma remove_in_keys: ∀ m k k', In k (keys m) → k ≠ k' → In k (keys (remove m k')).
Proof.
intros. apply in_keys in H. destruct H as [v P].
erewrite <- get_remove_other in P; eauto.
eapply keys_in; eauto.
Qed.
End Maps.
Section MapDomains.
Context {K:Type}.
Variable DecEq: ∀ (k1 k2 : K), {k1 = k2} + {k1 ≠ k2}.
Maps with equal domains.
Definition DomEq {X Y: Type} (m1: map K X) (m2: map K Y) : Prop :=
∀ k, In k (keys m1) ↔ In k (keys m2).
Lemma DomEq_set :
∀ X Y m1 m2,
@DomEq X Y m1 m2 →
∀ k,
In k (keys m1) →
∀ (v: X),
DomEq (set DecEq m1 k v) m2.
Proof.
intros.
split;intros.
apply in_keys_set in H1. inv H1; eapply H; eauto.
apply set_in_keys. right. eapply H; eauto.
Qed.
End MapDomains.