proposition: Lemma triple_ifthenelse: forall b c1 c2 P Q, [[ atrue b //\\ P ]] c1 [[ Q ]] -> [[ afalse b //\\ P ]] c2 [[ Q ]] -> [[ P ]] IFTHENELSE b c1 c2 [[ Q ]].
proof: Proof. intros; intros R IND s h PRE. destruct (beval b s) eqn:B. - assert (IND1: independent_of R (modified_by c1)). { red; intros. apply IND with s1; auto. cbn; intros; apply H1; tauto. } destruct (H R IND1 s h) as (s' & h' & EXEC & POST). rewrite lift_simple_conj. split; auto. exists s', h'; split; auto. eapply star_step. apply red_ifthenelse. rewrite B. auto. - assert (IND2: independent_of R (modified_by c2)). { red; intros. apply IND with s1; auto. cbn; intros; apply H1; tauto. } destruct (H0 R IND2 s h) as (s' & h' & EXEC & POST). rewrite lift_simple_conj. split; auto. exists s', h'; split; auto. eapply star_step. apply red_ifthenelse. rewrite B. auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)