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

Merge pull request #40 from samuelgruetter/hoare_triple_big_step_while

Browse source 
explain hoare_triple_big_step_while
This commit is contained in:
Adam Chlipala 2020-04-02 08:19:54 -04:00 committed by GitHub
commit 75c04e1448
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
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'.
(* Let's prove that the intuitive description given above really applies to this
* predicate. First, a lemma, which is difficult to summarize intuitively!
* More or less precisely this obligation shows up in the main proof below. *)
* predicate. First, a helper lemma which we will need 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,
(forall h v h' v', exec h v c h' v'
-> I h v