Zulip Chat Archive

Stream: general

Topic: fin simp normal form


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 12 2020 at 16:37):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 12 2020 at 17:51):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 12 2020 at 18:01):

Numeric literals don't use that coercion, right?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 12 2020 at 18:18):

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

view this post on Zulip Mario Carneiro (Aug 12 2020 at 18:18):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 12 2020 at 18:19):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Aug 12 2020 at 19:29):

There's also a lemma about lt_last

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 12 2020 at 19:30):

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

view this post on Zulip 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.

view this post on Zulip 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)?

view this post on Zulip Mario Carneiro (Aug 12 2020 at 19:32):

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

view this post on Zulip Mario Carneiro (Aug 12 2020 at 19:32):

sure, that works for me

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 19:32):

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

view this post on Zulip Mario Carneiro (Aug 12 2020 at 19:33):

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

view this post on Zulip Mario Carneiro (Aug 12 2020 at 19:33):

the instance isn't registered

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 19:38):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 12 2020 at 19:38):

Yes but that will apparently break numeric literals too

view this post on Zulip Reid Barton (Aug 12 2020 at 19:38):

at least all the ones starting from 2

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 19:39):

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

view this post on Zulip Mario Carneiro (Aug 12 2020 at 19:39):

I never count that high anyway

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 19:39):

Yes, I rarely get to 2

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 19:43):

https://arxiv.org/abs/0810.2106

view this post on Zulip Reid Barton (Aug 12 2020 at 19:43):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 19:43):

"many"

view this post on Zulip 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.

view this post on Zulip Reid Barton (Aug 12 2020 at 19:43):

A: Odd

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 12 2020 at 20:17):

Right, this is similar to nat subtraction

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 12 2020 at 20:27):

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

view this post on Zulip Yakov Pechersky (Aug 12 2020 at 21:24):

It's a bit0 and bit1 issue?

view this post on Zulip 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 }

view this post on Zulip Yakov Pechersky (Aug 12 2020 at 23:06):

Could those be in the direction of simp normal form?

view this post on Zulip 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:

view this post on Zulip Yakov Pechersky (Aug 13 2020 at 00:12):

Ah, but could be useful for the rolle theorem one

view this post on Zulip Yakov Pechersky (Aug 13 2020 at 00:13):

There are other ones cooking regarding addition of one

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Aug 13 2020 at 00:21):

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

view this post on Zulip 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).

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Aug 14 2020 at 11:18):

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

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Aug 23 2020 at 01:30):

#3769 will simp to 0 and 1 iirc

view this post on Zulip Yury G. Kudryashov (Aug 23 2020 at 01:53):

Which lemma in #3769?

view this post on Zulip 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?

view this post on Zulip Yakov Pechersky (Aug 23 2020 at 02:31):

It's mk_zero_eq_zero I think

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Aug 23 2020 at 02:32):

And guessing which fin n you're working in.

view this post on Zulip 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