Equiv_Jの練習問題 WHILE_true

3772 ワード

Softwarefoundations ProofCafe Coq ssreflect Coq テキストリンク

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.

Author And Source

この問題について(Equiv_Jの練習問題 WHILE_true), 我々は、より多くの情報をここで見つけました https://qiita.com/yoshihiro503/items/260b9342ab049778ef11

著者帰属：元の著者の情報は、元のURLに含まれています。著作権は原作者に属する。

Content is automatically searched and collected through network algorithms . If there is a violation . Please contact us . We will adjust (correct author information ,or delete content ) as soon as possible .