boolean - 用 Prop 替换布尔值的 coq 策略

Question

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

如果没有，我怎么写一个？

Answer 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.