proposition: Lemma t_apply_empty: forall A x v, @t_empty A v x = v.
proof: Proof. Admitted. Lemma t_update_eq : forall A (m: total_map A) x v, (t_update m x v) x = v. Proof. Admitted. Theorem t_update_neq : forall (X:Type) v x1 x2 (m : total_map X), x1 <> x2 -> (t_update m x1 v) x2 = m x2. Proof. Admitted. Lemma t_update_shadow : forall A (m: total_map A) v1 v2 x, t_update (t_update m x v1) x v2 = t_update m x v2. Proof. Admitted. Lemma beq_idP : forall x y, reflect (x = y) (beq_id x y). Proof. Admitted. Theorem t_update_same : forall X x (m : total_map X), t_update m x (m x) = m. Proof. Admitted. Theorem t_update_permute : forall (X:Type) v1 v2 x1 x2 (m : total_map X), x2 <> x1 -> (t_update (t_update m x2 v2) x1 v1) = (t_update (t_update m x1 v1) x2 v2). 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 : id) (v : A) := t_update m x (Some v). Lemma apply_empty : forall A x, @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