CODEWITHSUNDEEP
formal-verificationlean
redjamjar
redjamjar

Reputation: 771

Termination for Wrapped `Fin n` in Lean4

The following example type checks in Lean 4, but I am confused why the termination_by declaration is required.

import Mathlib.Tactic.Linarith

def Idx (n:Nat) := Fin n

def sum(k:Idx n) : Nat :=
  if p:k.val=0 then 0
  else
    have p : k.val-1 < k.val := (Nat.pred_lt p);
    let km1 : Idx n := {val:=k.val-1,isLt:=(by linarith [k.isLt])};
    1+(sum km1)
  termination_by sum k => k.val

Specifically, a very similar example does not require it:

def sum2(k:Fin n) : Nat :=
  if p:k.val=0 then 0
  else
    have p : k.val-1 < k.val := (Nat.pred_lt p);
    let km1 : Fin n := {val:=k.val-1,isLt:=(by linarith [k.isLt])};
    1+(sum2 km1)

Obviously, it has something to do with the fact that I've wrapped the Fin n with Idx n. I tried adding a @[simp] annotation, but that didn't help.

(also am interested in whether the example can be improved)

Upvotes: 3

Views: 93

Answers (1)

Joachim Breitner
Joachim Breitner

Reputation: 25782

The problem is that by writing

def Idx (n:Nat) := Fin n

that type class search won’t find instances for Idx that it would find for Fin, in particular not the SizeOf instance used for recursion.

As @jthulhu mentioned, using abbrev is the appropriate fix for this.

Upvotes: 1

Related Questions