proposition: Lemma assume_eval_sound: forall a Res S s, V.In (aeval a s) Res -> ST.In s S -> ST.In s (assume_eval a Res S).
proof: Proof. induction a; cbn; intros. - rewrite V.isIn_1 by auto. auto. - replace s with (update x (s x) s). apply ST.set_1; auto. apply V.meet_1; auto. apply functional_extensionality; intros y. unfold update; destruct (string_dec x y); congruence. - set (n1 := aeval a1 s) in *. set (n2 := aeval a2 s) in *. set (N1 := Aeval a1 S). set (N2 := Aeval a2 S). assert (V.In n1 N1) by (apply Aeval_sound; auto). assert (V.In n2 N2) by (apply Aeval_sound; auto). apply IHa1; fold n1. apply V.meet_1. auto. replace n1 with ((n1 + n2) - n2) by lia. apply V.sub_1; auto. apply IHa2; fold n2. apply V.meet_1. auto. replace n2 with ((n1 + n2) - n1) by lia. apply V.sub_1; auto. auto. - set (n1 := aeval a1 s) in *. set (n2 := aeval a2 s) in *. set (N1 := Aeval a1 S). set (N2 := Aeval a2 S). assert (V.In n1 N1) by (apply Aeval_sound; auto). assert (V.In n2 N2) by (apply Aeval_sound; auto). apply IHa1; fold n1. apply V.meet_1. auto. replace n1 with ((n1 - n2) + n2) by lia. apply V.add_1; auto. apply IHa2; fold n2. apply V.meet_1. auto. replace n2 with (n1 - (n1 - n2)) by lia. apply V.sub_1; auto. auto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)