Search code examples
booleancoqproof

coq tactic for replacing bools with Prop

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?

Solution

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