Nested inductives - Option in custom type

Stream: lean4

[Wrenna Robson]

The following (which I think is a MWE) doesn't work:

inductive BTree (β : Type u) : Nat → Type u where
  | leaf : (n : ℕ) → β → BTree β n
  | node : {n : ℕ} → Option (BTree β n) → Option (BTree β n) → BTree β (n + 1)

I get this message:

(kernel) invalid nested inductive datatype 'Option',
nested inductive datatypes parameters
cannot contain local variables.

This seems reasonable enough: is there a way of modifying my definition to achieve this?

[Wrenna Robson]

Oho: this seems to work:

inductive BTree (β : Type u) : (n : Nat) → Type u where
  | leaf : β → BTree β n
  | node : Option (BTree β n) → Option (BTree β n) → BTree β (n + 1)

[Edward van de Meent]

i think it will be easier to have the Nat not be a parameter, but rather a result of a function, similar to Vector compared to List. (it will help you keep out of dependent type hell).

[Wrenna Robson]

Hmm - I see why I'd want that, but I do wantto restrict "node" in this way... I think? Though perhaps I can simply avoid it.

[Wrenna Robson]

Hmm... I do think it would be much trickier to get some of the other properties I want without that.

[Edward van de Meent]

i'd like to point out that you will be able to construct empty nodes with arbitrary depths with the type as-is... is this what you want?

[Wrenna Robson]

Yep.

[Edward van de Meent]

huh

[Edward van de Meent]

what's your application, if i may ask?

[Wrenna Robson]

I am trying to prove something about the treeHash function used in XMSS.

[Wrenna Robson]

https://www.rfc-editor.org/rfc/rfc8391#section-4.1.6

[Arthur Adjedj]

What you want is a nested indexed datatype. Lean currently doesn't manage those. One solution would be to (manually) convert your nested inductive type into a mutual type such as this one:

mutual
inductive OptionBTree (β : Type u) : Nat → Type u
  | none : OptionBTree β n
  | some : BTree β n → OptionBTree β n

inductive BTree (β : Type u) : (n : Nat) → Type u where
  | leaf : β → BTree β n
  | node : OptionBTree β n → OptionBTree β n → BTree β (n + 1)
end

[Edward van de Meent]

lean does manage it tho? you may have previously come across versions with Lists, for that matter.

[Wrenna Robson]

Yeah my second version above works :)

[Edward van de Meent]

i seem to recall it was a special implementation for only a few basic inductive types tho, but Option is among them

[Edward van de Meent]

(i could be wrong)

[Arthur Adjedj]

Wrenna Robson said:

Yeah my second version above works :)

I get the following error on your second version (running on nightly):

inductive BTree (β : Type u) : (n : Nat) → Type u where
  | leaf : β → BTree β n
  | node : Option (BTree β n) → Option (BTree β n) → BTree β (n + 1)
/-(kernel) invalid nested inductive datatype 'Option', nested inductive datatypes parameters cannot contain local variables.-/

[Wrenna Robson]

Odd. I do get it in a fresh file, but I don't in my other one, but I really thought I wasn't using any imports

[Arthur Adjedj]

Edward van de Meent said:

lean does manage it tho? you may have previously come across versions with Lists, for that matter.

Lean manages nested inductive types, and managed indexed inductive types, but it does not manage nested indexed inductive types. For example, the following fails:

inductive Foo (A : Type)

set_option inductive.autoPromoteIndices false in
inductive Bar (A : Type) : Nat → Type
  | bar : Foo (Bar A n) → Bar A n

[Wrenna Robson]

Ah, this works:

inductive BTree {n : ℕ} (β : Type u) : (n : ℕ) → Type u where
  | leaf : β → BTree β 0
  | node : Option (BTree β n) → Option (BTree β n) → BTree β (n + 1)

[Wrenna Robson]

I had a variable somewhere that was introducing the {n : ℕ}

[Wrenna Robson]

So that's not really what I want, certainly.

[Arthur Adjedj]

Wrenna Robson said:

Odd. I do get it in a fresh file, but I don't in my other one, but I really thought I wasn't using any imports

No imports can solve this. Are you sure you sent the "right" definition ? something like this would pass, because Nat would be promoted to a parameter instead of an index.

inductive BTree (β : Type u) : (n : Nat) → Type u where
  | leaf : β → BTree β n
  | node : Option (BTree β n) → Option (BTree β n) → BTree β n --used to be BTree β (n+1)

Nevermind, you answered already

[Wrenna Robson]

As I say, I had variable {n : Nat} much further above, and that was causing it to "work" (but you can see why actually it doesn't so much work)

[Edward van de Meent]

out of curiosity, why does removing the Nat parameter fix this issue?

[Wrenna Robson]

Well, it makes my above example not work, so it doesn't so much fix it as reveal that my "fix" was not.

[Wrenna Robson]

The mutual definition above does work, but might be somewhat unwieldy.

[Edward van de Meent]

it turns out i just need to read through your message more carefully: because Nat is an index here, and as you said, lean doesn't manage nested indexed inductives.

[Wrenna Robson]

Essentially the issue arises because I am constructing the tree "downwards" rather than upwards.

In the application, I am trying to prove that calculating the hash of a tree with 2^n leaf nodes in the "natural" recursive way (if n = 0, done, otherwise split into two halves, calculate their hashes, find hash of the result) is the same as using a "stack" (as the reference implementation of treeHash does).

[Wrenna Robson]

The difference essentially is that you massively save on storage space, because you only actually need to store ~ n things at once, rather than 2^n things.

[Wrenna Robson]

Basically you calculate hashes "when you need them", adding a leaf at a time.

[Arthur Adjedj]

I mean, to be clearer, Lean does manage some instances of nested indexed inductive types. Namely, as long as the indices appearing in the nested occurences do not contain free variables (read: variables introduced in the constructor itself), then it's all good, but it won't manage it if free variables are appearing in the indices. Since in @Wrenna Robson's example, the n appearing in the index is introduced as a parameter, Lean doesn't complain, despite the fact that it is indeed a nested indexed inductive types.

[Wrenna Robson]

This turns out to sort of be analogous to binary number succession (you can model your stack as a list of Option types and basically adding a new leaf and calculating any new hashes is analogous to adding 1 to the binary number and doing the carries).

[Wrenna Robson]

And it's really surprisingly hard to prove them equivalent despite the fact it's "obviously" true.

[Edward van de Meent]

Wrenna Robson said:

Essentially the issue arises because I am constructing the tree "downwards" rather than upwards.

in that case, i still don't get why you want the "depth" value to be constant over the construction?

[Wrenna Robson]

I don't, I want it to descend.

[Wrenna Robson]

Hence the n + 1. But it may not be the right choice.

[Arthur Adjedj]

If you're expected to work with 2^n leaves, wouldn't you want your node to be of type BTree β n → BTree β n → BTree β (n + 1) ?

[Wrenna Robson]

Yeah so obviously that does work (and is what I had before) - the thing is that I want to allow for "truncated" trees, or unknown trees - basically to represent when I've not loaded in all the leaves.

[Wrenna Robson]

Essentially it doesn't seem like induction on n is ever quite enough - I would like to be able to construct my tree by adding a leaf at a time and performing cancellations as appropriate (if I have two leaves with a value specified at a node, I can replace that node with a leaf of height + 1 whose value is the hash of the other two).

[Wrenna Robson]

But that means I need to be able to work with, essentially, any number of leaves from 0 to 2^n (inclusive).

[Wrenna Robson]

I could just do something like this:

inductive BTree (β : Type u) : ℕ → Type u where
  | leaf : (n : ℕ) → Option β → BTree β n
  | node : {n : ℕ} → BTree β n → BTree β n → BTree β (n + 1)

[Wrenna Robson]

This has proven fairly fruitful, but I'm not sure it's quite right.

[Edward van de Meent]

i'd recommend the following (to avoid dependent type hell):

import Mathlib.Util.CompileInductive
inductive BTree (β : Type u) : Type u where
  | leaf : β → BTree β
  | node : Option (BTree β) → Option (BTree β) → BTree β

compile_inductive% BTree

def BTree.depth {β:Type u} (t : BTree β) : Nat :=
  t.rec (fun _ => 0) (fun _ _ l r => (max l r) + 1) 0 (fun _ n => n)

def BTree' (β : Type u) (n:Nat) : Type u := {t:BTree β // t.depth = n}

[Wrenna Robson]

Oho

[Edward van de Meent]

note that this doesn't enforce the 2^n stuff, the shape can be weird. but it should at least give you a way out of having to rewrite inside the type of things

[Wrenna Robson]

Yeah that is always Bad.

[Wrenna Robson]

It does mean that if t = node l r, you know that the depth of l and r are less than the depth of t, but no more than that I think?

[Edward van de Meent]

exactly that, yes

[Wrenna Robson]

Well, I suppose one of them at least has to have depth one less than it.

[Edward van de Meent]

no, both

[Wrenna Robson]

Well, l could have depth 0, say, no?

[Wrenna Robson]

And then the depth of t will be r.depth + 1

[Edward van de Meent]

the depth of a .node is the maximum of the depths of subtrees plus 1. so it is always larger than both depths.

[Wrenna Robson]

No I get that

[Wrenna Robson]

I'm just saying that the one with the larger depth (if they have different depths) will obviously be equal to the maxmimum, one less than it.

[Wrenna Robson]

Wheras the other can range anywhere inbetween.