Skip to content

Instantly share code, notes, and snippets.

@yoshihiro503

yoshihiro503/WHILE_true.v

Created December 28, 2013 06:49
Show Gist options
  • Save yoshihiro503/8156768 to your computer and use it in GitHub Desktop.
Save yoshihiro503/8156768 to your computer and use it in GitHub Desktop.
Download ZIP
Equiv_Jの練習問題 WHILE_true ref: http://qiita.com/yoshihiro503/items/260b9342ab049778ef11
Raw
WHILE_true.v
Theorem WHILE_true: forall b c,
bequiv b BTrue ->
cequiv
(WHILE b DO c END)
(WHILE BTrue DO SKIP END).
Proof.
move => b c H.
unfold cequiv => st st'.
split => HH.
- destruct(WHILE_true_nonterm b c st st' H). by assumption.
- destruct(WHILE_true_nonterm BTrue SKIP st st').
- unfold bequiv. by reflexivity.
- by assumption.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment