Bug in by_contra!

Stream: mathlib4

[Violeta Hernández]

Just stumbled across something weird

import Mathlib.SetTheory.Ordinal.Arithmetic

theorem recursion (a : Ordinal) : a = a + 0 := by
  apply le_antisymm
  · by_contra! h
    have := recursion (a + 0) -- looks for a + 0 < a, finds ¬ a ≤ a + 0
    rw [add_zero] at this
    exact h.ne' this
  · rw [add_zero]
termination_by a

[Violeta Hernández]

This doesn't happen if you replace Ordinal by ℕ

[Violeta Hernández]

Do excuse the cheeky proof, but this triggered in a more serious but similar mathematical argument

[Violeta Hernández]

This might be by_contra! at fault, or it might be the termination checker, I don't really know

[Ruben Van de Velde]

decreasing_by simp at h at the end fixes it

[Joachim Breitner]

The issue is related to push_neg. If you replace by_contra! h with by_contra h; push_neg at h you see that the goal that the termination checker sees is the one produced by by_contra.

This is the proof term (the `PreDefinition) that gets passed to the termination checker:

[Elab.definition.wf] replaceRecApps:
      le_antisymm
        (Decidable.byContradiction fun h =>
          let_fun this := recursion (a + 0);
          LT.lt.ne' (Eq.mp (Mathlib.Tactic.PushNeg.not_le_eq a (a + 0)) h)
            (Eq.mp (congrArg (fun _a => _a = _a + 0) (add_zero a)) this))
        (Eq.mpr (id (congrArg (fun _a => _a ≤ a) (add_zero a))) (le_refl a))

For some reason the this is bound outside the work done by push_neg.