decidable instances in indicator lemmas

Stream: general

[Floris van Doorn]

I just saw #13834 by @Eric Wieser and I'm curious why we are doing this.
We rarely have [decidable (a ∈ s)], I guess the main examples are (co)finite sets on types with decidable equality.
The PR shows that this leads to quite some cases where you have to add an extra classical to the argument. And we've had some times-outs when checking decidable (but maybe that was only for decidable equality?)
In a few cases, you might actually be able to have a decidable instance, but there are many ways you can still solve your goal (congr, convert, simp, simp_rw, split_ifs, ...). Sure, it is confusing, but I think it will be confusing more often when you're missing a classical in your environment (and note that we're almost always rewriting from left-to-right with docs#set.indicator_apply, so there usually won't be any trouble unifying the LHS with your expression).

Similar remarks apply to #11708. I was helping @Ashvni Narayanan yesterday adopting the suggested comments, and it seems weird to me to consider whether decidable (a ∈ U) when U is a clopen set in a topological space. Sure, it might happen a couple of times, but it will not be relevant the vast majority of times. I thought we were moving away from such "constructive" considerations?

[Eric Wieser]

This was following what I've seen called "Yury's rule", which essentially states "never write a lemma that mentions a specific decidable instance when you could mention a generic one"

[Anne Baanen]

(That rule applies to any class living in Type, in particular fintype.)

[Floris van Doorn]

I agree that rule is generally good to follow.
Do we want to follow this rule this strictly?
In this case we rarely have a decidable instance and the decidable instance only occurs in the RHS of a lemma that you'll almost always use to rewrite left-to-right.
But maybe always following the rule is easier.
(cc @Yury G. Kudryashov)

[Yury G. Kudryashov]

In any case, I don't understand why do we need all these letI in #13834. What's wrong with open_locale classical? You can still add [decidable _] arguments when you need them.

[Yury G. Kudryashov]

E.g., rw [indicator] should work without classical.

[Yury G. Kudryashov]

Same question about the code using indicator: why not open_locale classical?

[Eric Wieser]

The danger with open_locale classical is that it encoruages you to forget to write your lemmas with the appropriate decidable assumptions

[Eric Wieser]

If I finished my linter for that then I guess it wouldn't matter

[Gabriel Ebner]

but there are many ways you can still solve your goal ([...] simp, simp_rw, [...])

I just want to point out that simp and simp_rw (in general) don't solve goals with different (non-canonical) decidable instances. Think for example about ite p 0 1 = ite p 0 1, simp won't solve this, and simp_rw [eq_self_iff_true] won't crack it either.

[Eric Rodriguez]

I thought this was the point of your new congr changes for simp recently?

[Gabriel Ebner]

Before the congruence lemma change, simp would introduce non-canonical decidable instances. (So it was impossible to avoid them.) But the change won't help if there are already non-canonical decidable instances in the input formula (or in the rhs of a simp lemma).

[Floris van Doorn]

Oh, good to know. Thanks for the correction!

[Yury G. Kudryashov]

Eric Wieser said:

The danger with open_locale classical is that it encoruages you to forget to write your lemmas with the appropriate decidable assumptions

AFAIR, @Mario Carneiro suggested the following trick:

1. Disable open_locale classical.
2. Add [decidable*] assumptions to all lemmas that have errors in their statements (not proofs).
3. Restore open_locale classical.
4. Fix any proofs, if needed.

[Eric Wieser]

Yes, that works as a way to fix things but doesn't really help prevent new mistakes being introduced

[Sebastien Gouezel]

Can we hack something so that begin ... end opens classical, so that it would be available in the proofs (at least tactic proofs) but not in statements? On second thought, it's probably way too hacky though.

[Yaël Dillies]

This is bad still, because classical in proofs can introduce bad decidable instances.

[Eric Wieser]

I think the problem with tactic#classical is it introduces the instance with too high a priority

[Yaël Dillies]

It already happened to me that I had to replace classical why haveI := classical.dec_eq α to avoid poisoning other types with conflicting decidability instances.

[Yaël Dillies]

Yeah everything would work better if classical and open_locale classical weren't synonyms for "Poison me now".

[Eric Wieser]

The former is "poison my proof", the latter is "poison my statement but make my proof easier"

[Eric Wieser]

We need something in between

[Yaël Dillies]

The second can also poison your proof.

[Eric Wieser]

Do you have a #mwe?

[Eric Wieser]

Regarding "the priority is too strong"; can docs#tactic.set_basic_attribute be used to locally enable an instance?

[Eric Rodriguez]

I've definitely found many proofs where I had to replace classicalwith letI := classical.dec_eq X

[Eric Rodriguez]

Also, this hack wouldn't work for lean4 as there's no begin/end

[Eric Wieser]

What does lean4 use as a marker to enter tactic mode?

[Eric Wieser]

I read the begin / end comment as "when in tactic mode", which should work just fine in lean 4

[Eric Rodriguez]

It's just by, iirc. I think a beginc/byc may be nice though.

[Eric Wieser]

I think if we can fix the bad behavior of docs#tactic.classical tactic this mostly becomes moot

[Eric Rodriguez]

I mean, golfing is always nice :)

[Eric Rodriguez]

more mathematician-mode is always good

[Mario Carneiro]

re: lean4, why isn't by classical; ... sufficient?

[Reid Barton]

How can a proof be poisoned?

[Yaël Dillies]

It can if you're constructing an object internal to the proof.

[Eric Wieser]

Eric Wieser said:

Regarding "the priority is too strong"; can docs#tactic.set_basic_attribute be used to locally enable an instance?

Let's see if this works: #14122

[Eric Wieser]

CI seems to pass locally, and this tidies up a handful of weird congrs in proofs

[Eric Wieser]

Interestingly a bunch of uses of classical really just meant resetI