showing injectivity

Stream: new members

[Adeeb K]

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]

Here is all I have so far

[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 }


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
  rw nat.succ_eq_add_one,
  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]

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

[Adeeb K]

Should I cut down the size of the code block?

[Adeeb K]

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

[Kevin Buzzard]

Try the split_ifs tactic

[Adeeb K]

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]

I'm getting this error:

no if-then-else expressions to split

[Reid Barton]

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

[Kevin Buzzard]

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

[Adeeb K]

I did write out a proof on paper

[Reid Barton]

Okay, what did you do at this point then?

[Reid Barton]

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]

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]

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

[Reid Barton]

So you are splitting based on the output of relabel?

[Adeeb K]

yes

[Reid Barton]

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

[Reid Barton]

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

[Adeeb K]

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]

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]

Adeeb K said:

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

Actually, this is not true, is it?

[Adeeb K]

It should be by miss_proof we gave earlier

[Reid Barton]

Adeeb K said:

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]

Adeeb K said:

It should be by miss_proof we gave earlier

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

[Adeeb K]

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]

because f x_1 = f y_1

[Adeeb K]

by injectivity of lift_one and f right?

[Reid Barton]

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

[Adeeb K]

right right

[Adeeb K]

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]

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

[Adeeb K]

but wouldn't that imply that 2 = 20?

[Reid Barton]

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]

oh, so this means I should introduce a lemma

[Reid Barton]

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]

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

[Adeeb K]

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]

contradiction, so no such pair exist?

[Adeeb K]

though I made a leap here

[Adeeb K]

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

[Reid Barton]

This is not the correct formula for relabel

[Reid Barton]

It is a good general direction though.

[Adeeb K]

what's not the correct formula?

[Adeeb K]

oh, the way I split it up?

[Reid Barton]

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

[Adeeb K]

oh right right

[Adeeb K]

other way around

[Adeeb K]

((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]

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

[Adeeb K]

I wrote down the statement of the lemma:

[Adeeb K]

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]

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

[Reid Barton]

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

[Adeeb K]

it is?

[Adeeb K]

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]

There is no f in the statement of relabel_behavior.

[Adeeb K]

oh right..

[Reid Barton]

But, something like it is true and useful.

[Adeeb K]

I'm not sure I see it?

[Patrick Massot]

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

[Adeeb K]

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]

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

[Adeeb K]

yes

[Reid Barton]

Patrick, you make it sound like The Matrix

[Patrick Massot]

Lean: the red pill.

[Adeeb K]

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]

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

[Adeeb K]

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

[Adeeb K]

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]

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

[Adeeb K]

wait wait wait one second

[Adeeb K]

sorry I meant this:

[Adeeb K]

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]

It's getting closer but still not correct.

[Adeeb K]

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

[Reid Barton]

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

[Adeeb K]

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

[Adeeb K]

so it would be better like this:

[Adeeb K]

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

[Adeeb K]

is this closer?

[Adeeb K]

which is really 3 cases?

[Adeeb K]

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

[Reid Barton]

I think it is okay now.

[Adeeb K]

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

[Adeeb K]

I introv p, which gives me the following window:

[Adeeb K]

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]

how can I split the goal?

[Adeeb K]

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]

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

[Kevin Buzzard]

Adeeb K said:

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]

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

[Kevin Buzzard]

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

[Adeeb K]

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]

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

[Adeeb K]

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]

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

[Adeeb K]

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

[Kevin Buzzard]

Kevin Buzzard said:

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

[Adeeb K]

but I keep getting errors when I do so..

[Kevin Buzzard]

Kevin Buzzard said:

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

[Adeeb K]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

unfold at p2 doesn't make any sense

[Kevin Buzzard]

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

[Adeeb K]

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.

[Johan Commelin]

What is p2?

[Adeeb K]

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

[Johan Commelin]

Did you mean unfold relabel at p2?

[Reid Barton]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

The core tactics were only recently documented.

[Kevin Buzzard]

[makes a note to PR better docs for unfold]

[Adeeb K]

thanks again

[Adeeb K]

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

[Adeeb K]

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

[Adeeb K]

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

[Kenny Lau]

rw nat.sub_zero at p

[Adeeb K]

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

[Kenny Lau]

erw nat.sub_zero at p

[Adeeb K]

it still has the same error

[Kenny Lau]

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

[Kenny Lau]

actually

[Kenny Lau]

change k < x.1 at p

[Adeeb K]

match failed

[Adeeb K]

I have no idea what's going on..

[Kenny Lau]

MWE

[Adeeb K]

sure thing

[Adeeb K]

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},



    }, --contradiction case

    {
      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]

my problem is right above cases lt_or_eq_of_le rw_h4,

[Kenny Lau]

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

[Kenny Lau]

in the definition of finite_subset:

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

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

[Mario Carneiro]

not there

[Mario Carneiro]

you need {k // k < n} there

[Adeeb K]

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]

I'll paste the code here again:

[Mario Carneiro]

The correct version of inequality_fact is nat.sub_lt_sub_right_iff

[Adeeb K]

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},



    }, --contradiction case

    {
      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]

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

[Kenny Lau]

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]

(also it was \le not <)

[Adeeb K]

okay! give me a second to change it

[Kenny Lau]

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

[Kenny Lau]

here's your MWE mathlib-stylized

[Adeeb K]

oh damn. Thank you so much!

[Adeeb K]

wait

[Adeeb K]

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]

change x.fst to x.1

[Adeeb K]

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

[Adeeb K]

Here, lemme get an example

[Adeeb K]

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]

here there is an error at cases p2,

[Adeeb K]

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

[Reid Barton]

I wonder why it ever worked.

[Reid Barton]

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

[Kenny Lau]

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

[Adeeb K]

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]

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

[Adeeb K]

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

[Adeeb K]

I'm not sure how to fix lift_finite_injective

[Reid Barton]

Use Kevin's helpful ext_iff lemma.

[Reid Barton]

This is its time to shine.

[Adeeb K]

okay, I'll try it

[Adeeb K]

okay, it did the trick

[Adeeb K]

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]

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

[Adeeb K]

lemme try that

[Adeeb K]

it works!

[Adeeb K]

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

[Adeeb K]

Right now, my plan is this:

[Adeeb K]

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]

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

[Adeeb K]

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

[Adeeb K]

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

[Adeeb K]

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

[Adeeb K]

to repeat the latest from the noob questions thread

[Adeeb K]

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

[Kenny Lau]

read the error

[Adeeb K]

...I have to flip the equality?

[Mario Carneiro]

eq.symm or ne.symm

[Adeeb K]

ah, thank you

[Adeeb K]

@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]

Kenny Lau said:

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

Kenny Lau said:

and after you prove it, rw dif_neg hnk

[Adeeb K]

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

[Adeeb K]

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]

what is the error

[Adeeb K]

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]

read the error

[Kenny Lau]

and read what I told you

[Kenny Lau]

Kenny Lau said:

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

Kenny Lau said:

and after you prove it, rw dif_neg hnk

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

also stop abbreviating terms

[Adeeb K]

what abbreviating?

[Kenny Lau]

have m_x := (miss x),

[Kenny Lau]

I retract my comment about k

[Adeeb K]

alright

[Kenny Lau]

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]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

but to Lean they are not definitionally equivalent

[Adeeb K]

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

[Kenny Lau]

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

[Adeeb K]

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]

but your two lets should bave haves because they are propositions

[Kenny Lau]

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

[Kenny Lau]

yeah so use it and dif_neg

[Adeeb K]

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

[Adeeb K]

okay one sec

[Adeeb K]

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]

this is in response to typing

rw dif_neg (not_le.mpr h1_strict)

[Kenny Lau]

did you forget at h

[Adeeb K]

...oh whoops

[Adeeb K]

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]

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

[Kenny Lau]

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

[Adeeb K]

ah right right

[Adeeb K]

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?

[Kenny Lau]

right

[Adeeb K]

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]

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

[Kevin Buzzard]

It's not true

[Kevin Buzzard]

Using subtraction on naturals is not a good idea in general

[Adeeb K]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

According to lean

[Adeeb K]

oh I see

[Adeeb K]

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

[Kevin Buzzard]

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

[Adeeb K]

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]

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

[Adeeb K]

ah alright

[Kevin Buzzard]

I have a meeting in 4 minutes :-/

[Adeeb K]

ah gotcha, have fun then!

[Adeeb K]

question

[Adeeb K]

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]

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

[Adeeb K]

I got it

[Adeeb K]

another question though:

[Adeeb K]

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]

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

[Kenny Lau]

rw \l ext_iff

[Adeeb K]

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

[Kenny Lau]

right

[Kevin Buzzard]

Deleted

[Adeeb K]

thanks again for all the help!