Zulip Chat Archive

Stream: Is there code for X?

Topic: recovering from an `exists`


view this post on Zulip Scott Morrison (Jun 19 2020 at 14:12):

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?

view this post on Zulip Reid Barton (Jun 19 2020 at 14:15):

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

view this post on Zulip Reid Barton (Jun 19 2020 at 14:15):

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

view this post on Zulip Reid Barton (Jun 19 2020 at 14:16):

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

view this post on Zulip Scott Morrison (Jun 19 2020 at 14:22):

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?"

view this post on Zulip Scott Morrison (Jun 19 2020 at 14:22):

Okay, I have a horrible proof now!

view this post on Zulip David Wärn (Jun 19 2020 at 16:31):

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⟩⟩

view this post on Zulip Scott Morrison (Jul 13 2020 at 00:59):

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

view this post on Zulip Mario Carneiro (Jul 13 2020 at 01:01):

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

view this post on Zulip Scott Morrison (Jul 13 2020 at 01:06):

Yes!

view this post on Zulip Scott Morrison (Jul 13 2020 at 01:06):

I'll get to it eventually. :-)


Last updated: May 16 2021 at 05:21 UTC