sizeOf of an array and its toList

Stream: general

[Juneyoung Lee]

Can I prove the equality of sizeOf arr and sizeOf arr.toList? Don't know where to start. :/ How people typically find lemmas that are related to sizeOf as well as some interested function (like toList)?

theorem tmp: ∀ (x:Array Nat), sizeOf x = sizeOf x.toList := by
  intro x
  -- ??

[Kenny Lau]

I would recommend to not use sizeOf, we have List.length and Array.size

[Juneyoung Lee]

It seems sizeOf is for termination checking, right? I indeed need to prove termination of a recursive function.

[Robin Arnez]

You can also use termination_by l.length

[Chris Bailey]

Fwiw the statement you have is false, Array's sizeOf is 1 + x.toList._sizeOf_1. You can prove that though.

theorem tmp: ∀ (x:Array Nat), sizeOf x = 1 + (sizeOf x.toList) := by
  intro x
  simp [SizeOf.sizeOf, Array._sizeOf_1]
  done

[Juneyoung Lee]

@Robin Arnez The argument was an inductive data type that has an array as its argument, something like this:

inductive MyTy where
| leaf: MyTy
| nonLeaf: Array MyTy → MyTy

def f (t:MyTy): List MyTy :=
  match t with
  | .leaf => []
  | .nonLeaf a => List.flatten (List.map f (a.toList))

@Chris Bailey Thanks, that was the answer that I wanted. :)

[Aaron Liu]

In this case the "correct" thing to do (in my opinion) would be to have two mutually recursive definitions, acting on the MyTy and List MyTy respectively, and then maybe perhaps also write some csimp lemmas if those are needed.

[Aaron Liu]

This lets you do structural recursion instead

[Juneyoung Lee]

Hi Aaron, thanks for a suggestion. I tried this, but this seems to fail; do you have any idea about how to fix this?

mutual
def flist (a:List MyTy): List (List MyTy) := -- Says it failed to infer structural recursion
  List.map f a

def f (t:MyTy): List MyTy :=
  match t with
  | .leaf => []
  | .nonLeaf a => List.flatten (flist a.toList)
end

[Aaron Liu]

Well you can't just write List.map

[Aaron Liu]

you have to write out the whole thing

[Aaron Liu]

like with a match

[Malvin Gattinger]

If you want to keep the definition with map you can also define your own .length instead of sizeOf and then prove termination like this. It needs a lot of Mathlib though.

import Mathlib.Algebra.Order.BigOperators.Group.List
import Mathlib.Algebra.Order.Group.Nat

inductive MyTy where
| leaf: MyTy
| nonLeaf: List MyTy → MyTy

def MyTy.length : MyTy → Nat
| .leaf => 1
| .nonLeaf l => 1 + (l.map MyTy.length).sum

def f (t: MyTy) : List MyTy :=
  match t with
  | .leaf => []
  | .nonLeaf a => (a.map f).flatten
-- Actually all the rest can be omitted, see Josh Cohen below ;-)
termination_by
  t.length
decreasing_by
  next t h =>
    simp only [MyTy.length, gt_iff_lt]
    have := @List.le_sum_of_mem _ _ _ _ (l.map MyTy.length) t.length (by aesop)
    omega

[Juneyoung Lee]

Thanks Malvin. It seems if the argument of nonLeaf is List MyTy, not Array MyTy, Lean4 can smartly prove that the function f terminates. It is great to still know that when the measure is defined as t.length it can be proven like your proof.
How can we print the measure of f that Lean used for the List MyTy version? Wondering whether #synth SizeOf MyTy is the right result.

[Malvin Gattinger]

I have never used #synth before but it suggests MyTy._sizeOf_inst which can be shown with #reduce MyTy._sizeOf_inst :thinking:

[Malvin Gattinger]

Oh, and these work, suggesting that sizeOf actually does recurse into the list in a useful way?

#reduce sizeOf [MyTy.leaf]  -- 3
#reduce sizeOf [(MyTy.nonLeaf [])]  -- 4
#reduce sizeOf [sizeOf (MyTy.nonLeaf [MyTy.leaf])]  -- 6

[Juneyoung Lee]

Was never aware of #reduce :), thanks. (probably it was one of the most basic commands in Lean4, but I was forgetting it; I was using eval instead)

[Malvin Gattinger]

No need for a custom .length actually :drum:

import Mathlib.Algebra.Order.BigOperators.Group.List
import Mathlib.Algebra.Order.Group.Nat

inductive MyTy where
| leaf: MyTy
| nonLeaf: List MyTy → MyTy

theorem helper (l : List MyTy) : (List.map sizeOf l).sum < sizeOf l := by
  induction l
  · simp_all
  case cons t ts IH =>
    simp
    omega

def f (t: MyTy) : List MyTy :=
  match t with
  | .leaf => []
  | .nonLeaf l => (l.map f).flatten
-- the rest is not needed!
decreasing_by
  next t h =>
    simp [gt_iff_lt]
    have := @List.le_sum_of_mem _ _ _ _ (l.map sizeOf) (sizeOf t) (by aesop)
    have : (l.map sizeOf).sum < sizeOf l := helper l
    omega

[Josh Cohen]

I believe the following works as well:

inductive MyTy where
| leaf: MyTy
| nonLeaf: Array MyTy → MyTy

def f (t:MyTy): List MyTy :=
  match t with
  | .leaf => []
  | .nonLeaf a => List.flatten (Array.map f a).toList

[Malvin Gattinger]

Funny, so with (a.map f).toList it can prove termination easily, but with (a.toList.map f) it cannot.

[Josh Cohen]

The reason this works (I believe) is here: #new members > Understanding the termination checker for nested recursion

[Malvin Gattinger]

Thanks! Maybe I am mixing it up now, but do I understand correctly that docs#Array.toList_map used by simp will turn (a.map f).toList into (a.toList.map f), so from an expression that the termination checker can deal with into one that it cannot deal with?

[Aaron Liu]

Juneyoung Lee said:

Hi Aaron, thanks for a suggestion. I tried this, but this seems to fail; do you have any idea about how to fix this?

mutual
def flist (a:List MyTy): List (List MyTy) := -- Says it failed to infer structural recursion
  List.map f a

def f (t:MyTy): List MyTy :=
  match t with
  | .leaf => []
  | .nonLeaf a => List.flatten (flist a.toList)
end

like this

inductive MyTy where
| leaf: MyTy
| nonLeaf: Array MyTy → MyTy

mutual
def flist (a : List MyTy) : List (List MyTy) :=
  match a with
  | [] => []
  | x :: xs => f x :: flist xs

def f (t : MyTy) : List MyTy :=
  match t with
  | .leaf => []
  | .nonLeaf a => List.flatten (flist a.toList)
end

[Mirek Olšák]

Regarding sizeOf, constructors have their equations for sizeof, in case of Array

#check Array.mk.sizeOf_spec -- Array.mk.sizeOf_spec.{u} {α : Type u} [SizeOf α]
      -- (toList : List α) : sizeOf { toList := toList } = 1 + sizeOf toList

So the size of an Array is exactly one more than of the appropriate List.

[Mirek Olšák]

That avoids unpacking the internal _size_of_1...

[Juneyoung Lee]

Thank you all. Every answer was very helpful. :)