proposition: Theorem dce_correct_terminating: forall s c s', cexec s c s' -> forall L s1, agree (live c L) s s1 -> exists s1', cexec s1 (dce c L) s1' /\ agree L s' s1'.
proof: Proof. induction 1; intros L s1 AG. - exists s1; split. constructor. auto. - cbn in *. destruct (IdentSet.mem x L) eqn:is_live. + assert (EVAL: aeval a s = aeval a s1) by (eapply aeval_agree; eapply agree_mon; eauto; fsetdec). econstructor; split. apply cexec_assign. rewrite EVAL. apply agree_update_live. eapply agree_mon; eauto. fsetdec. + econstructor; split. apply cexec_skip. apply agree_update_dead. auto. red; intros. assert (IdentSet.mem x L = true) by (apply IdentSet.mem_1; auto). congruence. - cbn in *. destruct (IHcexec1 _ _ AG) as (s1' & EXEC1 & AG1). destruct (IHcexec2 _ _ AG1) as (s2' & EXEC2 & AG2). exists s2'; split. apply cexec_seq with s1'; auto. auto. - cbn in *. assert (EVAL: beval b s = beval b s1) by (eapply beval_agree; eapply agree_mon; eauto; fsetdec). destruct (IHcexec L s1) as (s1' & EXEC' & AG'). eapply agree_mon; eauto. destruct (beval b s); fsetdec. exists s1'; split. apply cexec_ifthenelse. rewrite <- EVAL. destruct (beval b s); auto. auto. - change (dce (WHILE b c) L) with (WHILE b (dce c (live (WHILE b c) L))). destruct (live_while_charact b c L) as (P & Q & R). assert (EVAL: beval b s = beval b s1) by (eapply beval_agree; eapply agree_mon; eauto; fsetdec). exists s1; split. apply cexec_while_done. congruence. eapply agree_mon; eauto. - change (dce (WHILE b c) L) with (WHILE b (dce c (live (WHILE b c) L))). destruct (live_while_charact b c L) as (P & Q & R). assert (EVAL: beval b s = beval b s1) by (eapply beval_agree; eapply agree_mon; eauto; fsetdec). destruct (IHcexec1 (live (WHILE b c) L) s1) as (s1' & EXEC1 & AG1). eapply agree_mon; eauto. destruct (IHcexec2 L s1') as (s2' & EXEC2 & AG2). auto. exists s2'; split. apply cexec_while_loop with s1'; auto. congruence. auto. Qed.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation)