proposition: Lemma slow_add_correct: forall s, s "x" >= 0 -> exists s', star red (slow_add, s) (SKIP, s') /\ s' "y" = s "y" + s "x".
proof: Proof. assert (REC: forall v, 0 <= v -> forall s, s "x" = v -> exists s', star red (slow_add, s) (SKIP, s') /\ s' "y" = s "y" + s "x"). { intros v0 v0POS. pattern v0. apply natlike_ind; auto. - intros. exists s; split. + apply star_one. apply red_while_done. cbn. rewrite H. apply Z.leb_nle. lia. + lia. - intros v VPOS REC s EQ. set (s1 := update "x" v s). set (s2 := update "y" (s "y" + 1) s1). destruct (REC s2) as (s' & REDS & EQ'). auto. exists s'; split. + eapply star_step. apply red_while_loop. cbn. rewrite EQ. apply Z.leb_le. lia. eapply star_step. apply red_seq_step. apply red_seq_step. apply red_assign. eapply star_step. apply red_seq_step. apply red_seq_done. eapply star_step. apply red_seq_step. apply red_assign. eapply star_step. apply red_seq_done. cbn. replace (s "x" - 1) with v by lia. apply REDS. + rewrite EQ'. cbn. lia. } intros. eapply REC; eauto. lia. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)