simpNF lint with optional args

Stream: batteries

[cmlsharp]

My scan PR for arrays is currently failing CI because simpNF wants me to specify the optional arguments (start and stop indices) on the LHS of every theorem.

so e.g.

theorem scanl_reverse {f : β → α → β} {as : Array α} :
    scanl f init as.reverse = reverse (scanr (flip f) init as) := by

would need to be written as

theorem scanl_reverse {f : β → α → β} {as : Array α} :
    scanl f init as.reverse 0 as.size = reverse (scanr (flip f) init as) := by

To me it seems like this clutters up the theorem definitions. Should I make this change to every theorem, or if not is it possible to disable this lint?

[cmlsharp]

(the fact that the array versions have start/stop indices is just for parity with Array.foldl/foldr and so Subarray.scan* can be implemented in terms of the array version.

[Jovan Gerbscheid]

It's a bit hard to help if you don't share the error message of simpNF

[cmlsharp]

.../Batteries/Data/Array/Scan.lean:355:1: error: @Array.scanl_reverse Left-hand side simplifies from
  Array.scanl f init as.reverse
to
  Array.scanl f init as.reverse 0 as.size
using
  simp only [*, @Array.size_reverse]
Try to change the left-hand side to the simplified term!

[cmlsharp]

I suppose the issue here is that the default argument ends up becoming 'as.reverse.size', which simpNF wants to simplify to as.size. That's fair enough I suppose but it requires me to specify the default argument in the theorem statement.

Analogous theorems for Array.foldl in the standard library do not infect the theorem statement like this

[cmlsharp]

(just for reference this is the type of Array.scanl

def scanl (f : β → α → β) (init : β) (as : Array α) (start := 0) (stop := as.size) : Array β

[Jovan Gerbscheid]

Exactly, and the simpNF linter has a good point: if you have the LHS with as.reverse.size, then this simp lemma is useless. Those theorems in the standard library are also useless simp theorems.

[Jovan Gerbscheid]

Sorry I was wrong, in the standard library they do address this issue correctly. They have the following theorem for simp:

/-- Variant of `foldl_reverse` with a side condition for the `stop` argument. -/
@[simp] theorem foldl_reverse' {xs : Array α} {f : β → α → β} {b} {stop : Nat}
    (w : stop = xs.size) :
    xs.reverse.foldl f b 0 stop = xs.foldr (fun x y => f y x) b :=

[cmlsharp]

ah I see, so the righgt way to handle such cases is to provide two versions of the lemma, one "main" version without optional args specified or a simp annotation and then an equivalent lemma with the simp annotation and the optional arguments specified (and simplified)?

[Jovan Gerbscheid]

Indeed. Their Array.foldl_reverse' version has an extra stop variable with a hypothesis stop = xs.size. I presume that this comes in handy if xs is e.g. a literal array, something like #[x,y,z], in which case the simplified form of #[x,y,z].reverse.size is 3. If the lemma had xs.size inlined in xs.reverse.foldl f b 0 xs.size, then unification would fail to unify #[x,y,z].size with 3.