fin simp normal form

Stream: general

[Reid Barton]

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]

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]

(By the way, it's really cool that show_term {ext} works.)

[Yakov Pechersky]

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]

In this case I can just write simp, refl but I think I shouldn't have to.

[Dan Stanescu]

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]

I kind of think the coercion from nat to fin just shouldn't exist

[Reid Barton]

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

[Reid Barton]

Numeric literals don't use that coercion, right?

[Reid Barton]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

The main times you actually want it are when you really mean zmod instead of fin

[Mario Carneiro]

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

[Mario Carneiro]

I guess we could remove + on fin, but how disruptive would that be?

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

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]

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]

There's also a lemma about lt_last

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

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

[Dan Stanescu]

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]

I mean -- is it a lattice? If so, shouldn't we be using \top for the top element of fin (n+1)?

[Mario Carneiro]

any linear order is a lattice, the operations are min and max

[Mario Carneiro]

sure, that works for me

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

the instance isn't registered

[Mario Carneiro]

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]

In my model of fin n, fin_lt_succ should be the statement that delta^{n,0} x < delta^{n,n} x

[Kevin Buzzard]

where delta^{n+1,i} is the map from fin n to fin (n+1) which misses i

[Reid Barton]

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]

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]

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

[Reid Barton]

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]

If we remove add from fin then the coercion goes too, right?

[Reid Barton]

If you're "in the fin zone" and acutely aware of this issue it's not hard to avoid it

[Reid Barton]

Yes but that will apparently break numeric literals too

[Reid Barton]

at least all the ones starting from 2

[Kevin Buzzard]

Well maybe we should be encouraging people to think about fin n more like this

[Mario Carneiro]

I never count that high anyway

[Dan Stanescu]

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]

Yes, I rarely get to 2

[Reid Barton]

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]

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

[Kevin Buzzard]

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]

https://arxiv.org/abs/0810.2106

[Reid Barton]

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

[Kevin Buzzard]

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]

"many"

[Dan Stanescu]

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]

A: Odd

[Joseph Myers]

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]

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]

Right, this is similar to nat subtraction

[Reid Barton]

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]

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

[Joseph Myers]

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]

Didn't we once discover there's a special case for treating nat + specifically in instance search?

[Joseph Myers]

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

[Reid Barton]

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

[Yakov Pechersky]

It's a bit0 and bit1 issue?

[Yakov Pechersky]

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]

Could those be in the direction of simp normal form?

[Reid Barton]

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

[Yakov Pechersky]

Ah, but could be useful for the rolle theorem one

[Yakov Pechersky]

There are other ones cooking regarding addition of one

[Dan Stanescu]

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]

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

[Kevin Buzzard]

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]

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]

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

[Yury G. Kudryashov]

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]

#3769 will simp to 0 and 1 iirc

[Yury G. Kudryashov]

Which lemma in #3769?

[Yury G. Kudryashov]

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]

It's mk_zero_eq_zero I think

[Yakov Pechersky]

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

[Yakov Pechersky]

And guessing which fin n you're working in.

[Yury G. Kudryashov]

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