automated bugs

Stream: general

[Damiano Testa]

I wrote a small testing suite for finding common meta-programming bugs. It is quite rudimentary, but it found bugs in abel and in cancel_denoms. I have not used it extensively, but here is the PR, in case someone is curious!

Any comments are very welcome!

#12054

[Damiano Testa]

Here are the two auto-bugs:

import Mathlib.Tactic.CancelDenoms
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Abel

universe u

section cancel_denoms
variable {α : Type u} [LinearOrderedField α] (a b : α)

-- found by automated testing
example (h : a > 0) : a / 5 > 0 := by
  have := 0  -- works if you comment
  cancel_denoms
  exact h

end cancel_denoms

section abel

-- found by automated testing
example [AddCommGroup α] (a b s : α) : -b + (s - a) = s - b - a := by
  have := 0  -- works if you comment
  abel_nf

end abel

[Alex J. Best]

Wow this is very very cool!

[Kim Morrison]

Can we separate out the fixes to tactics in a separate PR?

[Damiano Testa]

Separated:

• #12083 -- cancel_denoms;
• #12084 -- abel.

[Kim Morrison]

Eric just left comments on #12083, and I've :peace_sign:'d #12084.

[Eric Wieser]

I think my comments apply to both; I think we're solving the symptom not the problem here

[Eric Wieser]

The problem is that we're performing syntactic matching when we should almost certainly be performing reducible defeq matching

[Eric Wieser]

In both cases, I think a whnfR, immediately before doing expression matching, is the right approach

[Eric Wieser]

(or switching to use ~q(), but that's a more involved change with more downsides)

[Damiano Testa]

Ok, so at least in one case, this means making a "pure" def into a "monadic" one: is that correct?

[Damiano Testa]

Oh, I see that this is what you wrote in the PR!

[Damiano Testa]

I'm going to wait for #12084 to build and then will merge: if you have anything against it, let me know!

With the fix, abel should work at reducible transparency, which seems to be what everyone wants and there is a test checking this.