## 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 fins -- 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.

"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.

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

lemma fin.coe_eq_cast_succ {n : ℕ} (i : fin n) : (i : fin (n + 1)) = i.cast_succ :=
begin
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 ⊢,