Recursion with HList

Stream: Program verification

[Marcin Kostrzewa]

Hey! I'm trying to model a simple type with Lean and I'm stuck proving termination. I'm using the following definition of HList:

inductive HList {α : Type v} (β : α → Type u) : List α → Type (max u v) where
| nil : HList β []
| cons : ∀ {a : α} {as : List α}, β a → HList β as → HList β (a :: as)

and

inductive Tp
| nat
| bool
| fn : List Tp → Tp → Tp

def Tp.denote
| Tp.nat => Nat
| Tp.bool => Bool
| Tp.fn args result => HList denote args → denote result

for representation of Types. Tp.denote does not converge and I'm not even sure what measure to use for termination_by – everything I try gives me a free-variable-out-of-nowhere in the decreasing_by goal. FWIW it seems like HList is a red herring, a similar definition with a simple List.map:

def Tp.toList : Tp → List Tp
| Tp.nat => []
| Tp.bool => []
| Tp.fn args result => List.join (args.map toList)

fails similarly. What am I missing? Is there any way to get these kinds of definitions to work?

[Marcus Rossel]

I don't understand your definition of Tp.fn. Is it's argument supposed to be a function of type List Tp → Tp? Because in that case you would have to write | fn : (List Tp → Tp) → Tp. But that won't compile due to positivity constraints on inductive types.

[Marcin Kostrzewa]

No, fn is the non-dependent arrow type, not a pi type. The expected result of denote $ .fn [.nat, .bool] .nat is (isomorphic to) Nat × Bool -> Nat.

[Marcus Rossel]

Hmm, I'm also confused by the proof goal and error message:

inductive HList {α} (β : α → Type _) : List α → Type _ where
  | nil : HList β []
  | cons : ∀ {a : α} {as : List α}, β a → HList β as → HList β (a :: as)

inductive Tp where
  | nat
  | bool
  | fn : List Tp → Tp → Tp

def Tp.denote : Tp → Type _
  | .nat            => Nat
  | .bool           => Bool
  | .fn args result => (HList denote args) → denote result
  termination_by t => t    -- ^^^^^^
/-
failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
args: List Tp
result a✝: Tp
⊢ sizeOf a✝ < 1 + sizeOf args + sizeOf result
-/

def Tp.denote' : Tp → Type _
  | .nat            => Nat
  | .bool           => Bool
  | .fn args result => (HList denote' args) → denote' result
  termination_by structural t => t
/-
failed to infer structural recursion:
Cannot use parameter #1:
  unexpected occurrence of recursive application
    denote'
-/

[Marcus Rossel]

cc @Joachim Breitner

[Joachim Breitner]

HList is a higher order function, recursion through higher-order functions rarely works, because the termination checker cannot know that HList is applying its arguments only to elements of the list.

For well-founded recursion, using args.attach might help.

For structural recursion, if HList was a function, and not an inductive, you could try to use a mutual definition of TP.denote' and TP.denoteList' that essentially inlines HList.

[Joachim Breitner]

Well-founded recursion will not work here well if you want to use Tp.denote in types, as well-founded definitoins don't reduce well.

[Joachim Breitner]

Here is how I’d approach this:

inductive Tp where
  | nat
  | bool
  | fn : List Tp → Tp → Tp

mutual

def Tp.denote : Tp → Type
  | .nat            => Nat
  | .bool           => Bool
  | .fn args result => denoteArgs args → denote result
termination_by structural t => t

def Tp.denoteArgs : List Tp → Type
  | [] => Unit
  | a::args => denote a × denoteArgs args
termination_by structural ts => ts

end

example : (Tp.fn [.nat, .nat] .bool).denote =  (Nat × (Nat × Unit) → Bool) := rfl

[Marcin Kostrzewa]

Thank you so much! The biggest issue with HList as a def is that my terms have HList-typed fields and they don't compile with defined HLists. So I guess I'll have to juggle two different reps? Unless you have some idea if this can be made to compile (app is the issue, works fine with the inductive HList):

@[reducible]
def HList' (emb : α → Type) (ts : List α) : Type := match ts with
| [] => PUnit
| t :: ts => emb t × HList' emb ts

inductive Term (rep : Tp → Type) : Tp → Type where
| lam : (HList' rep paramTps → Term rep outTp) → Term rep (Tp.fn paramTps outTp)
| app : Term rep (Tp.fn args outTp) → HList' (Term rep) args → Term rep outTp

Also specifically thank you both for pointing out terminating_by structural – I've been on Lean 4.10, bumping 4.11 made many more definitions compile :D

[Joachim Breitner]

Yes, for Term I think inductive HList is your only option. Lean does not support nested inductives through defs