recovering from an `exists`

Stream: Is there code for X?

[Scott Morrison]

Is it possible to construct

example {α : Type} [fintype α] {P : α → Prop} [decidable_pred P] (h : ∃ a, P a) :
  trunc (Σ' a, P a) :=

by looking through the elems of the fintype?

[Reid Barton]

I think so--basically use subsingleton-ness of trunc to eliminate the quotient in fintype \a to a list of elements

[Reid Barton]

then take the first element satisfying the predicate, which has to exist

[Reid Barton]

The form of your question seems slightly at odds with the stream it's posted in, though :upside_down:

[Scott Morrison]

Hm, okay. :-) I guess I have sometimes use "Is there code for X?" to also include "Does anyone want to proof / sketch for me X?"

[Scott Morrison]

Okay, I have a horrible proof now!

[David Wärn]

import data.fintype.basic
open finset

lemma trunc_of_nonempty_multiset {α} (s : multiset α) : (∃ x, x ∈ s) → trunc α :=
quotient.rec_on_subsingleton s $ λ l h,
  match l, h with
    | [],       _ := false.elim (by tauto)
    | (a :: _), _ := trunc.mk a
  end

lemma trunc_of_nonempty_of_fintype {α} [fintype α] (h : nonempty α) : trunc α :=
trunc_of_nonempty_multiset univ.val (by simp)

example {α : Type} [fintype α] {P : α → Prop} [decidable_pred P] (h : ∃ a, P a) :
  trunc (Σ' a, P a) :=
trunc_of_nonempty_of_fintype $ exists.elim h $ λ a ha, ⟨⟨a, ha⟩⟩

[Scott Morrison]

Just for the record this made it into mathlib as #3166, in data.fintype.basic.

[Mario Carneiro]

Shouldn't this be using subtype instead of Sigma'?

[Scott Morrison]

Yes!

[Scott Morrison]

I'll get to it eventually. :-)