Strange push_neg behaviour

Stream: mathlib4

[Sophie Morel]

I've been having some trouble recently with push_neg (and hence also contrapose!) in Lean4. I was always able to fix my proofs by using more targeted rewrites with lemmas like not_exists etc, but I'm wondering if there is a better way to fix the problem. Here is a MWE:

import Mathlib.Tactic
import Mathlib.Init.Algebra.Order

variable {α : Type _}

example (r : LinearOrder α) (s : Preorder α) (a b : α) : ¬(s.lt a b → r.lt a b) := by
  push_neg -- now the goal is s.lt a b ∧ s.le b a !

/- Error message:
application type mismatch
  id
    (Eq.trans (Mathlib.Tactic.PushNeg.not_implies_eq (a < b) (a < b))
      (congrArg (And (a < b)) (Mathlib.Tactic.PushNeg.not_lt_eq a b)))
argument has type
  (¬(a < b → a < b)) = (a < b ∧ b ≤ a)
but function has type
  (¬(a < b → a < b)) = (a < b ∧ b ≤ a) → (¬(a < b → a < b)) = (a < b ∧ b ≤ a)
-/

So push_neg changed the goal into something that is not equivalent, but it also generated an error so I didn't end up writing a wrong proof. (It did stump me for quite a while before I realized what was going on, because in my original example the push_neg was hidden in a contrapose! in the middle of a long proof, and the error message told me that the problem was at the beginning of the statement.)
Does anybody know what is going on here ?

[Yury G. Kudryashov]

push_neg is a mathlib tactic, so I moved the thread here.

[Yury G. Kudryashov]

Probably, push_neg doesn't work well when you have two *Order instances that don't agree with each other.

[Kyle Miller]

push_neg knows about LT.lt and so on and it synthesizes some LinearOrder instances to make some conversions. It's not expecting that you have overlapping instances like this. Do you mean to have a separate Preorder? This comes from the LinearOrder.

variable [LinearOrder α]
#synth Preorder α

[Sophie Morel]

Unfortunately I'm proving stuff about the set of (total) preorders on a type, so I don't really have a choice...

[Yury G. Kudryashov]

push_neg can try to unify LT.lt from generated LinearOrder with the one it sees.

[Sophie Morel]

(In fact, in my original proof I had at least four different orders floating around.)

[Yury G. Kudryashov]

@Frédéric Dupuis fixed one bug in this code some time ago (push_neg tried to apply not_lt on a partial order)

[Sophie Morel]

Yury G. Kudryashov said:

push_neg can try to unify LT.lt from generated LinearOrder with the one it sees.

Is there any way for me to tell push_neg not to do that ? At this point I have to avoid it in a lot of proofs.

[Yury G. Kudryashov]

There is a way: open the source code in Mathlib/Tactic/PushNeg.lean and fix it.

[Kyle Miller]

I'm looking into it right now

[Yury G. Kudryashov]

Unfortunately, I'm not good enough with Lean 4 meta programming to do it.

[Sophie Morel]

Yury G. Kudryashov said:

There is a way: open the source code in Mathlib/Tactic/PushNeg.lean and fix it.

Okay, or I could juste use rw ! :grinning_face_with_smiling_eyes:

[Sophie Morel]

My knowledge of Lean4 metaprogramming is nil...

[Sophie Morel]

Kyle Miller said:

I'm looking into it right now

Thanks Kyle !

[Kyle Miller]

@Sophie Morel It still needs to pass CI, but here's a fix: mathlib4#4478

[Sophie Morel]

Wow !