Zulip Chat Archive

Stream: new members

Topic: showing injectivity


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

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

Here is all I have so far

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

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

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

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

Should I cut down the size of the code block?

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

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

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 19:08):

Try the split_ifs tactic

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

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

I'm getting this error:

no if-then-else expressions to split

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

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 19:10):

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

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

I did write out a proof on paper

view this post on Zulip Reid Barton (Apr 28 2020 at 19:10):

Okay, what did you do at this point then?

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

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

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

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

view this post on Zulip Reid Barton (Apr 28 2020 at 19:12):

So you are splitting based on the output of relabel?

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

yes

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

view this post on Zulip Reid Barton (Apr 28 2020 at 19:13):

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

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

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

view this post on Zulip Reid Barton (Apr 28 2020 at 19:15):

Adeeb K said:

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

Actually, this is not true, is it?

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

It should be by miss_proof we gave earlier

view this post on Zulip Reid Barton (Apr 28 2020 at 19:16):

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?

view this post on Zulip Reid Barton (Apr 28 2020 at 19:16):

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.

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

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

because f x_1 = f y_1

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

by injectivity of lift_one and f right?

view this post on Zulip Reid Barton (Apr 28 2020 at 19:17):

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

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

right right

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

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

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

but wouldn't that imply that 2 = 20?

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

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

oh, so this means I should introduce a lemma

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

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

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

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

contradiction, so no such pair exist?

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

though I made a leap here

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

view this post on Zulip Reid Barton (Apr 28 2020 at 19:23):

This is not the correct formula for relabel

view this post on Zulip Reid Barton (Apr 28 2020 at 19:25):

It is a good general direction though.

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

what's not the correct formula?

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

oh, the way I split it up?

view this post on Zulip Reid Barton (Apr 28 2020 at 19:27):

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

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

oh right right

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

other way around

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

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

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

I wrote down the statement of the lemma:

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

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

view this post on Zulip Reid Barton (Apr 28 2020 at 19:39):

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

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

it is?

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

view this post on Zulip Reid Barton (Apr 28 2020 at 19:43):

There is no f in the statement of relabel_behavior.

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

oh right..

view this post on Zulip Reid Barton (Apr 28 2020 at 19:44):

But, something like it is true and useful.

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

I'm not sure I see it?

view this post on Zulip Patrick Massot (Apr 28 2020 at 19:44):

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

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

view this post on Zulip Patrick Massot (Apr 28 2020 at 19:46):

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

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

yes

view this post on Zulip Reid Barton (Apr 28 2020 at 19:47):

Patrick, you make it sound like The Matrix

view this post on Zulip Patrick Massot (Apr 28 2020 at 19:48):

Lean: the red pill.

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

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

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

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

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

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

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

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

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

wait wait wait one second

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

sorry I meant this:

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

view this post on Zulip Reid Barton (Apr 28 2020 at 19:54):

It's getting closer but still not correct.

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

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

view this post on Zulip Reid Barton (Apr 28 2020 at 19:56):

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

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

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

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

so it would be better like this:

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

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

is this closer?

view this post on Zulip Adeeb K (Apr 28 2020 at 20:00):

which is really 3 cases?

view this post on Zulip Adeeb K (Apr 28 2020 at 20:02):

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

view this post on Zulip Reid Barton (Apr 28 2020 at 20:03):

I think it is okay now.

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

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

view this post on Zulip Adeeb K (Apr 28 2020 at 20:08):

I introv p, which gives me the following window:

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

view this post on Zulip Adeeb K (Apr 28 2020 at 20:09):

how can I split the goal?

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

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

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 20:42):

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.

view this post on Zulip Reid Barton (Apr 28 2020 at 20:45):

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 20:47):

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

view this post on Zulip Adeeb K (Apr 28 2020 at 20:48):

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

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

view this post on Zulip Adeeb K (Apr 28 2020 at 20:49):

but I keep getting errors when I do so..

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 20:49):

Kevin Buzzard said:

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

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

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 20:52):

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

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

view this post on Zulip Adeeb K (Apr 28 2020 at 20:54):

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

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 20:54):

unfold at p2 doesn't make any sense

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 20:54):

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

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

view this post on Zulip Johan Commelin (Apr 28 2020 at 20:58):

What is p2?

view this post on Zulip Adeeb K (Apr 28 2020 at 20:58):

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

view this post on Zulip Johan Commelin (Apr 28 2020 at 20:59):

Did you mean unfold relabel at p2?

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

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

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

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 21:01):

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

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 21:01):

The core tactics were only recently documented.

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

[makes a note to PR better docs for unfold]

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

thanks again

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

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

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

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 00:08):

rw nat.sub_zero at p

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 00:15):

erw nat.sub_zero at p

view this post on Zulip Adeeb K (Apr 29 2020 at 00:16):

it still has the same error

view this post on Zulip Kenny Lau (Apr 29 2020 at 00:16):

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 00:17):

actually

view this post on Zulip Kenny Lau (Apr 29 2020 at 00:17):

change k < x.1 at p

view this post on Zulip Adeeb K (Apr 29 2020 at 00:20):

match failed

view this post on Zulip Adeeb K (Apr 29 2020 at 00:20):

I have no idea what's going on..

view this post on Zulip Kenny Lau (Apr 29 2020 at 00:20):

MWE

view this post on Zulip Adeeb K (Apr 29 2020 at 00:20):

sure thing

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



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

view this post on Zulip Adeeb K (Apr 29 2020 at 00:23):

my problem is right above cases lt_or_eq_of_le rw_h4,

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

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

view this post on Zulip Mario Carneiro (Apr 29 2020 at 00:29):

not there

view this post on Zulip Mario Carneiro (Apr 29 2020 at 00:29):

you need {k // k < n} there

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

view this post on Zulip Adeeb K (Apr 29 2020 at 00:32):

I'll paste the code here again:

view this post on Zulip Mario Carneiro (Apr 29 2020 at 00:33):

The correct version of inequality_fact is nat.sub_lt_sub_right_iff

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



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

view this post on Zulip Adeeb K (Apr 29 2020 at 00:34):

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

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 00:36):

(also it was \le not <)

view this post on Zulip Adeeb K (Apr 29 2020 at 00:39):

okay! give me a second to change it

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 00:44):

here's your MWE mathlib-stylized

view this post on Zulip Adeeb K (Apr 29 2020 at 00:48):

oh damn. Thank you so much!

view this post on Zulip Adeeb K (Apr 29 2020 at 01:12):

wait

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 01:12):

change x.fst to x.1

view this post on Zulip Adeeb K (Apr 29 2020 at 01:13):

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

view this post on Zulip Adeeb K (Apr 29 2020 at 01:13):

Here, lemme get an example

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

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

here there is an error at cases p2,

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

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

view this post on Zulip Reid Barton (Apr 29 2020 at 01:20):

I wonder why it ever worked.

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 01:20):

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

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

view this post on Zulip Reid Barton (Apr 29 2020 at 01:24):

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

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

view this post on Zulip Adeeb K (Apr 29 2020 at 01:40):

I'm not sure how to fix lift_finite_injective

view this post on Zulip Reid Barton (Apr 29 2020 at 01:41):

Use Kevin's helpful ext_iff lemma.

view this post on Zulip Reid Barton (Apr 29 2020 at 01:41):

This is its time to shine.

view this post on Zulip Adeeb K (Apr 29 2020 at 01:51):

okay, I'll try it

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

okay, it did the trick

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

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

view this post on Zulip Adeeb K (Apr 29 2020 at 02:12):

lemme try that

view this post on Zulip Adeeb K (Apr 29 2020 at 02:12):

it works!

view this post on Zulip Adeeb K (Apr 29 2020 at 02:12):

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

view this post on Zulip Adeeb K (Apr 29 2020 at 02:13):

Right now, my plan is this:

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

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

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

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

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

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

view this post on Zulip Adeeb K (Apr 29 2020 at 02:31):

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

view this post on Zulip Adeeb K (Apr 29 2020 at 08:03):

to repeat the latest from the noob questions thread

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 08:04):

read the error

view this post on Zulip Adeeb K (Apr 29 2020 at 08:04):

...I have to flip the equality?

view this post on Zulip Mario Carneiro (Apr 29 2020 at 08:05):

eq.symm or ne.symm

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

ah, thank you

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

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

view this post on Zulip Adeeb K (Apr 29 2020 at 08:10):

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

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 08:14):

what is the error

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 08:14):

read the error

view this post on Zulip Kenny Lau (Apr 29 2020 at 08:14):

and read what I told you

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 08:15):

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 08:15):

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 08:16):

also stop abbreviating terms

view this post on Zulip Adeeb K (Apr 29 2020 at 08:16):

what abbreviating?

view this post on Zulip Kenny Lau (Apr 29 2020 at 08:16):

have m_x := (miss x),

view this post on Zulip Kenny Lau (Apr 29 2020 at 08:16):

I retract my comment about k

view this post on Zulip Adeeb K (Apr 29 2020 at 08:16):

alright

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

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 08:17):

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 08:17):

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

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

but to Lean they are not definitionally equivalent

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 08:20):

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

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 08:20):

but your two lets should bave haves because they are propositions

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

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

yeah so use it and dif_neg

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

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

okay one sec

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

view this post on Zulip Adeeb K (Apr 29 2020 at 08:22):

this is in response to typing

rw dif_neg (not_le.mpr h1_strict)

view this post on Zulip Kenny Lau (Apr 29 2020 at 08:23):

did you forget at h

view this post on Zulip Adeeb K (Apr 29 2020 at 08:24):

...oh whoops

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

view this post on Zulip Adeeb K (Apr 29 2020 at 08:26):

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 08:27):

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

view this post on Zulip Adeeb K (Apr 29 2020 at 08:28):

ah right right

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 08:32):

right

view this post on Zulip Adeeb K (Apr 29 2020 at 08:36):

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

view this post on Zulip Adeeb K (Apr 29 2020 at 08:36):

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

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 08:37):

It's not true

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 08:38):

Using subtraction on naturals is not a good idea in general

view this post on Zulip Adeeb K (Apr 29 2020 at 08:38):

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

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 08:38):

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

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 08:38):

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

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 08:39):

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

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 08:39):

According to lean

view this post on Zulip Adeeb K (Apr 29 2020 at 08:39):

oh I see

view this post on Zulip Adeeb K (Apr 29 2020 at 08:40):

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

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 08:40):

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

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

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 08:41):

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

view this post on Zulip Adeeb K (Apr 29 2020 at 08:41):

ah alright

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 08:41):

I have a meeting in 4 minutes :-/

view this post on Zulip Adeeb K (Apr 29 2020 at 08:41):

ah gotcha, have fun then!

view this post on Zulip Adeeb K (Apr 29 2020 at 08:51):

question

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

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

view this post on Zulip Adeeb K (Apr 29 2020 at 09:13):

I got it

view this post on Zulip Adeeb K (Apr 29 2020 at 09:13):

another question though:

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

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 09:15):

rw \l ext_iff

view this post on Zulip Adeeb K (Apr 29 2020 at 09:16):

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

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

right

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 09:55):

Deleted

view this post on Zulip Adeeb K (Apr 29 2020 at 10:03):

thanks again for all the help!


Last updated: May 14 2021 at 00:42 UTC