Missing array lemmas for grind

[tdardinier]

The following code computes the average of an array. The straightforward loop invariant invariant s = (a.take i).sum, using Lean constructs, does not work well, because Grind is missing key facts about how Array.sum and slicing interact (such as lemma for_grind in the code below).

It could be useful to identify such helpful Array lemmas and add them to grind when a user tries to verify a program manipulating arrays.

import CaseStudies.Velvet.Std
import CaseStudies.TestingUtil

set_option loom.semantics.termination "total"
set_option loom.semantics.choice "demonic"

--------------------------------------------------------
-- Task 1: Computing an average value of the array
--------------------------------------------------------

@[grind]
lemma for_grind (a: Array Int) (i: Nat) (h: i < a.size):
  (a.take (i + 1)).sum = (a.take i).sum + a[i]! :=
    sorry

@[grind]
lemma final_res (a: Array Int):
  a = a.take a.size
  := by
    exact Eq.symm Array.extract_size

method arrayAverage(a: Array Int) return (avg: Int)
  ensures avg = Array.sum a / a.size
  do
    let mut i := 0
    let mut s := 0
    while i < a.size
      invariant s = (a.take i).sum
      invariant i ≤ a.size
      decreasing a.size - i
    do
      let elem := a[i]!
      s := s + elem
      i := i + 1
    return s / a.size

-- Testing
-- DivM.res ⟨4, ()⟩
#eval (arrayAverage #[1,2,3,4,5,6,7]).run

prove_correct arrayAverage by
  loom_solve