help with a PR?

Stream: maths

[Matias Heikkilä]

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ä]

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]

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]

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).