Zulip Chat Archive

Stream: general

Topic: noncomputable if


Reid Barton (Oct 23 2019 at 21:58):

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 (Oct 23 2019 at 22:01):

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 (Oct 23 2019 at 22:02):

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

Reid Barton (Oct 23 2019 at 22:25):

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 (Oct 23 2019 at 23:00):

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

Reid Barton (Oct 23 2019 at 23:02):

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

Mario Carneiro (Oct 23 2019 at 23:08):

you don't usually apply an equality

Mario Carneiro (Oct 23 2019 at 23:09):

lean's term mode handling of congruence is pretty anemic

Mario Carneiro (Oct 23 2019 at 23:10):

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


Last updated: Dec 20 2023 at 11:08 UTC