Replacing "true = false"

Using Coq
1

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!

2

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.

3

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.
4

@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. :slight_smile:

@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!