noncomputable if

Stream: general

[Reid Barton]

I sort of wish we had two ifs, one defined in terms of decidable like the built-in one, and a noncomputable one defined in terms of choice. That way we would never have to worry about which proof of decidability appears in the statements of lemmas. Is this crazy?

[Reid Barton]

Thinking of lemmas such as s.prod (λ x, (ite (a = x) b 1)) = ite (a ∈ s) b 1: of course the lemma is true whether or not the evidence of decidable (a = x) has anything to do with the evidence of decidable (a ∈ s), but the lemma statement might require them to be related in a specific way (depending on exactly what instance parameters it assumes).

[Reid Barton]

This is also in the spirit of "classical semantics, computable algorithms specified in terms of them"

[Reid Barton]

Well, it's also the case that it's possible to write these lemmas in a way that they can be applied in any situation, regardless of the choices of decidable instances. It's just really awkward to do so.

[Mario Carneiro]

it seems like this is a failing of rewriting and congr stuff to not be able to properly ignore decidable args

[Reid Barton]

Or subsingletons in general. Though it is also nice to just be able to apply things, without tactics.

[Mario Carneiro]

you don't usually apply an equality

[Mario Carneiro]

lean's term mode handling of congruence is pretty anemic

[Mario Carneiro]

for some reason congr thinks it's best to create congr lemmas on the fly all the time, even though there is only one for each definition so they could easily be auto-generated with the definition