## Stream: new members

### Topic: Finishing off induction for pigeonhole

#### Adeeb K (Apr 21 2020 at 01:15):

Hello everyone! I am working on implementing the pigeonhole principle in lean for a school project. I have the following formulation for a finite subset of n elements:

def finite_subset (n : ℕ) := Σ' k, k < n


From this, I have a definition that lifts finite subsets of m elements to any finite subset of more elements:

def lift_finite (m n : ℕ) (p : m < n) : finite_subset m → finite_subset n
:= λ k, ⟨k.1, lt.trans k.2 p⟩


and finally a small lemma:

lemma succ_greater_than_nat (n : ℕ) : nat.succ n > n


My formulation for pigeonhole is the following:

theorem pigeonhole_principle
(n m : ℕ)
(f : finite_subset n → finite_subset m)
: (n > m) → ¬(injective f)


I proceeded by induction and was able to prove the base case but am stuck on the next step. I have this:

intros n_gt_m f_injective,
induction n with d hd,
...  --base case, done
let g := f ∘ (lift_finite d (d+1) (succ_greater_than_nat d)),
let hd' := hd g,


It is enough to show that d > m to get that g cannot be injective, but I have that d + 1 > m, which means that d ≥ m, which is where I'm stuck. Does anybody have any idea how to proceed? Thank you!

#### Adeeb K (Apr 21 2020 at 01:24):

Oh shoot, I forgot to send the corresponding lean goal at the last line:

m d : ℕ ,
hd : ∀ (f : finite_subset d → finite_subset m), d > m → injective f → false,
f : finite_subset (nat.succ d) → finite_subset m,
n_gt_m : nat.succ d > m
f_injective: injective f
g: finite_subset d → finite_subset m
hd' : d > m → injective g → false := hd g


#### Bryan Gin-ge Chen (Apr 21 2020 at 01:32):

It'll be easier for us to help you if you include something we can directly copy+paste into our editors (a "minimum working example" or MWE).

#### Adeeb K (Apr 21 2020 at 01:37):

Sure!

import tactic

def injective {X Y} (f : X → Y)
:= ∀ x₁ x₂, f x₁ = f x₂ → x₁ = x₂

def range {X Y} (f : X → Y)
:= { y | ∃ x, f x = y }

/--
Type of pairs (k,p) where k
is a natural number and p is a witness to the proof that k < n.
-/
def finite_subset (n : ℕ) := Σ' k, k < n

def lift_finite (m n : ℕ) (p : m < n) : finite_subset m → finite_subset n
:= λ k, ⟨k.1, lt.trans k.2 p⟩

lemma pred_exists (n : ℕ) (p: n > 0) : exists k, nat.succ k = n
:=
begin
induction n with d hd,
{linarith,},
{
existsi d,
refl}
end

lemma succ_greater_than_nat (n : ℕ) : nat.succ n > n
:=
begin
linarith,
end

/--
Pigeonhole principle, induction on n
-/
theorem pigeonhole_principle
(n m : ℕ)
(f : finite_subset n → finite_subset m)
: (n > m) → ¬(injective f)
:= begin
intros n_gt_m f_injective,

induction n with d hd,

linarith, -- case d=0

let g := f ∘ (lift_finite d (d+1) (succ_greater_than_nat d)),

let hd' := hd g,
/-
induction m with d hd,
{
cases pred_exists n n_gt_m with k hk,
let n_gt_k := succ_greater_than_nat k,
rw hk at n_gt_k,
let fk := f ⟨k, n_gt_k⟩,
let fk2 := fk.2,
linarith,
},
{
let n_gt_d : n>d :=
begin
exact lt.trans (succ_greater_than_nat d)  n_gt_m,
end,
sorry
},

-/
end


#### Mario Carneiro (Apr 21 2020 at 01:55):

By the way, finite_subset already exists in lean, by the name fin

#### Mario Carneiro (Apr 21 2020 at 01:56):

similarly with function.injective and set.range

#### Mario Carneiro (Apr 21 2020 at 01:58):

succ_greater_than_nat is nat.lt_succ_self

#### Adeeb K (Apr 21 2020 at 01:59):

@Mario Carneiro thanks, got it!

#### Mario Carneiro (Apr 21 2020 at 01:59):

lift_finite is fin.cast_le (with a different precondition)

#### Mario Carneiro (Apr 21 2020 at 02:01):

pred_exists is nat.exists_eq_succ_of_ne_zero although the precondition is slightly different

#### Adeeb K (Apr 21 2020 at 02:05):

thanks again haha!
I guess I have a long ways to go to being acquainted with the libraries.
Is there any library function that would help me resolve my issue with d in the induction step? I can't tell if the problem thus far has to do with a lack of vocabulary of a deeper error into the formulation of the proof

#### Mario Carneiro (Apr 21 2020 at 02:05):

Unfortunately I'm not a lint but a decent approximation is by library_search, which will find theorems from the library by type

#### Adeeb K (Apr 21 2020 at 02:06):

oh nice, that's really useful

#### Adeeb K (Apr 21 2020 at 02:07):

wait, could you give me an example of using library_search?

#### Mario Carneiro (Apr 21 2020 at 02:08):

What is the role of your commented out block? If I uncomment it I get an error about n not found

#### Mario Carneiro (Apr 21 2020 at 02:09):

import tactic

lemma pred_exists (n : ℕ) (p: n ≠ 0) : exists k, n = nat.succ k := by library_search


#### Adeeb K (Apr 21 2020 at 02:14):

It was my original attempt at induction on m, but I got stuck with that, so I switch to induction on n

#### Mario Carneiro (Apr 21 2020 at 02:14):

In your setup you tried to prove d > m from d + 1 > m, which isn't going to work. You can't always rely on the inductive hypothesis because then there would be nothing to the proof. Without thinking too hard about the theorem itself, here you should probably split into cases: either d > m or d = m. In the first case, you can use the inductive hypothesis. In the second case there is something to prove

#### Adeeb K (Apr 21 2020 at 02:17):

I'm not sure how to split into cases from what I have

#### Adeeb K (Apr 21 2020 at 02:17):

I mean, I see why, but I'm at a loss at how to do it given my existing work

#### Mario Carneiro (Apr 21 2020 at 02:19):

theorem pigeonhole_principle (n m : ℕ) (f : finite_subset n → finite_subset m) :
n > m → ¬ injective f :=
begin
intros n_gt_m f_injective,
induction n with d hd,
{ linarith, /- case d=0 -/ },
let g := f ∘ (lift_finite d (d+1) (succ_greater_than_nat d)),
let hd' := hd g,
rcases lt_or_eq_of_le (nat.lt_succ_iff.1 n_gt_m) with h | rfl,
{ apply hd' h,
sorry /- injective g -/ },
{ sorry /- prove f : finite_subset (nat.succ m) → finite_subset m is not injective -/ }
end


#### Mario Carneiro (Apr 21 2020 at 02:21):

here lt_or_eq_of_le (nat.lt_succ_iff.1 n_gt_m)  is a proof that d > m \/ d = m, and rcases does the case split and replaces d with m in the second branch

#### Adeeb K (Apr 21 2020 at 02:22):

Also, so d > m means that d + 1 > m by transitivity, so I'm done
for d = m, I'm not sure how to proceed, but my idea is this: there is a clear identity injection from finite_subset d to finite_subset m when d = m. Suppose towards contradiction there is an injection from finite_subset (d + 1) to finite_subset m. We replace d with m, meaning there is an injection from finite_subset (m + 1) to finite_subset m...and I'm stuck from there

#### Mario Carneiro (Apr 21 2020 at 02:23):

you don't want to prove d + 1 > m from d > m, the proof is going the other way around

#### Mario Carneiro (Apr 21 2020 at 02:23):

you need d > m and you have d + 1 > m

ah I see

#### Mario Carneiro (Apr 21 2020 at 02:25):

As for proving that there is no injection from m+1 to m, this is indeed the core of the proof, and here you have to step back from the code and ask what the maths proof is

#### Adeeb K (Apr 21 2020 at 02:27):

what do you mean with rcases replaces d with m in the second branch?

#### Mario Carneiro (Apr 21 2020 at 02:27):

you will notice in the second branch that d does not exist anymore

#### Mario Carneiro (Apr 21 2020 at 02:27):

and everywhere there used to be d there is now an m

#### Mario Carneiro (Apr 21 2020 at 02:28):

which is why f is an injection from m+1 to m instead of d+1 to m

#### Adeeb K (Apr 21 2020 at 02:29):

I see, but I'm still having a hard time understanding this all. What is the

with h | rfl


#### Bryan Gin-ge Chen (Apr 21 2020 at 02:30):

You can read more about rcases (and most other tactics) in the mathlib docs here.

#### Mario Carneiro (Apr 21 2020 at 02:30):

that's a pattern, that describes what kind of case split to do. the | means to do a split on the or, producing an assumption on the left that is being named h, and on the right the rfl means "case split on the equality", doing the replacement of d for m that I mentioned

#### Adeeb K (Apr 21 2020 at 02:32):

I see. I'll have to take some time to get comfortable with that, but that makes enough sense

#### Adeeb K (Apr 21 2020 at 02:33):

what does

apply hd' h


do here?

#### Mario Carneiro (Apr 21 2020 at 02:34):

hd' h is a proof of injection g -> false, so since the goal is false, apply hd' h changes the goal to injection g

#### Adeeb K (Apr 21 2020 at 02:35):

ah, so my goal here is to show that g is injective?

#### Mario Carneiro (Apr 21 2020 at 02:35):

yes, and that should be easy enough

#### Mario Carneiro (Apr 21 2020 at 02:36):

In fact, if you use function.injective and fin.cast_le you will find the theorem already exists :)

#### Adeeb K (Apr 21 2020 at 02:38):

what if I want to put it in terms of what I've already written though? (just as an exercise in being comfortable with using my own definitions haha)

#### Mario Carneiro (Apr 21 2020 at 02:38):

It's still an easy proof. Go ahead and try it

#### Adeeb K (Apr 21 2020 at 02:40):

I'm just sort of confused having all of the hypotheses in front of me. I have that f is injective, and that already takes finite_subset (d + 1) to finite_subset m

#### Adeeb K (Apr 21 2020 at 02:41):

I'm not sure what tactics I'd use to introduce two variables x1 and x2 and show that if g x1 = g x2, then x1 = x2

#### Mario Carneiro (Apr 21 2020 at 02:42):

None of that matters

#### Mario Carneiro (Apr 21 2020 at 02:42):

You can prove that g is injective without anything about f

#### Mario Carneiro (Apr 21 2020 at 02:42):

theorem lift_finite_injective (m n : ℕ) (p : m < n) : injective (lift_finite m n p) := sorry


#### Mario Carneiro (Apr 21 2020 at 02:43):

when proving a forall statement, the tactic to introduce variables is intro or intros

#### Adeeb K (Apr 21 2020 at 02:46):

okay, so here into this new theorem, I'd introduce x1 and x2 right? the arguments are two naturals m, n, and a proof that m < n.

#### Adeeb K (Apr 21 2020 at 02:47):

so I let f := lift_finite m n p

#### Adeeb K (Apr 21 2020 at 02:48):

and I have to introduce the proposition that f x1 = f x2?

#### Adeeb K (Apr 21 2020 at 02:51):

okay, this is what I have so far:

theorem lift_finite_injective (m n : ℕ) (p : m < n) : injective (lift_finite m n p)
:= begin

introv x1 f,
sorry
end


#### Mario Carneiro (Apr 21 2020 at 04:24):

Does anyone know why the first argument in the introv application here is x1 rather than the equality argument? That seems to go against the documentation of introv

#### Mario Carneiro (Apr 21 2020 at 04:25):

If you unfold injective first it works correctly

#### Adeeb K (Apr 21 2020 at 04:28):

my current plan is this:

/- pf sketch

--  suppose f x1 = f x2 = < k, pf: k < n >

--  we know x1 = < l , pf: k < m > and x2 = < j , pf: j < m >

--  note that (f x1).1 = (f x2).1 = k

--  furthermore, k < m < n

--  then x1 = < k, pf: k < m > = x2

--  done
-/


#### Adeeb K (Apr 21 2020 at 04:28):

I'm just not sure how to translate that into tactics

#### Mario Carneiro (Apr 21 2020 at 04:34):

you can do this with just cases and refl

#### Mario Carneiro (Apr 21 2020 at 04:34):

to do this step -- we know x1 = < l , pf: k < m > and x2 = < j , pf: j < m > use cases x1

#### Adeeb K (Apr 21 2020 at 04:36):

okay, so I do cases x1 and cases x2?

#### Adeeb K (Apr 21 2020 at 04:37):

how do I note that x1_fst = (f x1).1?

#### Mario Carneiro (Apr 21 2020 at 04:38):

that's true by definition (it won't be x1 after the cases, it will be <x1_fst, x1_snd>)

#### Mario Carneiro (Apr 21 2020 at 04:38):

so you don't have to say anything

#### Adeeb K (Apr 21 2020 at 04:45):

oh so then how can I conclude that x1_fst = x2_fst? I see that clearly x1_fst = (f x1).1 = (f x2).2 = x2_fst but I'm not sure how to type it out

#### Mario Carneiro (Apr 21 2020 at 04:47):

the easiest way is actually cases on the equality you have

#### Mario Carneiro (Apr 21 2020 at 04:47):

which is in fact <x1_fst, ...> = <x2_fst, ...>

#### Adeeb K (Apr 21 2020 at 04:57):

what do you mean with cases here?

#### Mario Carneiro (Apr 21 2020 at 04:58):

cases f

#### Mario Carneiro (Apr 21 2020 at 04:59):

the fact that you can do "case analysis" on an equality is one of the more mind bending things you can do in type theory but it's super useful

#### Adeeb K (Apr 21 2020 at 04:59):

ahhhh I see I see

#### Adeeb K (Apr 21 2020 at 05:02):

so now I have < x1_fst, x1_snd> = <x1_fst, x2_snd>, and I want to make it so that I have a match

#### Adeeb K (Apr 21 2020 at 05:02):

would I apply a rw or apply tactic here?

#### Johan Commelin (Apr 21 2020 at 05:05):

@Adeeb K I haven't been following along... Is that your goal or a hypothesis?

#### Adeeb K (Apr 21 2020 at 05:06):

I think I got it - I just applied a simple refl and it finished off the proof. Seems I need practice applying the basics. That...and reading more through the HoTT book.

#### Johan Commelin (Apr 21 2020 at 05:06):

Have you played the natural number game?

#### Johan Commelin (Apr 21 2020 at 05:07):

It's a great way of practicing the simple tactics

#### Adeeb K (Apr 21 2020 at 05:07):

only up to the third world

#### Adeeb K (Apr 21 2020 at 05:16):

now I'm showing composition of injective functions is injective. Not sure how to unpack that, but I'll try it with cases

#### Adeeb K (Apr 21 2020 at 05:21):

wait, so I still have stuff to finish for pigeonhole

#### Adeeb K (Apr 21 2020 at 05:22):

what tactic / proof is there to show that (g ∘ f) x = g (f x)?

#### Kenny Lau (Apr 21 2020 at 05:22):

refl

no but like

#### Adeeb K (Apr 21 2020 at 05:23):

Right now I have:
(g ∘ f) x1 = (g ∘ f) x2

#### Kenny Lau (Apr 21 2020 at 05:23):

change g (f x1) = g (f x2)

#### Adeeb K (Apr 21 2020 at 05:23):

How do I rewrite this as:
g (f x1) = g (f x2)?

lemme try that

#### Adeeb K (Apr 21 2020 at 05:24):

I'm getting an error

#### Adeeb K (Apr 21 2020 at 05:24):

tactic.change failed, given type
g (f x) = g (f x₂)
is not definitionally equal to
x = x₂


#### Johan Commelin (Apr 21 2020 at 05:24):

change allows you to change your goal to anything that is equal to the old goal by definition.

#### Johan Commelin (Apr 21 2020 at 05:25):

Aah but those two are certainly not the same goals

#### Johan Commelin (Apr 21 2020 at 05:25):

You need something like g \circ f is injective to do that

#### Kenny Lau (Apr 21 2020 at 05:25):

change g (f x1) = g (f x2) at H

#### Adeeb K (Apr 21 2020 at 05:26):

ah nice that worked!

#### Adeeb K (Apr 21 2020 at 05:27):

okay so now I want to use the injectivity of g to say f x1 = f x2

#### Johan Commelin (Apr 21 2020 at 05:28):

apply hg

#### Johan Commelin (Apr 21 2020 at 05:28):

Where hg : injective g

#### Adeeb K (Apr 21 2020 at 05:28):

error:

invalid apply tactic, failed to unify
x = x₂
with
?m_1 = ?m_2


#### Johan Commelin (Apr 21 2020 at 05:29):

Aah, right, same problem again...

wait

one sec

#### Johan Commelin (Apr 21 2020 at 05:29):

have foo : f x1 = f x2 := hg H

I got it

#### Adeeb K (Apr 21 2020 at 05:30):

I applied injectivity in reverse order and got it

#### Adeeb K (Apr 21 2020 at 05:30):

p3 : g (f x) = g (f x₂)
⊢ x = x₂


#### Adeeb K (Apr 21 2020 at 05:31):

I did apply p1 which is injective f

#### Adeeb K (Apr 21 2020 at 05:31):

Then I got

p3 : g (f x) = g (f x₂)
⊢ f x = f x₂


#### Adeeb K (Apr 21 2020 at 05:31):

then apply p2 which is injective g

#### Adeeb K (Apr 21 2020 at 05:31):

p3 : g (f x) = g (f x₂)
⊢ g (f x) = g (f x₂)


#### Adeeb K (Apr 21 2020 at 05:32):

to which I finally just applied p3 and got my desired result for the lemma

#### Adeeb K (Apr 21 2020 at 05:32):

with this, the first part of the induction step for pigeonhole is done

so uh

#### Adeeb K (Apr 21 2020 at 05:40):

suppose I have

g :=  f ∘ lift,
inj : injective (f ∘ lift)


#### Adeeb K (Apr 21 2020 at 05:41):

how do I conclude

inj : injective (g)


?

#### Mario Carneiro (Apr 21 2020 at 05:42):

I think you want inj : injective (f ∘ lift)?

#### Mario Carneiro (Apr 21 2020 at 05:42):

If so, then inj : injective g and you don't have to say anything

#### Adeeb K (Apr 21 2020 at 05:42):

really? right now I'm not sure if I have that

#### Mario Carneiro (Apr 21 2020 at 05:43):

those two are the same to lean

#### Adeeb K (Apr 21 2020 at 05:43):

how do I conclude injective g then? refl?

#### Mario Carneiro (Apr 21 2020 at 05:43):

just pretend it says injective g already

#### Mario Carneiro (Apr 21 2020 at 05:43):

if your goal is injective g, then exact inj will work

#### Adeeb K (Apr 21 2020 at 05:44):

ah, yeah it worked

#### Adeeb K (Apr 21 2020 at 05:44):

now the nontrivial case lol

#### Adeeb K (Apr 21 2020 at 05:45):

where d = m

#### Adeeb K (Apr 21 2020 at 06:18):

I'm not exactly sure how to start this part of the proof

#### Adeeb K (Apr 21 2020 at 06:37):

basically, all classical proofs to show that there's no injection from a set of m + 1 elements to one of m elements I recall end up using the contrapositive

well, not all

#### Johan Commelin (Apr 21 2020 at 06:40):

So... formalise a classical proof...

#### Adeeb K (Apr 21 2020 at 06:52):

I'm not sure how that'd help me here

#### Johan Commelin (Apr 21 2020 at 06:52):

Why not? What are you trying to do?

#### Adeeb K (Apr 21 2020 at 06:55):

suppose towards contradiction that there exists such an injective functionL: call it f
let M be the set of m + 1 elements and N be the set of m elements. We see that |f(M)| = m +1 but |N| = m
it is not possible for f to be injective, since each f(x) \in N for x \in M, but there are fewer possible values for f(x) than there are x

#### Adeeb K (Apr 21 2020 at 06:55):

So I feel like I'm going in circles restating what I'm out to prove in the first place

#### Johan Commelin (Apr 21 2020 at 06:58):

Can you post a copy-pasteble chunk of code (include import and variables statements)? AKA an MWE

yeah sure

#### Adeeb K (Apr 21 2020 at 07:05):

import tactic

def injective {X Y} (f : X → Y)
:= ∀ x₁ x₂, f x₁ = f x₂ → x₁ = x₂

def range {X Y} (f : X → Y)
:= { y | ∃ x, f x = y }

/--
Type of pairs (k,p) where k
is a natural number and p is a witness to the proof that k < n.
-/
def finite_subset (n : ℕ) := Σ' k, k < n

def lift_finite (m n : ℕ) (p : m < n) : finite_subset m → finite_subset n
:= λ k, ⟨k.1, lt.trans k.2 p⟩

lemma pred_exists (n : ℕ) (p: n > 0) : exists k, nat.succ k = n
:=
begin
induction n with d hd,
{linarith,},
{
existsi d,
refl
}
end

lemma succ_greater_than_nat (n : ℕ) : nat.succ n > n
:=
begin
linarith
end

/--
The lifting function is injective
-/
theorem lift_finite_injective (m n : ℕ) (p : m < n) : injective (lift_finite m n p)
:= begin

/- pf sketch

--  suppose f x1 = f x2 = < k, pf: k < n >

--  we know x1 = < l , pf: k < m > and x2 = < j , pf: j < m >

--  note that (f x1).1 = (f x2).1 = k

--  furthermore, k < m < n

--  then x1 = < k, pf: k < m > = x2

--  done
-/

introv x p2,
cases x,
cases x₂,
cases p2,
refl
end

theorem comp_inj_is_inj
{X Y Z} (f : X → Y) (g : Y → Z)
(p1 : injective f)
(p2 : injective g)
:  injective (g ∘ f)
:= begin

introv x p3,
change g (f x) = g (f x₂) at p3,
apply p1,
apply p2,
apply p3,
end

/--
Pigeonhole principle, induction on n
-/
theorem pigeonhole_principle
(n m : ℕ)
(f : finite_subset n → finite_subset m)
: (n > m) → ¬(injective f)
:= begin

intros n_gt_m f_injective,
induction n with d hd,
{ linarith, /- case d = 0 -/ },

let succ_for_lift := (succ_greater_than_nat d),
let lift := (lift_finite d (d+1) succ_for_lift),
let g := f ∘ lift,
let hd' := hd g,

rcases lt_or_eq_of_le (nat.lt_succ_iff.1 n_gt_m) with h | rfl,

{   /- case where d > m -/
/- prove injective g -/
apply hd' h,
let lift_injective := (lift_finite_injective d (d+1) succ_for_lift),
let g_injective := comp_inj_is_inj lift f lift_injective f_injective,
exact g_injective,
},

{   /- case where d = m -/
/- prove f : finite_subset (nat.succ m) → finite_subset m is not injective -/

sorry
}

end


#### Kenny Lau (Apr 21 2020 at 07:06):

first come up with a math proof

#### Kenny Lau (Apr 21 2020 at 07:06):

then formalize it

#### Adeeb K (Apr 21 2020 at 07:09):

alright
It's pretty late where I am, so I'll be heading to bed for now. Thank you everyone for your help!

#### Adeeb K (Apr 21 2020 at 07:09):

I'll be back in a few hours probably

#### Patrick Stevens (Apr 21 2020 at 07:44):

basically, all classical proofs to show that there's no injection from a set of m + 1 elements to one of m elements I recall end up using the contrapositive

I wrote a constructive one in Agda a while back. Hint for the maths proof: if you have an injection f: [m+1] -> [m], consider that f sends 1 somewhere, and note that you must use induction because it's a constructively-true thing about the natural numbers. State the inductive hypothesis, and try to use it.

I see

#### Adeeb K (Apr 21 2020 at 17:55):

I am already using induction here, and this is the second case that I'm handling
I'll send what I currently have

#### Adeeb K (Apr 21 2020 at 17:56):

import tactic

def injective {X Y} (f : X → Y)
:= ∀ x₁ x₂, f x₁ = f x₂ → x₁ = x₂

def range {X Y} (f : X → Y)
:= { y | ∃ x, f x = y }

/--
Type of pairs (k,p) where k
is a natural number and p is a witness to the proof that k < n.
-/
def finite_subset (n : ℕ) := Σ' k, k < n

def lift_finite (m n : ℕ) (p : m < n) : finite_subset m → finite_subset n
:= λ k, ⟨k.1, lt.trans k.2 p⟩

lemma pred_exists (n : ℕ) (p: n > 0) : exists k, nat.succ k = n
:=
begin
induction n with d hd,
{linarith,},
{
existsi d,
refl
}
end

lemma succ_greater_than_nat (n : ℕ) : nat.succ n > n
:=
begin
linarith
end

/--
The lifting function is injective
-/
theorem lift_finite_injective (m n : ℕ) (p : m < n) : injective (lift_finite m n p)
:= begin

/- pf sketch

--  suppose f x1 = f x2 = < k, pf: k < n >

--  we know x1 = < l , pf: k < m > and x2 = < j , pf: j < m >

--  note that (f x1).1 = (f x2).1 = k

--  furthermore, k < m < n

--  then x1 = < k, pf: k < m > = x2

--  done
-/

introv x p2,
cases x,
cases x₂,
cases p2,
refl
end

theorem comp_inj_is_inj
{X Y Z} (f : X → Y) (g : Y → Z)
(p1 : injective f)
(p2 : injective g)
:  injective (g ∘ f)
:= begin

introv x p3,
change g (f x) = g (f x₂) at p3,
apply p1,
apply p2,
apply p3,
end

/--
Pigeonhole principle, induction on n
-/
theorem pigeonhole_principle
(n m : ℕ)
(f : finite_subset n → finite_subset m)
: (n > m) → ¬(injective f)
:= begin

intros n_gt_m f_injective,
induction n with d hd,
{ linarith, /- case d = 0 -/ },

let succ_for_lift := (succ_greater_than_nat d),
let lift := (lift_finite d (d+1) succ_for_lift),
let g := f ∘ lift,
let hd' := hd g,

rcases lt_or_eq_of_le (nat.lt_succ_iff.1 n_gt_m) with h | rfl,

{   /- case where d > m -/
/- prove injective g -/
apply hd' h,
let lift_injective := (lift_finite_injective d (d+1) succ_for_lift),
let g_injective := comp_inj_is_inj lift f lift_injective f_injective,
exact g_injective,
},

{   /- case where d = m -/
/- prove f : finite_subset (nat.succ m) → finite_subset m is not injective -/

sorry
}

end


#### Adeeb K (Apr 21 2020 at 18:08):

So going off @Patrick Stevens 's advice, I have injective f : [m + 1] → [m]. I have set up finite sets finite_subset m to be all pairs <k, pf: k < m>. We consider f([m + 1]). Since f is injective, we know that for distinct x1, x2 : finite_subset (m + 1), if f x1 = f x2 then x1 = x2.

#### Adeeb K (Apr 21 2020 at 18:11):

We consider the image of f. By my current inductive hypothesis, I have

hd : ∀ (f : finite_subset m → finite_subset m), m > m → injective f → false,


#### Adeeb K (Apr 21 2020 at 18:14):

I'm not sure if I should consider the image or the pre-image here.

#### Kenny Lau (Apr 21 2020 at 18:14):

m > m is false

#### Adeeb K (Apr 21 2020 at 18:15):

I realize that much, so what does that give me?

Nothing

#### Kenny Lau (Apr 21 2020 at 18:16):

you should write down a maths proof first

#### Adeeb K (Apr 21 2020 at 18:17):

I'm just figuring out how to word a constructive proof for pigeonhole

#### Kenny Lau (Apr 21 2020 at 18:19):

it doesn't need to be constructive

#### Kenny Lau (Apr 21 2020 at 18:19):

you just need to make sure that it isn't circular

#### Adeeb K (Apr 21 2020 at 18:20):

Alright, makes sense

quick question

#### Adeeb K (Apr 21 2020 at 18:27):

just something I forgot to ask last night: is there a function in the library that lets me say a natural number is either 0 or not?

#### Kenny Lau (Apr 21 2020 at 18:27):

cases n

gotcha thanks

#### Kenny Lau (Apr 21 2020 at 18:29):

how about you write down a maths proof first before touching Lean

#### Adeeb K (Apr 21 2020 at 18:29):

yeah I'm on that right now - this was just something I forgot

#### Kenny Lau (Apr 21 2020 at 18:36):

this has been a demonstration of the relativity of simultaneity in Einstein's theory of relativity

#### Kenny Lau (Apr 21 2020 at 18:36):

whaddup I'm Kenny I'm (age removed) and I'm a physicist

#### Kenny Lau (Apr 21 2020 at 18:37):

(nobody will get this reference)

#### Adeeb K (Apr 21 2020 at 19:03):

Okay I believe I have something

#### Adeeb K (Apr 21 2020 at 19:04):

We want to show that there exists no injection f : [m + 1] → [m], where [m] here denotes the set {0, 1, ..., m - 1}.

#### Adeeb K (Apr 21 2020 at 19:06):

we proceed by induction. The base case m = 0 is clear since if we suppose not, we end up with f(0) = f(1) = 0, which is a contradiction.

#### Kenny Lau (Apr 21 2020 at 19:07):

[0] is empty, not {0}

#### Kevin Buzzard (Apr 21 2020 at 19:07):

The case m=0 is clear because there are no functions [1]->[0], injective or not

#### Adeeb K (Apr 21 2020 at 19:11):

Now, we know that there is no injective f : [m] → [m - 1] and want to show this for f : [m + 1] → [m], where [m]. Suppose not, to which we assume there exists such f. We know that f(m) = k for some k < m. Then we consider the restriction of f to [m]. By injectivity we know that if for any j in {0, ..., m}, f j = f k → j = k. So when we restrict f, the image of the function lives in [m - 1]. However, by our inductive hypothesis, there is no injective function that maps [m] to [m - 1]. Contradiction.

#### Adeeb K (Apr 21 2020 at 19:14):

I see a small problem.

#### Adeeb K (Apr 21 2020 at 19:16):

I know that f(m) = k, but I don't know if k = m - 1, which means I know that the restriction of f to [m] must necessarily map to a set of only m - 1 elements, but they may not all 'live' in [m - 1] unless I relabel them.

#### Adeeb K (Apr 21 2020 at 19:23):

So, does this suggest I can't use the idea of restrictions?

#### Kenny Lau (Apr 21 2020 at 19:23):

this suggests you relabel them

#### Adeeb K (Apr 21 2020 at 19:23):

That's the first thing that came to mind to use an inductive hypothesis

oh

#### Adeeb K (Apr 21 2020 at 19:25):

I'm not exactly sure how to do that. How do I know a priori that I have a collection of size m - 1 if I only have that they are type finite_subset (m + 1)?

#### Adeeb K (Apr 21 2020 at 19:26):

I have some vague idea that relabelling itself is an injective function

#### Adeeb K (Apr 21 2020 at 19:27):

if we have some number k that sits in {0, 1, ..., m}, then my relabelling function would basically this:
for all j < k, j maps to j + 1. Otherwise, if j > k, then j maps to j.

#### Adeeb K (Apr 21 2020 at 19:28):

wait shoot that's backwards

#### Adeeb K (Apr 21 2020 at 19:28):

it should be:
for all j > k, j maps to j - 1. Otherwise, if j < k, then it is mapped to itself.

#### Adeeb K (Apr 21 2020 at 19:29):

call this function relabel. We can show it is injective.

#### Adeeb K (Apr 21 2020 at 19:31):

and so when we restrict f to [m], and relabel, we should have an injective function relabel ∘ f : [m] → [m - 1]

#### Adeeb K (Apr 21 2020 at 19:32):

which is a contradiction. Is there anything I missed?

#### Kenny Lau (Apr 21 2020 at 19:34):

relabel itself isn't injective (let's say you send k to k)

#### Kenny Lau (Apr 21 2020 at 19:34):

but relabel \o f is injective

#### Kenny Lau (Apr 21 2020 at 19:34):

other than that, LGTM

#### Kenny Lau (Apr 21 2020 at 19:34):

oh and you implicitly restricted f to [m] I guess

#### Adeeb K (Apr 21 2020 at 19:35):

yeah I'm not exactly sure how to carry out restriction

#### Kenny Lau (Apr 21 2020 at 19:35):

compose it with [m] -> [m+1]

#### Kenny Lau (Apr 21 2020 at 19:35):

relabel o f o lift

I see I see

#### Adeeb K (Apr 21 2020 at 19:36):

wait, so then what does relabel's function signature become?

#### Kenny Lau (Apr 21 2020 at 19:36):

relabel : [m] -> [m-1]

#### Kenny Lau (Apr 21 2020 at 19:36):

f: [m+1] -> [m]

#### Kenny Lau (Apr 21 2020 at 19:36):

lift: [m] -> [m+1]

#### Adeeb K (Apr 21 2020 at 19:37):

ah so this is exactly why I can't say relabel is injective, but relabel composed with an injective function is in fact injective?

#### Kenny Lau (Apr 21 2020 at 19:38):

no, it's because f o lift misses k that relabel k o f o lift is injective

ah gotcha

#### Adeeb K (Apr 21 2020 at 19:40):

...stupid question, but how would I define this in lean?

#### Adeeb K (Apr 21 2020 at 19:41):

relabel, that is. I'm not sure how to give cases for j < k and j > k.

don't forget k

#### Kenny Lau (Apr 21 2020 at 19:41):

if j \le k then j else j-1

#### Adeeb K (Apr 21 2020 at 19:42):

ah gotcha gotcha.

#### Adeeb K (Apr 21 2020 at 19:47):

I'm getting some errors

#### Adeeb K (Apr 21 2020 at 19:47):

here's what I have for relabel so far

#### Adeeb K (Apr 21 2020 at 19:47):

def relabel_finite_set
(m k : ℕ)
(p: k < m)
: finite_subset m → finite_subset (m - 1)
:= λ j, if j.1 ≤ k then ⟨j.1, lt.trans j.1 p⟩ else ⟨j.1 - 1, lt.trans j.1 p⟩


#### Adeeb K (Apr 21 2020 at 19:47):

but I have this error in both tuples:

type mismatch at application
lt.trans j.fst
term
j.fst
has type
ℕ : Type
but is expected to have type
j.fst < ?m_1 : Prop


#### Kevin Buzzard (Apr 21 2020 at 19:48):

Looks like lean wanted j.2

#### Kevin Buzzard (Apr 21 2020 at 19:49):

Or maybe it's called j.is_lt or something

#### Adeeb K (Apr 21 2020 at 19:49):

I have this then:

type mismatch at application
lt.trans j.snd p
term
p
has type
k < m
but is expected to have type
m < m - 1


#### Kevin Buzzard (Apr 21 2020 at 19:49):

It's going to be hard to come up with something of that type

#### Kenny Lau (Apr 21 2020 at 19:49):

if H : j.1 \le k

#### Adeeb K (Apr 21 2020 at 19:50):

how would I compose that with p to get j < m - 1?

#### Adeeb K (Apr 21 2020 at 19:54):

I'm not sure how to use H here

#### Adeeb K (Apr 26 2020 at 22:42):

Hello guys, and thanks for all the help from last time!

#### Adeeb K (Apr 26 2020 at 22:43):

I'm not sure if I should make a new topic or just get this post up to speed with my progress

#### Adeeb K (Apr 26 2020 at 22:44):

Basically, I've got pigeonhole done after assuming a few sorry's in my helper functions, but I am having trouble showing that (relabel m k p) ∘ f ∘ lift` is an injective function

#### Adeeb K (Apr 26 2020 at 22:49):

ah I'll just make a new thread entirely since this is a separate issue.

Last updated: May 16 2021 at 05:21 UTC