用 Prop 替换布尔值的 coq 策略

【问题标题】：coq tactic for replacing bools with Prop用 Prop 替换布尔值的 coq 策略
【发布时间】：2013-06-27 22:27:32
【问题描述】：

coq 中是否有一种证明策略，它采用表达式（andb、orb、implb 等）中的所有布尔运算并将它们替换为命题连接词（and、or、impl）并将布尔变量 x 封装在 Is_true( x) ?

如果没有，我怎么写？

【问题讨论】：

【解决方案1】：

您可以使用重写数据库，例如：

Require Import Setoid.
Require Import Bool.

Lemma andb_prop_iff x y: Is_true (x && y) <-> Is_true x /\ Is_true y.
Proof.
  split; [apply andb_prop_elim | apply andb_prop_intro].
Qed.

Lemma orb_prop_iff x y: Is_true (x || y) <-> Is_true x \/ Is_true y.
Proof.
  split; [apply orb_prop_elim | apply orb_prop_intro].
Qed.

Hint Rewrite
  andb_prop_iff
  orb_prop_iff
  : quotebool.

Goal forall a b c, Is_true (a && b || c && (b || a)).
  intros.
  autorewrite with quotebool.

【讨论】：