Software Foundations: Total and Partial Maps

Maps.v

Require Import Bool.
Require Import Logic.FunctionalExtensionality.
Require Import String.

Definition key := string.

Module Total.

Definition map A := key -> A.

Definition empty {A} (a : A) : map A :=
  fun _ => a.

Definition update {A} (m : map A) k v :=
  fun k' => if eqb k k' then v else m k'.

Notation "'_' '!->' v" := (empty v)
  (at level 100, right associativity).

Notation "k '!->' v ';' m" := (update m k v)
  (at level 100, v at next level, right associativity).

Lemma apply_empty : forall {A} k (v : A),
  (_ !-> v) k = v.
Proof. unfold empty. reflexivity. Qed.

Lemma update_eq : forall {A} (m : map A) k v,
  (k !-> v ; m) k = v.
Proof.
  unfold update. intros. rewrite eqb_refl. reflexivity.
Qed.

Theorem update_neq : forall {A} (m : map A) k k' v,
  k <> k' -> (k !-> v ; m) k' = m k'.
Proof.
  unfold update.
  intros.
  rewrite <- eqb_neq in H.
  rewrite H.
  reflexivity.
Qed.

Lemma update_shadow : forall {A} (m : map A) k v v',
  (k !-> v ; k !-> v' ; m) = (k !-> v ; m).
Proof.
  intros.
  apply functional_extensionality.
  intros k'.
  unfold update.
  destruct (eqb k k'); reflexivity.
Qed.

Lemma eqbP : forall k k',
  reflect (k = k') (eqb k k').
Proof.
  intros.
  destruct (eqb k k') eqn:?.
  - apply ReflectT.
    apply eqb_eq.
    assumption.
  - apply ReflectF.
    apply eqb_neq.
    assumption.
Qed.

Lemma eqbP' : forall k k',
  reflect (k = k') (eqb k k').
Proof.
  intros.
  apply iff_reflect.
  rewrite eqb_eq.
  reflexivity.
Qed.

Theorem update_same : forall {A} (m : map A) k,
  (k !-> m k ; m) = m.
Proof.
  intros.
  apply functional_extensionality.
  intros k'.
  unfold update.
  destruct (eqb k k') eqn:?.
  - apply eqb_eq in Heqb.
    rewrite Heqb.
    reflexivity.
  - reflexivity.
Qed.

Theorem update_permute : forall {A} (m : map A) k k' v v',
  k <> k' -> (k !-> v ; k' !-> v' ; m) = (k' !-> v' ; k !-> v ; m).
Proof.
  intros.
  apply functional_extensionality.
  intros k''.
  unfold update.
  destruct (eqb k k'') eqn:Heqb, (eqb k' k'') eqn:Heqb'; try reflexivity.
  (* The only case that isn't solved by simple reflection is when k = k',
  which goes against our hypothesis. *)
  apply eqb_eq in Heqb.
  apply eqb_eq in Heqb'.
  destruct Heqb, Heqb'.
  exfalso.
  apply H.
  reflexivity.
Qed.

End Total.

Module Partial.

Import Total.

Definition map A := map (option A).

Definition empty {A} : map A := empty None.

Definition update {A} (m : map A) k v := update m k (Some v).

Notation "k '|->' v ';' m" := (update m k v)
  (at level 100, v at next level, right associativity).

Notation "k '|->' v" := (update empty k v)
  (at level 100).

Lemma apply_empty : forall {A} k,
  @empty A k = None.
Proof. unfold empty. reflexivity. Qed.

Lemma update_eq : forall {A} (m : map A) k v,
  (k |-> v ; m) k = Some v.
Proof. intros. apply update_eq. Qed.

Theorem update_neq : forall {A} (m : map A) k k' v,
  k <> k' -> (k |-> v ; m) k' = m k'.
Proof. intros. apply update_neq. assumption. Qed.

Lemma update_shadow : forall {A} (m : map A) k v v',
  (k |-> v ; k |-> v' ; m) = (k |-> v ; m).
Proof. intros. apply update_shadow. Qed.

Theorem update_same : forall {A} (m : map A) k v,
  m k = Some v -> (k |-> v ; m) = m.
Proof.
  unfold update.
  intros.
  rewrite <- H.
  apply update_same.
Qed.

Theorem update_permute : forall {A} (m : map A) k k' v v',
  k <> k' -> (k |-> v ; k' |-> v' ; m) = (k' |-> v' ; k |-> v ; m).
Proof. intros. apply update_permute. assumption. Qed.

End Partial.