How to use unique existence?

Stream: new members

[Rui Liu]

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]

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]

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

[Kevin Buzzard]

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]

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]

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

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

[Kevin Buzzard]

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

[Chris B]

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]

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