Stream: new members

Topic: How to use unique existence?

Rui Liu (Nov 11 2020 at 20:26):

Let's say we define the unique existence in the following way:

def unique (S: Type) (P: S → Prop) : Prop := (∃ x:S,P x) ∧ (∀ x y: S, (P x ∧ P y) → x = y)

Now I should be able to get from a proof of h: unique(S, P) to the object s: S and the proof p: P s. How do I get to it?

Chris B (Nov 11 2020 at 21:04):

You can use the recursor, or one of the "sugar-added" approaches to using the recursor.

theorem use_unique (S : Type) (P : S -> Prop) : unique S P -> true
| (and.intro (Exists.intro s p) _) := trivial

theorem use_unique' (S : Type) (P : S -> Prop) : unique S P -> true
| ⟨⟨s, h⟩, _ := trivial

-- directly using recursor
theorem use_unique'' (S : Type) (P : S -> Prop) (h : unique S P) : true :=
Exists.rec_on (h.elim_left) (λ s p_of_s, trivial)

The recursor for Exists can only eliminate into Prop though, so something that directly extracts them is going to be noncomputable AFAIK. See classical.indefinite_description.

Yakov Pechersky (Nov 11 2020 at 21:12):

However, there is docs#finset.choose where a unique existence hypothesis can be used to generate a term of a type.

Kevin Buzzard (Nov 11 2020 at 21:51):

Yes this is noncomputable in general; classical.some is exactly the function you want, or if you're in tactic mode you can use choose (although beware the docstring, it covers a more general usage)

Rui Liu (Nov 11 2020 at 21:58):

Kevin Buzzard said:

Yes this is noncomputable in general; classical.some is exactly the function you want, or if you're in tactic mode you can use choose (although beware the docstring, it covers a more general usage)

classical.some seem to only give me s: S but not p: P s. Is there a way to get the proof of P s?

Oh actually never mind, I can see there's classical.some_spec. Thank you!

Rui Liu (Nov 11 2020 at 22:02):

@Chris B @Kevin Buzzard Out of curiosity, what do you mean by it's not computable? Is it because we can proof of the existence may already use classical logic?

Kevin Buzzard (Nov 11 2020 at 22:18):

https://xenaproject.wordpress.com/2019/06/11/the-inverse-of-a-bijection/

Kevin Buzzard (Nov 11 2020 at 22:19):

I was very surprised by this at first. There are computable bijections with noncomputable inverses.

Chris B (Nov 11 2020 at 22:59):

Rui Liu said:

Chris B Kevin Buzzard Out of curiosity, what do you mean by it's not computable? Is it because we can prove of the existence may already use classical logic?

The definition in the manual is pretty good: "Functions that make use of choice to produce data are incompatible with a computational interpretation, and do not produce bytecode. They have to be declared noncomputable".

The issue is that theorems like indefinite_description use classical.choice to turn your Exists into something that might be in Type.

Mario Carneiro (Nov 11 2020 at 23:18):

Unlike in ZFC, in lean there is no advantage to definite description over indefinite description. They are equally nonconstructive

Last updated: May 06 2021 at 22:13 UTC