finite choice / surjectivity of Pi-terms

Stream: maths

[Antoine Chambert-Loir]

I have two questions related to choice.
1) I am working on permutations on finite sets, and at some point, I needed to pick one point per orbit.
I am truly appalled at the prospect of using classical.choice for that, but I couldn't find instances of finite choice (a finite product of nonempty sets is nonempty).
2) In fact, I need to prove that a pi-term has a section, something like this

example (ι : Type*) [fintype ι] {α : Π (i : ι), Type*} (s : Π i, set (α i))
  (hs : ∀ i, (s i).nonempty) : ∃ (a : Π i, α i), ∀ i, a i ∈ s i := sorry

but I was rapidly blocked by the syntax of Lean… How to use use in that context, for example ?

[Johan Commelin]

Do you have fintype instances floating around? Or only finite?

[Johan Commelin]

Because under the hood a fintype carries around a list of elements, and you could probably grab an element out of that.

[Reid Barton]

This probably also needs ι to have decidable equality

[Kevin Buzzard]

existsi can be used instead of use, it's a more primitive version of use (for example existsi _ reliably works, but gives goals with metavariables...)

[Kevin Buzzard]

import tactic

example (ι : Type*) [fintype ι] {α : Π (i : ι), Type*} (s : Π i, set (α i))
  (hs : ∀ i, (s i).nonempty) : ∃ (a : Π i, α i), ∀ i, a i ∈ s i :=
begin
  use (λ i, (hs i).some),
  exact (λ i, (hs i).some_spec),
end

[Kevin Buzzard]

example (ι : Type*) [fintype ι] {α : Π (i : ι), Type*} (s : Π i, set (α i))
  (hs : ∀ i, (s i).nonempty) : ∃ (a : Π i, α i), ∀ i, a i ∈ s i :=
⟨λ i, (hs i).some, λ i, (hs i).some_spec⟩

[Kevin Buzzard]

(or is the point that you _really_ don't want to use AC for some reason?)

[Antoine Chambert-Loir]

Indeed, I _really_ do not want to use AC for those questions, when it's totally irrelevant: you don't use choice to choose an element in a finite product. On the other hand, it would be nice if Lean could detect by itself that this choice does not depend on AC.

[Sebastien Gouezel]

In mathlib, choice is used to prove excluded middle. The philosophy is really to use choice completely liberally, since it makes our life easier.

[Eric Rodriguez]

In some ways, in lean you need choice finitely unless you can construct a deterministic algorithm to choose some member of the finset

[Eric Wieser]

docs#fintype.choose exists, which might be relevant here

[Eric Rodriguez]

So if there's some linear order, you can choose the minimum, you can use fintype.choose if there exists only one as Eric W pointed out

[Eric Rodriguez]

But if there's many identical-looking possible elements, how does a deterministic program choose one?

[Eric Wieser]

docs#quotient.fin_choice is likely also relevant

[Antoine Chambert-Loir]

Sebastien Gouezel said:

In mathlib, choice is used to prove excluded middle. The philosophy is really to use choice completely liberally, since it makes our life easier.

(This reminds me of Bourbaki using choice to define quantifiers…)
About this philosophy, why not ? Except that we're working with a compiler that sometimes requires us to insert decidable predicates.

[Antoine Chambert-Loir]

Eric Wieser said:

docs#quotient.fin_choice is likely also relevant

I precisely had in mind a variant of this function.

[Sebastien Gouezel]

decidable is only relevant when you are writing an algorithm that you would use to compute things. And in this case, avoiding choice is absolutely necessary. Otherwise, just use classical.decidable to make your life easier!

[Eric Rodriguez]

(it also matters because all decidable instances are not subsingletons, so if you use something designed for decidable instances not noticing, it can lead to errors of the form "rw can't find X in the expression f X" (because the first X is @X classical.dec_eq and the second is @X some_other_instance)

[Sebastien Gouezel]

If you need a decidable assumption in a lemma, we all agree that you should have a corresponding typeclass assumption in the lemma, to avoid the issue you are mentioning. I was talking about things you do inside a proof.