Zulip Chat Archive

Stream: maths

Topic: help with a PR?


Matias Heikkilä (May 13 2022 at 10:52):

I've had a PR open for a long time (sorry it's been a crazy few weeks), but I could have another look at it now. Any ideas how to respond to this comment? https://github.com/leanprover-community/mathlib/pull/13487#discussion_r854995513

Matias Heikkilä (May 13 2022 at 10:53):

I think I get the idea, but I'm not sure what to do in practice. Would there be a similar place somewhere else in the code I could use for reference?

Kevin Buzzard (May 13 2022 at 10:55):

In type theory, "there exists a unique function with some property" is a strictly less useful claim than "here is something which produces the function with this property". The suggestion is that instead of proving there exists a unique f, you produce a function which actually spits out f. In type theory you have to do this with the axiom of choice (even if you've proved uniqueness), but this doesn't matter. Instead of having to extract the function from the proof that it exists and is unique, Johan is suggesting that you make the construction and then prove things about the construction.

Kevin Buzzard (May 13 2022 at 10:59):

import tactic

variables {α : Type} (P : α  Prop)

theorem my_existence_proof :  x : α, P x := sorry -- some work to prove something exists

noncomputable def the_actual_thing : α := (my_existence_proof P).some

theorem the_actual_thing.spec : P (the_actual_thing P) := (my_existence_proof P).some_spec

Now you don't ever have to say "the thing exists and is unique and has some property, so we can do cases on this theorem" -- you can actually just use the_actual_thing, and you prove everything you need about it right at the outset, and never use my_existence_proofever again (in your example you'll also need another theorem claiming uniqueness, but this is the point being made).


Last updated: Dec 20 2023 at 11:08 UTC