Require Export Strings.String.
Require Export Logic.FunctionalExtensionality.

Definition partial_map (A:Type) := string -> option A.

Definition empty {A:Type} : partial_map A := fun _ => None.

Definition update {A:Type} (m : partial_map A) (x : string) (v : A) :=
  fun x' => if eqb x x' then Some v else m x'.

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

Lemma update_eq : forall (A : Type) (m : partial_map A) x v,
  (x |-> v; m) x = Some v.
Proof.
  intros. unfold update.
  rewrite eqb_refl. reflexivity.
Qed.

Lemma update_neq : forall (A : Type) (m : partial_map A) x1 x2 v,
  x2 <> x1 ->
  (x2 |-> v; m) x1 = m x1.
Proof.
  intros. unfold update.
  rewrite <- eqb_neq in H. rewrite H. reflexivity.
Qed.

Lemma update_shadow : forall (A : Type) (m : partial_map A) x v1 v2,
  (x |-> v2; x |-> v1; m) = (x |-> v2; m).
Proof.
  intros. unfold update.
  apply functional_extensionality. intro y.
  destruct (eqb x y); reflexivity.
Qed.

Theorem update_permute : forall (A : Type) (m : partial_map A) x1 x2 v1 v2,
  x2 <> x1 ->
  (x1 |-> v1; x2 |-> v2; m) = (x2 |-> v2; x1 |-> v1; m).
Proof.
  intros. unfold update.
  apply functional_extensionality. intro y.
  destruct (eqb_spec x1 y); destruct (eqb_spec x2 y); try reflexivity.
  congruence.
Qed.

Definition inclusion {A:Type} (m m' : partial_map A) :=
  forall x v, m x = Some v -> m' x = Some v.

Lemma inclusion_update : forall (A : Type) (m m' : partial_map A) x vx,
  inclusion m m' ->
  inclusion (x |-> vx; m) (x |-> vx; m').
Proof with auto.
  intros * H. unfold inclusion. intros y vy.
  destruct (eqb_spec x y).
  - rewrite e. repeat rewrite update_eq...
  - repeat rewrite update_neq...
Qed.

Ltac solve_by_inverts n :=
  match goal with H : ?T |- _ =>
    match type of T with Prop =>
      solve [
        inversion H;
        match n with S (S (?n')) => subst; solve_by_inverts (S n') end ]
    end
  end.

Ltac solve_by_invert := solve_by_inverts 1.