help with termination

Stream: lean4

[Simon Daniel]

Hi all,
im stuck with writing a function definition and maybe someone can help me out, it seems kinda straightforward, but the lean compiler rejects it as being non-computable and non terminating:)
I have a inductive representing datatypes (Ty) and another inductive that represents Types (Lty Θ). Lty Θ is either a datatype, anotated by a sublist of Θ, or a function type.
if Θ' ⊆Θ , then lift is a function that can map an Lty Θ' -> Lty Θ, because all type annotating lists must then also be sublists of Θ.
the denote functions map my types to lean types.
I should be able to define the function f, However i struggle with the .fn case.
I tried matching with α, but the compiler seems to complain.
I think the problem is the dependency of matching α and the goal (α.lift p').den

inductive Ty
| unit

-- Tys get annotated by subsets of Θ
inductive Lty (Θ: List Nat) where
| ty (α: Ty) (ns: List Nat) (p: ps ⊆ Θ)
| fn (a b: Lty Θ)

-- might be needed?
abbrev sizeLty {Θ} : Lty Θ → Nat
| .ty _ _ _ => 1
| .fn a b => 1 + sizeLty a + sizeLty b

abbrev Lty.lift {Θ Θ'} (p: Θ' ⊆ Θ): Lty Θ' -> Lty Θ
| ty α ns p' => .ty α ns (fun _ a => p (p' a))
| fn a b => .fn (a.lift p) (b.lift p)

def Ty.den: Ty -> Type
| .unit => Unit

def Lty.den (lt: Lty Θ) := match lt with
| ty α ps _p => (Θ ⊆ ps) -> α.den
| fn a b => a.den  -> b.den

--fail to show termination for f, show: False :(
def f {Θ Θ'} {p': Θ' ⊆ Θ} : (α: Lty Θ') -> (v: α.den) -> (α.lift p').den
| .ty a ns q, v =>
  fun h: Θ ⊆ ns =>
    v (fun x hx => h (p' hx))
| .fn a b, v =>
  fun x =>
    f (.fn a b) v x
-- ? termination_by α => sizeLty α

[Robin Arnez]

I mean yeah, it doesn't terminate, you defined f (.fn a b) v x = f (.fn a b) v x

[Simon Daniel]

ahh okay that should have been obvious... i was playing arround with the proof goal and happy that i found anything that typechecks :sweat_smile:
im still not sure what the right definition for f (.fn a b) v x should be

[Simon Daniel]

A colleague suggested to adjust Lty, then defining the function f was straightforward. (i still feel like it should have been possible with my original Lty inductive)

inductive Ty
| unit

-- Tys get annotated by subsets of Θ
inductive Lty : List Nat → Type where
| ty (α: Ty) (ps: List Nat) (p: ps ⊆ Θ) : Lty Θ
| fn (a : Lty Θ') (b : Lty Θ'') (h : Θ ⊆ Θ) (h' : Θ'' ⊆ Θ) : Lty Θ

def Ty.den: Ty -> Type
| .unit => Unit

def Lty.den (lt: Lty Θ) := match lt with
| ty α ps _p => (Θ ⊆ ps) -> α.den
| fn a b _c _d => a.den  -> b.den

abbrev Lty.lift {Θ Θ':List Nat} (p: Θ' ⊆ Θ): Lty Θ' -> Lty Θ
| .ty a ps p' => .ty a ps (fun _ a => p (p' a))
| .fn a b c d => .fn a b (by simp) (by grind)


def f {Θ Θ'} {p': Θ' ⊆ Θ}: (α: Lty Θ') -> (v: α.den) -> (α.lift p').den
| .ty a ps q, v =>
  fun h: Θ ⊆ ps =>
    v (fun x hx => h (p' hx))
| .fn _ _ _ _, v =>
  fun h => v h