trying to define sizes of trees

Stream: general

[Frederick Pu]

Can someone please explain why I can define size for this kind of tree:

inductive Tree
| mk (val : Nat) (children : List Tree)

def Tree.size : Tree → Nat
| mk val [] => 1
| mk val (a::l) => a.size + (mk val l).size

but not for the below kind?

protected inductive ComputedAutoDiffTree.DiffTree (α : Type u) (β : Type v) : List Nat → Type (max u v)
| mk
    {outShape : List Nat}
    (parents : List (Σ shape, ComputedAutoDiffTree.DiffTree α β shape))
    (saved_tensors : Σ shapes, ShapedVector (DualTensor α β) shapes)
    (ctx : Σ shapes, EFunction α β shapes outShape)
    (tensor : DualTensor α β outShape)
    : ComputedAutoDiffTree.DiffTree α β outShape

protected def ComputedAutoDiffTree.DiffTree.size {α : Type u} {β : Type v} {shape : List Nat} : ComputedAutoDiffTree.DiffTree α β shape → Nat
| mk [] _ _ _ => 0
| mk (a::l) x y z => a.2.size + (mk l x y z).size
/-
fail to show termination for
  ComputedAutoDiffTree.DiffTree.size
with errors
failed to infer structural recursion:
Not considering parameter α of ComputedAutoDiffTree.DiffTree.size:
  it is unchanged in the recursive calls
Not considering parameter β of ComputedAutoDiffTree.DiffTree.size:
  it is unchanged in the recursive calls
Cannot use parameter #4:
  failed to eliminate recursive application
    (mk l x y z).size
Cannot use parameter shape:
  failed to eliminate recursive application
    a.snd.size


Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
             shape #1
1) 145:21-29     ?  ?
2) 145:32-49     _  _

#1: sizeOf x2

Please use `termination_by` to specify a decreasing measure.
-/

[Kyle Miller]

I'll take a look, but something I'd like to point out is that Lean now supports recursive structures. Here's using that along with a relatively clean way to define Tree.size, where you don't need to re-build a Tree with a synthetic node during recursion:

structure Tree where
  val : Nat
  children : List Tree

mutual
def Tree.size : Tree → Nat
  | { children, .. } => Tree.sizeAux children
def Tree.sizeAux : List Tree → Nat
  | [] => 1
  | x :: xs => x.size + Tree.sizeAux xs
end

[Kyle Miller]

Ah, your example isn't a #mwe, which would make it easier to help

[Kyle Miller]

Maybe this mutual suggestion might help you?

[Frederick Pu]

i think this is mwe:

protected inductive ComputedAutoDiffTree.DiffTree (α : Type u) (β : Type v) : List Nat → Type (max u v)
| mk
    (outShape : List Nat)
    (parents : List (Σ shape, ComputedAutoDiffTree.DiffTree α β shape))
    : ComputedAutoDiffTree.DiffTree α β outShape

protected def ComputedAutoDiffTree.DiffTree.size {α : Type u} {β : Type v} {shape : List Nat} : ComputedAutoDiffTree.DiffTree α β shape → Nat
| mk x [] => 0
| mk x (a::l) => a.2.size + (mk x l).size
/-
fail to show termination for
  ComputedAutoDiffTree.DiffTree.size
with errors
failed to infer structural recursion:
Not considering parameter α of ComputedAutoDiffTree.DiffTree.size:
  it is unchanged in the recursive calls
Not considering parameter β of ComputedAutoDiffTree.DiffTree.size:
  it is unchanged in the recursive calls
Cannot use parameter #4:
  failed to eliminate recursive application
    (mk x l).size
Cannot use parameter shape:
  failed to eliminate recursive application
    a.snd.size
    -/

[Kyle Miller]

This seems to work:

protected def ComputedAutoDiffTree.DiffTree.size {α : Type u} {β : Type v} {shape : List Nat}
    (t : ComputedAutoDiffTree.DiffTree α β shape) : Nat :=
  match t with
  | mk x [] => 0
  | mk x (a::l) =>
    have : sizeOf a.snd < 1 + sizeOf x + (1 + sizeOf a + sizeOf l) := by
      cases a
      simp
      omega
    a.2.size + (mk x l).size
termination_by sizeOf t

I guess the complexity is that Lean isn't able to automatically see that that a.2 is smaller in the recursive call.

[Kyle Miller]

(I got this have line by adding the termination_by then reading the error message.)

[Frederick Pu]

what is sizeOf?

[Frederick Pu]

cause isnt a.snd a DiffTree, so the type class instance wouldnt be defined yet right?

[Kyle Miller]

There's a SizeOf instance defined by inductive/structure whenever they're defining recursive types, and it provides this sizeOf function.

[Frederick Pu]

so how would i generalize this to the original type?

[Frederick Pu]

like im thinking about smth like

protected def ComputedAutoDiffTree.DiffTree.size {α : Type u} {β : Type v} {shape : List Nat} : ComputedAutoDiffTree.DiffTree α β shape → Nat
| mk [] _ _ _ => 0
| mk (a::l) x y z =>
    have : sizeOf a.snd < 1 + (1 + sizeOf a + sizeOf l) + sizeOf x.snd + sizeOf y.snd + sizeOf z := by
        cases x
        cases y
        cases z
        simp
        omega
    a.2.size + (mk l x y z).size
termination_by
 t => sizeOf t

but im not too sure what the motivation for the original solution was

[Kyle Miller]

That seems sensible — are you running into any issue?

[Frederick Pu]

nvm im slow ur supposed to do cases on a

protected def ComputedAutoDiffTree.DiffTree.size {α : Type u} {β : Type v} {shape : List Nat} : ComputedAutoDiffTree.DiffTree α β shape → Nat
| mk [] _ _ _ => 0
| mk (a::l) x y z =>
    have : sizeOf a.snd < 1 + (1 + sizeOf a + sizeOf l + sizeOf x + sizeOf y + sizeOf z) := by
        cases a
        simp
        omega
    a.2.size + (mk l x y z).size
termination_by
    x => sizeOf x

[Frederick Pu]

im still confused for what the intuition is tho

[Kyle Miller]

I did cases so that sizeOf a.snd would simplify

[Kyle Miller]

and so that sizeOf a would expand

[Kyle Miller]

omega doesn't know any relationship between sizeOf a.snd and sizeOf a, so it was to help it out.

[Frederick Pu]

no like why is that specific hypothesis enough to convince termination_by

[Kyle Miller]

Kyle Miller said:

(I got this have line by adding the termination_by then reading the error message.)

I copied it from the error message

[Kyle Miller]

I didn't think hard about it.

[Frederick Pu]

oh lol

[Frederick Pu]

sorry i just had exams so im legit room temp iq rn

[Kyle Miller]

It looks like the way it's working is that you take the sum of the sizeOf the arguments to ComputedAutoDiffTree.DiffTree.size, and if that's greater than sizeOf the recursive call to the function with a.snd, then it's able to argue the function terminates.

[Kyle Miller]

(And by "able to argue" that actually means "able to construct some term that implements the recursive function". If you #print the function you'll likely see some Nat.brecOn that's implementing the recursion.)

[Frederick Pu]

whats brecOn?

[Frederick Pu]

would you happen to know why rfl isn't working in this case?

protected inductive ComputedAutoDiffTree.DiffTree (α : Type u) (β : Type v) : List Nat → Type (max u v)
| mk : ComputedAutoDiffTree.DiffTree α β outShape
protected def ComputedAutoDiffTree.DiffTree.valid {α : Type u} {β : Type v} {shape : List Nat} : ComputedAutoDiffTree.DiffTree α β shape → Prop :=
  fun x => True

protected inductive AutoDiffTree.DiffTree (α : Type u) (β : Type v) : List Nat → Type (max u v)
| mk
    (outShape : List Nat)
    (parents : Array (Σ shape, AutoDiffTree.DiffTree α β shape))
    : AutoDiffTree.DiffTree α β outShape
| ofComputed {shape : List Nat}: ComputedAutoDiffTree.DiffTree α β shape → AutoDiffTree.DiffTree α β shape

def AutoDiffTree.DiffTree.valid {α : Type u} {β : Type v} {shape : List Nat} : AutoDiffTree.DiffTree α β shape → Prop
| mk _ #[] => True
| ofComputed computedTree => computedTree.valid
| mk _ parents => ∀ x ∈ parents, x.2.valid
termination_by
    t => sizeOf t
decreasing_by
    have : sizeOf x < sizeOf parents := Array.sizeOf_lt_of_mem (by assumption)
    cases x
    simp
    simp at this
    omega

example {α : Type u} {β : Type v} {shape : List Nat} (x : ComputedAutoDiffTree.DiffTree α β shape) : (AutoDiffTree.DiffTree.ofComputed x).valid = x.valid :=
  rfl
/-
    type mismatch
    rfl
  has type
    ?m.4183 = ?m.4183 : Prop
  but is expected to have type
    (AutoDiffTree.DiffTree.ofComputed x).valid = x.valid : Prop
-/