Data.Fin.Basic

Stream: mathlib4

[Jireh Loreaux]

I have a decent start on Data.Fin.Basic at mathlib4#1084, but it's a monster file. I won't be able to work on it any more tonight, so if anyone else wants to jump in that's fine, just say so here so people don't duplicate work. A few notes:

1. I have included a few things from the ad hoc ported file, which I have labeled with section from_ad_hoc. I felt these things might be necessary / helpful.
2. There are some hiccups in several places because (a) Fin is now a structure rather than a subtype and (b) numerals work differently in Lean 4. This has caused some rfl proofs to break.
3. There are some syntactically duplicated lemmas (because coercions are unfolded) which I have left in for the moment, but we can perhaps remove them (with #aligns to the other version) before finishing the PR.

[Yaël Dillies]

fin being a structure has been backported to mathlib by Gabriel.

[Yaël Dillies]

So it would be interested to figure out exactly why the refls broke.

[Jireh Loreaux]

the rfls broke because of numerals I think, not the structure.

[Jireh Loreaux]

Sorry, I got confused because the structure fields in mathlib3 are val and property, so I just thought it was a subtype.

[Yaël Dillies]

Ah okay, that would make sense.

[Moritz Doll]

I've fixed a couple of errors, but my Lean time is up for today (maybe a I do a bit more in the evening).

[Moritz Doll]

I've removed the {a b : Fin n} and added the hypotheses where necessary as it caused really weird errors

[Moritz Doll]

also I've changed quite a few proofs from rfl or ext rfl to ext; simp. This is might be bad for performance, but since we have to port this file, I think it is acceptable for now

[Jireh Loreaux]

I think simp is the right way to go here because things just aren't rfl anymore. As for a, b, did you see the Zulip thread about this?

[Kevin Buzzard]

What was rfl and is no longer rfl?

[Jireh Loreaux]

Not at my machine, but search the file for "was" and you should see some examples.

[Kevin Buzzard]

Whatever this means:

section from_ad_hoc
-- porting note: this comes from the ad hoc port of this file
variable [Nonempty (Fin n)]

@[to_additive_fixed_numeral]
instance : OfNat (Fin n) x where
  ofNat := Fin.ofNat' x Fin.size_positive'

, it has the property that (0 : Fin n).val = 0 is no longer rfl.

[Kevin Buzzard]

-- Lean 3
import tactic

example (b : ℕ) : (0 : ℕ) % b = 0 := rfl

-- Lean 4 (quoting from core)
@[simp] theorem zero_mod (b : Nat) : 0 % b = 0 := by
  rw [mod_eq]
  have : ¬ (0 < b ∧ b = 0) := by
    intro ⟨h₁, h₂⟩
    simp_all
  simp [this]

That's the problem.

[Reid Barton]

Any chance we can get rid of the weird mod stuff in Fin?

[Kevin Buzzard]

This is also in core Lean 4:

protected def ofNat {n : Nat} (a : Nat) : Fin n.succ :=
  ⟨a % (n+1), Nat.mod_lt _ (Nat.zero_lt_succ _)⟩

protected def ofNat' {n : Nat} (a : Nat) (h : n > 0) : Fin n :=
  ⟨a % n, Nat.mod_lt _ h⟩

...

instance : OfNat (Fin (no_index (n+1))) i where
  ofNat := Fin.ofNat i

[Reid Barton]

It would be nice if numeric literals were just an error if they cannot be proved to be in range--is that possible in Lean 4?

[Mario Carneiro]

it is kind of possible, but we are really limited by the fact that you can't call tactics in typeclass search

[Jireh Loreaux]

@Kevin Buzzard, the stuff from the ad hoc port didn't break rfl, it was already broken (most likely by the stuff in core).

[Moritz Doll]

Jireh Loreaux said:

I think simp is the right way to go here because things just aren't rfl anymore. As for a, b, did you see the Zulip thread about this?

No I did not. I saw that there was a zulip thread linked in the source, but I just went ahead and fixed the errors :sweat_smile:

[Eric Wieser]

Is there a reason mod can't be defined in a way that makes this rfl?

[Kevin Buzzard]

Lean 3 says that there is no reason why it can't be done, but maybe that's not the question you mean.

[Eric Wieser]

Is that true? Lean 3 didn't use mod here so it was irrelevant how it was defined

[Eric Wieser]

But defining ofNat casewise on 0 1 and n.succ.succ would presumably solve this for 0 and 1

[Kevin Buzzard]

Oh I think I misunderstood what "this" referred to.

[Patrick Massot]

In this file there is a well-founded definition that no longer works. In the current state of the file we see:

@[elab_as_elim]
def reverseInduction {n : ℕ} {C : Fin (n + 1) → Sort _} (hlast : C (Fin.last n))
    (hs : ∀ i : Fin n, C i.succ → C (castSucc i)) : ∀ i : Fin (n + 1), C i
  | i =>
    if hi : i = Fin.last n then _root_.cast (congr_arg C hi.symm) hlast
    else by
      set j : Fin n := ⟨i, lt_of_le_of_ne (Nat.le_of_lt_succ i.2) fun h => hi (Fin.ext h)⟩ with hj
      have wf : n + 1 - j.succ < n + 1 - i := by
        have := Fin.eta i i.isLt
        rw [←this]
        rw [tsub_lt_tsub_iff_left_of_le]
        · simp [succ_mk, lt_add_iff_pos_right, Nat.succ_le_iff]
        · rw [succ_mk, add_le_add_iff_right]
          exact j.isLt.le
      have hi : i = Fin.castSucc j := Fin.ext rfl
      exact _root_.cast (congr_arg C hi.symm) (hs _ (reverseInduction hlast hs j.succ))
termination_by' ⟨_, measure_wf fun i : Fin (n + 1) => n + 1 - i⟩

with errors on the last two lines. I tried as a blind fix to change the last line to termination_by' ⟨_, (measure fun i : Fin (n + 1) => n + 1 - i).wf⟩ which does get rid of the error on the last line, but still doesn't satisfy the termination checker.

[Gabriel Ebner]

The syntax for termination_by is now a bit different. You can just write termination_by _ => n + 1 - i now (and don't need to use measure etc.).

[Gabriel Ebner]

I've pushed a fixed version of reverseInduction:

@[elab_as_elim]
def reverseInduction {C : Fin (n + 1) → Sort _} (hlast : C (Fin.last n))
    (hs : ∀ i : Fin n, C i.succ → C (castSucc i)) (i : Fin (n + 1)) : C i :=
  if hi : i = Fin.last n then _root_.cast (congr_arg C hi.symm) hlast
  else
    let j : Fin n := ⟨i, lt_of_le_of_ne (Nat.le_of_lt_succ i.2) fun h => hi (Fin.ext h)⟩
    have : n - i < n + 1 - i :=
      lt_of_eq_of_lt (Nat.add_sub_add_right ..).symm
        (Nat.sub_lt_sub_left i.2 (Nat.lt_succ_self i))
    have hi : i = Fin.castSucc j := Fin.ext rfl
    _root_.cast (congr_arg C hi.symm) (hs _ (reverseInduction hlast hs j.succ))
termination_by _ => n + 1 - i

[Patrick Massot]

Thanks Gabriel!

[Kevin Buzzard]

I proposed a fix for addCases at https://github.com/leanprover-community/mathlib4/pull/1084#discussion_r1062398734 . Regarding succAbove_zero no longer being refl, it can be proved by simp [succAbove], but is the issue that we want it to be rfl or has that ship sailed?

[Eric Wieser]

Adding this to the top of the Data.Fin.Basic file seems to restore the old semantics of 0 and 1:

-- we do not want this instance, and want `instOfNat`, the one that goes via `AddMonoidWithOne`, instead
attribute [-instance] Fin.instOfNatFinHAddNatInstHAddInstAddNatOfNat

instance : Zero (Fin (n + 1)) where
  zero := ⟨0, succ_pos _⟩

instance : One (Fin (n + 1)) where
  one := Fin.ofNat 1

cc @Mario Carneiro.

[Mario Carneiro]

what is that instance?

[Mario Carneiro]

is that from core?

[Eric Wieser]

You mean it's not obvious from the name? :upside_down:

docs4#Fin.instOfNatFinHAddNatInstHAddInstAddNatOfNat

[Eric Wieser]

Yes

[Mario Carneiro]

I see, is there something we can do with priorities to avoid it?

[Mario Carneiro]

attribute [-instance] doesn't really work, that's local-only

[Eric Wieser]

Where's the instance implied by docs4#AddMonoidWithOne? docs4#instOfNat

[Johan Commelin]

We should add superCaliFragilisticExpialiDocious to the end of every instance name, just because we can.

[Eric Wieser]

What's the Lean4 syntax for instance priority?

[Mario Carneiro]

instance (priority := high)