simp normal form for `Vector` indexing: `get` vs `.[.]`

Stream: mathlib4

[Alex Keizer]

In a recent PR the question came up of what we want the simp normal form of indexing a Vector \a n by a Fin n to be, either Vector.get or the .[.] notation.

For Array, we take the .[.] notation as the normal form, while for List we use List.get.
But, we generally don't index List's as much.

So, two questions for the community:

• Do we want to standardize on a consistent simp normal form, using either a get function or the .[.] notation, accros List, Vector, Array, and any other potential collections? And
• Which of the two forms should we use as the simp normal form for Vector in particular?

[Scott Morrison]

I would propose we use .get for List and [.] for Array and Vector.

[Scott Morrison]

In fact, I'd propose we consider changing the definition of Vector to be in terms of Array rather than List!

[Alex Keizer]

It turns out that Std has the following simp-lemma:

@[simp] theorem getElem_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
    a[i] = a[i.1] := rfl

Meaning that the actual simp normal form will be x[i.1]/x[Fin.val i]. This seems like quite a footgun to me: it's not immediately apparent that a goal with x[i] got rewritten to x[↑i] (the arrow is quite small in my vscode font, at least), making it surprising to see that a simp-lemma which accidentally used the x[i] form is not actually firing.

How is this problem avoided with Array? Should we maybe get rid of the Fin instance of GetElem entirely, so that simp-lemmas can not use the wrong form?

[Gabriel Ebner]

The linter will catch that.

[Alex Keizer]

Which linter? It doesn't seem to be working for me (I'm not seeing any indication in vscode at least) in a theorem where I wrote v[i.succ.1], even though it seems the normal form for that one should rather be v[i.1 + 1]'i.succ.2

[Mario Carneiro]

that one is in simp normal form though?

[Mario Carneiro]

well maybe i.succ.1 should be rewritten to i.1 + 1 but maybe there is no such simp lemma (or it's not a dsimp lemma, which would be required in this case since there is a dependency)

[Alex Keizer]

Is it? The following makes me believe that there is already such a lemma, or am I misunderstanding what simp normal form means?

import Mathlib.Data.Vector
import Mathlib.Data.Fin.Basic

example (v : Vector α (n+1)) (i : Fin n) : v[i.succ] = z := by
  simp
  -- Goal is: `⊢ v[↑i + 1] = z`

EDIT: added imports for an MWE

EDIT2: Hmm, by dsimp doesn't rewrite the goal, so I guess your point about it not being a dsimp lemma is true. I'm afraid I don't entirely know how that relates to determining what the simp normal form is/should be. I'm just seeing that my goals with v[i.succ.1] got rewritten to v[i.1 + 1] by simp, so I concluded the latter should be the normal form. Is this wrong?

[Mario Carneiro]

You just wrote something different than your previous message. The example has v[i.succ] but you are talking about v[i.succ.1]

[Alex Keizer]

Ah, you're right, it seems I minimized wrongly, sorry about that. Changing it to v[i.succ.1] doesn't actually change anything, though.

import Mathlib.Data.Vector
import Mathlib.Data.Fin.Basic

example (v : Vector α (n+1)) (i : Fin n) : v[i.succ.1] = z := by
  simp
  -- Goal is: `⊢ v[↑i + 1] = z`

Back to my original question about the linter: the following is also not showing any indication, even though this one I am 100% sure it is not in simp-normal form:

@[simp]
theorem bad_theorem (v : Vector α n) (i j : Fin n) (h : i = j) : v[i] = v[j] := by
  simp -- Goal: ⊢ v[↑i] = v[↑j]
  rw[h]

Is this linter supposed to run interactively, or do I need to explicitly run something?

[Alex J. Best]

You need to put #lint at the bottom of your file for the simp linters

[Gabriel Ebner]

Also, bad_theorem is not a simp theorem no matter how you write the indices, since the rhs has more variables than the lhs so simp won't know what to rewrite to. Syntactically, it could be a @[congr] lemma--but there's no need to add it since the built-in congruences work just fine for getElem.

[Alex Keizer]

Sure, I wasn't actually proposing to add bad_theorem as a simp-lemma, I just wanted an example of something which is definitely not in simp normal form.

[Alex Keizer]

Regardless, I now have 2 PRs for mathlib: #4994 makes the change to v[i.1] as normal form, and #5421 is an alternate proposal that removes the simp attribute from getElem_fin and use v[i] as the normal form. (I've also submitted a PR to std which removes the simp attribute directly at the declaration).

For both PRs I've only made the changes in Vector files, so CI is still failing on downstream files. But, I wanted to first get some more opinions and reach consensus on which direction to go in. So far, there are three options:

1. Stick with the status quo: Vector.get (my personal preference, but there does seem consensus that we want to move away from it)
2. Use getElem with Fin, i.e., v[i]. This is #5421
3. Use getElem with Nat, i.e., v[i.1]. This is the original PR #4994

Benefits of option 1

I like get xs i because it has less implicit variables and no type class synthesis.
Thus, it plays nicer with type inference. Then again, there is no harm in specifying types a bit more, so I don't particularly mind this point.

example (xs : Vector α n) (i) : xs.get i = b := sorry
example (xs : Vector α n) (i : Fin n) : xs[i] = b := sorry

More importantly, moving to getElem causes a few simp lemmas to no longer infer their arguments automatically.
Compare the three versions of scanl_get (Admittedly, by far the most affected proof, most proofs were fine).

/-- The original/Option 1: `get v i` -/
(scanl f b v).get i.succ = f ((scanl f b v).get (Fin.castSucc i)) (v.get i) := by
  cases' n with n
  · exact i.elim0
  induction' n with n hn generalizing b
  · have i0 : i = 0 := Fin.eq_zero _
    simp [scanl_singleton, i0, get_zero]; simp [get_eq_get]
  · rw [← cons_head_tail v, scanl_cons, get_cons_succ]
    refine' Fin.cases _ _ i
    · simp only [get_zero, scanl_head, Fin.castSucc_zero, head_cons]
    · intro i'
      simp only [hn, Fin.castSucc_fin_succ, get_cons_succ]

/-- Option 2: `v[i]` -/
theorem scanl_get (i : Fin n) :
    (scanl f b v)[i.succ] = f ((scanl f b v)[Fin.castSucc i]) v[i] := by
  cases' n with n
  · exact i.elim0
  induction' n with n hn generalizing b
  · have i0 : i = (0 : Fin 1) := Fin.eq_zero _
    simp [scanl_singleton, i0, get_zero]; simp [get_eq_get]
  · rw [← cons_head_tail v, scanl_cons, get_cons_succ (n:=n+2) _ _ i]
    refine' Fin.cases _ _ i
    · simp only [get_zero (n:=n+2), get_zero (n:=n+1), scanl_head, Fin.castSucc_zero, head_cons]
    · intro i'
      simp only [hn, Fin.castSucc_fin_succ, get_cons_succ (n:=n+2), get_cons_succ (n:=n+1)]

/-- Option 3: `v[i.1]` -/
theorem scanl_get (i : Fin n) :
    (scanl f b v)[i.1 + 1]'i.succ.2 = f ((scanl f b v)[i.1]) v[i.1] := by
  cases' n with n
  · exact i.elim0
  induction' n with n hn generalizing b
  · simp [scanl_singleton, get_zero, get_eq_get, get_cons_succ _ _ i]
  · rw [← cons_head_tail v, scanl_cons, get_cons_succ_nat (n:=n+2) _ _ i.1]
    refine' Fin.cases _ _ i
    · simp [get_zero_nat (n := n + 1), get_zero_nat (n := n + 2), scanl_head, head_cons]
    · intro i'
      simp only [Fin.val_succ, hn, get_cons_succ_nat (n := n + 2), get_cons_succ_nat (n := n + 1)]

In particular, notice how in option 1 simp[get_zero] and simp[get_cons_succ] just work, but in the other two we have to specify the value of n for it to do the rewrite.

Benefits of Option 2 (vs. option 3)

My reason for suggesting the alternative PR, is that for option 3 the normal form of what used to be get xs i.succ should now be spelled xs[i.1 + 1]'i.succ.2, which felt a bit to verbose to me.
I think the effect of sticking with option 3 (v[i.1]) would be that the easiest way to state theorems would be to avoid Fin entirely, and state them as v[i]'h where i : Nat and h : i < n. I quite like the Fin abstraction, so I would prefer to keep it!

[Alex Keizer]

@Chris Hughes @Gabriel Ebner and @Scott Morrison, I'd like your opinions on this in particular!

[Mario Carneiro]

The part I don't understand re: the std change is that std doesn't define Vector or Bitvec at all, the theorems under discussion are about arrays

[Alex Keizer]

Well, Std provides a generic GetElem \a (Fin n) _ _ instance for any implementors of GetElem \a Nat _ _. We want to index Vectors with both Nat and Fin n, so we define GetElem (Vector a n) Nat, which gives us GetElem (Vector a n) (Fin n) _ _ (but also GetElem (Vector a n) (Fin m) _ _, with appropriate side conditions ) from this generic instance in Std. The lemma in question, that rewrites v[i] for i : Fin n into v[i.1] applies to all versions of this generic GetElem cont (Fin n) instance, so also Vectors

[Alex Keizer]

I guess an alternative would be to restrict that GetElem instance to just Arrays. In fact, I would be in favour of that, so that we can have a more specialized instance for Vector, only allowing a Fin n to index a Vector \a n if the indices match.

[Alex Keizer]

Actually, part way through the change I've had to define a specialized GetElem instance anyway

section GetElem
  variable (cont : ℕ → Type u)

  instance [GetElem (cont n) Nat elem (fun _ i => i < n)] :
      GetElem (cont n) (Fin n) elem fun _ _ => True where
    getElem xs i _ := getElem xs i.1 i.2

end GetElem

Which makes the std change no longer necessary. Still, I do think we should restrict that generic instance from std to just Arrays anyway.
If we have both then the following is accepted, but refers to the generic instance (the indices don't match), and rewrites that do use the new instance won't apply.

example (v : Vector \a (n+1)) (i : Fin n) : a := v[i]

Since the pretty printer does not show which instance is used by default, this makes for very painful debugging

[Mario Carneiro]

I think you should stick with Vector.get. The generic instance is supposed to unfold in this way, while the Vector.get function can assert that the indices match

[Mario Carneiro]

the reasons seem to be similar as to why List uses a get function

[Alex Keizer]

I think List can't even define the stricter GetElem function, since the approriate index type Fin (xs.length) depends on the concrete list being indexed, whereas for Vector we know the index from the vector type alone.

[Andrés Goens]

would that mean there'd be no GetElem for Fin n for Array at all? Because one thing I've always found confusing with this is that something like a classical loop in do notation won't work:

def foo (a : Array Nat) : Nat := Id.run do
let mut res := 0
for i in Array.range a.size do
  res := res + a[i]
return res

and thought if there was a similar function range' (a : Array) -> Array (Fin a.size) then that should work with the GetElem instance the way you'd expect it to

[Alex Keizer]

There is one, it's the problematic generic instance, but it effectively ignores the index n. Instead, it takes as side-condition a proof that the value i.val is less than the size of the array/vector.

[Alex Keizer]

So that you can index an array of size 2 with 1 : Fin 4, even though the index is too high (because the actual value is still in bounds)

[Andrés Goens]

I see, yeah that sounds more problematic for sure, maybe it makes sense to just have an instance for the case that n is the size of the array? I'm not sure I understand why the instance by itself is problematic for simp normal form?

[Alex Keizer]

Because if you write v[Fin.succ i], then the side condition is sometimes inferred as (Fin.succ i).1 < n and other times as i.1 + 1 < n. These are different types, so if your lemma used on side condition, and your goal another, then the rewrite fails

[Andrés Goens]

oh I guess you mean if you have an instance you want to be able to reason about it and thus need a simp normal form, yeah that makes sense

[Chris Hughes]

I have a strong preference for either Option 1 or Option 2 as a simp normal form. Using Fin is usually much better than using a Nat and a proof. The proof term can make rewriting difficult, since it depends on the Nat, and we can define operations on Fin which bundle the proofs, and avoid us having to write the same proofs over again. We've already moved away from List.NthLE in the transition from mathlib3 to mathlib4.

[Alex Keizer]

Andrés Goens said:

I see, yeah that sounds more problematic for sure, maybe it makes sense to just have an instance for the case that n is the size of the array? I'm not sure I understand why the instance by itself is problematic for simp normal form?

Also, for arrays it's not possible to only have an instance for Fin (xs.size), since the index type is not able to depend on the concrete array being indexed. I guess that's why the current instance is set up with the side condition

[Alex Keizer]

Chris Hughes said:

I have a strong preference for either Option 1 or Option 2 as a simp normal form. Using Fin is usually much better than using a Nat and a proof. The proof term can make rewriting difficult, since it depends on the Nat, and we can define operations on Fin which bundle the proofs, and avoid us having to write the same proofs over again. We've already moved away from List.NthLE in the transition from mathlib3 to mathlib4.

I guess with Mario preferring not to make the changes to Std needed to make Option 2 not be a big footgun, that leaves only Option 1 (sticking with Vector.get)?

[Tobias Grosser]

Cool. Option 1 seems to be a good one.

[Alex Keizer]

Allright, then I'll restore the PR to using get