# Zulip Chat Archive

## 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?

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

Nope

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

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.

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

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):

Adam Topaz said:

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

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

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`

. `fin`

is 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