proposition: Theorem HoareWhileRule : forall (P:state->Prop)(b:bExp)(i:inst)(s s':state), (forall s1 s2:state, P s1 -> evalB s1 b = Some true -> exec s1 i s2 -> P s2)-> P s -> exec s (WhileDo b i) s' -> P s' /\ evalB s' b = Some false.
proof: Proof. intros P b i s s' H. cut (forall i':inst, exec s i' s' -> i' = WhileDo b i -> P s -> P s' /\ evalB s' b = Some false); eauto. intros i' Hexec; elim Hexec; try (intros; discriminate). intros s0 i0 e Heval Heq; injection Heq; intros H1 H2. match goal with | id:(e = b) |- _ => rewrite <- id; auto end. intros; match goal with | id:(_ = _) |- _ => injection id; intros H' H'' end. subst i0 b;eauto. Qed.
imports: ZArith List Arith Lia Zwf Relations JMeq List Vector