## Stream: new members

### Topic: Coercion question

#### Dan Stanescu (Aug 04 2020 at 16:20):

I have the following in my context:

with the corresponding types:

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 (Aug 04 2020 at 16:20):

does exact h3 work?

Nope

apply h3?

#### Dan Stanescu (Aug 04 2020 at 16:21):

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

No, it doesn't.

#### Kevin Buzzard (Aug 04 2020 at 16:22):

just bite the bullet and do cases on i and j

#### Adam Topaz (Aug 04 2020 at 16:22):

finish would probably work :)

#### Kevin Buzzard (Aug 04 2020 at 16:22):

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

#### Kevin Buzzard (Aug 04 2020 at 16:23):

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

#### Dan Stanescu (Aug 04 2020 at 16:24):

finish would probably work :)

It doesn't. I wish it did.

#### Adam Topaz (Aug 04 2020 at 16:24):

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

#### Dan Stanescu (Aug 04 2020 at 16:26):

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 (Aug 04 2020 at 16:56):

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 (Aug 04 2020 at 17:00):

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

#### Reid Barton (Aug 04 2020 at 17:03):

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

#### Dan Stanescu (Aug 04 2020 at 18:26):

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 (Aug 04 2020 at 18:36):

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 (Aug 04 2020 at 18:37):

see the top of data.fin

#### Dan Stanescu (Aug 06 2020 at 14:23):

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 (Aug 06 2020 at 14:33):

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 (Aug 07 2020 at 11:18):

this is a nightmare to prove.

#### Kevin Buzzard (Aug 07 2020 at 11:19):

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

#### Kevin Buzzard (Aug 07 2020 at 11:20):

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

#### Shing Tak Lam (Aug 07 2020 at 11:24):

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


nice!

#### Shing Tak Lam (Aug 07 2020 at 11:26):

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 (Aug 07 2020 at 14:05):

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 !

Last updated: May 14 2021 at 00:42 UTC