proving mutual dependent termination

Stream: new members

[Simon Daniel]

Hello, Im trying to write a Free Monad (hope its the correct term) that captures a certain sequence of effects.

mutual
  inductive Eff:  Type -> Type 1 where
  | A :  Eff Unit

  inductive M: Type -> Type 1  where
  | Do :  Eff b -> (b -> M a) -> M a
  | Return: a -> M a
end

def M.bind: M α → (α → M β) → M β
  | M.Do eff next, next' => M.Do eff (fun x => bind (next x) next')
  | M.Return v, next' => next' v
-- cannot defer termination

mutual
  def Eff.fn: Eff a -> a
  | Eff.A => ()

  def M.fn: M a -> a
  | M.Return v => v
  | M.Do eff next =>
    M.fn (next eff.fn)
  -- cannot defer termination
end

the inductive M represents the Sequence structure while Eff is a inductive listing all my effects. When not using mutual, Lean can figure out termination by itself, but how can I do it with Mutual? I could stuff M and Eff into one big inductive but the code gets kinda messy

[Arthur Adjedj]

This sort of code relies heavily on structural recursion: it's much easier to write such functions using recursors than it is to find a well-behaved measure to do well-founded recursion over. The issue is that Lean doesn't know how to check for structural recursion over mutual inductive types. In your case, it means that it tries to do well-founded recursion over your functions, but fails because of this.

[Simon Daniel]

im hearing the term "recursors" for the first time, i noticed that lean fails to check structural recursion for mutual inductive types (probalby because its hard?)
only solution i came up with is combining both inductives into

inductive M: Type -> Type 1  where
| Do_A :  M Unit -> (Unit -> M a) -> M a
| Do_B :  M Nat -> (Nat -> M a) -> M a
-- possibly many effects
| Return: a -> M a

which should be equivalent but more messy, ill look up recursors