issue !4#994: decide regression

Stream: triage

[Random Issue Bot]

Today I chose issue 994 for discussion!

decide regression
Created by @Scott Morrison (@semorrison) on 2022-12-13
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose issue #994 for discussion!

decide regression
Created by @Kim Morrison (@kim-em) on 2022-12-13
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Kyle Miller]

This is the "decide doesn't support free variables in the goal anymore" issue.

I think this won't be supported, even under an option. It makes decide really sensitive to the exact definitions of the decidable instances. It's possible to write of_decide_eq_true rfl manually to go ahead anyway, and notice that it succeeds for the example from the mathlib issue, but the second fails.

example (k : ℕ) : ¬ (k + 2 : ℤ) < 2 := of_decide_eq_true rfl -- succeeds
example (k : ℕ) : ¬ (2 + k : ℤ) < 2 := of_decide_eq_true rfl -- error: application type mismatch

We also have omega now, which proves both.

[Johan Commelin]

So shall we close this?

[Patrick Massot]

Can we take this as a documentation opportunity? Or is it already clearly documented in the doc of decide? Then I think we can close.