At least three elements

Stream: Is there code for X?

[Joachim Breitner]

What is the most natural way to express an assumption stating “A type X has at least three elements”?
Maybe simply card X > 2 (using the a coercion from nat to cardinal)?
In the proof I’ll need to use this to obtain an element that’s different from two given elements of the type.

I see there are similar lemmas cardinal.two_le_iff. Maybe I should add cardinal.three_le_iff

[Johan Commelin]

Is it a finite type?

[Joachim Breitner]

No, that would be too restrictive.

[Johan Commelin]

There is fintype.card and cardinal.mk. The two are different.

[Yaël Dillies]

This same condition came up in our work with Bhavik. I wish there was a very_nontrivial typeclass...

[Johan Commelin]

Would cardinal.three_le_iff generalize to exists_finset_card_of_blabla_foo_bar?

[Johan Commelin]

Where you somehow want to say that if you know m + n ≤ cardinal.mk X and s : finset X has s.card ≤ m then there is a t : finset X with n ≤ t.card and s.disjoint t?

[Johan Commelin]

With may some special casing for n = 1 and n = 2, where you don't get a t : finset X but some hands-on elements

[Joachim Breitner]

Looks reasonable, although pragmatically I think I still want the convenient tree_le_iff' lemma :-D

[Yaël Dillies]

docs#finset.card_eq_three

[Kyle Miller]

This seems somewhat compelling:

def card_ge (α : Type*) (n : ℕ) : Prop := ∃ (s : finset α), s.card = n

especially given the lemma Yael mentioned.

[Yaël Dillies]

I was thinking the same, but as a class.

[Kyle Miller]

A reason I like this is that it's very "local": you don't need there to be any sort of object that's the cardinality of the whole type, you just need to present a finite set with a certain number of elements.

[Kyle Miller]

That seems like a reasonable class to have. Any reason not to have it be a class?

[Yaël Dillies]

Maybe it could be stated with cardinals.

[Johan Commelin]

I think 98% of the use cases will be for natural numbers

[Johan Commelin]

Should this then replace nontrivial?

[Yaël Dillies]

And nonempty? That sounds like a bootstrapping problem.

[Kyle Miller]

I'm not sure there are any theoretical problem to nonempty being in terms of card_ge, but that seems like more trouble than it's worth (the definitions of multiset and finset would have to find their way to core...)

It looks like nontrivial isn't that deep, so it seems replaceable (it could be an abbreviation)

[Reid Barton]

A class?? :scream_cat: Can someone who understands explain this to me?

[Adam Topaz]

nonempty (fin 3 ↪ α)

[Kyle Miller]

@Reid Barton Just some overengineering for the handful of cases that should probably ever appear: [card_ge α 1], [card_ge α 2], [card_ge α 3]. (Assuming the pre-existing cardinality classes should be unified.)

[Adam Topaz]

E.g.

import data.matrix.notation
import tactic

lemma foobar {α : Type*} (a b c : α)
  (h1 : a ≠ b) (h2 : a ≠ c) (h3 : b ≠ c) : nonempty (fin 3 ↪ α) :=
⟨⟨![a,b,c], by { intros i j, fin_cases i; fin_cases j, tidy }⟩⟩

[Adam Topaz]

This has the benefit of being easily generalizable (to a point... the automation gets pretty slow)

import data.matrix.notation
import tactic

instance foobar {α : Type*} (a b c d : α) :
  a ≠ b → a ≠ c → a ≠ d →
  b ≠ c → b ≠ d →
  c ≠ d →
  nonempty (fin 4 ↪ α) := λ h1 h2 h3 h4 h5 h6,
⟨⟨![a,b,c,d], by { intros i j, fin_cases i; fin_cases j, tidy }⟩⟩

[Reid Barton]

@Kyle Miller I mean why not just make it a Prop. Wouldn't it make everyone happier?

[Reid Barton]

i.e., not a class

[Mario Carneiro]

I think the best way is to use list.nodup [a, b, c], which definitionally unfolds to something pretty close to what you want

[Mario Carneiro]

It's not too hard to massage an assumption like fintype.card X >= 3 into that