Zulip Chat Archive

Stream: maths

Topic: proving size at least 3


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Aug 13 2018 at 10:38):

cardinal.mk is the interface function

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 13 2018 at 10:58):

just 3 seconds apart!

view this post on Zulip Kevin Buzzard (Aug 13 2018 at 18:33):

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

view this post on Zulip 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 :-/

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Aug 14 2018 at 19:37):

noo... my heart, it hurts

view this post on Zulip Mario Carneiro (Aug 14 2018 at 19:38):

n is easier than 3

view this post on Zulip Kevin Buzzard (Aug 14 2018 at 19:39):

So 4 is easier than 3? :-)

view this post on Zulip Mario Carneiro (Aug 14 2018 at 19:39):

3 is easier than 3

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 14 2018 at 19:44):

there are theorems showing equivalence to the finite versions in cardinal

view this post on Zulip Kevin Buzzard (Aug 14 2018 at 19:44):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 14 2018 at 19:46):

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


Last updated: May 12 2021 at 07:17 UTC