@gebner I've now made the change from get v i to v[i.1] as simp normal form in Vector files. The CI is still unhappy, because some downstream files are still broken and have to be updated. But before I continue on to fix those, I want to check in with you and confirm that this is indeed the direction we want to go to.

With the new simp normal form, some simp lemmas are not firing automatically anymore, and have to be explicitly given some of their arguments. Compare the following two proofs of Vector.scanl_get (admittedly, the worst case, most proofs worked just fine)

theorem scanl_get (i : Fin n) :
    (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]

And the new version:

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)]

Notice how get_cons_succ does not work, but instead we have to get_cons_succ_nat (n := n + 2), get_cons_succ_nat (n := n + 1) --- get_cons_succ_nat is a new version of the lemma in terms of i : Nat and h : i < n, instead of the old spelling in terms of i : Fin n, because the simplifier is quite aggresive with destructuring into Nats.

Maybe it would be beneficial to get rid of getElem_fin as a simp-lemma (or even reverse it), so that we can at least keep indexing with Fins instead of Nats as the normal-form

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

If we don't, then it would probably be less painful to write all theorems in terms of i : Nat and h : i < n instead of i : Fin n.

EDIT: I've proposed removing the simp attribute from this lemma at leanprover-community/batteries#162

The consensus on Zulip seems to be that we want to stick with Vector.get for the normal form, so I've reverted the PR back to the original.
I have stashed the reverted changes in a add-vector-api-opt3 branch, might we want to revisit this decision.

✌️ alexkeizer can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors merge

Build failed:

• Build

bors merge

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style