termination_by case wise

Stream: general

[Bhakti Shah]

This is probably really dumb but i've been confused for a bit: I have two mutually recursive functions and i need to specify termination. The structure is something like

mutual
def outer (a : Expr) : Except A B := match a with
| C1 m => -- not a recursive call
| C2 m => do
let x <- outer m
ok x
| C3 m => do -- m : List Expr
let x <- inner m
ok x
... variations of the three

def inner (a : List Expr) : Except A C :=
if a == [] then ok []
else do
let h <- outer a.head
let t <- inner a.tail
ok head :: tail

proving termination for inner is simple as List.length a is decreasing.
the only way i can think of proving termination for outer is by pattern matching on each Expr constructor. for constructors with an argument that is a collection type the decreasing size seems simple enough.
this is the dumb part of the question but how do i prove termination for constructors matching the structure ofC1, that is, no recursive calls? It seems intuitive that hitting that case means terminating right away because we just return immediately but i have no idea how to say something is actually decreasing. I'm assuming the termination checker doesn't usually complain about this case but if i'm doing a match statement in the termination_by clause i need to specify a relation for each arm.
this is the slightly less dumb part but how do i prove termination for a C2 type? in my head it's just if the internal call to outer terminates then that arm terminates but i'm not sure how to specify that.

thank you :)

[Mario Carneiro]

@Bhakti Shah Could you make a #mwe?

[Mario Carneiro]

It sounds to me like this is an induction on sizeOf

[Mario Carneiro]

which is also the default

[Mario Carneiro]

but it would probably simplify the termination proof significantly if you used pattern matching in inner instead of if-else

[Mario Carneiro]

def inner (a : List Expr) : Except A C :=
match a with
| [] => ok []
| h :: t => do ok (<- outer h) :: (<- inner t)

[Bhakti Shah]

sorry about that, here's an mwe:

inductive Expr where
| C1 (m : Nat)
| C2 (m : Expr)
| C3 (m : List Expr)
deriving instance Inhabited for Expr

mutual
  def outer (a : Expr) : Except Bool Nat := match a with
  | .C1 m => .error false
  | .C2 m => do
  let x <- outer m
  .ok x
  | .C3 m => do
  let x <- inner m
  .ok x[0]!

  def inner (a : List Expr) : Except Bool (List Nat) :=
  match a with
  | [] => .ok []
  | _ => do
  .ok ((<- outer a[0]!) :: (<- inner a.tail!))
end
termination_by
outer a => match a with
| .C1 m => sizeOf m
| .C2 m => sizeOf m
| .C3 m => List.length m
inner a => List.length a

This is a far simpler case than what I have but I can't prove termination on this either. I'm not sure if I'm using sizeOf correctly, though

I guess I understand why it's refusing to accept termination (the C2 case), but I'm not sure how to do it (or even if it can be done) in a case where you have something like this.

[Sebastian Ullrich]

As Mario said, this is an induction on sizeOf, at least if you correctly match on the list in inner

mutual
  def outer (a : Expr) : Except Bool Nat := match a with
  | .C1 m => .error false
  | .C2 m => do
  let x <- outer m
  .ok x
  | .C3 m => do
  let x <- inner m
  .ok x[0]!

  def inner (a : List Expr) : Except Bool (List Nat) :=
  match a with
  | [] => .ok []
  | x::xs => do
  .ok ((<- outer x) :: (<- inner xs))
end

[Bhakti Shah]

that does in fact seem to work for this simple case, though not for the more complex one I have. I'll try to mess with the pattern matching a bit more before i ask about that, though. Thank you!
[edit: It was in fact just a matter of switching out a couple other head and tail instances :)]