## Stream: new members

### Topic: showing injectivity

#### Adeeb K (Apr 28 2020 at 18:51):

I have a definition of a function using the if-then-else pattern, and I want to break it up into cases based on that definition. How can I do so? The context is that I am trying to show a function is injective

#### Adeeb K (Apr 28 2020 at 18:52):

Here is all I have so far

#### Adeeb K (Apr 28 2020 at 18:52):

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 }

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

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

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

-- forgot library function, lifted from square root prime code
-- credit to github user dm1237
lemma succ_eq_add_one (n : ) : nat.succ n = n + 1 :=
begin
exact rfl,
end

-- forgot library function
lemma my_le_trans
(j k m : )
(p1: k < m)
(p2: j  k)
: j < m - 1
:=
begin
intros,
-- try induction?
sorry,
end

lemma inequality_fact
(j m : )
(p: j < m)

: j - 1 < m - 1
:= begin
intros,
sorry
end

/--
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

/--
Every pair that lives in finite_subest m lives in finite_subset n
where m < n
-/
def lift_finite (m n : ) (p : m < n) : finite_subset m  finite_subset n
:= λ k, k.1, lt.trans k.2 p

/--
Application of lift_finite from m to m + 1
-/
def lift_one
(m : )
: finite_subset m  finite_subset (m + 1)
:= (lift_finite m (m+1) (succ_greater_than_nat m))

lemma lift_one_fst {m} (j : finite_subset m) : (lift_one m j).fst = j.fst
:=
begin
refl,

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

/--
The lifting from m to m + 1 injective
-/
lemma lift_one_injective (m : )
: injective (lift_one m)
:= begin
apply lift_finite_injective m (m + 1) (succ_greater_than_nat m),
end

lemma ext_iff (n : ) (a b : finite_subset n) : a = b  a.1 = b.1 :=
begin
cases a,
cases b,
split,
{ intro h, rw h},
{ intro h, cases h, refl,}
end

def relabel
(m k : )
(p: k < m)
: finite_subset m  finite_subset (m - 1)
:= λ j, if H : j.1  k then j.1, my_le_trans j.1 k m p H  else j.1 - 1, inequality_fact j.1 m j.2

/-
This formalizes the notion that when f is injective and misses k
in the codomain then when we relabel to bring m to m - 1,
composition is injective
-/
lemma relabel_with_inj_f_misses_k_is_inj
(m k : )
(p: k < m)
(f: finite_subset m  finite_subset m)
(inj: injective f)
: injective ((relabel m k p)  f)
:=
begin
intros x,
intros,

sorry,
end

--proof that f : [m + 2] -> [m + 1] restricted
--to [m + 1] = {0, 1, ..., m} does not hit f(m + 1)
lemma miss_proof
{m} (f : finite_subset (m + 2)  finite_subset (m + 1))
(inj : injective f)
{pf: m + 1 < m + 2}
:  j : finite_subset (m + 1), (f  lift_one (m + 1)) j  f m + 1,  pf
:= begin

introv p,
change f (lift_one (m+1) j) = f m + 1,  pf at p,
let p2 := inj (lift_one (m+1) j) m + 1,  pf,
let p3 := p2 p,
rw ext_iff at p3,
rw lift_one_fst at p3,
let p4 := j.2,
linarith,

end

lemma relabel_inj
(m k : )
(p: k < m)
(f: finite_subset (m + 2)  finite_subset (m + 1))
(inj: injective f)
{pf} (miss:  j : finite_subset (m + 1), (f  lift_one (m + 1)) j  k,  pf )
: injective ((relabel (m + 1) k pf)  f  lift_one (m + 1))
:=
begin
introv x,
let y := x₂,
intros,
change (relabel (m + 1) k pf (f (lift_one (m + 1) x))) = (relabel (m + 1) k pf (f (lift_one (m + 1) x₂))) at a,
let x_l := (lift_one (m + 1) x),
let y_l := (lift_one (m + 1) x₂),
change relabel (m + 1) k pf (f x_l) = relabel (m + 1) k pf (f y_l) at a,
let r_x_l := relabel (m + 1) k pf (f x_l),
let r_y_l := relabel (m + 1) k pf (f y_l),
change r_x_l = r_y_l at a,

sorry,

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_one d),
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 g_injective := comp_inj_is_inj (lift_one d) f (lift_one_injective d) f_injective,
exact g_injective,
},

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

induction m with l hl,

{
let e:= f 0,_ ,
let e2 := e.2,
linarith,
exact n_gt_m,
},

let k := f l + 1, succ_greater_than_nat (l + 1), -- let k = f(l + 1)
let violator := f  (lift_one (l + 1)),
let restriction := (relabel (l + 1) k.1 k.2)  violator,
let violator_is_inj := comp_inj_is_inj (lift_one (l + 1)) f (lift_one_injective (l + 1)) f_injective,
let res_is_inj := relabel_with_inj_f_misses_k_is_inj (l + 1) k.1 k.2 violator violator_is_inj,
/- contradiction, since restriction: [m] →  [m - 1] is injective,
but this can't be true IH
-/
refine hl _ _ _ _ ,
{
intros,
linarith,
},
{
exact restriction,
},
{
exact succ_greater_than_nat _,
},
{
exact res_is_inj,
},

}

end

#### Adeeb K (Apr 28 2020 at 18:53):

I am trying to prove relabel_inj. It uses the definition of relabel.

#### Adeeb K (Apr 28 2020 at 18:57):

Should I cut down the size of the code block?

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

I tried cases but that seems to come from if I do induction on k?

#### Kevin Buzzard (Apr 28 2020 at 19:08):

Try the split_ifs tactic

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

so split_ifs at a, where a : relabel (m + 1) k pf (f x_l) = relabel (m + 1) k pf (f y_l)?

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

I'm getting this error:

no if-then-else expressions to split

#### Reid Barton (Apr 28 2020 at 19:10):

I think this lemma will benefit from some strategic planning and maybe writing out a proof on paper first.

#### Kevin Buzzard (Apr 28 2020 at 19:10):

https://leanprover-community.github.io/mathlib_docs/tactics.html#split_ifs

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

I did write out a proof on paper

#### Reid Barton (Apr 28 2020 at 19:10):

Okay, what did you do at this point then?

#### Reid Barton (Apr 28 2020 at 19:11):

There is a better way to go about this than forging ahead with case splits here--I don't know whether it is a "spoiler" though.

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

at this point, I split the proof into two cases based on the definition of relabel. Either the RHS = LHS ≤ k or RHS = LHS > k

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

then, by miss_proof, we know that RHS = LHS != k

#### Reid Barton (Apr 28 2020 at 19:12):

So you are splitting based on the output of relabel?

yes

#### Reid Barton (Apr 28 2020 at 19:12):

Okay, that is better than what I thought you were intending, but not what split_ifs does.

#### Reid Barton (Apr 28 2020 at 19:13):

Still, I think breaking things down into more lemmas would help.

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

then I should be able to conclude that either f x_l = f y_l or (< (f x_1) - 1, (f x_1).snd >) = (< (f y_1) - 1, (f y_1).snd >), both of which would give me that x = y by injectivity of lift_one and f

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

I'm not sure how to split this into lemmas, or at least it isn't _immediately_ obvious to me how to do so

#### Reid Barton (Apr 28 2020 at 19:15):

then, by miss_proof, we know that RHS = LHS != k

Actually, this is not true, is it?

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

It should be by miss_proof we gave earlier

#### Reid Barton (Apr 28 2020 at 19:16):

then I should be able to conclude that either f x_l = f y_l or (< (f x_1) - 1, (f x_1).snd >) = (< (f y_1) - 1, (f y_1).snd >), both of which would give me that x = y by injectivity of lift_one and f

How do you know that both f x_1 and f y_1 fall into the same case of relabel?

#### Reid Barton (Apr 28 2020 at 19:16):

It should be by miss_proof we gave earlier

But this is about the input of relabel, not the output of relabel.

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

this whole proof to show that the composition is injective is to lead up to a contradiction in pigeonhole principle - I end up getting this whole thing is an injective function from [m + 1] to [m] which is a contradiction according to my inductive hypothesis

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

because f x_1 = f y_1

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

by injectivity of lift_one and f right?

#### Reid Barton (Apr 28 2020 at 19:17):

Wait, that's what you're trying to prove.

right right

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

but by the definition of relabel, they have to either be <= k or > k right? You can't be <= k and > k at the same time

#### Reid Barton (Apr 28 2020 at 19:18):

How do you know, for example, that relabel 100 7 _ 3 isn't equal to relabel 100 7 _ 21.

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

but wouldn't that imply that 2 = 20?

#### Reid Barton (Apr 28 2020 at 19:19):

Well, of course it's because 3 doesn't equal 20 but you have to consider this case and really use the definition of relabel somehow.

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

oh, so this means I should introduce a lemma

#### Reid Barton (Apr 28 2020 at 19:20):

So I think this means in your paper proof you are implicitly assuming something which is "obvious" about the behavior of relabel, and you should figure out what it is and formulate it as a lemma.

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

if (relabel m k p) x = (relabel m k p) y
then x, y <= k or x, y > k

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

suppose not - then WLOG there exists x, y such that x <= k and y > k, but then ((relabel m k p) x).1 = x - 1 < k <= y = ((relabel m k p) y).2

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

contradiction, so no such pair exist?

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

though I made a leap here

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

I assumed then x, y <= k or x, y > k if and only if !(x <= k and y > k)

#### Reid Barton (Apr 28 2020 at 19:23):

This is not the correct formula for relabel

#### Reid Barton (Apr 28 2020 at 19:25):

It is a good general direction though.

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

what's not the correct formula?

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

oh, the way I split it up?

#### Reid Barton (Apr 28 2020 at 19:27):

((relabel m k p) x).1 = x - 1 < k <= y = ((relabel m k p) y).2

oh right right

other way around

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

((relabel m k p) x).1 = x <= k <= y = ((relabel m k p) y).2
which means either ((relabel m k p) x).1 < ((relabel m k p) y).2, contradiction

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

or ((relabel m k p) x).1 = ((relabel m k p) y).2 = k, contradiction by miss_proof

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

I wrote down the statement of the lemma:

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

lemma relabel_behavior
(m k : )
(p: k < m)
{pf} (miss:  j : finite_subset m, (relabel m k p) j  k,  pf )
:  x y : finite_subset m, (x.1  k  y.1  k)  (x.1 > k  y.1 > k)
:=
begin
sorry
end

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

Not sure how to translate the proof above into lean - I imagine it would use a lot of transitivity of inequalities?

#### Reid Barton (Apr 28 2020 at 19:39):

Well this lemma is true but useless, because miss is just false.

it is?

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

wait, how? If I have an injective function f from {0, 1, ..., m + 1} to {0, 1, ..., m } (no such function exists, but this is a lemma that helps me set up the conclusion to pigeonhole by assuming such an injective function exists in the first place), and I restrict my domain to {0, 1, ..., m } instead, then there is no element in the domain that will equal f(m + 1) since f is injective

#### Reid Barton (Apr 28 2020 at 19:43):

There is no f in the statement of relabel_behavior.

oh right..

#### Reid Barton (Apr 28 2020 at 19:44):

But, something like it is true and useful.

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

I'm not sure I see it?

#### Patrick Massot (Apr 28 2020 at 19:44):

Adeeb, it seems you should think much more seriously about the proof on paper.

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

I (believe) I understand the proof, but there are a bunch of steps I think I didn't write out explicitly since they felt ''obvious''

#### Patrick Massot (Apr 28 2020 at 19:46):

But you're here to unlearn that feeling, right?

yes

#### Reid Barton (Apr 28 2020 at 19:47):

Patrick, you make it sound like The Matrix

#### Patrick Massot (Apr 28 2020 at 19:48):

Lean: the red pill.

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

Okay, so miss is not true simply because if k < m - 1 then k + 1 < m, which means that there is in fact an element for which relabel m k p j = <k, pf>

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

and I probably don't really care about miss in the first place

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

what I care about is showing that either x, y <= k or x, y > k

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

So what I have now is:

lemma relabel_behavior
(m k : )
(p: k < m)
:  x y : finite_subset m, (x.1  k  y.1  k)  (x.1 > k  y.1 > k)
:=
begin
sorry
end

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

is this the full 'useful' statement, or is there another detail I'm missing?

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

wait wait wait one second

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

sorry I meant this:

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

lemma relabel_behavior
(m k : )
(p: k < m)
:  x y : finite_subset m,
(relabel m k p) x = (relabel m k p) y
(x.1  k  y.1  k)  (x.1 > k  y.1 > k)
:=
begin
sorry
end

#### Reid Barton (Apr 28 2020 at 19:54):

It's getting closer but still not correct.

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

is there something I'm missing or am I asserting something that's too strong?

#### Reid Barton (Apr 28 2020 at 19:56):

Does the statement look true to you? Forget about the pigeonhole proof.

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

uh I think it probably doesn't match the way I have relabel defined

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

so it would be better like this:

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

lemma relabel_behavior
(m k : )
(p: k < m)
:  x y : finite_subset m,
(relabel m k p) x = (relabel m k p) y
(x.1  k  y.1  k)  (x.1  k  y.1  k)
:=
begin
sorry
end

is this closer?

#### Adeeb K (Apr 28 2020 at 20:00):

which is really 3 cases?

#### Adeeb K (Apr 28 2020 at 20:02):

Is there something really big and obvious that I'm missing, or is it more subtle?

#### Reid Barton (Apr 28 2020 at 20:03):

I think it is okay now.

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

alright, cool! Then...I'm not sure how to start after maybe an intros or introv

#### Adeeb K (Apr 28 2020 at 20:08):

I introv p, which gives me the following window:

#### Adeeb K (Apr 28 2020 at 20:08):

1 goal
m k : ,
p : k < m,
x y : finite_subset m,
p : relabel m k p x = relabel m k p y
x.fst  k  y.fst  k  x.fst  k  y.fst  k

#### Adeeb K (Apr 28 2020 at 20:09):

how can I split the goal?

#### Adeeb K (Apr 28 2020 at 20:15):

actually, I'm sort of lost as to how I would get cases to examine the relabel m k p x in the first place

#### Adeeb K (Apr 28 2020 at 20:36):

wait, would split_ifs help me here to split the goal or split the cases for relabel's output?

#### Kevin Buzzard (Apr 28 2020 at 20:42):

how can I split the goal?

Have you read Theorem Proving In Lean or played the natural number game? If you don't know what to do with a goal which is just logical connectives and propositions then perhaps you've bitten off more than you can chew.

#### Reid Barton (Apr 28 2020 at 20:45):

Well, I don't think the NNG covers if, does it?

#### Kevin Buzzard (Apr 28 2020 at 20:46):

I thought the question was what to do with x.fst ≤ k ∧ y.fst ≤ k ∨ x.fst ≥ k ∧ y.fst ≥ k?

#### Adeeb K (Apr 28 2020 at 20:47):

Well, I'm sort of asking about both. I'm wondering how I can split up relabel m k p x into cases for its output

#### Kevin Buzzard (Apr 28 2020 at 20:47):

@Adeeb K if you read the documentation for split_ifs you will see exactly what it does.

#### Adeeb K (Apr 28 2020 at 20:47):

as for x.fst ≤ k ∧ y.fst ≤ k ∨ x.fst ≥ k ∧ y.fst ≥ k I'll do more of the natural number game - I think I got 3-4 worlds in my last time

#### Kevin Buzzard (Apr 28 2020 at 20:47):

In particular, split_ifs will only work if it can see an if

#### Adeeb K (Apr 28 2020 at 20:48):

and I should be able to apply it to a statement that isn't the goal?

#### Kevin Buzzard (Apr 28 2020 at 20:48):

Kevin Buzzard said:

Adeeb K if you read the documentation for split_ifs you will see exactly what it does.

#### Adeeb K (Apr 28 2020 at 20:49):

but I keep getting errors when I do so..

#### Kevin Buzzard (Apr 28 2020 at 20:49):

Kevin Buzzard said:

In particular, split_ifs will only work if it can see an if

#### Adeeb K (Apr 28 2020 at 20:51):

relabel is defined with an if-then-else and starts with an if. Do you mean I have to manually put the if into my expression?

#### Kevin Buzzard (Apr 28 2020 at 20:52):

Yes, it really need to be able to see an if. Can you unfold?

#### Kevin Buzzard (Apr 28 2020 at 20:54):

Some tactics work up to definitional equality, and some up to syntactic equality. In other words, some tactics will be fine if what you point them at is equal by definition to what they're expecting (e.g. exact) but others will only work if what you point them at is literally the string of characters they are expecting (e.g. rw or split_ifs).

#### Adeeb K (Apr 28 2020 at 20:54):

I get an error for the simplify tactic failing to simplify when I unfold at p2

#### Kevin Buzzard (Apr 28 2020 at 20:54):

unfold at p2 doesn't make any sense

#### Kevin Buzzard (Apr 28 2020 at 20:54):

https://leanprover-community.github.io/mathlib_docs/tactics.html#unfold

#### Adeeb K (Apr 28 2020 at 20:56):

okay, I just read through unfold. I'm not sure how to use it in this case, or what my constants as arguments would be in this case.

What is p2?

#### Adeeb K (Apr 28 2020 at 20:58):

p2 : relabel m k p x = relabel m k p y

#### Johan Commelin (Apr 28 2020 at 20:59):

Did you mean unfold relabel at p2?

#### Reid Barton (Apr 28 2020 at 20:59):

The documentation is written in such jargon that someone who understands it would probably already know how to use unfold.
More useful would be an example or links to TPIL or similar.

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

oh, that makes sense
sorry I wasn't seeing it earlier..

#### Kevin Buzzard (Apr 28 2020 at 21:01):

Yes, the documentation is a bit crappy for unfold :-/

#### Kevin Buzzard (Apr 28 2020 at 21:01):

The core tactics were only recently documented.

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

[makes a note to PR better docs for unfold]

thanks again

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

I'll chew on some of the cases before asking for help with the main theorem

#### Adeeb K (Apr 29 2020 at 00:05):

okay right now I have two cases: nat.sub k 0 < x.fst and nat.sub k 0 = x.fst

#### Adeeb K (Apr 29 2020 at 00:05):

suppose p : nat.sub k 0 < x.fst. Is there a tactic that lets me conclude k < x.fst?

#### Kenny Lau (Apr 29 2020 at 00:08):

rw nat.sub_zero at p

#### Adeeb K (Apr 29 2020 at 00:15):

rewrite tactic failed, did not find instance of the pattern in the target expression
?m_1 - 0

#### Kenny Lau (Apr 29 2020 at 00:15):

erw nat.sub_zero at p

#### Adeeb K (Apr 29 2020 at 00:16):

it still has the same error

#### Kenny Lau (Apr 29 2020 at 00:16):

change k - 0 < x.1 at p; rw nat.sub_zero at p

actually

#### Kenny Lau (Apr 29 2020 at 00:17):

change k < x.1 at p

match failed

#### Adeeb K (Apr 29 2020 at 00:20):

I have no idea what's going on..

MWE

sure thing

#### Adeeb K (Apr 29 2020 at 00:22):

import tactic

lemma inequality_fact
(j m : )
(p: j < m)

: j - 1 < m - 1
:= begin
intros,
sorry
end

lemma ext_iff (n : ) (a b : finite_subset n) : a = b  a.1 = b.1 :=
begin
cases a,
cases b,
split,
{ intro h, rw h},
{ intro h, cases h, refl,}
end

lemma relabel_behavior
(m k : )
(p: k < m)
:  x y : finite_subset m,
(relabel m k p) x = (relabel m k p) y
(x.1  k  y.1  k)  (x.1  k  y.1  k)
:=
begin
introv p2,
unfold relabel at p2,
split_ifs at p2,
{ left,
split,
exact h,
exact h_1,
},

{
right,
split,

{
cases lt_or_eq_of_le h,
{
let q := le_of_not_ge h_1,
cases lt_or_eq_of_le q,

{ exfalso,
let h4 := inequality_fact k y.fst h_3,
rw ext_iff at p2,
change x.fst = y.fst - 1 at p2,
let p2refl := eq.symm p2,
rw p2refl at h4,
let rw_h4 := nat.le_of_pred_lt h4,
change k < x.fst at rw_h4,

cases lt_or_eq_of_le rw_h4,

{linarith,},

{},

--change k ≤ x.fst at h4,
sorry},

{

sorry},

{
exact le_of_eq (eq.symm h_2),
},
},

exact le_of_not_ge h_1,
},

{
right,
split,
exact le_of_not_ge h,
-- same proof but symmetric
{sorry

},

},

{
right,
split,
exact le_of_not_ge h,
exact le_of_not_ge h_1,
},
end

#### Adeeb K (Apr 29 2020 at 00:23):

my problem is right above cases lt_or_eq_of_le rw_h4,

#### Kenny Lau (Apr 29 2020 at 00:26):

1. inequality_fact is wrong (j=0, m=1)
2. finite_subset doesn't exist
3. relabel doesn't exist

#### Kenny Lau (Apr 29 2020 at 00:28):

in the definition of finite_subset:

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

there's no need to use Σ': Σ by itself would be fine

not there

#### Mario Carneiro (Apr 29 2020 at 00:29):

you need {k // k < n} there

#### Adeeb K (Apr 29 2020 at 00:32):

ooh shoot lemme give the remaining code. For inequality_fact I'm aware there's a small error for the 0 case, but I was going to go back and prove the fixed version after I finished the main lemma

#### Adeeb K (Apr 29 2020 at 00:32):

I'll paste the code here again:

#### Mario Carneiro (Apr 29 2020 at 00:33):

The correct version of inequality_fact is nat.sub_lt_sub_right_iff

#### Adeeb K (Apr 29 2020 at 00:34):

import tactic

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

lemma inequality_fact
(j m : )
(p: j < m)
: j - 1 < m - 1
:= begin
intros,
sorry
end

lemma ext_iff (n : ) (a b : finite_subset n) : a = b  a.1 = b.1 :=
begin
cases a,
cases b,
split,
{ intro h, rw h},
{ intro h, cases h, refl,}
end

def relabel
(m k : )
(p: k < m)
: finite_subset m  finite_subset (m - 1)
:= λ j, if H : j.1  k then j.1, my_le_trans j.1 k m p H  else j.1 - 1, inequality_fact j.1 m j.2

lemma relabel_behavior
(m k : )
(p: k < m)
:  x y : finite_subset m,
(relabel m k p) x = (relabel m k p) y
(x.1  k  y.1  k)  (x.1  k  y.1  k)
:=
begin
introv p2,
unfold relabel at p2,
split_ifs at p2,
{ left,
split,
exact h,
exact h_1,
},

{
right,
split,

{
cases lt_or_eq_of_le h,
{
let q := le_of_not_ge h_1,
cases lt_or_eq_of_le q,

{ exfalso,
let h4 := inequality_fact k y.fst h_3,
rw ext_iff at p2,
change x.fst = y.fst - 1 at p2,
let p2refl := eq.symm p2,
rw p2refl at h4,
let rw_h4 := nat.le_of_pred_lt h4,
change k < x.fst at rw_h4,

cases lt_or_eq_of_le rw_h4,

{linarith,},

{},

--change k ≤ x.fst at h4,
sorry},

{

sorry},

{
exact le_of_eq (eq.symm h_2),
},
},

exact le_of_not_ge h_1,
},

{
right,
split,
exact le_of_not_ge h,
-- same proof but symmetric
{sorry

},

},

{
right,
split,
exact le_of_not_ge h,
exact le_of_not_ge h_1,
},
end

#### Adeeb K (Apr 29 2020 at 00:34):

@Mario Carneiro I'll substitute that in and modify accordingly then. Thanks!

#### Kenny Lau (Apr 29 2020 at 00:36):

the answer to the nat.sub x 0 is that you used let instead of have:

have rw_h4 := nat.le_of_pred_lt h4,
change k  x.1 at rw_h4,

#### Kenny Lau (Apr 29 2020 at 00:36):

(also it was \le not <)

#### Adeeb K (Apr 29 2020 at 00:39):

okay! give me a second to change it

#### Kenny Lau (Apr 29 2020 at 00:44):

import tactic

lemma inequality_fact (j m : ) (h : j < m) : j - 1 < m - 1 := sorry

def finite_subset (n : ) := { k // k < n }

def relabel (m k : ) (h : k < m) (j : finite_subset m) : finite_subset (m - 1) :=
if H : j.1  k then j.1, sorry else j.1 - 1, sorry

lemma ext_iff (n : ) (a b : finite_subset n) : a = b  a.1 = b.1 :=
subtype.ext

lemma relabel_behavior (m k : ) (h : k < m) (x y : finite_subset m) (hxy : relabel m k h x = relabel m k h y) :
(x.1  k  y.1  k)  (x.1  k  y.1  k) :=
begin
unfold relabel at hxy,
split_ifs at hxy with hxk hyk hyk,
{ left; split; assumption },
{ right; split,
{ rw subtype.mk_eq_mk at hxy,
cases lt_or_eq_of_le hxk with hxlk hxek,
{ rw hxy at hxlk, exact absurd (nat.le_of_pred_lt hxlk) hyk },
{ exact ge_of_eq hxek } },
{ exact le_of_not_ge hyk } },
{ right; split,
{ exact le_of_not_ge hxk },
{ rw subtype.mk_eq_mk at hxy,
cases lt_or_eq_of_le hyk with hylk hyek,
{ rw  hxy at hylk, exact absurd (nat.le_of_pred_lt hylk) hxk },
{ exact ge_of_eq hyek } } },
{ right; split; apply le_of_not_ge; assumption }
end

#### Adeeb K (Apr 29 2020 at 00:48):

oh damn. Thank you so much!

wait

#### Adeeb K (Apr 29 2020 at 01:12):

so changing the definition of finite_subset introduced a few errors into my existing code. Can I give you a snippet of the stuff that has errors?

#### Kenny Lau (Apr 29 2020 at 01:12):

change x.fst to x.1

#### Adeeb K (Apr 29 2020 at 01:13):

the errors don't pertain to that, at least not as far as I can tell?

#### Adeeb K (Apr 29 2020 at 01:13):

Here, lemme get an example

#### Adeeb K (Apr 29 2020 at 01:17):

import tactic

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

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

theorem lift_finite_injective (m n : ) (p : m < n) :
injective (lift_finite m n p)
:= begin
introv x p2,
cases x,
cases x₂,
cases p2,
refl,
end

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

here there is an error at cases p2,

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

the error is: cases tactic failed, unexpected failure when introducing auxiliary equatilies

#### Reid Barton (Apr 29 2020 at 01:20):

I wonder why it ever worked.

#### Reid Barton (Apr 29 2020 at 01:20):

Anyways, I wouldn't recommend changing your definitions in the middle of working on a huge proof...

#### Kenny Lau (Apr 29 2020 at 01:20):

hmm I wonder why it doesn't work in this case

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

it seems only this proof was affected. Luckily, no other proofs were affected ( as far as I can tell based on a glance at the errors)

#### Reid Barton (Apr 29 2020 at 01:24):

By the way, where did you learn introv? I've never seen anyone else use it.

#### Adeeb K (Apr 29 2020 at 01:26):

I was browsing the mathlib section looking at intro and intros. This tactic appeared right after those, so I checked it out.

#### Adeeb K (Apr 29 2020 at 01:40):

I'm not sure how to fix lift_finite_injective

#### Reid Barton (Apr 29 2020 at 01:41):

This is its time to shine.

#### Adeeb K (Apr 29 2020 at 01:51):

okay, I'll try it

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

okay, it did the trick

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

theorem lift_finite_injective (m n : ) (p : m < n) :
injective (lift_finite m n p)
:= begin
introv x p2,
cases x,
cases x₂,
rw ext_iff at p2,
exact (ext_iff m x_val, x_property x₂_val, x₂_property).mpr p2,
end

#### Reid Barton (Apr 29 2020 at 02:11):

Okay. May I suggest:

theorem lift_finite_injective (m n : ) (p : m < n) :
injective (lift_finite m n p) :=
begin
intros x₁ x₂ h,
rw ext_iff at  h,
exact h
end

lemme try that

it works!

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

thank you! I'll examine the differences at these two approaches later tonight

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

Right now, my plan is this:

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

from relabel_behavior, I know that relabel m k p f (x_l) = relabel m k p f (y_l) implies f (x_1) <= k and f (y_1) <= k, or f (x_1) >= k and f (y_1) >= k

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

I want to make a lemma where z <= k implies (relabel m k p) z = < z, z < m>

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

and another where z >= k implies (relabel m k p) z = < z - 1, z - 1 < m >

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

this shouldn't be too hard based on the definition of relabel, right?

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

actually...I'm not sure how to start

#### Adeeb K (Apr 29 2020 at 08:03):

to repeat the latest from the noob questions thread

#### Adeeb K (Apr 29 2020 at 08:03):

I see. I'm getting an error from the following:

let h1_strict := lt_of_le_of_ne h1 m_x,

which is giving me the error:

type mismatch at application
lt_of_le_of_ne h1 m_x
term
m_x
has type
¬((f  lift_one (m + 1)) x).val = (f m + 1, _⟩).val
but is expected to have type
(f m + 1, _⟩).val  (f (lift_one (m + 1) x)).val

#### Adeeb K (Apr 29 2020 at 08:04):

...I have to flip the equality?

#### Mario Carneiro (Apr 29 2020 at 08:05):

eq.symm or ne.symm

ah, thank you

#### Adeeb K (Apr 29 2020 at 08:09):

@Kenny Lau I still don't understand how to use dif_neg here now that I have proofs for (f ⟨m + 1, _⟩).val < (f (lift_one (m + 1) x)).valand (f ⟨m + 1, _⟩).val < (f (lift_one (m + 1) y)).val

#### Kenny Lau (Apr 29 2020 at 08:10):

Kenny Lau said:

have hnk : \not k \le ...,

Kenny Lau said:

and after you prove it, rw dif_neg hnk

#### Adeeb K (Apr 29 2020 at 08:10):

I'm getting an error. should I send an MWE?

#### Adeeb K (Apr 29 2020 at 08:13):

Here it is @Kenny Lau

import tactic

def injective {X Y} (f : X  Y) :=  x₁ x₂, f x₁ = f x₂  x₁ = x₂
lemma succ_greater_than_nat (n : ) : nat.succ n > n := sorry
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
def lift_one (m : ) : finite_subset m  finite_subset (m + 1) := (lift_finite m (m+1) (succ_greater_than_nat m))
theorem lift_finite_injective (m n : ) (p : m < n) : injective (lift_finite m n p) := sorry
lemma lift_one_injective (m : )  : injective (lift_one m) := sorry
def relabel (m k : ) (h : k < m) (j : finite_subset m) : finite_subset (m - 1) :=
if H : j.1  k then j.1, sorry else j.1 - 1, sorry
lemma apply_relabel_lt (m k : ) (hkm : k < m) (z : finite_subset m) (h2 : z.1  k) (h3 : z.1 < m - 1) : relabel m k hkm z = z.1, h3 := sorry
lemma apply_relabel_gt (m k : ) (hkm : k < m) (z : finite_subset m) (h2 : k < z.1) (h3 : z.1 - 1 < m - 1) : relabel m k hkm z = z.1 - 1, h3 := sorry
lemma relabel_behavior (m k : ) (h : k < m) (x y : finite_subset m) (hxy : relabel m k h x = relabel m k h y) : (x.1  k  y.1  k)  (x.1  k  y.1  k) := sorry

lemma relabel_inj (m k : ) (hkm : k < m + 1)
(f: finite_subset (m + 2)  finite_subset (m + 1))
(inj : injective f)
(pf : (f  m + 1, succ_greater_than_nat (m + 1) ).1 < m + 1)
(miss :  j : finite_subset (m + 1), (f  lift_one (m + 1)) j  f m + 1,  succ_greater_than_nat (m + 1) ) :
injective ((relabel (m + 1) (f m + 1, succ_greater_than_nat (m + 1)).1 pf)  f  lift_one (m + 1)) :=
begin
intros x y h,
change (relabel (m + 1) (f  m + 1, succ_greater_than_nat (m + 1) ).1 pf (f (lift_one (m + 1) x))) = (relabel (m + 1) (f  m + 1, succ_greater_than_nat (m + 1) ).1 pf (f (lift_one (m + 1) y))) at h,
rcases relabel_behavior _ _ _ _ _ h with h1, h2 | h1, h2⟩; unfold relabel at h,
{ sorry },
{
have m_x := (miss x),
replace m_x := mt subtype.eq m_x,
have m_y := (miss y),
replace m_y := mt subtype.eq m_y,
let h1_strict := lt_of_le_of_ne h1 (ne.symm m_x),
let h2_strict := lt_of_le_of_ne h2 (ne.symm m_y),

rw dif_neg h1_strict, --type mismatch at application dif_neg h1_strict
sorry },
end

#### Kenny Lau (Apr 29 2020 at 08:14):

what is the error

#### Adeeb K (Apr 29 2020 at 08:14):

type mismatch at application
dif_neg h1_strict
term
h1_strict
has type
(f m + 1, _⟩).val < (f (lift_one (m + 1) x)).val
but is expected to have type
¬?m_1

#### Kenny Lau (Apr 29 2020 at 08:14):

and read what I told you

#### Kenny Lau (Apr 29 2020 at 08:15):

Kenny Lau said:

have hnk : \not k \le ...,

Kenny Lau said:

and after you prove it, rw dif_neg hnk

#### Kenny Lau (Apr 29 2020 at 08:15):

you need to prove \not k \le ...

#### Kenny Lau (Apr 29 2020 at 08:15):

first of all there's not even a k in the h1_strict

#### Kenny Lau (Apr 29 2020 at 08:16):

also stop abbreviating terms

#### Adeeb K (Apr 29 2020 at 08:16):

what abbreviating?

#### Kenny Lau (Apr 29 2020 at 08:16):

have m_x := (miss x),

#### Kenny Lau (Apr 29 2020 at 08:16):

I retract my comment about k

alright

#### Kenny Lau (Apr 29 2020 at 08:17):

type mismatch at application
dif_neg h1_strict
term
h1_strict
has type
(f m + 1, _⟩).val < (f (lift_one (m + 1) x)).val
but is expected to have type
¬?m_1
state:
m k : ,
hkm : k < m + 1,
f : finite_subset (m + 2)  finite_subset (m + 1),
inj : injective f,
pf : (f m + 1, _⟩).val < m + 1,
miss :  (j : finite_subset (m + 1)), (f  lift_one (m + 1)) j  f m + 1, _⟩,
x y : finite_subset (m + 1),
h1 : (f (lift_one (m + 1) x)).val  (f m + 1, _⟩).val,
h2 : (f (lift_one (m + 1) y)).val  (f m + 1, _⟩).val,
h :
dite ((f (lift_one (m + 1) x)).val  (f m + 1, _⟩).val)
(λ (H : (f (lift_one (m + 1) x)).val  (f m + 1, _⟩).val), (f (lift_one (m + 1) x)).val, _⟩)
(λ (H : ¬(f (lift_one (m + 1) x)).val  (f m + 1, _⟩).val), (f (lift_one (m + 1) x)).val - 1, _⟩) =
dite ((f (lift_one (m + 1) y)).val  (f m + 1, _⟩).val)
(λ (H : (f (lift_one (m + 1) y)).val  (f m + 1, _⟩).val), (f (lift_one (m + 1) y)).val, _⟩)
(λ (H : ¬(f (lift_one (m + 1) y)).val  (f m + 1, _⟩).val), (f (lift_one (m + 1) y)).val - 1, _⟩),
m_x : ¬((f  lift_one (m + 1)) x).val = (f m + 1, _⟩).val,
m_y : ¬((f  lift_one (m + 1)) y).val = (f m + 1, _⟩).val,
h1_strict : (f m + 1, _⟩).val < (f (lift_one (m + 1) x)).val := lt_of_le_of_ne h1 (ne.symm m_x),
h2_strict : (f m + 1, _⟩).val < (f (lift_one (m + 1) y)).val := lt_of_le_of_ne h2 (ne.symm m_y)
x = y

#### Kenny Lau (Apr 29 2020 at 08:17):

because this time the clause in the dite is (f (lift_one (m + 1) x)).val ≤ (f ⟨m + 1, _⟩).val

#### Kenny Lau (Apr 29 2020 at 08:17):

so you need to prove ¬(f (lift_one (m + 1) x)).val ≤ (f ⟨m + 1, _⟩).val

#### Kenny Lau (Apr 29 2020 at 08:17):

which to you is equivalent to ... > ...

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

but to Lean they are not definitionally equivalent

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

would not_le.mpr ((f (lift_one (m + 1) x)).val ≤ (f ⟨m + 1, _⟩).val) give me what I'm looking for?

#### Kenny Lau (Apr 29 2020 at 08:20):

oh and I retract my comment about miss x being an abbreviation

#### Adeeb K (Apr 29 2020 at 08:20):

I library searched for a function after writing a small lemma, and that is what I got:

lemma lib
(x y : )
(p: x > y)
: ¬ x  y
:= begin
exact not_le.mpr p,
end

#### Kenny Lau (Apr 29 2020 at 08:20):

but your two lets should bave haves because they are propositions

#### Kenny Lau (Apr 29 2020 at 08:20):

basically, the principle is that if you see a let in your code then you're doing something wrong

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

yeah so use it and dif_neg

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

alright, changed them to have's. I'll ask about have vs let tomorrow since it's pretty late and I want to finish this theorem up as soon as I can

okay one sec

#### Adeeb K (Apr 29 2020 at 08:22):

rewrite tactic failed, did not find instance of the pattern in the target expression
dite ((f (lift_one (m + 1) x)).val  (f m + 1, _⟩).val) ?m_2 ?m_3

#### Adeeb K (Apr 29 2020 at 08:22):

this is in response to typing

rw dif_neg (not_le.mpr h1_strict)

#### Kenny Lau (Apr 29 2020 at 08:23):

did you forget at h

...oh whoops

#### Adeeb K (Apr 29 2020 at 08:25):

alright, I'm not sure to go from here. This is what the goal window shows:

1 goal
m k : ,
hkm : k < m + 1,
f : finite_subset (m + 2)  finite_subset (m + 1),
inj : injective f,
pf : (f m + 1, _⟩).val < m + 1,
miss :  (j : finite_subset (m + 1)), (f  lift_one (m + 1)) j  f m + 1, _⟩,
x y : finite_subset (m + 1),
h1 : (f (lift_one (m + 1) x)).val  (f m + 1, _⟩).val,
h2 : (f (lift_one (m + 1) y)).val  (f m + 1, _⟩).val,
m_x : ¬((f  lift_one (m + 1)) x).val = (f m + 1, _⟩).val,
m_y : ¬((f  lift_one (m + 1)) y).val = (f m + 1, _⟩).val,
h1_strict : (f m + 1, _⟩).val < (f (lift_one (m + 1) x)).val,
h2_strict : (f m + 1, _⟩).val < (f (lift_one (m + 1) y)).val,
h :
(f (lift_one (m + 1) x)).val - 1, _⟩ =
dite ((f (lift_one (m + 1) y)).val  (f m + 1, _⟩).val)
(λ (H : (f (lift_one (m + 1) y)).val  (f m + 1, _⟩).val), (f (lift_one (m + 1) y)).val, _⟩)
(λ (H : ¬(f (lift_one (m + 1) y)).val  (f m + 1, _⟩).val), (f (lift_one (m + 1) y)).val - 1, _⟩)
x = y

#### Adeeb K (Apr 29 2020 at 08:26):

how do I unpack the if-then-else pattern for h?

#### Kenny Lau (Apr 29 2020 at 08:27):

prove the same thing for y and use dif_neg...

ah right right

#### Adeeb K (Apr 29 2020 at 08:30):

so if I have h : ⟨(f (lift_one (m + 1) x)).val - 1, _⟩ = ⟨(f (lift_one (m + 1) y)).val - 1, _⟩,, then I can conclude that (f (lift_one (m + 1) x)).val - 1 = (f (lift_one (m + 1) y)).val - 1 by extensionality right?

right

#### Adeeb K (Apr 29 2020 at 08:36):

uh so at this point, I have basically that $q - 1 = r - 1$, where $q, r \in \mathbb{N}$. When I used library_search, I came up with nothing for q - 1 = r - 1 implies q = r.

#### Adeeb K (Apr 29 2020 at 08:36):

Is there something small (or large) that I'm missing to make that statement?

It's not true

#### Kevin Buzzard (Apr 29 2020 at 08:38):

Using subtraction on naturals is not a good idea in general

#### Adeeb K (Apr 29 2020 at 08:38):

is it because there isn't closure in the naturals under subtraction?

#### Kevin Buzzard (Apr 29 2020 at 08:38):

No, it's because by definition there is closure in the naturals under subtraction

#### Kevin Buzzard (Apr 29 2020 at 08:38):

Which means that what you're using can't be actual subtraction

#### Kevin Buzzard (Apr 29 2020 at 08:39):

0-1=1-1=0 in the naturals

#### Kevin Buzzard (Apr 29 2020 at 08:39):

According to lean

oh I see

#### Adeeb K (Apr 29 2020 at 08:40):

uh, so based on this step...I'm stuck then?

#### Kevin Buzzard (Apr 29 2020 at 08:40):

I haven't been following the details I'm afraid

#### Adeeb K (Apr 29 2020 at 08:40):

well basically I have this:

h : (f (lift_one (m + 1) x)).val - 1, _⟩.val = (f (lift_one (m + 1) y)).val - 1, _⟩.val

#### Kevin Buzzard (Apr 29 2020 at 08:41):

I'm "at work" right now so am only glancing at the chat

ah alright

#### Kevin Buzzard (Apr 29 2020 at 08:41):

I have a meeting in 4 minutes :-/

#### Adeeb K (Apr 29 2020 at 08:41):

ah gotcha, have fun then!

question

#### Adeeb K (Apr 29 2020 at 08:52):

if I have h : LHS = RHS, how can I assign a name to the left hand side? That is, can I have have left_hand_side := LHS?

#### Adeeb K (Apr 29 2020 at 08:53):

I'm trying to say have LHS := ⟨(f (lift_one (m + 1) x)).val - 1, _⟩, but I keep getting the following error:

invalid constructor ⟨...⟩, expected type must be known

I got it

#### Adeeb K (Apr 29 2020 at 09:13):

another question though:

#### Adeeb K (Apr 29 2020 at 09:14):

Suppose I have h_jump : (f (lift_one (m + 1) x)).val = (f (lift_one (m + 1) y)).val. And I also have the extensionality theorem:

lemma ext_iff (n : ) (a b : finite_subset n) : a = b  a.1 = b.1 :=
begin
cases a,
cases b,
split,
{ intro h, rw h},
{ intro h, cases h, refl,}
end

#### Adeeb K (Apr 29 2020 at 09:15):

how would I conclude that (f (lift_one (m + 1) x)) = (f (lift_one (m + 1) y))?

rw \l ext_iff

#### Adeeb K (Apr 29 2020 at 09:16):

oh, so the \l just says to use the implication in the other direction then?

right

Deleted

#### Adeeb K (Apr 29 2020 at 10:03):

thanks again for all the help!

Last updated: May 14 2021 at 00:42 UTC