Coercion question

Stream: new members

[Dan Stanescu]

I have the following in my context:

context.png

with the corresponding types:

xtxtype.png

I didn't find a way to obtain the goal, everything seems to fail (norm_cast, fin.coe_eq_val, fin.coe_fin_lt.mp). Does anyone see something that might work here?

[Kevin Buzzard]

does exact h3 work?

[Dan Stanescu]

Nope

[Adam Topaz]

apply h3?

[Dan Stanescu]

Funny I didn't try this last one. I'll give it a try in a sec.

[Dan Stanescu]

No, it doesn't.

[Kevin Buzzard]

just bite the bullet and do cases on i and j

[Adam Topaz]

finish would probably work :)

[Kevin Buzzard]

I think h3 might say something like j % (n + 2) < (i + 1) % (n + 2) or something

[Kevin Buzzard]

and you can prove j % (n + 2) = j by mod_lt or something

[Dan Stanescu]

Adam Topaz said:

finish would probably work :)

It doesn't. I wish it did.

[Adam Topaz]

Oh, I see the coercion is going into fin (n+2). Missed that.

[Dan Stanescu]

Kevin Buzzard said:

I think h3 might say something like j % (n + 2) < (i + 1) % (n + 2) or something

Thanks, I'll have to try cases I guess. Maybe I get to see if there's a hidden problem somewhere in the process.

[Shing Tak Lam]

import data.fin tactic

example (n : ℕ) (i j : fin n) (h : (j.val : fin (n+2)) < (i.val.succ : fin (n+2))) : j.val < i.val.succ :=
begin
  have h1 : (j.val : fin (n+2)).val = j.val,
  { rw fin.coe_val_of_lt (show j.1 < n + 2, by linarith [j.2]) },
  have h2 : (i.val.succ : fin (n+2)).val = i.val.succ,
  { rw fin.coe_val_of_lt (show i.1 + 1 < n + 2, by linarith [i.2]) },
  change (j.val : fin (n+2)).val < (i.val.succ : fin (n+2)).val at h,
  rwa [h1, h2] at h,
end

[Reid Barton]

This looks like a situation it would be better not to get into in the first place

[Reid Barton]

e.g. if h3 was stated in terms of things like cast_succ

[Dan Stanescu]

Reid Barton said:

e.g. if h3 was stated in terms of things like cast_succ

That h3 comes from something like this:

    rcases lt_trichotomy ((i+1) : fin (n+2) ) (j : fin (n+2)) with h1|h2|h3,

and is the one case that leads to false. I did expect to have trouble with it, the other two worked like a charm. How could I have done a better job with cast_succ?

[Reid Barton]

Don't write things like ((i+1) : fin (n+2)) (you implicitly used a coercion here) but instead use methods of fin designed for this purpose

[Reid Barton]

see the top of data.fin

[Dan Stanescu]

Reid Barton said:

Don't write things like ((i+1) : fin (n+2)) (you implicitly used a coercion here) but instead use methods of fin designed for this purpose

This is very good advice, unfortunately I just got it too late and am not sure what to do now. I have a rather dense 200-lines proof that hinges on this one sorry:

import data.fin
import tactic

lemma fin_lt_succ (n : ℕ) (i : fin (n + 1)) : (i : fin (n+2)) < ((i+1) : fin (n+2)) := sorry

which I thought was easy when I outlined the proof, but it turns out I couldn't bring to completion (one of the ways I tried is below). Does anyone see how to finish this? I can't seem to figure out how to use an alternative at the place I need this.

lemma fin_lt_succ (n : ℕ) (i : fin (n + 1)) : (i : fin (n+2)) < ((i+1) : fin (n+2)) :=
begin
    apply fin.lt_iff_val_lt_val.mpr,
    have h1 : i.val < n+2, linarith [i.2],
    have h2 := @fin.coe_val_of_lt (n+1) i.val h1,
    sorry,
end

[Jalex Stark]

import tactic

lemma fin_lt_succ (n : ℕ) (i : fin (n + 1)) : (i : fin (n+2)) < ((i+1) : fin (n+2)) :=
begin
  apply fin.lt_iff_val_lt_val.mpr,
  convert nat.lt_succ_self _,
  sorry
end

[Kevin Buzzard]

this is a nightmare to prove.

[Kevin Buzzard]

The case i = 0 is defeq to 0 < (0 + (0 + 1) % (n + (0 + 1) + 1)) % (n + bit0 (0 + 1)),

[Kevin Buzzard]

Just refactor, it will be easier and will save you more pain later

[Shing Tak Lam]

Fwiw I've proven this (PM with Dan). I have a better proof that doesn't use norm cast and things, but I'm on my phone rn.

lemma fin_lt_succ (n : ℕ) (i : fin (n + 1)) : (i : fin (n+2)) < (i+1) :=
begin
  cases i with i hi,
  change (_ : fin (n+2)).val < (_ : fin (n+2)).val,
  simp only [fin.coe_mk, coe_coe],
  norm_cast,
  rw [fin.coe_val_of_lt, fin.coe_val_of_lt]; omega,
end

[Kevin Buzzard]

nice!

[Shing Tak Lam]

There's a few more fin lemmas that I was gonna PR today, but my internet decided to not work very well. I'll try and PR these to mathlib tomorrow (should these be PR-ed?)

[Dan Stanescu]

Kevin Buzzard said:

this is a nightmare to prove.

I really think this would be useful in mathlib. finis a great type to have for finite-length sequences, as the discussion initiated by @Patrick Thomas about partitions/Riemann sums also suggests. This result is very helpful when working with strict_mono sequences, which will be needed in many circumstances, most probably including that case (refining partitions). Kudos @Shing Tak Lam !