Recursion through `Array`

Stream: general

[Joachim Breitner]

How would I define this function without using partial:

inductive T : Type where
  | mk : Array T -> T

partial def T.size : T → Nat
  | .mk cs => cs.foldl (init := 0) fun n c => n + c.size

My best bet would be to assume we have a Array.attach like docs#List.attach and do something like

inductive T : Type where
  | mk : Array T -> T

opaque Array.attach : (a : Array α)  → Array ({ x : α // x ∈ a.data })

def T.size : T → Nat
  | .mk cs => cs.attach.foldl (init := 0) fun n ⟨c,hc⟩ => n + c.size
termination_by _ t => sizeOf t

(which doesn’t work yet but I believe I could make it work) but I wonder if there is a better direction.

[Arthur Adjedj]

(deleted)

[Joachim Breitner]

Here is a way that seems to work:

inductive T : Type where
  | mk : Array T -> T

opaque Array.attach {α} : (a : Array α)  → Array ({ x : α // x ∈ a.data })

@[simp]
theorem Array.sizeOf_eq {α} [SizeOf α] (cs : Array α) :
    sizeOf cs = 1 + sizeOf cs.data := rfl

def T.size : T → Nat
  | .mk cs => cs.attach.foldl (init := 0) fun n ⟨c, _hc⟩ => n + c.size
termination_by _ t => sizeOf t

Do I really have to tell Lean to unfold sizeOf here?

[Joachim Breitner]

Ah, looks like there is setup for such recursion in https://leanprover-community.github.io/mathlib4_docs/Init/Data/Array/Mem.html, but it (needlessly) requires decidable equality on the elements, and I can’t quite get Array.sizeOf_lt_of_mem to work here.

[Joachim Breitner]

This works:

inductive T : Type where
  | mk : Array T -> T

opaque Array.attach {α} [DecidableEq α]: (a : Array α) → Array ({ x : α // x ∈ a })

instance : DecidableEq T := sorry

macro "array_mem_dec" : tactic =>
  `(tactic| first
    | apply Array.sizeOf_lt_of_mem; assumption; done
    | apply Nat.lt_trans (Array.sizeOf_lt_of_mem ?h)
      case' h => assumption
      simp_arith)

macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_mem_dec)

def T.size : T → Nat
  | .mk cs => cs.attach.foldl (init := 0) fun n ⟨c, _hc⟩ => n + c.size

Is the setup in Init.Data.Array.Mem incomplete? It defines Array.sizeOf_lt_of_mem, but doesn’t register it with decreasing_trivial in the same way that List.sizeOf_lt_of_mem is set up. Maybe a simple omission because nobody complained loudly enough yet. If that’s the case, then <https://github.com/leanprover/lean4/pull/2774> should improve matters. If and once that tickles through to std4 I can also add Array.attach there.