Finishing off induction for pigeonhole

Stream: new members

[Adeeb K]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

similarly with function.injective and set.range

[Mario Carneiro]

succ_greater_than_nat is nat.lt_succ_self

[Adeeb K]

@Mario Carneiro thanks, got it!

[Mario Carneiro]

lift_finite is fin.cast_le (with a different precondition)

[Mario Carneiro]

pred_exists is nat.exists_eq_succ_of_ne_zero although the precondition is slightly different

[Adeeb K]

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]

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]

oh nice, that's really useful

[Adeeb K]

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

[Mario Carneiro]

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

[Mario Carneiro]

import tactic

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

[Adeeb K]

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

[Mario Carneiro]

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]

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

[Adeeb K]

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

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

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

[Adeeb K]

ah I see

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Adeeb K]

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

with h | rfl

[Bryan Gin-ge Chen]

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

[Mario Carneiro]

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]

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

[Adeeb K]

what does

apply hd' h

do here?

[Mario Carneiro]

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]

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

[Mario Carneiro]

yes, and that should be easy enough

[Mario Carneiro]

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

[Adeeb K]

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]

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

[Adeeb K]

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]

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]

None of that matters

[Mario Carneiro]

You can prove that g is injective without anything about f

[Mario Carneiro]

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

[Mario Carneiro]

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

[Adeeb K]

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]

so I let f := lift_finite m n p

[Adeeb K]

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

[Adeeb K]

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]

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]

If you unfold injective first it works correctly

[Adeeb K]

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]

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

[Mario Carneiro]

you can do this with just cases and refl

[Mario Carneiro]

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

[Adeeb K]

okay, so I do cases x1 and cases x2?

[Adeeb K]

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

[Mario Carneiro]

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

[Mario Carneiro]

so you don't have to say anything

[Adeeb K]

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]

the easiest way is actually cases on the equality you have

[Mario Carneiro]

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

[Adeeb K]

what do you mean with cases here?

[Mario Carneiro]

cases f

[Mario Carneiro]

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]

ahhhh I see I see

[Adeeb K]

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]

would I apply a rw or apply tactic here?

[Johan Commelin]

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

[Adeeb K]

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]

Have you played the natural number game?

[Johan Commelin]

It's a great way of practicing the simple tactics

[Adeeb K]

only up to the third world

[Adeeb K]

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]

wait, so I still have stuff to finish for pigeonhole

[Adeeb K]

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

[Kenny Lau]

refl

[Adeeb K]

no but like

[Adeeb K]

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

[Kenny Lau]

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

[Adeeb K]

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

[Adeeb K]

lemme try that

[Johan Commelin]

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

[Adeeb K]

I'm getting an error

[Adeeb K]

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

[Johan Commelin]

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

[Johan Commelin]

Aah but those two are certainly not the same goals

[Johan Commelin]

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

[Kenny Lau]

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

[Adeeb K]

ah nice that worked!

[Adeeb K]

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

[Johan Commelin]

apply hg

[Johan Commelin]

Where hg : injective g

[Adeeb K]

error:

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

[Johan Commelin]

Aah, right, same problem again...

[Adeeb K]

wait

[Adeeb K]

one sec

[Johan Commelin]

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

[Adeeb K]

I got it

[Adeeb K]

I applied injectivity in reverse order and got it

[Adeeb K]

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

[Adeeb K]

I did apply p1 which is injective f

[Adeeb K]

Then I got

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

[Adeeb K]

then apply p2 which is injective g

[Adeeb K]

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

[Adeeb K]

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

[Adeeb K]

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

[Adeeb K]

so uh

[Adeeb K]

suppose I have

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

[Adeeb K]

how do I conclude

inj : injective (g)

?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Adeeb K]

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

[Mario Carneiro]

those two are the same to lean

[Adeeb K]

how do I conclude injective g then? refl?

[Mario Carneiro]

just pretend it says injective g already

[Mario Carneiro]

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

[Adeeb K]

ah, yeah it worked

[Adeeb K]

now the nontrivial case lol

[Adeeb K]

where d = m

[Adeeb K]

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

[Adeeb K]

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

[Adeeb K]

well, not all

[Johan Commelin]

So... formalise a classical proof...

[Adeeb K]

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

[Johan Commelin]

Why not? What are you trying to do?

[Adeeb K]

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]

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

[Johan Commelin]

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

[Adeeb K]

yeah sure

[Adeeb K]

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

[Kenny Lau]

first come up with a math proof

[Kenny Lau]

then formalize it

[Adeeb K]

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]

I'll be back in a few hours probably

[Patrick Stevens]

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.

[Adeeb K]

I see

[Adeeb K]

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]

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

[Adeeb K]

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]

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]

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

[Kenny Lau]

m > m is false

[Adeeb K]

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

[Reid Barton]

Nothing

[Kenny Lau]

you should write down a maths proof first

[Adeeb K]

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

[Kenny Lau]

it doesn't need to be constructive

[Kenny Lau]

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

[Adeeb K]

Alright, makes sense

[Adeeb K]

quick question

[Kenny Lau]

quick answer

[Adeeb K]

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]

cases n

[Adeeb K]

gotcha thanks

[Kenny Lau]

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

[Adeeb K]

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

[Kenny Lau]

[Kenny Lau]

see i answered before you asked

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

(nobody will get this reference)

[Adeeb K]

Okay I believe I have something

[Adeeb K]

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]

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]

[0] is empty, not {0}

[Kevin Buzzard]

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

[Adeeb K]

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]

I see a small problem.

[Adeeb K]

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]

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

[Kenny Lau]

this suggests you relabel them

[Adeeb K]

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

[Adeeb K]

oh

[Adeeb K]

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]

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

[Adeeb K]

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]

wait shoot that's backwards

[Adeeb K]

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

[Adeeb K]

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

[Adeeb K]

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

[Adeeb K]

which is a contradiction. Is there anything I missed?

[Kenny Lau]

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

[Kenny Lau]

but relabel \o f is injective

[Kenny Lau]

other than that, LGTM

[Kenny Lau]

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

[Adeeb K]

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

[Kenny Lau]

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

[Kenny Lau]

relabel o f o lift

[Adeeb K]

I see I see

[Adeeb K]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Adeeb K]

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]

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

[Adeeb K]

ah gotcha

[Adeeb K]

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

[Adeeb K]

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

[Kenny Lau]

don't forget k

[Kenny Lau]

if j \le k then j else j-1

[Adeeb K]

ah gotcha gotcha.

[Adeeb K]

I'm getting some errors

[Adeeb K]

here's what I have for relabel so far

[Adeeb K]

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]

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

[Kenny Lau]

read the error

[Kevin Buzzard]

Looks like lean wanted j.2

[Kevin Buzzard]

Or maybe it's called j.is_lt or something

[Adeeb K]

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]

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

[Kenny Lau]

if H : j.1 \le k

[Adeeb K]

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

[Adeeb K]

I'm not sure how to use H here

[Adeeb K]

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

[Adeeb K]

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

[Adeeb K]

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]

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