Non-local behaviour in `abel`

Stream: mathlib4

[Heather Macbeth]

I am experiencing seemingly non-local behaviour in abel, and wondered if anyone else could reproduce it.

import Mathlib.Tactic.Abel

variable [Ring α]

lemma foo (a c : α) (f : α → α) :
    f a * c + f a - f (a * c + a) = f a * c - f (a * c) - (f (a * c + a) - f (a * c) - f a) := by
  abel

example (a : α) (c : ℕ) (y z : ℤ) (f : α → α)
    (hz : f a * c - f (a * c) = @Int.cast α Ring.toIntCast z)
    (hy : f (a * c + a) - f (a * c) - f a = y) :
    ∃ z : ℤ, f a * ↑(Nat.succ c) - f (a * ↑(Nat.succ c)) = ↑z := by -- HERE
  use z - y
  rw [Nat.cast_succ, mul_add, mul_add, mul_one, mul_one]
  rw [Int.cast_sub, ← hz, ← hy]
  exact foo a c f

example (a : α) (c : ℕ) (y z : ℤ) (f : α → α)
    (hz : f a * c - f (a * c) = @Int.cast α Ring.toIntCast z)
    (hy : f (a * c + a) - f (a * c) - f a = y) :
    ∃ z : ℤ, f a * ↑(Nat.succ c) - f (a * ↑(Nat.succ c)) = z := by
  use z - y
  rw [Nat.cast_succ, mul_add, mul_add, mul_one, mul_one]
  rw [Int.cast_sub, ← hz, ← hy]
  abel -- fails with "Try this ..."
  done

[Heather Macbeth]

Where marked -- HERE, change ↑z to z. On my machine this makes the failure in the next example go away.

[Heather Macbeth]

:ping_pong: This behaviour persists for me today on fresh mathlib. Can anyone else reproduce it?

[Kevin Buzzard]

I can reproduce. Whatever is going on?

[Heather Macbeth]

@Mario Carneiro any ideas? This bug is pretty weird ...

[Heather Macbeth]

I tracked it down as a test case for something experienced by @Anatole Dedecker and me in mathlib4#1304.

[Kevin Buzzard]

import Mathlib.Tactic.Abel

variable [Ring α]

-- -- the evil example: uncomment me to break your definition!
-- example (a : α) (c : ℕ) (y z : ℤ) (f : α → α) :
--     f a * ↑c + f a - f (a * ↑c + a) = ↑(z - y) := by
--   sorry

def foo (a : α) (c : ℕ) (y z : ℤ) (f : α → α)
    (hz : f a * c - f (a * c) = @Int.cast α Ring.toIntCast z)
    (hy : f (a * c + a) - f (a * c) - f a = y) :
    ∃ z : ℤ, f a * ↑(Nat.succ c) - f (a * ↑(Nat.succ c)) = z := by
  use z - y
  rw [Nat.cast_succ, mul_add, mul_add, mul_one, mul_one]
  rw [Int.cast_sub, ← hz, ← hy]
  abel
  done

Live streaming on the discord

[Kevin Buzzard]

this can't happen, right?

import Mathlib.Tactic.Abel

variable [Ring α]

-- -- the evil example: uncomment me to break your definition!
-- example (a : α) (c : ℕ) (y z : ℤ) (f : α → α) :
--     f a * ↑c + f a - f (a * ↑c + a) = ↑(z - y) := by
--   sorry

-- -- I am the antidote -- uncomment me and your definition will work again!
-- def antidote (a : α) (c : ℕ) (y z : ℤ) (f : α → α)
--     (hy: f (a * ↑c + a) - f (a * ↑c) - f a = ↑y)
--     (hz: f a * ↑c - f (a * ↑c) = ↑z) :
--     f a * ↑c + f a - f (a * ↑c + a) = ↑(z - y) := by
--    rw [Int.cast_sub, ← hz, ← hy]
--    abel

def foo (a : α) (c : ℕ) (y z : ℤ) (f : α → α)
    (hz : f a * c - f (a * c) = @Int.cast α Ring.toIntCast z)
    (hy : f (a * c + a) - f (a * c) - f a = y) :
    ∃ z : ℤ, f a * ↑(Nat.succ c) - f (a * ↑(Nat.succ c)) = z := by
  use z - y
  rw [Nat.cast_succ, mul_add, mul_add, mul_one, mul_one]
  rw [Int.cast_sub, ← hz, ← hy]
  abel
  done

[Kevin Buzzard]

I'm assuming others can reproduce. I'm on Ubuntu 20.04.5 LTS

[Kevin Buzzard]

Lean (version 4.0.0-nightly-2023-01-04, commit 905d3204ae08, Release)

[David Renshaw]

I can reproduce the problem too.

[David Renshaw]

Same behavior with just able_nf, with narrows it down a bit I think.

[David Renshaw]

I'm trying looking at the output after doing

set_option trace.abel true
set_option trace.abel.detail true

[Kevin Buzzard]

import Mathlib.Tactic.Abel

variable [Ring α]

-- theorem uncommenting_me_breaks_foo (a : α) (c : ℕ) (f : α → α) : f a * ↑c + f a - f (a * ↑c + a)
--     = f a * ↑c - f (a * ↑c) - (f (a * ↑c + a) - f (a * ↑c) - f a) :=
-- Eq.trans
--   (sorry)
--   (Eq.symm
--     (Mathlib.Tactic.Abel.unfold_sub (f a * ↑c - f (a * ↑c)) (f (a * ↑c + a) - f (a * ↑c) - f a)
--       (Mathlib.Tactic.Abel.termg (-1) (f (a * ↑c + a))
--         (Mathlib.Tactic.Abel.termg 1 (f a) (Mathlib.Tactic.Abel.termg 1 (f a * ↑c) 0)))
--       (Mathlib.Tactic.Abel.subst_into_addg (f a * ↑c - f (a * ↑c)) (-(f (a * ↑c + a) - f (a * ↑c) - f a))
--         (Mathlib.Tactic.Abel.termg (-1) (f (a * ↑c)) (Mathlib.Tactic.Abel.termg 1 (f a * ↑c) 0))
--         (Mathlib.Tactic.Abel.termg (-1) (f (a * ↑c + a))
--           (Mathlib.Tactic.Abel.termg 1 (f (a * ↑c)) (Mathlib.Tactic.Abel.termg 1 (f a) 0)))
--         (Mathlib.Tactic.Abel.termg (-1) (f (a * ↑c + a))
--           (Mathlib.Tactic.Abel.termg 1 (f a) (Mathlib.Tactic.Abel.termg 1 (f a * ↑c) 0)))
--         (Mathlib.Tactic.Abel.unfold_sub (f a * ↑c) (f (a * ↑c))
--           (Mathlib.Tactic.Abel.termg (-1) (f (a * ↑c)) (Mathlib.Tactic.Abel.termg 1 (f a * ↑c) 0))
--           (Mathlib.Tactic.Abel.subst_into_addg (f a * ↑c) (-f (a * ↑c)) (Mathlib.Tactic.Abel.termg 1 (f a * ↑c) 0)
--             (Mathlib.Tactic.Abel.termg (-1) (f (a * ↑c)) 0)
--             (Mathlib.Tactic.Abel.termg (-1) (f (a * ↑c)) (Mathlib.Tactic.Abel.termg 1 (f a * ↑c) 0))
--             (Mathlib.Tactic.Abel.term_atomg (f a * ↑c))
--             (Mathlib.Tactic.Abel.subst_into_negg (f (a * ↑c)) (Mathlib.Tactic.Abel.termg 1 (f (a * ↑c)) 0)
--               (Mathlib.Tactic.Abel.termg (-1) (f (a * ↑c)) 0) (Mathlib.Tactic.Abel.term_atomg (f (a * ↑c)))
--               (Mathlib.Tactic.Abel.term_neg 1 (f (a * ↑c)) 0 (-1) 0 (Eq.refl (-1)) neg_zero))
--             (Mathlib.Tactic.Abel.const_add_termg (Mathlib.Tactic.Abel.termg 1 (f a * ↑c) 0) (-1) (f (a * ↑c)) 0
--               (Mathlib.Tactic.Abel.termg 1 (f a * ↑c) 0) (add_zero (Mathlib.Tactic.Abel.termg 1 (f a * ↑c) 0)))))
--         (sorry)
--         (sorry))))


def foo (a : α) (c : ℕ) (y z : ℤ) (f : α → α)
    (hz : f a * c - f (a * c) = @Int.cast α Ring.toIntCast z)
    (hy : f (a * c + a) - f (a * c) - f a = y) :
    ∃ z : ℤ, f a * ↑(Nat.succ c) - f (a * ↑(Nat.succ c)) = z := by
  use z - y
  rw [Nat.cast_succ, mul_add, mul_add, mul_one, mul_one]
  rw [Int.cast_sub, ← hz, ← hy]
  abel
  done

I need to go now. I took the other route and tried to see which part of the term it was generating was causing the problem. Maybe the above helps? I need to go and make dinner for 4 now though, so I'll be gone a while.

[Kevin Buzzard]

Last few things: when abel fails the goal becomes

f a * ↑c + (f a + -1 • f (a * ↑c + a)) = f a + (f a * ↑c + -1 • f (a * ↑c + a))

so some simp lemma might have kicked in or not kicked in? And even better, abel suggests abel_nf, which closes the goal ;-)

[Kevin Buzzard]

import Mathlib.Tactic.Abel

variable [Ring α]

-- theorem uncommenting_me_breaks_foo (x : α) :
--   -x = (-1 : ℤ) • (x) + (0 : α) := sorry

def foo (a : α) (c : ℕ) (y z : ℤ) (f : α → α)
    (hz : f a * c - f (a * c) = @Int.cast α Ring.toIntCast z)
    (hy : f (a * c + a) - f (a * c) - f a = y) :
    ∃ z : ℤ, f a * ↑(Nat.succ c) - f (a * ↑(Nat.succ c)) = z := by
  use z - y
  rw [Nat.cast_succ, mul_add, mul_add, mul_one, mul_one]
  rw [Int.cast_sub, ← hz, ← hy]
  abel
  done

[Kevin Buzzard]

So abel seems to be using the theorem uncommenting_me_breaks_foo. It turns the goal

f a * ↑c + f a - f (a * ↑c + a) = f a * ↑c - f (a * ↑c) - (f (a * ↑c + a) - f (a * ↑c) - f a)

into the goal

f a * ↑c + (f a + -1 • f (a * ↑c + a)) = f a + (-1 • f (a * ↑c + a) + f a * ↑c)

if uncommenting_me_breaks_foo : -x = (-1 : ℤ) • (x) + (0 : α) is declared, and then it gets lost. It would be interesting to check which tags uncommenting_me_breaks_foo has, I'm assuming none, but you never can tell with Lean 4. I think that now someone who knows something about linarith has to take over.

[David Renshaw]

what does this have to do with linarith?

[Heather Macbeth]

Probably a typo for abel? @Kevin Buzzard

[Mario Carneiro]

abel, unlike ring, does not use a list of atoms as state to deduplicate defeq terms, it uses Expr.quickLt which compares the hashes of the expressions. In particular, this makes it sensitive to changes in FVarId naming, which makes atom ordering nondeterministic. So this explains why a change in an unrelated example can cause the tactic to behave differently.

[Mario Carneiro]

What it doesn't explain is why it doesn't always find the proof, because even if atom ordering is nondeterministic it should still be consistent over a given run

[Mario Carneiro]

Here's the trace from the working invocation (edited for clarity):

[abel] running on an equality `f a * ↑c + f a - f (a * ↑c + a) = f a * ↑c - f (a * ↑c) - (f (a * ↑c + a) - f (a * ↑c) - f a)`.

[abel] found a proof that `f a * ↑c + f a - f (a * ↑c + a) =
    Mathlib.Tactic.Abel.termg (-1) (f (a * ↑c + a))
      (Mathlib.Tactic.Abel.termg 1 (f a * ↑c) (Mathlib.Tactic.Abel.termg 1 (f a) 0))`

[abel] found a proof that `f a * ↑c - f (a * ↑c) - (f (a * ↑c + a) - f (a * ↑c) - f a) =
    Mathlib.Tactic.Abel.termg (-1) (f (a * ↑c + a))
      (Mathlib.Tactic.Abel.termg 1 (f a * ↑c) (Mathlib.Tactic.Abel.termg 1 (f a) 0))`

[abel] verified that the simplified forms are identical

and the trace from the failing version:

[abel] running on an equality `f a * ↑c + f a - f (a * ↑c + a) = f a * ↑c - f (a * ↑c) - (f (a * ↑c + a) - f (a * ↑c) - f a)`.

[abel] found a proof that `f a * ↑c + f a - f (a * ↑c + a) =
    Mathlib.Tactic.Abel.termg 1 (f a * ↑c)
      (Mathlib.Tactic.Abel.termg (-1) (f (a * ↑c + a)) (Mathlib.Tactic.Abel.termg 1 (f a) 0))`

[abel] found a proof that `f a * ↑c - f (a * ↑c) - (f (a * ↑c + a) - f (a * ↑c) - f a) =
    Mathlib.Tactic.Abel.termg 1 (f a * ↑c)
      (Mathlib.Tactic.Abel.termg 1 (f a) (Mathlib.Tactic.Abel.termg (-1) (f (a * ↑c + a)) 0))`

As you can see, the atom ordering is different in the two cases, but the weird part is that the atom ordering is different even just for the two sides of the second equation.

[Mario Carneiro]

mathlib4#1394

[Heather Macbeth]

Thank you Mario.