proposition: Theorem thm_hoare_correct : forall P Q c, |- {{P}} c {{Q}} -> |= {{P}} c {{Q}}.
proof: Proof. unfold HoareValid. induction 1. - sauto. - sauto. - sauto inv: BigStep. - sauto inv: BigStep. - intros *. remember (While b Do c). induction 1; qauto inv: BigStep. - sauto unfold: entails. Qed.
imports: Hammer(Tactics Reflect) String Arith Lia Relations