Tactic to Propify a bool expression

Question

Let's say I have bool expressions <bexp> consisting of true, false, variables, eqb andb, orb and negb. When I see an expression of the form bexp = true or bexp = false, I want to convert them to prop expressions involving b = true, ~ b = true, b1 = b2, b1 <> b2, \/ and /\.

I want to do this so that I can use the usual tactic machinery like destruct, etc to handle them.

For example, if I have a hypothesis

H: negb b && b0 || eqb b b0 && lexltb bs1 bs2 = true

I want it to become:

H : (~ b = true /\ b0 = true) \/ (b = b0 /\ lexltb bs1 bs2 = true)

I have tried implementing it this way:

Ltac propify :=
  repeat match goal with
  | [ H : ?b1 || ?b2 = true |- _ ] => apply orb_true_iff in H
  | [ H : ?b1 || ?b2 = false |- _ ] => apply orb_false_iff in H
  | [ H : ?b1 && ?b2 = true |- _ ] => apply andb_true_iff in H
  | [ H : ?b1 && ?b2 = false |- _ ] => apply andb_false_iff in H
  | [ H : negb ?b = true |- _ ] => apply negb_true_iff in H
  | [ H : negb ?b = false |- _ ] => apply negb_false_iff in H
  | [ H : eqb ?b1 ?b2 = true |- _ ] => apply eqb_prop in H
  | [ H : eqb ?b1 ?b2 = false |- _ ] => apply eqb_false_iff in H
  end.

However, this does not achieve this effect, since it only works at the hypothesis level, and does not further simplify parts of hypotheses.

How do I achieve this?

Answer 1

You can use the generalized rewrite tactic (enabled by importing Setoid) to apply iff lemmas under connectives. Use the in * modifier to rewrite both in the goal and in hypotheses.

To keep negb b = true when b is a variable, you need extra care to not indiscriminately rewrite with negb_true_iff. Use the context C [ M ] pattern to match M anywhere within a term (in the goal or in the hypothesis), and is_var to check whether something is a variable.

From Coq Require Import Setoid.
From Coq Require Import Bool.

Ltac propify :=
  repeat first [rewrite
    ?orb_true_iff, ?orb_false_iff,
    ?andb_true_iff, ?andb_false_iff,
    ?eqb_true_iff, ?eqb_false_iff,
    ?negb_false_iff
    in * |
    (* special case for negb_true_iff to not rewrite with variables,
       and to normalize b = false to negb b = true *)
    match goal with
    | [ |- context C [ negb ?e = true ] ] =>
        tryif is_var e then fail (* backtrack *) else rewrite (negb_true_iff e)
    | [ H : context C [ negb ?e = true ] |- _ ] =>
        tryif is_var e then fail (* backtrack *) else rewrite (negb_true_iff e) in H
    | [ b : bool |- _ ] => rewrite (iff_sym (negb_true_iff b)) in *
    end ].

Goal forall b b0 z,
negb b && b0 || eqb b b0 && z = true ->
negb b && b0 || eqb b b0 && z = false.
Proof.
  intros.
  propify.
(* Goal:

b, b0, z : bool
H : negb b = true /\ b0 = true \/ b = b0 /\ z = true

========================= (1 / 1)

(b = true \/ negb b0 = true) /\ (b <> b0 \/ negb z = true)
 *)
```