Proving recursive termination with Vector.mapM

Stream: new members

[James Parker]

Hi. I'm attempting to prove a recursive function that uses Vector.mapM terminates with decreasing_by. The function includes something like Vector.mapM (λ c => ...) cs. When proving termination, I have something like the following in the context:

c : T
cs : Array T

I'm able to prove termination if I add the assumption have hMem : c ∈ cs := by sorry and then use Array.sizeOf_lt_of_mem hMem. Is there a way to get hMem just from the use of Vector.mapM, or is there a better approach to proving the termination?

Also, I need the lemma :def lt_add (a b c : ℕ) : a < b -> a < b + c. Does this already exist in Mathlib? I couldn't find it with Loogle or Moogle.

Thanks!

[Aaron Liu]

Try docs#Vector.attach

[Aaron Liu]

Also lt_add is docs#Nat.lt_add_right

[James Parker]

Thanks! That's what we needed. Now I'm left with the goal (hV ▸ cs'.toVector).toArray = cs'. Do you have any suggestions here? grind actually says it succeeds, but we get the following type error:

error: ././././File.lean:22:4: application type mismatch
  { toArray := cs', size_toArray := ⋯ }.toArray
argument has type
  Vector T cs'.toList.length
but function has type
  Vector T 4 → Array (ZKExpr f)

[Robin Arnez]

use cs'.toVector.cast instead, that should work better

[Robin Arnez]

or Vector.mk