Tree with fixed branching

Stream: lean4

[Tomas Skrivan]

I'm trying to define data structure for trees with fixed branching factor. With the help of this question I have managed to get it compile, but I'm confused why I have to use Vector and can't use NArray

inductive Vector (α : Type u) : Nat → Type u where
  | nil  : Vector α 0
  | cons : α → Vector α n → Vector α (n+1)

def NArray (α : Type u) (n : Nat) : Type u := {u : Array α // u.size = n}

inductive Node (Data : Type) (n : Nat) : Type where
| empty : Node Data n
| node  (children : Vector (Node Data n) n) : Node Data n
| leaf  (data : Data) : Node Data n

With (children : NArray (Node Data n) n) it produces an error

(kernel) arg #3 of 'Node.node' contains a non valid occurrence of the datatypes being declared

Or another attempt | node (children : Array (Node Data n)) (h : children.size = n) : Node Data n produces

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

I would much rather deal with Array then with Vector. Also from performance perspective, I'm expecting Array to be faster.

[Leonardo de Moura]

@Tomas Skrivan Mario answered this question for Lists here https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20requiring.20proofs.20on.20inductive.20constructors/near/277021847
It is the same thing here but with Array instead of List.

[Tomas Skrivan]

I must have completely misunderstand the answer, I will read it again properly.

[Leonardo de Moura]

Note that Arrays are defined in Lean as a wrapper around List, and the runtime has special support for their basic operations.
In the future, we can do the same for NArray and Vector.

[Tomas Skrivan]

Is there a need for writing special runtime support for NArray? As it is just a pair of Array and a proof, the proof get eliminated in runtime so NArray is effectively just Array. In general, it would be nice if runtime performace of Subtype P, P : α → Prop, is the same as for α.

[Leonardo de Moura]

The problem is your Node example above. The NArray defined as a subtype prevents us from using it in a type like Node.

[Leonardo de Moura]

If we define NArray as a simple wrapper around Vectorlike Array is a wrapper around List, then Node works, but to get the runtime behavior we want, we need support in the runtime.

[Tomas Skrivan]

Right, I think I see the problem. Still do not understand why NArray as subtype is causing problem in the definition of Node, but that is due to my lack of type theory knowledge :grinning:

[Leonardo de Moura]

We should probably write documentation for this. This is a recurrent question.

[Mario Carneiro]

I believe unsafe inductive is always an option if you really want a certain runtime representation. I think it will allow some crazy dependencies in this case

[Mario Carneiro]

it is unfortunate that there is no equivalent of partial for inductives - the fact that unsafe is viral really makes this approach inconvenient to work with

[Tomas Skrivan]

I'm considering working with:

inductive Node (Data : Type) : Type where
| empty : Node Data
| node  (children : Array (Node Data)) : Node Data
| leaf  (data : Data) : Node Data

partial def Node.FixedBranching (n : Nat) : Node Data → Prop
| empty => True
| node children => children.size = n ∧ ∀ i, (children.get i).FixedBranching n
| leaf _ => True

structure MNode (Data : Type) (m : Nat) where
  node : Node Data
  fix_branching : node.FixedBranching m

Not sure how to show termination though. I should learn the new termination syntax.

[Leonardo de Moura]

I often find inductive predicates more convenient to use than definitions such FixedBranching.

inductive Node.FixedBranching (n : Nat) : Node Data → Prop where
  | empty : FixedBranching n empty
  | leaf  : (d : Data) → FixedBranching n (leaf d)
  | node  : {cs : Array (Node Data)} → cs.size = n → (∀ i, FixedBranching n (cs.get i)) → FixedBranching n (node cs)

[Tomas Skrivan]

Nice! probably easier to deal with in proofs and does not have a problem with termination.