Selecting element from finite type

Stream: Is there code for X?

[Jure Taslak (Slovenia)]

Let's say I have a finite type α. Is there a way to extract/select an element x : α?
I want to prove a lemma of the sort "Either p x holds, or we remove x from α and recursively try the procedure again. Because α is finite, the procedure must halt"

[Johan Commelin]

@Jure Taslak (Slovenia) Do you know the type is nonempty?

[Jure Taslak (Slovenia)]

I know that the following holds: ∃ x, p x but I need a way to extract such an x

[Filippo A. E. Nuccio]

Have you had a look at https://leanprover-community.github.io/mathlib_docs/init/classical.html#classical.some ?

[Eric Wieser]

docs#fintype.choose if you know there is a unique element satisfying p

[Filippo A. E. Nuccio]

Oh, it was finite!

[Filippo A. E. Nuccio]

@Jure Taslak (Slovenia) docs#classical.some helps in case of general types.

[Jure Taslak (Slovenia)]

Aha this choose should do it, thank you.
Edit: aha, the issue is I don't know (and it might not be true) that the x is unique.

[Eric Wieser]

Jure Taslak (Slovenia) said:

Let's say I have a finite type α. Is there a way to extract/select an element x : α?
I want to prove a lemma of the sort "Either p x holds, or we remove x from α and recursively try the procedure again. Because α is finite, the procedure must halt"

It sounds like you're in a proof, so you don't need classical at all, and can just use rcases h where h : ∃ x, p x

[Jure Taslak (Slovenia)]

Yes, I was working with finite types in particular.

[Jure Taslak (Slovenia)]

The problem is, I only have the exsistential quantifier and the rcases tactic gives me the error: "induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop"

[Anne Baanen]

In that case, the tactic#choose allows you to (noncomputably) get such an x.

[Eric Wieser]

It sounds like you might not be proving a lemma after all, but defining a value?

[Jure Taslak (Slovenia)]

Ok using choose works, but it indeed makes the lemma noncomputable.
But since my type α is finite, there should be something like fintype.choose, which doesn't require a unique element satisfying p x right?

[Jure Taslak (Slovenia)]

yes perhaps that is a better way to phrase it, I need a value, satisfying some predicate.

[Reid Barton]

Eric Wieser said:

It sounds like you might not be proving a lemma after all, but defining a value?

Probably defining a value in the course of proving a lemma.

[Eric Wieser]

Jure Taslak (Slovenia) said:

Ok using choose works, but it indeed makes the lemma noncomputable.
But since my type α is finite, there should be something like fintype.choose, which doesn't require a unique element satisfying p x right?

Lemmas can't be noncomputable. If lean is asking you to add the noncomputable keyword, then you should be in a def.

[Jure Taslak (Slovenia)]

I don't want things to be noncomputable, as I eventually want to use typeclasses to make lean compute some examples. But for that I need it to choose an element from a finite type.

[Jure Taslak (Slovenia)]

My naive thinking is to take the underlying set and give it an arbitrary linear order, then take the max element. But perhaps there is a much easier way of doing it.

[David Wärn]

See docs#trunc_sigma_of_exists and adjacent definitions

[Eric Wieser]

Nice find! That should maybe cross-reference fintype.choose