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!