用Prop代替bool的常见策略 [英] coq tactic for replacing bools with Prop

问题描述

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的常见策略的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！