Alternative induction principle for Arrays

Stream: general

[Yicheng Qian]

Proving theorems about Arrays in Lean using induction is difficult. Since Lean has many lemmas about arrays that involve push, would it be helpful to have the following induction principle:

def List.concat_rec.{u, v}
  {α : Type u} {motive : List α → Sort v} (nil : motive [])
  (conc : (head : List α) → (tail : α) → motive head → motive (head.concat tail))
  (t : List α) : motive t :=
  let rec go : (t : List α) → motive t.reverse
    | .nil => nil
    | .cons head tail => by
      rw [List.reverse_cons, ← List.concat_eq_append]
      exact conc _ _ (go _)
  List.reverse_reverse t ▸ go t.reverse

def Array.push_rec.{u, v}
  {α : Type u} {motive : Array α → Sort v} (nil : motive #[])
  (push : (head : Array α) → (tail : α) → motive head → motive (head.push tail))
  (t : Array α) : motive t :=
  List.concat_rec nil (fun head => push ⟨head⟩) t.toList

[Wrenna Robson]

List.reverseRecOn exists

[Wrenna Robson]

Now, that uses l ++ [a] instead of l.concat a. Per List.concat_eq_append, that is the simp-normal form. Which I've always thought was a little odd but there we go.

[Wrenna Robson]

However I think this would not be a good recursor for Arrays, or rather I think it would be but it should ideally be constructed differently, because you want it to be able to build data efficiently as well, right?

[Robin Arnez]

Oh wow docs#List.reverseRecOn is really slow (quadratic time!). This implementation seems better.

[Robin Arnez]

(deleted)

[Robin Arnez]

Here's a better implementation of pushRec:

@[elab_as_elim]
def Array.pushRec.{u, v}
    {α : Type u} {motive : Array α → Sort v} (empty : motive #[])
    (push : (a : Array α) → (v : α) → motive a → motive (a.push v))
    (t : Array α) : motive t :=
  if h : t.isEmpty then
    cast (congrArg motive ?_) empty
  else
    cast (congrArg motive ?_) (push t.pop (t.back ?_) (pushRec empty push _))
termination_by t.size
decreasing_by grind [Array.isEmpty_iff_size_eq_zero]
where finally all_goals grind [Array.isEmpty_iff_size_eq_zero]

[Yicheng Qian]

Wrenna Robson said:

However I think this would not be a good recursor for Arrays, or rather I think it would be but it should ideally be constructed differently, because you want it to be able to build data efficiently as well, right?

I'm not sure if we would like to use this recursor to build data in addition to building proof. I think the preferred way of writing Array programs is to use for loop and access the elements of the array using getElem because Lean has special support for certain Array operations. But I'm not sure.

[Wrenna Robson]

Could we build the recursor using for loops?

[Aaron Liu]

You would have to make it dependently typed

[Yicheng Qian]

Robin Arnez said:

Here's a better implementation of pushRec:

@[elab_as_elim]
def Array.pushRec.{u, v}
    {α : Type u} {motive : Array α → Sort v} (empty : motive #[])
    (push : (a : Array α) → (v : α) → motive a → motive (a.push v))
    (t : Array α) : motive t :=
  if h : t.isEmpty then
    cast (congrArg motive ?_) empty
  else
    cast (congrArg motive ?_) (push t.pop (t.back ?_) (pushRec empty push _))
termination_by t.size
decreasing_by grind [Array.isEmpty_iff_size_eq_zero]
where finally all_goals grind [Array.isEmpty_iff_size_eq_zero]

@Robin Arnez Which version of Lean are you using? I'm getting syntax error on my end.

[Robin Arnez]

Yeah you need to be v4.22.0

[Robin Arnez]

This is using very recent additions

[Aaron Liu]

Robin Arnez said:

Oh wow docs#List.reverseRecOn is really slow (quadratic time!). This implementation seems better.

Is it? I think this one is quadratic time too.

[Robin Arnez]

Isn't this one it O(n) reverse and O(n) traverse?

[Robin Arnez]

Ah I see another reversal is hidden under the _

[Robin Arnez]

Yeah I guess quadratic time as well then