proposition: Lemma HoareWhileRule_aux : forall (P:state->Prop)(b:bExp)(i:inst)(s s':state), exec s (WhileDo b i) s' -> (forall s1 s2:state, P s1 -> evalB s1 (get_test_from_while b (WhileDo b i)) = Some true -> exec s1 (get_body_from_while (WhileDo b i)) s2 -> P s2)-> P s -> P s' /\ evalB s' (get_test_from_while b (WhileDo b i)) = Some false.
proof: Proof. intros P b i s s' Hexec. generalize (I:is_while (WhileDo b i)). elim Hexec;try(auto;simpl; intros; contradiction). simpl. intros s0 s1 s2 i0 e Heval Hexec1 IH1 Hexec2 IH2 _ IH_invariant HP. apply IH2;auto. apply IH_invariant with s0;auto. Qed.
imports: ZArith