proposition: Lemma triple_while: forall P variant b c, (forall v, [[ atrue b //\\ aequal variant v //\\ P]] c [[ alessthan variant v //\\ P]]) -> [[ P ]] WHILE b c [[ afalse b //\\ P ]].
proof: Proof. intros P variant b c TR. assert (REC: forall v, [[ aequal variant v //\\ P ]] WHILE b c [[ afalse b //\\ P ]]). { induction v using (well_founded_induction (Z.lt_wf 0)). intros R IND s h PRE. assert (IND1: independent_of R (modified_by c)). { red; intros; apply IND with s1; auto. } destruct (beval b s) eqn:B. - destruct (TR v R IND1 s h) as (s1 & h1 & EXEC1 & POST1). rewrite lift_simple_conj. split; auto. rewrite lift_simple_conj in POST1. destruct POST1 as (LT & POST1). destruct (H (aeval variant s1) LT R IND s1 h1) as (s2 & h2 & EXEC2 & POST2). rewrite lift_simple_conj. split; auto. red; auto. exists s2, h2; split; auto. eapply star_step. apply red_while_loop. auto. eapply star_trans. apply star_red_seq_step. eexact EXEC1. eapply star_step. apply red_seq_done. exact EXEC2. - rewrite lift_simple_conj in PRE. destruct PRE as (EQ & POST1). exists s, h; split. + apply star_one. apply red_while_done. auto. + rewrite lift_simple_conj. split; auto. } intros R IND s h PRE. apply (REC (aeval variant s) R IND s h). rewrite lift_simple_conj. split; auto. red; auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)