How to prove termination when mapping over a list?

Stream: Is there code for X?

[Atticus Kuhn]

I'm trying to prove the semantics of a language that has record/product types, so I have the following code:

inductive Ty : Type where
  | bool : Ty
  | record : (List Ty) → Ty
  | string : Ty
  | int :  Ty

inductive HList {α : Type} (β : α → Type) : List α → Type where
  | nil : HList β []
  | cons {x xs} : β x → HList β xs → HList β (x :: xs)

@[reducible, simp]
def Ty.denote (t : Ty) : Type :=
  match t with
  | .bool => Bool
  | .int => Int
  | .string => String
  | .record l => HList Ty.denote l

This gives the error:

termiation.lean:11:2
failed to set reducibility status, `denote` is not a definition

Note: Use `set_option allowUnsafeReducibility true` to override reducibility status validation
termiation.lean:11:13
Cannot add `simp` attribute to `denote`: It is not a proposition nor a definition (to unfold)

Note: The `[simp]` attribute can be added to lemmas that should be automatically used by the simplifier and to definitions that the simplifier should automatically unfold
termiation.lean:12:4
fail to show termination for
  Ty.denote
with errors
failed to infer structural recursion:
Cannot use parameter t:
  unexpected occurrence of recursive application
    denote


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
l : List Ty
t : Ty
⊢ sizeOf t < 1 + sizeOf l

I tried to prove this program is decreasing with:

inductive Ty : Type where
  | bool : Ty
  | record : (List Ty) → Ty
  | string : Ty
  | int :  Ty

inductive HList {α : Type} (β : α → Type) : List α → Type where
  | nil : HList β []
  | cons {x xs} : β x → HList β xs → HList β (x :: xs)

@[reducible, simp]
def Ty.denote (t : Ty) : Type :=
  match t with
  | .bool => Bool
  | .int => Int
  | .string => String
  | .record l => HList Ty.denote l
decreasing_by
  simp
  sorry

This requires the proof goal

Tactic state
1 goal
l : List Ty
t : Ty
⊢ sizeOf t < 1 + sizeOf l

As far as I understand this, l is a list and t is an element of l. Thus, this should be provable, but how can I ensure that Lean accepts this function?

[Robin Arnez]

It isn't very pretty but HList (fun ⟨x, _⟩ => Ty.denote x) l.attach (note that this is a different type though!) The problem with HList Ty.denote l is that Ty.denote is provided in such a way that it might be called with any value, not just the ones in l.

[Atticus Kuhn]

Robin Arnez said:

The problem with HList Ty.denote l is that Ty.denote is provided in such a way that it might be called with any value, not just the ones in l.

What do you mean by this? I thought that t was an element of l. My intuition is that HList is like a type-level map, so it should map over each element. How could Ty.denote be called on an element not in l?

[Atticus Kuhn]

Is there any way to disable the termination checker in Lean? Or is there any downside to marking all definitions in a project as unsafe?

[Aaron Liu]

my solution (inspired by docs#List.TProd)

inductive Ty : Type where
  | bool : Ty
  | record : (List Ty) → Ty
  | string : Ty
  | int :  Ty

-- inductive HList {α : Type} (β : α → Type) : List α → Type where
--   | nil : HList β []
--   | cons {x xs} : β x → HList β xs → HList β (x :: xs)

@[reducible, simp]
def Ty.denote (t : Ty) : Type :=
  match t with
  | .bool => Bool
  | .int => Int
  | .string => String
  | .record l => Ty.denoteList l
where
  @[reducible, simp]
  Ty.denoteList (t : List Ty) : Type :=
    match t with
    | [] => Unit
    | x :: xs => Ty.denote x × Ty.denoteList xs

[Aaron Liu]

Atticus Kuhn said:

Robin Arnez said:

The problem with HList Ty.denote l is that Ty.denote is provided in such a way that it might be called with any value, not just the ones in l.

What do you mean by this? I thought that t was an element of l. My intuition is that HList is like a type-level map, so it should map over each element. How could Ty.denote be called on an element not in l?

well HList could be something weird like

#check fun {α : Type} (β : α → Type) (l : List α) => open Classical in if ∀ x ∉ l, Nonempty (β x) then Nat else l.head?.elim Empty β

which depends on stuff not in l and the termination checker only really sees its type and this has the same type