proposition: Lemma t_apply_empty : forall (A : Type) (x : string) (v : A), (_ !-> v) x = v.
proof: Proof. Admitted. Lemma t_update_eq : forall (A : Type) (m : total_map A) x v, (x !-> v ; m) x = v. Proof. Admitted. Theorem t_update_neq : forall (A : Type) (m : total_map A) x1 x2 v, x1 <> x2 -> (x1 !-> v ; m) x2 = m x2. Proof. Admitted. Lemma t_update_shadow : forall (A : Type) (m : total_map A) x v1 v2, (x !-> v2 ; x !-> v1 ; m) = (x !-> v2 ; m). Proof. Admitted. Theorem t_update_same : forall (A : Type) (m : total_map A) x, (x !-> m x ; m) = m. Proof. Admitted. Theorem t_update_permute : forall (A : Type) (m : total_map A) v1 v2 x1 x2, x2 <> x1 -> (x1 !-> v1 ; x2 !-> v2 ; m) = (x2 !-> v2 ; x1 !-> v1 ; m). Proof. Admitted. Definition partial_map (A : Type) := total_map (option A). Definition empty {A : Type} : partial_map A := t_empty None. Definition update {A : Type} (m : partial_map A) (x : string) (v : A) := (x !-> Some v ; m). 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). Definition examplepmap := ("Church" |-> true ; "Turing" |-> false). Lemma apply_empty : forall (A : Type) (x : string), @empty A x = None. Proof. intros. unfold empty. rewrite t_apply_empty. reflexivity. Qed.
imports: Coq(Arith.Arith) Coq(Bool.Bool) Coq.Strings.String Coq(Logic.FunctionalExtensionality) Coq(Lists.List)