pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-28 07:16:20 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

explain hoare_triple_big_step_while

Browse source
This commit is contained in:
Samuel Gruetter 2020-04-01 21:49:00 -04:00
parent 7bc0425ccf
commit 1c97e1a389
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
HoareLogic.v
View file

@ -138,8 +138,10 @@ Inductive hoare_triple : assertion -> cmd -> assertion -> Prop :=
-> hoare_triple P' c Q'. -> hoare_triple P' c Q'.
(* Let's prove that the intuitive description given above really applies to this (* Let's prove that the intuitive description given above really applies to this
* predicate. First, a lemma, which is difficult to summarize intuitively! * predicate. First, a helper lemma which we will need in the main proof below.
* More or less precisely this obligation shows up in the main proof below. *) * It says that if the loop body preserves the invariant, and executing the loop
* terminates, then after executing the loop, the invariant still holds, and the
* loop condition is false. *)
Lemma hoare_triple_big_step_while: forall (I : assertion) b c, Lemma hoare_triple_big_step_while: forall (I : assertion) b c,
(forall h v h' v', exec h v c h' v' (forall h v h' v', exec h v c h' v'
-> I h v -> I h v