proposition: Theorem Cexec_sound: forall c s s' S, ST.In s S -> cexec s c s' -> ST.In s' (Cexec c S).
proof: Proof. Opaque niter. induction c; intros s s' S PRE EXEC; cbn. - inversion EXEC; subst. auto. - inversion EXEC; subst. apply ST.set_1; auto. apply Aeval_sound; auto. - inversion EXEC; subst. eauto. - inversion EXEC; subst. destruct (beval b s). apply ST.join_1; eauto. apply ST.join_2; eauto. - set (F := fun X => ST.join S (Cexec c X)). set (X := postfixpoint F). assert (L : ST.le (F X) X) by (apply postfixpoint_sound). assert (REC: forall s1 c1 s2, cexec s1 c1 s2 -> c1 = WHILE b c -> ST.In s1 X -> ST.In s2 X). { induction 1; intro EQ; inversion EQ; subst; intros. - auto. - apply IHcexec2; auto. apply L. unfold F. apply ST.join_2. eapply IHc; eauto. } eapply REC; eauto. apply L. unfold F. apply ST.join_1. auto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) CDF(Sequences IMP)