Zulip Chat Archive

Stream: mathlib4

Topic: Data.Fin.Basic


Jireh Loreaux (Dec 16 2022 at 22:32):

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 (Dec 16 2022 at 22:39):

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

Yaël Dillies (Dec 16 2022 at 22:39):

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

Jireh Loreaux (Dec 16 2022 at 22:40):

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

Jireh Loreaux (Dec 16 2022 at 22:40):

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 (Dec 16 2022 at 22:40):

Ah okay, that would make sense.

Moritz Doll (Dec 17 2022 at 01:54):

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 (Dec 17 2022 at 11:06):

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

Moritz Doll (Dec 17 2022 at 11:07):

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 (Dec 17 2022 at 12:34):

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 (Dec 17 2022 at 13:15):

What was rfl and is no longer rfl?

Jireh Loreaux (Dec 17 2022 at 14:49):

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

Kevin Buzzard (Dec 17 2022 at 20:35):

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 (Dec 17 2022 at 20:38):

-- 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 (Dec 17 2022 at 20:39):

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

Kevin Buzzard (Dec 17 2022 at 20:43):

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 (Dec 17 2022 at 20:57):

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 (Dec 17 2022 at 21:05):

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

Jireh Loreaux (Dec 17 2022 at 22:05):

@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 (Dec 17 2022 at 23:20):

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 (Dec 22 2022 at 18:58):

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

Kevin Buzzard (Dec 22 2022 at 19:21):

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 (Dec 22 2022 at 20:55):

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

Eric Wieser (Dec 22 2022 at 20:58):

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

Kevin Buzzard (Dec 22 2022 at 21:05):

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

Patrick Massot (Jan 03 2023 at 10:40):

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 (Jan 03 2023 at 20:55):

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 (Jan 03 2023 at 20:56):

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 (Jan 03 2023 at 21:24):

Thanks Gabriel!

Kevin Buzzard (Jan 05 2023 at 12:55):

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 (Jan 05 2023 at 21:57):

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 (Jan 05 2023 at 21:58):

what is that instance?

Mario Carneiro (Jan 05 2023 at 21:58):

is that from core?

Eric Wieser (Jan 05 2023 at 21:58):

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

docs4#Fin.instOfNatFinHAddNatInstHAddInstAddNatOfNat

Eric Wieser (Jan 05 2023 at 21:58):

Yes

Mario Carneiro (Jan 05 2023 at 21:58):

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

Mario Carneiro (Jan 05 2023 at 21:59):

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

Eric Wieser (Jan 05 2023 at 21:59):

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

Johan Commelin (Jan 05 2023 at 21:59):

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

Eric Wieser (Jan 05 2023 at 22:01):

What's the Lean4 syntax for instance priority?

Mario Carneiro (Jan 05 2023 at 22:02):

instance (priority := high)


Last updated: Dec 20 2023 at 11:08 UTC