Coq: rewriting under if-then-else

Question

I sometimes need to apply a simplification in a branch of an if-then-else without destructing the discriminee.

From Coq Require Import Setoid.

Lemma true_and :
  forall P, True /\ P <-> P.
Proof.
  firstorder.
Qed.

Goal (forall (b:bool) P Q, if b then True /\ P else Q).
  intros.
  Fail rewrite (true_and P).
Abort.

In this example rewrite fails (setoid_rewrite too), suggesting to register the following

• "subrelation eq (Basics.flip Basics.impl)": seems fair to me
• "subrelation iff eq": no way!

Why is the rewriting engine so demanding?

Answer 1

I think the rewriting strategies are failing because what you want is not a rewriting, it's a reduction (True /\ P is not technically equal to P). If you want to maintain the if then else statement, I'll suggest the following solution (yet a bit unsatisfactory):

In a Tactics.v file, add the following lemma and ltacs :

Lemma if_then_else_rewrite:
  forall (b: bool) (T1 T2 E1 E2 : Prop),
    (T1 -> T2) ->
    (E1 -> E2) ->
    (if b then T1 else E1) ->
    (if b then T2 else E2).
Proof.
  destruct b; auto.
Qed.

Ltac ite_app1 Th :=
  match goal with
  | H:_ |- if ?b then ?T2 else ?E =>
    eapply if_then_else_rewrite with (E1 := E) (E2 := E);
    [eapply Th | eauto |]
   end.


Ltac ite_app2 Th :=
  match goal with
  | H:_ |- if ?b then ?T else ?E2 =>
    eapply if_then_else_rewrite with (T1 := T) (T2 := T);
    [eauto | eapply Th |]
   end.

Then, when you have a goal with a top-level if then else, you can apply a theorem Th to either the left or right side with ite_app1 Th or ite_app2 Th. For example, you goal would be :

Goal (forall (b:bool) P Q, if b then (True /\ P) else Q).
  intros.
  ite_app1 true_and. (* -> if b then P else Q *)

You'll probably need to fine-tune the ltacs to your needs (apply in the context vs in the goal, etc.), but that's a first solution. Maybe someone can bring more ltac dark magic to solve this in a more general way.