by_contra performance

Stream: general

[Bolton Bailey]

Here is a performance issue that is causing me problems.

import data.finsupp.basic

section

universe u

parameter {F : Type u}
parameter [field F]

lemma test2 (A_β B_β A_α B_α : F) (h3 : B_β * A_β = 0)
(h4: B_α = 0)
(h2: A_α * B_β = 1)
(h5: B_β = 0 ∨ A_β = 0)
: A_β = 0  :=
begin
  by_contra,
end

end

Working in VSCode on my laptop, it takes a full 50 seconds for the by_contra tactic to finish processing. What is going on here?

[Bolton Bailey]

To explain what I mean more

begin
  apply by_contra,
  intro,
  -- by_contra,
end

Runs in less than a second. It feels like this should be equivalent to the tactic form, but something must be going on.

[Patrick Massot]

This is clearly a decidability issue.

[Patrick Massot]

Try adding open_locale classical before the lemma

[Patrick Massot]

Or maybe classical as the first proof line

[Bolton Bailey]

open locale classical makes it much faster yes

[Yaël Dillies]

The thing is that by_contra requires decidability of the proposition you're proving, so it first tries to prove that decidability by typeclass inference. But that takes an awful while because it doesn't find anything, and it eventually falls onto excluded middle.

[Bolton Bailey]

It doesn't seem like it requires decidability to me. https://leanprover-community.github.io/mathlib_docs/logic/basic.html#by_contra doesn't say anything about requiring decidability.

[Bryan Gin-ge Chen]

That's the theorem by_contra, but you're using a tactic: https://leanprover-community.github.io/mathlib_docs/tactics.html#by_contra%20/%20by_contradiction

[Bolton Bailey]

The docs do say, though, that the tactic version requires decidability. Why should this be the case?

[Bolton Bailey]

In other words, why isn't the by_contra tactic equivalent to apply by_contra, intro,?

[Patrick Massot]

Who can pretend to understand constructivists?

[Patrick Massot]

https://github.com/leanprover-community/lean/blob/a5822ea47ebc52eec6323d8f1b60f6ec025daf99/library/init/meta/tactic.lean#L1477-L1483 :shrug:

[Bolton Bailey]

Probably my import I guess

[Kevin Buzzard]

@Ashvni Narayanan this is the issue you discovered about two weeks ago, which is still on my job list to ask about here -- looks like I no longer need to.

[Mario Carneiro]

50 seconds to fail to prove decidable_eq F where field F sounds pretty extreme though. Using open_locale classical is probably the best workaround for this, but no typeclass search should be that bad