proposition: Lemma Triple_while: forall P variant b c, (forall v, [[ P //\\ atrue b //\\ aequal variant v ]] c [[ P //\\ alessthan variant v ]]) -> [[P]] WHILE b c [[P //\\ afalse b]].
proof: Proof. intros P variant b c T. assert (REC: forall v s, P s -> aeval variant s = v -> exists s', cexec s (WHILE b c) s' /\ (P s' /\ beval b s' = false)). { induction v using (well_founded_induction (Z.lt_wf 0)). intros. destruct (beval b s) eqn:B. - destruct (T v s) as (s1 & EXEC1 & (PS1 & LT1)). unfold aand, aequal, atrue; auto. destruct (H _ LT1 s1 PS1) as (s2 & EXEC2 & PS2). auto. exists s2; split; auto. apply cexec_while_loop with s1; auto. - exists s; split; auto. apply cexec_while_done; auto. } intros s PRE. apply REC with (v := aeval variant s); auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)