proposition: Lemma assume_test_sound: forall b res S s, beval b s = res -> ST.In s S -> ST.In s (assume_test b res S).
proof: Proof. induction b; cbn; intros. - subst res; auto. - subst res; auto. - set (Res := if res then V.eq_inv (Aeval a1 S) (Aeval a2 S) else V.ne_inv (Aeval a1 S) (Aeval a2 S)). assert (A: V.In (aeval a1 s) (fst Res) /\ V.In (aeval a2 s) (snd Res)). { unfold Res; destruct res; [ apply V.eq_inv_1 | apply V.ne_inv_1 ]; auto using Aeval_sound. - apply Z.eqb_eq; auto. - apply Z.eqb_neq; auto. } destruct A as [A1 A2]. destruct Res as [Res1 Res2]. auto using assume_eval_sound. - set (Res := if res then V.le_inv (Aeval a1 S) (Aeval a2 S) else V.gt_inv (Aeval a1 S) (Aeval a2 S)). assert (A: V.In (aeval a1 s) (fst Res) /\ V.In (aeval a2 s) (snd Res)). { unfold Res; destruct res; [ apply V.le_inv_1 | apply V.gt_inv_1 ]; auto using Aeval_sound. - apply Z.leb_le; auto. - apply Z.leb_nle in H. lia. } destruct A as [A1 A2]. destruct Res as [Res1 Res2]. auto using assume_eval_sound. - apply IHb; auto. rewrite <- H. rewrite negb_involutive; auto. - destruct res. + destruct (andb_prop _ _ H). auto. + destruct (andb_false_elim _ _ H); [apply ST.join_1 | apply ST.join_2]; auto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)