Zulip Chat Archive

Stream: maths

Topic: proving size at least 3


Kevin Buzzard (Aug 13 2018 at 10:35):

I would be interested in a relatively slick proof of either of the below examples:

import data.fintype
import set_theory.cardinal

-- fintype
open fintype
example (α : Type) [fintype α] (a b c : α) (Hab : a  b) (Hbc : b  c) (Hac : a  c) :
card α  3 := sorry

-- general
example (α : Type) (a b c : α) (Hab : a  b) (Hbc : b  c) (Hac : a  c) :
cardinal.mk α  3 := sorry

This is for pedagogical purposes and I don't really mind if we stick to fintypes or not.

As a side issue, is cardinal.mk really the way to talk about the cardinality of a type? Is there not some interface function?

Mario Carneiro (Aug 13 2018 at 10:38):

cardinal.mk is the interface function

Kenny Lau (Aug 13 2018 at 10:58):

import data.fintype
import set_theory.cardinal

@[derive decidable_eq]
inductive three : Type
| A : three
| B : three
| C : three

open three

instance : fintype three :=
{ elems := {A, B, C},
  complete := λ x, by cases x; simp }

theorem three.cardinal : cardinal.mk three = 3 :=
(cardinal.fintype_card three).trans $
show ((3 : nat) : cardinal) = 3, by simp

-- fintype
open fintype
example (α : Type) [fintype α] (a b c : α) (Hab : a  b) (Hbc : b  c) (Hac : a  c) :
  card α  3 :=
show card three  card α, from
card_le_of_injective (λ n, three.rec_on n a b c) $
λ x y h, by cases x; cases y; dsimp at h; cc

-- general
example (α : Type) (a b c : α) (Hab : a  b) (Hbc : b  c) (Hac : a  c) :
cardinal.mk α  3 :=
three.cardinal  nonempty.intro ⟨λ n, three.rec_on n a b c,
λ x y h, by cases x; cases y; dsimp at h; cc

Mario Carneiro (Aug 13 2018 at 10:58):

hm, I needed some additional library functions for this, attached. The main proof is not so hard:

@[simp] lemma fintype.card_coe (s : finset α) :
  fintype.card (s : set α) = s.card := card_attach

theorem card_le_of_finset {α} (s : finset α) :
  (s.card : cardinal)  cardinal.mk α :=
begin
  rw (_ : (s.card : cardinal) = cardinal.mk (s : set α)),
  { exact function.embedding.subtype _⟩ },
  rw [cardinal.fintype_card, fintype.card_coe]
end

-- fintype
open fintype
example (α : Type) [fintype α] (a b c : α) (Hab : a  b) (Hbc : b  c) (Hac : a  c) :
  card α  3 :=
finset.card_le_of_subset (finset.subset_univ a::b::c::0, by simp *⟩)

-- general
example (α : Type) (a b c : α) (Hab : a  b) (Hbc : b  c) (Hac : a  c) :
  cardinal.mk α  3 :=
begin
  suffices : ((3:) : cardinal)  cardinal.mk α, {simpa},
  exact card_le_of_finset a::b::c::0, by simp *⟩
end

Kenny Lau (Aug 13 2018 at 10:58):

just 3 seconds apart!

Kevin Buzzard (Aug 13 2018 at 18:33):

Thanks to both of you! [I've only just seen these].

Kevin Buzzard (Aug 13 2018 at 22:15):

This is one of those "easy in maths, hard in Lean" moments :-/ I am going to need stuff like "card X = 3 iff there exists a,b,c all distinct and every element of X must be a, b or c" [but I've gotta scoot]. I think I can take it from here but this is all a bit ugly. Mathematicians are so good at 3 :-/

Mario Carneiro (Aug 14 2018 at 02:04):

that latter fact is essentially exactly the definition of a fintype instance where the underlying multiset has three elements

Kevin Buzzard (Aug 14 2018 at 19:36):

Here's a proof for the cardinal case:

import set_theory.cardinal

lemma three (α : Type) (Hthree : cardinal.mk α = 3) :
   a b c : α, a  b  b  c  c  a   d : α, d = a  d = b  d = c :=
begin
  rw (show cardinal.mk (fin 3) = 3, by simp) at Hthree,
  cases (quotient.exact Hthree) with Hequiv,
  let a := Hequiv.symm 0,let b := Hequiv.symm 1,let c := Hequiv.symm 2,
  have H12 : a  b := by simp [Hequiv];exact dec_trivial,
  have H23 : b  c := by simp [Hequiv];exact dec_trivial,
  have H31 : c  a := by simp [Hequiv];exact dec_trivial,
  existsi a,existsi b,existsi c,
  refine H12,H23,H31,λ d,_⟩,
  cases H : (Hequiv d) with n Hn,
  cases n with e He,
    left,show d = Hequiv.symm 0,Hn,rw H,simp,
  cases e with e He,
    right,left,show d = Hequiv.symm 1,Hn,rw H,simp,
  cases e with e He,
    right,right,show d = Hequiv.symm 2,Hn,rw H,simp,
  exfalso,apply not_le_of_gt Hn,exact dec_trivial,
end

Now I need to do four :cry: (but that's the last one)

Mario Carneiro (Aug 14 2018 at 19:37):

noo... my heart, it hurts

Mario Carneiro (Aug 14 2018 at 19:38):

n is easier than 3

Kevin Buzzard (Aug 14 2018 at 19:39):

So 4 is easier than 3? :-)

Mario Carneiro (Aug 14 2018 at 19:39):

3 is easier than 3

Kevin Buzzard (Aug 14 2018 at 19:41):

I did think about doing the general case but at the end of the day I want to extract exactly those things in the conclusion, and I wasn't entirely sure how easy it would be if I had a list of size n or whatever, so I decided to bite the bullet now rather than later.

Mario Carneiro (Aug 14 2018 at 19:41):

trust me, it's way easier to conclude from the general statement, even if the final goal is exactly the statement you wrote

Mario Carneiro (Aug 14 2018 at 19:42):

hint: if you have a list of length 3, then you can match it against [a, b, c]

Kevin Buzzard (Aug 14 2018 at 19:42):

I was a bit surprised to see simp leave me with a goal not 0 = 1 in the H12 proof.

Mario Carneiro (Aug 14 2018 at 19:43):

and d \in [a, b, c] and list.nodup [a, b, c] will simplify to the disjunctions you wrote

Kevin Buzzard (Aug 14 2018 at 19:43):

This is the stupid cardinal version, because Richard Thomas complained that I was assuming unnecessary finiteness hypotheses.

Mario Carneiro (Aug 14 2018 at 19:44):

there are theorems showing equivalence to the finite versions in cardinal

Kevin Buzzard (Aug 14 2018 at 19:44):

Oh OK, maybe I'll take it from here. Thanks!

Kevin Buzzard (Aug 14 2018 at 19:45):

It's just my lack of experience which made me do the 3 case explicitly. I could see I could try for the n case, but I figured that doing the 3 case directly would be less painful. I guess your instincts immediately told you otherwise.

Mario Carneiro (Aug 14 2018 at 19:46):

even 2 is sometimes tricky, but certainly 2 < n < 3


Last updated: Dec 20 2023 at 11:08 UTC