Help with inductive family

Stream: new members

[Jesse Slater]

I am looking for some design advice about using inductive families.

I have a mathematical structure like this: A binary tree where each node has two children l and r, an associated finite type T, and an associated function f : ( Sum T (Sum l.T r.T ) -> Nat. For a leaf node T is Empty.

I will use this structure in computation, and also prove things about it.

I already have a working version of my computation, based on a representation which does not enforce much of the mathematical structure in the type system.
I currently just define a tree as Sigma (numNodes : Nat), Sigma (m : Nat), Fin numNodes -> Fin m -> Nat where m is the length of all the Ts of the tree appended together, and the values of each function are zero for all of the values of Fin m that they should not be able to see.

This works fine, but I would like to build more of the tree structure into Lean's type system. The properties I want to prove depend on the fact that the function associated with each node is 0 for all m not in T or T.l or T.r, so my proof has to include a whole lot of extra stuff about ensuring indicies are correct. If I could embed the structure of my tree in the type system, I would not have to worry about this.

(Please ask for clarification if any of that was unclear. What I say there leaves out a lot of detail, since I am trying to give the minimum context required to get a good answer. However, I may have left out too much detail.)

I am trying to represent my tree with an inductive family (this may be the wrong approach). Here is what I have:

instance
  {α β γ : Type}
  [Repr (α → γ)]
  [Repr (β → γ)] : Repr (α ⊕ β → γ) where
   reprPrec f _ :=
    let l : α → γ :=
      λ a => f (Sum.inl a)
    let r : β → γ :=
      λ b => f (Sum.inr b)
    "(" ++ repr l ++ " ⊕ " ++ repr r ++ ")"

inductive _Tree : (s : Nat) → Type where
  | nil :
    _Tree 0
  | ind
    (l : _Tree j)
    (r : _Tree k)
    (f : Fin s ⊕ Fin j ⊕ Fin k → Nat)
    : _Tree s
    deriving Repr

def _nil := _Tree.nil

def _ind := _Tree.ind _nil _nil
  (λ| .inl 0 => 1
    | .inl 1 => 2
    | _ => 0
    : Fin 2 ⊕ Fin 0 ⊕ Fin 0 → Nat)

def _ind' := _Tree.ind _ind _ind
  (λ| .inl 2 => 3
    | .inr (.inr 1) => 1
    | .inr (.inl 1) => 2
    | _ => 0
    : Fin 3 ⊕ Fin 2 ⊕ Fin 2 → Nat)

#eval _ind'

This all seems to work, and _ind' is what I am hoping to see. However, I am having trouble defining a function on _Tree.

Here is my attempt to define a function which takes my new inductive family representation, and converts it back to my old representation (which is something I will want to be able to do).

def flatten (f : _Tree s) : Σ numNodes : Nat, Σ n : Nat, Fin numNodes → Fin n → Nat :=
  match f with
  | _Tree.nil => ⟨0, 0, λ _ _ => 0⟩
  | _Tree.ind l r f =>
    let ⟨lnodes, ln, lf⟩ := flatten l
    let ⟨rnodes, rn, rf⟩ := flatten r
    ⟨ 1 + lnodes + rnodes,
      s + ln + rn,
      λ j k =>
        let j' :=
          finSumFinEquiv.invFun (Fin.cast (Nat.add_assoc 1 lnodes rnodes) j)
          |> Sum.map id finSumFinEquiv.invFun
        let k' :=
          finSumFinEquiv.invFun (Fin.cast (Nat.add_assoc s ln rn) k)
          |> Sum.map id finSumFinEquiv.invFun
        match j', k' with
        | .inl 0, .inl s' =>
          f (.inl s')
        | .inl 0, .inr (.inl ln') =>
          if ln' < ⟨0, sorry⟩ -- ln' < j✝
          then f (.inr (.inl (Fin.cast sorry ln')))
          else 0
        | .inl 0, .inr (.inr rn') =>
          if rn' < ⟨0, sorry⟩ -- rn' < k✝
          then f (.inr (.inr (Fin.cast sorry rn')))
          else 0
        | .inr (.inl lnodes'), .inr (.inl ln') =>
          lf lnodes' ln'
        | .inr (.inr rnodes'), .inr (.inr rn') =>
          rf rnodes' rn'
        | _, _ => 0
      ⟩

The second two cases of the second match are giving me trouble. Those cases handle the fact that a node can see the Ts associated with it's two child nodes. Where I have ln' < 0, what it should say is ln' is less than ls, where the left child has type _Tree ls. Currently, the info view tells me that the left child has type _Tree j✝. I don't know how to name j✝ to get access to it, or if that is possible.

Is my problem clear? Please ask for follow up clarification if not.

Is there some easy solution that I am missing, or is this approach to representing my tree with an inductive family fundamentally misguided?

[Jesse Slater]

Ok, I seem to have gotten it working. I just needed to name j✝ and k✝ by disabling implicit arguments of _Tree.ind.

def flatten (t : _Tree s) : Σ numNodes : Nat, Σ n : Nat, Fin numNodes → Fin n → Nat :=
  match t with
  | _Tree.nil => ⟨0, 0, λ _ _ => 0⟩
  | @_Tree.ind ls rs _ l r f =>
    let ⟨lnodes, ln, lf⟩ := flatten l
    let ⟨rnodes, rn, rf⟩ := flatten r
    ⟨ 1 + lnodes + rnodes,
      s + ln + rn,
      λ j k =>
        let j' :=
          finSumFinEquiv.invFun (Fin.cast (Nat.add_assoc 1 lnodes rnodes) j)
          |> Sum.map id finSumFinEquiv.invFun
        let k' :=
          finSumFinEquiv.invFun (Fin.cast (Nat.add_assoc s ln rn) k)
          |> Sum.map id finSumFinEquiv.invFun
        match j', k' with
        | .inl 0, .inl s' =>
          f (.inl s')
        | .inl 0, .inr (.inl ln') =>
          if h : ln' < ls -- ln' < j✝
          then f (.inr (.inl (Fin.castLT ln' h)))
          else 0
        | .inl 0, .inr (.inr rn') =>
          if h : rn' < rs -- rn' < k✝
          then f (.inr (.inr (Fin.castLT rn' h)))
          else 0
        | .inr (.inl lnodes'), .inr (.inl ln') =>
          lf lnodes' ln'
        | .inr (.inr rnodes'), .inr (.inr rn') =>
          rf rnodes' rn'
        | _, _ => 0
      ⟩

#eval flatten _ind'

This seems to work how I would expect.

I would still like design advice. Is this a good way to represent this structure? Are there any problems I am going to run into when I try to prove things about this representation?

[Jesse Slater]

Also, I am a bit concerned that there is something I am not understanding. What is the difference between these two definitions?

def flatten (t : _Tree s) : Σ numNodes : Nat, Σ n : Nat, Fin numNodes → Fin n → Nat :=
  match t with
  | _Tree.nil => ⟨0, 0, λ _ _ => 0⟩
  | @_Tree.ind ls rs _ l r f =>
    let ⟨lnodes, ln, lf⟩ := flatten l
    let ⟨rnodes, rn, rf⟩ := flatten r
    ⟨ 1 + lnodes + rnodes,
      s + ln + rn,
      λ j k =>
        let j' :=
          finSumFinEquiv.invFun (Fin.cast (Nat.add_assoc 1 lnodes rnodes) j)
          |> Sum.map id finSumFinEquiv.invFun
        let k' :=
          finSumFinEquiv.invFun (Fin.cast (Nat.add_assoc s ln rn) k)
          |> Sum.map id finSumFinEquiv.invFun
        match j', k' with
        | .inl 0, .inl s' =>
          f (.inl s')
        | .inl 0, .inr (.inl ln') =>
          if h : ln' < ls -- ln' < j✝
          then f (.inr (.inl (Fin.castLT ln' h)))
          else 0
        | .inl 0, .inr (.inr rn') =>
          if h : rn' < rs -- rn' < k✝
          then f (.inr (.inr (Fin.castLT rn' h)))
          else 0
        | .inr (.inl lnodes'), .inr (.inl ln') =>
          lf lnodes' ln'
        | .inr (.inr rnodes'), .inr (.inr rn') =>
          rf rnodes' rn'
        | _, _ => 0
      ⟩

def flatten' (t : _Tree __) : Σ numNodes : Nat, Σ n : Nat, Fin numNodes → Fin n → Nat :=
  match t with
  | _Tree.nil => ⟨0, 0, λ _ _ => 0⟩
  | @_Tree.ind ls rs s l r f =>
    let ⟨lnodes, ln, lf⟩ := flatten l
    let ⟨rnodes, rn, rf⟩ := flatten r
    ⟨ 1 + lnodes + rnodes,
      s + ln + rn,
      λ j k =>
        let j' :=
          finSumFinEquiv.invFun (Fin.cast (Nat.add_assoc 1 lnodes rnodes) j)
          |> Sum.map id finSumFinEquiv.invFun
        let k' :=
          finSumFinEquiv.invFun (Fin.cast (Nat.add_assoc s ln rn) k)
          |> Sum.map id finSumFinEquiv.invFun
        match j', k' with
        | .inl 0, .inl s' =>
          f (.inl s')
        | .inl 0, .inr (.inl ln') =>
          if h : ln' < ls -- ln' < j✝
          then f (.inr (.inl (Fin.castLT ln' h)))
          else 0
        | .inl 0, .inr (.inr rn') =>
          if h : rn' < rs -- rn' < k✝
          then f (.inr (.inr (Fin.castLT rn' h)))
          else 0
        | .inr (.inl lnodes'), .inr (.inl ln') =>
          lf lnodes' ln'
        | .inr (.inr rnodes'), .inr (.inr rn') =>
          rf rnodes' rn'
        | _, _ => 0
      ⟩
#eval flatten _ind'
#eval flatten' _ind'

They appear to do the same thing. Does it change anything that I name s in different places? I feel like I am missing something about how inductive families work.