proposition: Lemma ab_eval_i_a : forall e a g, i_a Ab.m g (to_a e) -> i_a Ab.m g (to_assert (ab_eval (ab_lookup e) a) a).
proof: Proof. intros e a g Hyp; induction a; simpl. apply ab_lookup_i_a; auto. unfold to_assert; case_eq (to_syn (of_int n));intros ps l Hts; simpl. rewrite f_p_lookup. rewrite lf'_app; simpl. rewrite <- to_syn_ok with (p:=syntax.lookup string_dec m (fun _ => True) ps) (s:=ps)(v := of_int n). apply of_int_correct. rewrite lf_lz_to_a; auto. auto. simpl; unfold to_assert. case_eq (to_syn (plus (ab_eval (ab_lookup e) a1)(ab_eval (ab_lookup e) a2))); intros ps l Hts; simpl. unfold to_assert in IHa1, IHa2. case_eq (to_syn (ab_eval (ab_lookup e) a1)); intros ps1 l1 Hts1. case_eq (to_syn (ab_eval (ab_lookup e) a2)); intros ps2 l2 Hts2. rewrite Hts1 in IHa1; rewrite Hts2 in IHa2; simpl in IHa1, IHa2. rewrite f_p_lookup. rewrite f_p_lookup in IHa1; rewrite f_p_lookup in IHa2. repeat rewrite lf'_app in * |- *;simpl in *|-*; repeat rewrite lf_lz_to_a in * |- *. rewrite <- to_syn_ok with (p:=syntax.lookup string_dec m (fun _ => True) ps) (v := (plus (ab_eval (ab_lookup e) a1) (ab_eval (ab_lookup e) a2))) (s := ps); auto. apply plus_correct. rewrite to_syn_ok with (p:=syntax.lookup string_dec m (fun _ => True) ps1) (l:=l1)(s:=ps1); auto. rewrite to_syn_ok with (p:=syntax.lookup string_dec m (fun _ => True) ps2) (l:=l2)(s:=ps2); auto. Qed.
imports: syntax little denot Bool List String ZArith axiom