Skip to content

Instantly share code, notes, and snippets.

@mukeshtiwari

mukeshtiwari/while_break_true.v

Created October 21, 2016 06:31
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save mukeshtiwari/e4a19f08114658c21ea703ad11f3bc41 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save mukeshtiwari/e4a19f08114658c21ea703ad11f3bc41 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
while_break_true.v
Theorem while_break_true : forall b c st st',
(WHILE b DO c END) / st \\ SContinue / st' ->
beval st' b = true ->
exists st'', c / st'' \\ SBreak / st'.
Proof.
intros. remember (WHILE b DO c END) as Hloop.
induction H; try (inversion HeqHloop); subst.
congruence. apply IHceval2. auto. auto.
apply IHceval.
b : bexp
c : com
st, st' : state
H0 : beval st' b = true
H1 : c / st \\ SBreak / st'
IHceval : c = (WHILE b DO c END) ->
beval st' b = true -> exists st'' : state, c / st'' \\ SBreak / st'
H : beval st b = true
HeqHloop : (WHILE b DO c END) = (WHILE b DO c END)
============================
c = (WHILE b DO c END)
subgoal 2 (ID 626) is:
beval st' b = true
@mukeshtiwari
Copy link
Author

mukeshtiwari commented Oct 21, 2016

Complete source code https://github.com/mukeshtiwari/Coq/blob/master/software-foundation-8.5/Imp.v

@cmangin
Copy link

cmangin commented Oct 21, 2016

Rather than applying IHceval, you can just do exists st.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment