Zulip Chat Archive

Stream: new members

Topic: Finishing off induction for pigeonhole


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

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

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

view this post on Zulip 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
rw nat.succ_eq_add_one,
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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 01:55):

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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 01:56):

similarly with function.injective and set.range

view this post on Zulip Mario Carneiro (Apr 21 2020 at 01:58):

succ_greater_than_nat is nat.lt_succ_self

view this post on Zulip Adeeb K (Apr 21 2020 at 01:59):

@Mario Carneiro thanks, got it!

view this post on Zulip Mario Carneiro (Apr 21 2020 at 01:59):

lift_finite is fin.cast_le (with a different precondition)

view this post on Zulip Mario Carneiro (Apr 21 2020 at 02:01):

pred_exists is nat.exists_eq_succ_of_ne_zero although the precondition is slightly different

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

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

view this post on Zulip Adeeb K (Apr 21 2020 at 02:06):

oh nice, that's really useful

view this post on Zulip Adeeb K (Apr 21 2020 at 02:07):

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

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

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

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

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

view this post on Zulip Adeeb K (Apr 21 2020 at 02:17):

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

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

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

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

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

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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 02:23):

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

view this post on Zulip Adeeb K (Apr 21 2020 at 02:24):

ah I see

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

view this post on Zulip Adeeb K (Apr 21 2020 at 02:27):

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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 02:27):

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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 02:27):

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

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

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

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

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

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

view this post on Zulip Adeeb K (Apr 21 2020 at 02:33):

what does

apply hd' h

do here?

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

view this post on Zulip Adeeb K (Apr 21 2020 at 02:35):

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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 02:35):

yes, and that should be easy enough

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

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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 02:38):

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

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

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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 02:42):

None of that matters

view this post on Zulip Mario Carneiro (Apr 21 2020 at 02:42):

You can prove that g is injective without anything about f

view this post on Zulip Mario Carneiro (Apr 21 2020 at 02:42):

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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 02:43):

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

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

view this post on Zulip Adeeb K (Apr 21 2020 at 02:47):

so I let f := lift_finite m n p

view this post on Zulip Adeeb K (Apr 21 2020 at 02:48):

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

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

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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 04:25):

If you unfold injective first it works correctly

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

view this post on Zulip Adeeb K (Apr 21 2020 at 04:28):

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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 04:34):

you can do this with just cases and refl

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

view this post on Zulip Adeeb K (Apr 21 2020 at 04:36):

okay, so I do cases x1 and cases x2?

view this post on Zulip Adeeb K (Apr 21 2020 at 04:37):

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

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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 04:38):

so you don't have to say anything

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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 04:47):

the easiest way is actually cases on the equality you have

view this post on Zulip Mario Carneiro (Apr 21 2020 at 04:47):

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

view this post on Zulip Adeeb K (Apr 21 2020 at 04:57):

what do you mean with cases here?

view this post on Zulip Mario Carneiro (Apr 21 2020 at 04:58):

cases f

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

view this post on Zulip Adeeb K (Apr 21 2020 at 04:59):

ahhhh I see I see

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

view this post on Zulip Adeeb K (Apr 21 2020 at 05:02):

would I apply a rw or apply tactic here?

view this post on Zulip Johan Commelin (Apr 21 2020 at 05:05):

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

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

view this post on Zulip Johan Commelin (Apr 21 2020 at 05:06):

Have you played the natural number game?

view this post on Zulip Johan Commelin (Apr 21 2020 at 05:07):

It's a great way of practicing the simple tactics

view this post on Zulip Adeeb K (Apr 21 2020 at 05:07):

only up to the third world

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

view this post on Zulip Adeeb K (Apr 21 2020 at 05:21):

wait, so I still have stuff to finish for pigeonhole

view this post on Zulip Adeeb K (Apr 21 2020 at 05:22):

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 05:22):

refl

view this post on Zulip Adeeb K (Apr 21 2020 at 05:22):

no but like

view this post on Zulip Adeeb K (Apr 21 2020 at 05:23):

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 05:23):

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

view this post on Zulip Adeeb K (Apr 21 2020 at 05:23):

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

view this post on Zulip Adeeb K (Apr 21 2020 at 05:23):

lemme try that

view this post on Zulip Johan Commelin (Apr 21 2020 at 05:24):

Kenny answers before you write your question.... C'est la vie.

view this post on Zulip Adeeb K (Apr 21 2020 at 05:24):

I'm getting an error

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

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

view this post on Zulip Johan Commelin (Apr 21 2020 at 05:25):

Aah but those two are certainly not the same goals

view this post on Zulip Johan Commelin (Apr 21 2020 at 05:25):

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 05:25):

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

view this post on Zulip Adeeb K (Apr 21 2020 at 05:26):

ah nice that worked!

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

view this post on Zulip Johan Commelin (Apr 21 2020 at 05:28):

apply hg

view this post on Zulip Johan Commelin (Apr 21 2020 at 05:28):

Where hg : injective g

view this post on Zulip Adeeb K (Apr 21 2020 at 05:28):

error:

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

view this post on Zulip Johan Commelin (Apr 21 2020 at 05:29):

Aah, right, same problem again...

view this post on Zulip Adeeb K (Apr 21 2020 at 05:29):

wait

view this post on Zulip Adeeb K (Apr 21 2020 at 05:29):

one sec

view this post on Zulip Johan Commelin (Apr 21 2020 at 05:29):

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

view this post on Zulip Adeeb K (Apr 21 2020 at 05:30):

I got it

view this post on Zulip Adeeb K (Apr 21 2020 at 05:30):

I applied injectivity in reverse order and got it

view this post on Zulip Adeeb K (Apr 21 2020 at 05:30):

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

view this post on Zulip Adeeb K (Apr 21 2020 at 05:31):

I did apply p1 which is injective f

view this post on Zulip Adeeb K (Apr 21 2020 at 05:31):

Then I got

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

view this post on Zulip Adeeb K (Apr 21 2020 at 05:31):

then apply p2 which is injective g

view this post on Zulip Adeeb K (Apr 21 2020 at 05:31):

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

view this post on Zulip Adeeb K (Apr 21 2020 at 05:32):

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

view this post on Zulip Adeeb K (Apr 21 2020 at 05:32):

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

view this post on Zulip Adeeb K (Apr 21 2020 at 05:39):

so uh

view this post on Zulip Adeeb K (Apr 21 2020 at 05:40):

suppose I have

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

view this post on Zulip Adeeb K (Apr 21 2020 at 05:41):

how do I conclude

inj : injective (g)

?

view this post on Zulip Mario Carneiro (Apr 21 2020 at 05:42):

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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 05:42):

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

view this post on Zulip Adeeb K (Apr 21 2020 at 05:42):

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

view this post on Zulip Mario Carneiro (Apr 21 2020 at 05:43):

those two are the same to lean

view this post on Zulip Adeeb K (Apr 21 2020 at 05:43):

how do I conclude injective g then? refl?

view this post on Zulip Mario Carneiro (Apr 21 2020 at 05:43):

just pretend it says injective g already

view this post on Zulip Mario Carneiro (Apr 21 2020 at 05:43):

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

view this post on Zulip Adeeb K (Apr 21 2020 at 05:44):

ah, yeah it worked

view this post on Zulip Adeeb K (Apr 21 2020 at 05:44):

now the nontrivial case lol

view this post on Zulip Adeeb K (Apr 21 2020 at 05:45):

where d = m

view this post on Zulip Adeeb K (Apr 21 2020 at 06:18):

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

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

view this post on Zulip Adeeb K (Apr 21 2020 at 06:38):

well, not all

view this post on Zulip Johan Commelin (Apr 21 2020 at 06:40):

So... formalise a classical proof...

view this post on Zulip Adeeb K (Apr 21 2020 at 06:52):

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

view this post on Zulip Johan Commelin (Apr 21 2020 at 06:52):

Why not? What are you trying to do?

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

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

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

view this post on Zulip Adeeb K (Apr 21 2020 at 07:05):

yeah sure

view this post on Zulip 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
rw nat.succ_eq_add_one,
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

view this post on Zulip Kenny Lau (Apr 21 2020 at 07:06):

first come up with a math proof

view this post on Zulip Kenny Lau (Apr 21 2020 at 07:06):

then formalize it

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

view this post on Zulip Adeeb K (Apr 21 2020 at 07:09):

I'll be back in a few hours probably

view this post on Zulip Patrick Stevens (Apr 21 2020 at 07:44):

Adeeb K said:

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.

view this post on Zulip Adeeb K (Apr 21 2020 at 17:54):

I see

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

view this post on Zulip 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
rw nat.succ_eq_add_one,
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

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

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

view this post on Zulip Adeeb K (Apr 21 2020 at 18:14):

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 18:14):

m > m is false

view this post on Zulip Adeeb K (Apr 21 2020 at 18:15):

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

view this post on Zulip Reid Barton (Apr 21 2020 at 18:15):

Nothing

view this post on Zulip Kenny Lau (Apr 21 2020 at 18:16):

you should write down a maths proof first

view this post on Zulip Adeeb K (Apr 21 2020 at 18:17):

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 18:19):

it doesn't need to be constructive

view this post on Zulip Kenny Lau (Apr 21 2020 at 18:19):

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

view this post on Zulip Adeeb K (Apr 21 2020 at 18:20):

Alright, makes sense

view this post on Zulip Adeeb K (Apr 21 2020 at 18:26):

quick question

view this post on Zulip Kenny Lau (Apr 21 2020 at 18:26):

quick answer

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 18:27):

cases n

view this post on Zulip Adeeb K (Apr 21 2020 at 18:28):

gotcha thanks

view this post on Zulip Kenny Lau (Apr 21 2020 at 18:29):

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

view this post on Zulip Adeeb K (Apr 21 2020 at 18:29):

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 18:35):

view this post on Zulip Kenny Lau (Apr 21 2020 at 18:35):

see i answered before you asked

view this post on Zulip Kenny Lau (Apr 21 2020 at 18:35):

from your point of view you'd probably say that i answered after you asked

view this post on Zulip Kenny Lau (Apr 21 2020 at 18:36):

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 18:36):

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 18:37):

(nobody will get this reference)

view this post on Zulip Adeeb K (Apr 21 2020 at 19:03):

Okay I believe I have something

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

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 19:07):

[0] is empty, not {0}

view this post on Zulip Kevin Buzzard (Apr 21 2020 at 19:07):

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

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

view this post on Zulip Adeeb K (Apr 21 2020 at 19:14):

I see a small problem.

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

view this post on Zulip Adeeb K (Apr 21 2020 at 19:23):

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 19:23):

this suggests you relabel them

view this post on Zulip Adeeb K (Apr 21 2020 at 19:23):

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

view this post on Zulip Adeeb K (Apr 21 2020 at 19:23):

oh

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

view this post on Zulip Adeeb K (Apr 21 2020 at 19:26):

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

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

view this post on Zulip Adeeb K (Apr 21 2020 at 19:28):

wait shoot that's backwards

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

view this post on Zulip Adeeb K (Apr 21 2020 at 19:29):

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

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

view this post on Zulip Adeeb K (Apr 21 2020 at 19:32):

which is a contradiction. Is there anything I missed?

view this post on Zulip Kenny Lau (Apr 21 2020 at 19:34):

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 19:34):

but relabel \o f is injective

view this post on Zulip Kenny Lau (Apr 21 2020 at 19:34):

other than that, LGTM

view this post on Zulip Kenny Lau (Apr 21 2020 at 19:34):

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

view this post on Zulip Adeeb K (Apr 21 2020 at 19:35):

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 19:35):

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 19:35):

relabel o f o lift

view this post on Zulip Adeeb K (Apr 21 2020 at 19:36):

I see I see

view this post on Zulip Adeeb K (Apr 21 2020 at 19:36):

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 19:36):

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 19:36):

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 19:36):

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

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

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

view this post on Zulip Adeeb K (Apr 21 2020 at 19:39):

ah gotcha

view this post on Zulip Adeeb K (Apr 21 2020 at 19:40):

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

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 19:41):

don't forget k

view this post on Zulip Kenny Lau (Apr 21 2020 at 19:41):

if j \le k then j else j-1

view this post on Zulip Adeeb K (Apr 21 2020 at 19:42):

ah gotcha gotcha.

view this post on Zulip Adeeb K (Apr 21 2020 at 19:47):

I'm getting some errors

view this post on Zulip Adeeb K (Apr 21 2020 at 19:47):

here's what I have for relabel so far

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

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 19:48):

read the error

view this post on Zulip Kevin Buzzard (Apr 21 2020 at 19:48):

Looks like lean wanted j.2

view this post on Zulip Kevin Buzzard (Apr 21 2020 at 19:49):

Or maybe it's called j.is_lt or something

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

view this post on Zulip Kevin Buzzard (Apr 21 2020 at 19:49):

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

view this post on Zulip Kenny Lau (Apr 21 2020 at 19:49):

if H : j.1 \le k

view this post on Zulip Adeeb K (Apr 21 2020 at 19:50):

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

view this post on Zulip Adeeb K (Apr 21 2020 at 19:54):

I'm not sure how to use H here

view this post on Zulip Adeeb K (Apr 26 2020 at 22:42):

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

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

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

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