Interaction of abel with casting

Stream: mathlib4

[Heather Macbeth]

Another failure in an abel proof, the one I was trying to isolate when I discovered
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Non-local.20behaviour.20in.20.60abel.60
Here I am working on top of Mario's bugfix mathlib4#1394.

import Mathlib.Tactic.Abel

variable [Ring α]

example (a : α) (b : ℕ) (f : α → α) :
    ∃ z : ℤ, f a * b - f (a * b) = z := by
  induction' b with c hc
  . sorry
  . rcases hc with ⟨z, hz⟩
    rw [Nat.succ_eq_add_one, Nat.cast_add, mul_add, mul_add, Nat.cast_one, mul_one, mul_one]
    have H : ∃ y : ℤ,  f (a * c + a) - f (a * c) - f a = y := sorry
    rcases H with ⟨y, hy⟩
    use z - y
    rw [Int.cast_sub, ← hz, ← hy]
    abel -- does not resolve goal
    done

lemma provable_by_abel (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 : α) (b : ℕ) (f : α → α) :
    ∃ z : ℤ, f a * b - f (a * b) = z := by
  induction' b with c hc
  . sorry
  . rcases hc with ⟨z, hz⟩
    rw [Nat.succ_eq_add_one, Nat.cast_add, mul_add, mul_add, Nat.cast_one, mul_one, mul_one]
    have H : ∃ y : ℤ,  f (a * c + a) - f (a * c) - f a = y := sorry
    rcases H with ⟨y, hy⟩
    use z - y
    rw [Int.cast_sub, ← hz, ← hy]
    apply provable_by_abel -- works

[Heather Macbeth]

Short version: abel can't resolve the goal, but a lemma which is provable by abel can resolve the goal.

I have tried to make this example smaller, but it's quite fiddly.

If you look at the goal state right before the abel call you'll see that some casts are @Nat.cast α AddMonoidWithOne.toNatCast and some casts are @Nat.cast α NonAssocRing.toNatCast, so maybe the rw [Nat.cast_add], which introduces this casting discrepancy, is the culprit. And if so, maybe the problem is not abel but our casting yoga. However, I wasn't able to make a smaller example where abel failed because of a casting discrepancy like that.

[Heather Macbeth]

Also note that neither norm_cast nor push_cast normalize away the AddMonoidWithOne.toNatCast/NonAssocRing.toNatCast discrepancy.

[Heather Macbeth]

Another apparent abel issue -- possibly the same:

import Mathlib.Tactic.Abel

variable [AddCommGroup α]

example (p q r s : α) : s + p - q = s - r - (q - r - p) := by abel -- works

example : True := by
  have H : ∀ (p q r s : α), s + p - q = s - r - (q - r - p) := by
    intro p q r s
    abel -- fails
    sorry
  sorry

Again I'm working on top of mathlib4#1394.

[Heather Macbeth]

This one looks kind of like yesterday's linarith bug
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.9C.94.20linarith.20failure
in that it has different behaviour when variables/hypotheses are introduced a proof than when they exist at the start of the proof.

[Mario Carneiro]

it's another missing withMainContext, I pushed a fix to the same PR

[Heather Macbeth]

@Mario Carneiro Thanks! That indeed fixes the previous issues.

Do you want to complete an abel fix hat trick?

import Mathlib.Tactic.Abel

variable [AddCommGroup α]

-- works
example (x y z : α) : y = x + z - (x - y + z) := by
  abel
  done

-- fails
example (x y z : α) : y = x + z - (x - y + z) := by
  have H : True := by sorry
  abel
  done

(working on top of the latest mathlib4#1394).

[Mario Carneiro]

fixed

[Heather Macbeth]

Btw, what does reduce the goal before testing for equality mean in your commit message about this fix?

[Mario Carneiro]

the problem was that the goal is not y = x + z - (x - y + z), it is mdata(noImplicitLambda) (y = x + z - (x - y + z)) so we have to remove the mdata node before testing if it is an equality

[Mario Carneiro]

it's generally a good idea to use whnfR before anything that literally pattern matches on an expression to skip things like mdata and abbreviations (unless you are specifically looking for the abbreviation or metadata)

[Heather Macbeth]

All abel calls in mathlib4#1304 work now!
https://github.com/leanprover-community/mathlib4/commit/898249c56c1b5c9c50eaa66a34c15de7cb916b51