# Zulip Chat Archive

## Stream: general

### Topic: fin simp normal form

#### Reid Barton (Aug 12 2020 at 16:36):

Is there a preferred form between `fin.val`

and the coercion to `nat`

? I have a `simp`

that gets stuck on `i.val = ↑i`

.

#### Reid Barton (Aug 12 2020 at 16:37):

`i.val`

is coming from the extensionality lemma `fin.eq_of_veq : ∀ {n : ℕ} {i j : fin n}, i.val = j.val → i = j`

#### Reid Barton (Aug 12 2020 at 16:37):

(By the way, it's really cool that `show_term {ext}`

works.)

#### Yakov Pechersky (Aug 12 2020 at 16:39):

I've been slowly chipping away at various `fin`

lemmas that should reduce these happenings. In your case (without seeing the whole thing), you might do `obtain ⟨i, hi⟩ := i`

and that could help.

#### Reid Barton (Aug 12 2020 at 16:41):

In this case I can just write `simp, refl`

but I think I shouldn't have to.

#### Dan Stanescu (Aug 12 2020 at 17:49):

For how useful it is, I think `fin`

needs a little more API. Sometimes even simple results may be a little tricky for a beginner, like this one:

```
example (n : ℕ) (i : fin (n + 1)) : i ≤ n :=
begin
have h1 := fin.le_last i, -- this doesn't immediately help
sorry
end
```

#### Reid Barton (Aug 12 2020 at 17:51):

I kind of think the coercion from `nat`

to `fin`

just shouldn't exist

#### Reid Barton (Aug 12 2020 at 17:54):

I mean the fact that there is a (much more sensible) coercion in the other direction ought to be a red flag

#### Reid Barton (Aug 12 2020 at 18:01):

Numeric literals don't use that coercion, right?

#### Reid Barton (Aug 12 2020 at 18:07):

To return to the original topic, is it an intentional decision to not have a simp lemma between `.val`

and the coercion in either direction?

#### Reid Barton (Aug 12 2020 at 18:08):

I would think it would be better to pick one--my mild preference would be for the coercion

#### Mario Carneiro (Aug 12 2020 at 18:18):

The coercion from nat to fin should not be used, it's not very well behaved

#### Mario Carneiro (Aug 12 2020 at 18:18):

The main times you actually want it are when you really mean `zmod`

instead of `fin`

#### Mario Carneiro (Aug 12 2020 at 18:19):

But we can't really make it not exist because it meets the criteria for `nat.cast`

#### Mario Carneiro (Aug 12 2020 at 18:19):

I guess we could remove `+`

on fin, but how disruptive would that be?

#### Mario Carneiro (Aug 12 2020 at 18:20):

we would lose numeric literals, which I think are used, if not in mathlib then in other projects

#### Kevin Buzzard (Aug 12 2020 at 18:27):

I think that `fin n`

has cemented itself as our de facto canonical type with `n`

terms, and this is an argument for its API just being things which are useful for manipulating maps `fin n -> X`

like e.g. some sensible map from `fin a \coprod fin b`

to `fin (a + b)`

, and all the maps used in simplicial homology from `fin n`

to `fin (n+1)`

etc. I think it's a great idea to remove `+`

on `fin`

. I think it was only there as a stop gap because people wanted Z/n and we didn't have `zmod`

yet.

#### Dan Stanescu (Aug 12 2020 at 19:14):

I need some help to clarify this. Here is a not-so-short example where I felt that I couldn't get away without some coercion. Is anyone willing to take a look and tell me how I could avoid getting into trouble (hence possibly also avoid using the two lemmas at the top)? The two relevant lines have comments ending in `-- here?`

```
import analysis.calculus.local_extr
import analysis.calculus.times_cont_diff
import analysis.calculus.iterated_deriv
import tactic data.fin
open set
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
lemma fin_le_last_val (n : ℕ) (i : fin (n + 2)) : i ≤ (n+1) :=
begin
have j0 : n + 1 < n + 1 + 1, linarith,
have j0 := @fin.coe_val_of_lt (n+1) (n+1) j0,
have h3 : i.val ≤ n + 1, linarith [i.is_lt],
apply fin.le_iff_val_le_val.mpr,
rw ← j0 at h3,
exact h3,
end
lemma exist_points_deriv (n : ℕ) (x : fin (n+2) → ℝ) (hx : strict_mono x) :
∀ (f : ℝ → ℝ), continuous_on f ( Icc (x 0) (x (n+1)) ) →
(∀ i, f (x i) = 0) →
∃ (xp : fin(n+1) → ℝ), strict_mono xp ∧
∀ (i : fin (n+1)), xp i ∈ ( Ioo (x 0) (x (n+1)) ) ∧ deriv f (xp i) = 0 :=
begin
intros f hf hxi,
have h1 : ∀ (i : fin (n+1)), ∃ y ∈ (Ioo (x i) (x (i+1))), deriv f y = 0,
intro i,
apply exists_deriv_eq_zero,
-- show x i < x (i+1)
exact hx (fin_lt_succ n i), ---- what to do here?
-- show f continuous on Icc (x i) (x (i+1))
have h02 : Icc (x i) (x (i+1)) ⊆ Icc (x 0) (x (n+1)),
intros z hz,
cases hz with hz1 hz2,
split,
have g3 := (strict_mono.le_iff_le hx).mpr (fin.zero_le i),
linarith,
have g3 := (strict_mono.le_iff_le hx).mpr (fin_le_last_val n (i+1)), ---- and here?
linarith,
exact continuous_on.mono hf h02,
-- show f (x i) = f (x (i+1))
rw [hxi i, hxi (i+1)],
-- this is just normal Rolle, exists_deriv_eq_zero
choose xp hxp using h1,
use xp, split,
intros i j hij,
cases (hxp i).1 with hi1 hi2, cases (hxp j).1 with hj1 hj2,
rcases lt_trichotomy ((i+1) : fin (n+2) ) (j : fin (n+2)) with h1|h2|h3,
-- case (i+1) < j
have hii1 := hx h1, linarith,
-- case (i+1) = j
rw h2 at hi2, linarith,
-- case j < (i+1) is not possible because i < j
exfalso,
have h3n : (j : ℕ) < ((i + 1) : ℕ), {
norm_num at h3,
change (j.val : fin (n+2)).val < (i.val.succ : fin (n+2)).val at h3,
rwa [fin.coe_val_of_lt (show j.1 < n + 2, by linarith [j.2]),
fin.coe_val_of_lt (show i.1 + 1 < n + 2, by linarith [i.2])] at h3,
},
have gf1 := nat.lt_succ_iff.mp h3n,
--strange as it looks, linarith still needs this
have hijn : (i : ℕ) < (j : ℕ), exact hij,
linarith,
intro i, split,
swap, exact (hxp i).2,
split,
cases ((hxp i).1) with g01 g02,
have := (strict_mono.le_iff_le hx).mpr (@fin.zero_le (n+1) i),
linarith,
cases ((hxp i).1) with g01 g02,
have := (strict_mono.le_iff_le hx).mpr (fin_le_last_val n (i+1)),
linarith, done
end
```

#### Kevin Buzzard (Aug 12 2020 at 19:28):

The first one is a coercion between `fin`

s -- that should be fine. In fact I think we could (and perhaps already did) name the `<`

-preserving maps from fin n to fin (n+1).

#### Yakov Pechersky (Aug 12 2020 at 19:29):

I have some fin lemmas written that should help with this. But what's wrong with the first two lemmas? I might just say i.succ instead of i + 1

#### Yakov Pechersky (Aug 12 2020 at 19:29):

There's also a lemma about lt_last

#### Kevin Buzzard (Aug 12 2020 at 19:30):

`last`

is an OK coercion (I mean, I don't mind coercing `n`

to `fin (n+1)`

) but ideally we should have notation for this. Is `fin n`

a complete lattice for n>0?

#### Dan Stanescu (Aug 12 2020 at 19:30):

Yakov Pechersky said:

There's also a lemma about le_last

Right, but that doesn't immediately help, see above in this thread.

#### Yakov Pechersky (Aug 12 2020 at 19:30):

Ah, I wrote it out but got distracted by my day job. I'll upload it when I can, sorry

#### Mario Carneiro (Aug 12 2020 at 19:30):

@Kevin Buzzard Yes, as I mentioned in the other thread any (nonempty) finite lattice is complete

#### Dan Stanescu (Aug 12 2020 at 19:31):

Yakov Pechersky said:

Ah, I wrote it out but got distracted by my day job. I'll upload it when I can, sorry

I do have a proof, but it's just not immediate. Not in the form I need it.

#### Kevin Buzzard (Aug 12 2020 at 19:31):

I mean -- is it a lattice? If so, shouldn't we be using `\top`

for the top element of `fin (n+1)`

?

#### Mario Carneiro (Aug 12 2020 at 19:32):

any linear order is a lattice, the operations are `min`

and `max`

#### Mario Carneiro (Aug 12 2020 at 19:32):

sure, that works for me

#### Kevin Buzzard (Aug 12 2020 at 19:32):

```
failed to synthesize type class instance for
⊢ has_top (fin 4)
```

#### Mario Carneiro (Aug 12 2020 at 19:33):

When I said it is a complete lattice, I mean mathematically

#### Mario Carneiro (Aug 12 2020 at 19:33):

the instance isn't registered

#### Mario Carneiro (Aug 12 2020 at 19:34):

It is a bit sad that we use `\top`

instead of a variant on `n`

though (which is definitely what the books will use)

#### Kevin Buzzard (Aug 12 2020 at 19:34):

In my model of `fin n`

, `fin_lt_succ`

should be the statement that `delta^{n,0} x < delta^{n,n} x`

#### Kevin Buzzard (Aug 12 2020 at 19:35):

where `delta^{n+1,i}`

is the map from fin n to fin (n+1) which misses i

#### Reid Barton (Aug 12 2020 at 19:36):

Mario Carneiro said:

It is a bit sad that we use

`\top`

instead of a variant on`n`

though (which is definitely what the books will use)

this is fixed if we write `T : nat`

and `fin (T + 1)`

#### Kevin Buzzard (Aug 12 2020 at 19:36):

What I want to argue is that all the mess which people are getting into using + (and note that it's just things like +1, it's not + in general) could perhaps be fixed if people were to just treat these things as finite total orders and use the standard convention for maps between them and their API.

#### Kevin Buzzard (Aug 12 2020 at 19:37):

then the first lemma would be in the API and the second would just be le_top.

#### Reid Barton (Aug 12 2020 at 19:37):

The trouble is if the coercion exists then people will use it, either because they don't know better or unintentionally even if they do

#### Kevin Buzzard (Aug 12 2020 at 19:38):

If we remove `add`

from `fin`

then the coercion goes too, right?

#### Reid Barton (Aug 12 2020 at 19:38):

If you're "in the `fin`

zone" and acutely aware of this issue it's not hard to avoid it

#### Reid Barton (Aug 12 2020 at 19:38):

Yes but that will apparently break numeric literals too

#### Reid Barton (Aug 12 2020 at 19:38):

at least all the ones starting from 2

#### Kevin Buzzard (Aug 12 2020 at 19:39):

Well maybe we should be encouraging people to think about `fin n`

more like this

#### Mario Carneiro (Aug 12 2020 at 19:39):

I never count that high anyway

#### Dan Stanescu (Aug 12 2020 at 19:39):

Reid Barton said:

If you're "in the

`fin`

zone" and acutely aware of this issue it's not hard to avoid it

You mean `cast_succ`

and the like?

#### Kevin Buzzard (Aug 12 2020 at 19:39):

Yes, I rarely get to 2

#### Reid Barton (Aug 12 2020 at 19:40):

You have to be alert to the possibility of Lean interpreting what you write as a coercion, and then use all the methods documented at the top of `data.fin`

to avoid it happening.

#### Reid Barton (Aug 12 2020 at 19:42):

I mean the other option is to add much better support for reasoning about the coercions somehow.

#### Kevin Buzzard (Aug 12 2020 at 19:42):

actually I just looked at some of my papers and I get to 2 quite a lot, but I rarely get to 3

#### Kevin Buzzard (Aug 12 2020 at 19:43):

https://arxiv.org/abs/0810.2106

#### Reid Barton (Aug 12 2020 at 19:43):

Q: What does a number theorist call a number greater than 2?

#### Kevin Buzzard (Aug 12 2020 at 19:43):

I give an example which shows the theory is nonempty, which uses sqrt(29) and 3, but other than that it's all 0,1,2.

#### Kevin Buzzard (Aug 12 2020 at 19:43):

"many"

#### Dan Stanescu (Aug 12 2020 at 19:43):

Kevin Buzzard said:

actually I just looked at some of my papers and I get to 2 quite a lot, but I rarely get to 3

I did get to 2 but that was it, not 3.

#### Reid Barton (Aug 12 2020 at 19:43):

A: Odd

#### Joseph Myers (Aug 12 2020 at 20:14):

I think of the coercion from `nat`

to `fin`

as like all the cases where a partial function is given some default value to make it a total function: I can convert a `nat`

value to `fin (n + 1)`

whenever convenient and supply the proof that the `nat`

value was within range for the conversion some time later when I need to use that fact. On the other hand, the proof I did using that approach (for an olympiad problem about a 2019 × 2019 grid, which I represented as `fin 2019 × fin 2019`

) ended up as over 3000 lines of Lean for a problem that's pretty easy mathematically, so this doesn't provide much evidence that that approach is useful. (With hindsight I suspect it would have been easier to work with `ℕ × ℕ`

or `ℤ × ℤ`

and avoid `fin 2019`

completely.)

#### Mario Carneiro (Aug 12 2020 at 20:17):

When I need to do that sort of thing, I will use a local notation like `#n`

that calls `fin.mk`

with `norm_num`

or something producing the proof

#### Reid Barton (Aug 12 2020 at 20:17):

Right, this is similar to `nat`

subtraction

#### Reid Barton (Aug 12 2020 at 20:19):

My view is that you're generally in a better position to explain why the `fin`

value is sensible (i.e. has the expected property, in this case that its `val`

equals the thing you put in) when you build it than when you want to reason about it later on. But this is to an extent contingent on how good our automation is at proving obvious facts.

#### Mario Carneiro (Aug 12 2020 at 20:20):

The nice thing about the local notation is that you can tailor the proof method to the use case

#### Joseph Myers (Aug 12 2020 at 20:22):

The values being converted weren't constants. The proofs typically ended up being `linarith`

, but after some preparation (e.g. various parts of the argument involved cases based on parity) - or there was a definition involving conversion to `fin`

, that was only used in proofs where the conversion was legitimate. Type class inference became happier once I switched from literal `fin 2019`

to more general `fin (n + 1)`

, I think before that it kept having to do kernel reduction to show 2019 is `succ 2018`

in order to deduce `has_zero (fin 2019)`

and similar.

#### Reid Barton (Aug 12 2020 at 20:23):

Didn't we once discover there's a special case for treating `nat`

`+`

specifically in instance search?

#### Joseph Myers (Aug 12 2020 at 20:26):

```
example : has_zero (fin 1024) := by apply_instance -- succeeds
example : has_zero (fin 1025) := by apply_instance -- fails
```

#### Reid Barton (Aug 12 2020 at 20:27):

`local notation `2019` := 2018 + 1`

:upside_down:

#### Yakov Pechersky (Aug 12 2020 at 21:24):

It's a bit0 and bit1 issue?

#### Yakov Pechersky (Aug 12 2020 at 23:06):

Some work:

```
lemma fin.coe_succ_eq_succ {n : ℕ} (i : fin n) : ((i : fin (n + 1)) + 1) = i.succ :=
begin
rw [fin.eq_iff_veq, fin.succ_val, coe_coe],
norm_cast,
apply fin.coe_coe_of_lt,
exact add_lt_add_right i.is_lt 1
end
lemma fin.coe_eq_cast_succ {n : ℕ} (i : fin n) : (i : fin (n + 1)) = i.cast_succ :=
begin
rw [fin.cast_succ, fin.cast_add, fin.cast_le, fin.cast_lt],
obtain ⟨i, hi⟩ := i,
rw fin.eq_iff_veq,
have : i.succ = i + 1 := rfl,
simp only [this],
apply fin.coe_val_of_lt,
exact nat.lt.step hi,
end
lemma fin.val_coe_eq_self {n : ℕ} (i : fin n) : (i : fin (n + 1)).val = i.val :=
by { rw fin.coe_eq_cast_succ, refl }
```

#### Yakov Pechersky (Aug 12 2020 at 23:06):

Could those be in the direction of simp normal form?

#### Reid Barton (Aug 12 2020 at 23:25):

If you inspect my original messages closely you will find they have nothing to do with this coercion :upside_down:

#### Yakov Pechersky (Aug 13 2020 at 00:12):

Ah, but could be useful for the rolle theorem one

#### Yakov Pechersky (Aug 13 2020 at 00:13):

There are other ones cooking regarding addition of one

#### Dan Stanescu (Aug 13 2020 at 00:17):

Yakov Pechersky said:

Ah, but could be useful for the rolle theorem one

Thanks Yakov. I do have all I need there. What I meant was that some of these results might be nice in the `fin`

API in `mathlib`

.

#### Yakov Pechersky (Aug 13 2020 at 00:21):

Sure thing. A general question then is whether the lemmas above should be simp lemmas.

#### Kevin Buzzard (Aug 13 2020 at 07:04):

I think that addition of 1 on `fin`

should be avoided to the extent that anything simplifying it to the sensible functions which have been set up us a great idea. On the other hand I think that users should think very hard before using addition in any way. There are functions for adding one and adding things bigger than one should be undefined unless you're adding a and moving from fin n to fin (n+a).

#### Dan Stanescu (Aug 13 2020 at 12:10):

I agree, but let me add that heavy use cases (like Yakov's and, admittedly to a lesser extent, mine) suggest that the functions that are available in `data.fin`

are not enough of an API yet. So I strongly advocate that this API be augmented.

This discussion might be veering away from Reid's initial post...

#### Johan Commelin (Aug 14 2020 at 11:18):

@Reid Barton I would prefer to have the coercion as simp normal form.

#### Yury G. Kudryashov (Aug 22 2020 at 21:09):

I'm dealing with `fin 3 → α`

and `fin 4 → α`

. While the most natural way to write arguments is `(f : fin 3 → α) 1`

, `fin_cases`

generates cases `⟨0, _⟩`

etc, and `simp`

doesn't convert in either direction.

#### Yakov Pechersky (Aug 23 2020 at 01:30):

#3769 will simp to 0 and 1 iirc

#### Yury G. Kudryashov (Aug 23 2020 at 01:53):

Which lemma in #3769?

#### Yury G. Kudryashov (Aug 23 2020 at 01:54):

I see that it'll work with `0`

and `1`

but I'm interested in `2`

and `3`

as well. Something like `mk_bit0`

/`mk_bit1`

?

#### Yakov Pechersky (Aug 23 2020 at 02:31):

It's mk_zero_eq_zero I think

#### Yakov Pechersky (Aug 23 2020 at 02:32):

I've played around with bit0 and bit1 lemmas but it gets complicated with the modular math

#### Yakov Pechersky (Aug 23 2020 at 02:32):

And guessing which fin n you're working in.

#### Yury G. Kudryashov (Aug 23 2020 at 03:32):

Works for me:

```
@[simp] lemma mk_zero (n : ℕ) : (⟨0, n.zero_lt_succ⟩ : fin (n + 1)) = 0 := rfl
@[simp] lemma mk_one (n : ℕ) (hn : 1 < n + 1) : (⟨1, hn⟩ : fin (n + 1)) = 1 :=
eq_of_veq (nat.mod_eq_of_lt hn).symm
@[simp] lemma mk_bit0 {m n : ℕ} (h : bit0 m < n) :
(⟨_, h⟩ : fin n) = bit0 ⟨m, (nat.le_add_right _ _).trans_lt h⟩ :=
eq_of_veq (nat.mod_eq_of_lt h).symm
@[simp] lemma mk_bit1 {m n : ℕ} (h : bit1 m < n + 1) :
(⟨bit1 m, h⟩ : fin (n + 1)) = bit1 ⟨m, (nat.le_add_right m m).trans_lt
((m + m).lt_succ_self.trans h)⟩ :=
begin
ext,
simp only [bit1, bit0] at h ⊢,
simp only [val_add, one_val, ← nat.add_mod, nat.mod_eq_of_lt h]
end
```

Last updated: May 11 2021 at 21:10 UTC