finset.some

Stream: Is there code for X?

[Yaël Dillies]

I'm trying to show that the type of atoms of finset α is equivalent to α. This is true because the atoms are precisely the singletons. To make this work, I need to extract an element out of a nonempty finset. Can this be made computable? Do we have it? finset.some doesn't exist.

[Floris van Doorn]

I expect we cannot make this computable as long as finset.nonempty is a Prop.

[Anne Baanen]

Why not? It should just be a quotient.lift out of subtype.val right?

[Yaël Dillies]

That's what I think too. You can do induction on the finset, which is the difference with set.

[Anne Baanen]

Wait no, I thought you wanted to extract an element from the atoms. Yeah, this is going to be noncomputable.

[Yaël Dillies]

I do, but I thought this could be computable more generally.

[Anne Baanen]

(finset.univ : finset (fin 2)).filter (λ i, (i = 0 ∧ ¬ riemann_hypothesis) ∨ (i = 1 ∧ riemann_hypothesis)).

[Yaël Dillies]

Eheh, I had in mind finsets that were themselves made computably.

[Anne Baanen]

(Depending on the definition of docs#finset.nonempty this is a full Brouwer-style counterexample showing it is indeed noncomputable for finsets with > 1 elements.)

[Yaël Dillies]

So how do I get the element out of an atom, precisely? Will that also work for set?

[Floris van Doorn]

You can do it if you make "s is an atom" contain data (like { x // x ∈ s}).
If it is a proposition, we can get a similar counterexample to Anne's, by taking the set of minimal elements of Anne's set (which will always be a singleton) (EDIT: oh wait, Anne's set is already a singleton)

[Anne Baanen]

With docs#quot.lift_on it should be possible right? Since taking the head of an list of elements of the underlying multiset will always return the same element.

[Floris van Doorn]

I expect you will need the decidability of (∈ s) at some point...

[Anne Baanen]

Showing there exists a finset containing all elements of { x | (x = 0 ∧ ¬ RH) ∨ (x = 1 ∧ RH) } is noncomputable. But given such a finset you can extract an element without problems.

[Floris van Doorn]

ah, I see what you mean... Yeah, I think you're right.

[Anne Baanen]

In other words, the decidability lives in docs#subtype.fintype.

[Yaël Dillies]

Unfortunately I don't have the luxury of changing the meaning of an atom. I have to work with {a // is_atom a} because I'm proving Birkhoff's representation theorem in the form of FinBoolAlgᵒᵖ ≌ Fintype and atoms is one of the functors. atoms (finset α) ≃ α is the unit (or counit? I never know).

[Anne Baanen]

Basically to do this computably you have to show ∀ (xs ys : list α), is_atom (xs : finset α) → is_atom (ys : finset α) → head xs = head ys → xs = ys, then you should be able to define head on multisets that are atoms via docs#quot.lift, then you restrict this to finsets (which are defined as a subtype of multisets).

[Kyle Miller]

@Yaël Dillies Do you have a proof that atoms have cardinality 1? If so, here's a sloppily-proved definition:

def multiset.from_atom {α : Type*} (m : multiset α) (h : m.card = 1) : α :=
quot.rec (λ (l : list α) (h : multiset.card (coe l) = 1),
  match l, h with
  | [], h := by simpa using h
  | (x :: _), h := x
  end)
begin
  intros a b hab,
  cases a; cases b,
  refl,
  exfalso, have := list.nil_perm.mp hab, injection this,
  exfalso, have := list.perm_nil.mp hab, injection this,
  have : (a_hd :: a_tl : multiset α) = b_hd :: b_tl := multiset.coe_eq_coe.mpr hab,
  simp! [this],
  ext h',
  change multiset.card (b_hd :: b_tl : multiset α) = 1 at h',
  have h'' := h',
  rw [← this] at h'',
  simp [list.length_eq_zero] at h' h'',
  subst_vars,
  simp at this,
  subst_vars,
end m h

def finset.from_atom {α : Type*} (s : finset α) (h : s.card = 1) : α :=
s.val.from_atom h

[Kyle Miller]

As far as I know, there's no way to generically extract an element from an arbitrary nonempty finset: if there is more than one element, which one do you choose?

But if there's precisely one element, then you can dig into the underlying list and extract it computably.

[Yaël Dillies]

I have a draft at #10865

[Kyle Miller]

I see you have is_atom_iff, so that plugs into docs#finset.card_eq_one

[Bhavik Mehta]

You can also do finset.from_atom more directly by using docs#finset.choose

[Yakov Pechersky]

Or you define an arbitrary linear order on the underlying type because it's finite (as seen as the subtype of things in the finset), and sort on those and pick the first one