From 1c97e1a3899aa7044b65d65cd446a94ee4374cb7 Mon Sep 17 00:00:00 2001 From: Samuel Gruetter Date: Wed, 1 Apr 2020 21:49:00 -0400 Subject: [PATCH] explain hoare_triple_big_step_while --- HoareLogic.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/HoareLogic.v b/HoareLogic.v index 2ddf399..74a62a0 100644 --- a/HoareLogic.v +++ b/HoareLogic.v @@ -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