# Replacing "true = false"

Hi! I’ve been learning Ltac by scribbling together a tactic that tidies things up for me. In my case, I seem to occasionally wind up with goals of the form `true = false \/ P` that I would like to simplify to just `P`. In order to be robust via compositionality, though, I’d like to tell the tactic to do two things:

• Whenever we see `False \/ P`, use `right` to replace it with `P`
• Whenever we see `Q \/ P`, do work to simplify equalities.

It is, bizarrely enough, this second part that I can’t figure out how to do. Consider this silly toy example:

``````Lemma foo : forall (x : nat), true = false \/ x >= 0.
Proof.
intro x.
``````

I wind up in this proof state:

``````1 goal
x : nat
______________________________________(1/1)
true = false \/ x >= 0
``````

Is there a good way to transform the `true = false` into `False`? (There are obviously a bunch of different ways to prove this silly lemma, but reducing `true = false` to `False` is the crux of my dilemma.)

`rewrite` won’t work here because (IIUC) it only rewrites within equalities. `discriminate` wants to finish the proof. `replace` won’t help because we can’t prove `(true = false) = False`. This feels like a ridiculous thing to ask about, but this problem doesn’t seem particularly conducive to my search engine.

My thanks!

I’m no Ltac expert, but here’s a little MWE I cooked up:

``````Lemma ignore_left : forall (P Q : Prop),
~ P -> Q -> P \/ Q.
Proof. auto. Qed.

Lemma ignore_right : forall (P Q : Prop),
~ Q -> P -> P \/ Q.
Proof. auto. Qed.

Require Import Lia.
Ltac prove_false := auto || lia || discriminate || contradiction.
Ltac ignore_false_branch :=
match goal with
| [|- ?P \/ ?Q] =>
let H := fresh "H" in
(assert (~ P) as H by prove_false; apply ignore_left; auto; clear H) ||
(assert (~ Q) as H by prove_false; apply ignore_right; auto; clear H)
end.

Theorem example : forall n, 0 <= n \/ true = false.
Proof.
intros. ignore_false_branch. (* left with 0 <= n goal *)
lia.
Qed.
``````

This really only does the first part of what you’re asking, but I think strengthening an automatic false-prover is a more approachable task then reducing arbitrary terms into intermediate terms.

The important chunk here is `prove_false`, which you should probably specialize for whatever goals you’re encountering. I just threw some tactics together.

You can use setoid_rewrite with some lemmas:

``````Require Import Setoid Morphisms.

Lemma true_neq_false : true = false <-> False.
Proof. split;intros H;inversion H. Qed.

Lemma false_or_id P : False \/ P <-> P.
Proof. tauto. Qed.

Lemma foo : forall (x : nat), true = false \/ x >= 0.
Proof.
intro x.
setoid_rewrite true_neq_false; setoid_rewrite false_or_id.
(* goal: x >= 0 *)
``````

instead of listing the lemmas in the proof you can also use autorewrite:

``````
Hint Rewrite true_neq_false false_or_id : goalsimpl.

Lemma foo : forall (x : nat), true = false \/ x >= 0.
Proof.
intro x.
autorewrite with goalsimpl.
``````

@SkySkimmer Thanks! This is exactly the information I needed. The documentation on `setoid_rewrite` is a bit sparse in the manual, so I’m a naïve enough user that I missed it.

@caverill It was just the second part that I wasn’t sure how to do, but your solution to the first part uses some techniques that I should definitely learn. Thanks for the example!