本文介绍了用Prop代替bool的常见策略的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！
问题描述
coq中是否有一个证明策略，该表达式将表达式中的所有布尔运算(andb，orb，implb等)都用命题连接词(和，或impl)替换，并将布尔变量x封装在Is_true(x)?
Is there a proof tactic in coq which takes all the boolean operations in an expression (andb, orb, implb, etc) and replaces them with Propositional connectives (and, or, impl) and encapsulates the boolean variables x in Is_true(x) ?
如果没有，我该怎么写?
If not, how can I write one?
推荐答案
您可以使用重写数据库，例如:
You could use a rewrite database, for instance:
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.
这篇关于用Prop代替bool的常见策略的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！