How to recurse over a general inductive type?

Stream: general

[nrs]

Consider the following mutually recursive type, which stands for a general inductive type:

structure Signature where
  symbols : Type
  arity : symbols -> Nat

mutual
  inductive W_Aux_Vect (sig : Signature) : Nat -> Type _
  | nil : W_Aux_Vect sig 0
  | cons : W sig -> W_Aux_Vect sig n -> W_Aux_Vect sig (n + 1)

  inductive W_Aux_Ext (sig : Signature)
  | mk : (s : sig.symbols) -> W_Aux_Vect sig (sig.arity s) -> W_Aux_Ext sig

  inductive W (sig : Signature)
  | sup : W_Aux_Ext sig -> W sig
end

It should be more or less clear that if sig.symbols is Empty or there is no s : sig.symbols such that sig.arity s = 0, then W sig is empty. So assuming W sig avoids both of these conditions, is there any way to traverse this type without more information? for instance a super simple W sig -> Unit function that either returns unit if W sig is a bottom node (i.e. it is made from an W_Aux_Ext whose (s : sig.symbols) has sig.arity s = 0), or keeps recursing until it finds one. All attempts of mine to do this have failed due to there being metavariables at the time to recurse, so I've been investigating how brecOn works to see if using it might offer a way forward.

[nrs]

figured it out, here's an implementation of sizeOf that works for the W corresponding to Nat, but don't know yet if we can state things about arbitrary W

def NatSig : Signature := ⟨Fin2 2, fun | .fz => 0 | .fs .fz => 1⟩

compile_inductive% W

def mkNatW : Nat -> W NatSig
| .zero => ⟨.fz, .nil⟩
| .succ n => ⟨.fs .fz, .cons (mkNatW n) .nil⟩

def NatWsizeOf (mainw : W sig) : Nat :=
  @W.rec
    sig
    (fun _ _ => Nat)
    (fun _ => Nat)
    (fun _ => Nat)
    (0 : Nat)
    (fun w vec motw motvec => (1 + motw : Nat))
    (fun s vec motvec => (motvec : Nat))
    (fun ext motext => (motext : Nat ))
  mainw

#eval W.sizeOf (mkNatW 10) -- 10

edit: adding motvec to 1 + motw might give a size function for an arbitrary W?

[Frederick Pu]

what's Fin2

[Frederick Pu]

id say a good general approach would be to just write the function naturally using pattern matching and then prove termination_by using sizeOf

[Frederick Pu]

see: #general > trying to define sizes of trees @ 💬
for more info