4

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?

pjm
  • 269
  • 1
  • 8

1 Answers1

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.

cbl
  • 101
  • 1
  • 3
  • Thanks! Following your suggestion I came up with the following tactic which still take advantage of the rewriting engine (efficient at selecting sub-terms except under if-then-else...): `Ltac ite_rewrite Hr := rewrite Hr || match goal with | |- context [ if _ then _ else _ ] => rewrite if_then_else_rewrite; [ | ite_rewrite Hr; reflexivity | ite_rewrite Hr; reflexivity ] | _ => idtac end.` (after changing implications with equivalences in `if_then_else_rewrite`) – pjm Apr 29 '21 at 14:29
  • Yeah that is better ! You may find it useful at some point that the tactic create new goals that are not solved immediately (i.e. where `reflexivity` is not enough), so you can do your rewrites and have still complex proofs for the rewrite without expliciting them before (forward reasoning tend to be more fragile to definition/lemma changes). – cbl Apr 29 '21 at 15:39