mutually recursive instances

Stream: lean4

[Gabriel DORIATH DÖHLER]

Given a typeclass myTC with one field f.
An instance for a recursive type T requires to define the field by structural induction on T.
So, we have to define an inductive function g separately and then use it to declare the instance (instance : myTC T where f := g).
Now, imagine that the body of g needs an instance myTC T' (where T' is another type) but to resolve myTC T', you need the instance of myTC T.
This might look like it doesn't terminate.
But, in my case, myTC T' uses the field f of the instance myTC T only for smaller values.
So, in theory, everything terminates.
The problem is that we have to define g before we can define the instance myTC T and we have to define the instance myTC T, in order to, define g (because of the recursive call).
Chicken and the egg problem...

There are 3 solutions:
1) Inline typeclass resolution in the body of g to replace the use of the instance by a recursive call to g. But sadly in my application this solution isn't appropriate.
2) Trick lean into replacing the recursive call generated by typeclass resolution by itself.
3) Modify typeclass resolution.
I would like to avoid solution 3.
Do you know how to implement the second idea? Or do you have any other solutions?

This situation is not made up. A solution would be really nice for my use case.

Here is an artificial example:
I would like to be able to write:

inductive T where
  | cons : Option (Prod Nat T) -> T
  | nil : T

inductive T' where
  | cons' : Option (Prod Nat T) -> T'

variable (a : Type u)
class myTC where
  f : a -> a

open myTC
open T
open T'

mutual

instance [I : myTC T] : myTC T' where
  f x := match x with
    | cons' none => cons' none
    | cons' (some (n, y)) => cons' (some (n, f y)) -- `f y` uses `I`

def g (x : T) : T := match x with
  -- x > y
  | cons y => match f (cons' y)  with -- Lean doesn't accept that.
    | cons' res => cons res
  /-
  Indeed, `f (cons' y)` requires the instance `myTC T'` which requires `myTC T`.
  But even with the mutual block, Lean doesn't to figure it out.
  In the case `y = none`, it works.
  In the case `y = some (n, z)`, x > z.
  And, `myTC T` is only needed to call `f z` which is defined as `g z`.
  So, my definition makes sense.
  -/
  | nil => nil

instance : myTC T where
  f := g

end

The solution one would be (but it isn't appropriate in my setting):

def g (x : T) : T := match x with
  -- We inline the result of typeclass resolution.
  | cons y => match (match cons' y with
    | cons' none => cons' none
    | cons' (some (n, z)) => cons' (some (n, g z))) -- `f` is replaced by `g` here.
    -- x = cons y = cons (cons' (some (n, z))) so, x > z.
    with
      | cons' res => cons res
  | nil => nil
  /- Lean isn't able to prove termination automatically because of the multiple wrapping and unwrapping.
  (Lean isn't able to prove x > z.)
  The termination is proved automatically when useless `cons'` are removed in the mattern matching. -/

instance : myTC T where
  f := g

Many thanks for reading this far :)

[Reid Barton]

If I turn your instances into defs and perform the instance synthesis manually (using f (self := [...])) then I get an error about "structural recursion does not handle mutually recursive functions". So I think that needs to be dealt with anyways.

[pcpthm]

I suggest to first define bare functions in a mutual block then define instances because extra wrapping in the class structure makes structural recursion inapplicable.

This works:

mutual
def f : T' → T'
| cons' none => cons' none
| cons' (some (n, y)) => cons' (some (n, g y))

def g : T → T
| cons y => match f (cons' y) with
  | cons' res => cons res
| nil => nil
end

instance : myTC T' := ⟨f⟩
instance : myTC T := ⟨g⟩

[Gabriel DORIATH DÖHLER]

Thank you very much for your answers! But, it doesn't work in my case because what you did is inlining the typeclass resolution.
In my case, I want to avoid that because the typeclass resolution might look something like that: myTC T needs myTC T' which needs my TC'' which needs myTC T''' which needs ... which needs myTC T (but the arguments are decreasing at recursive calls). I do not want to inline this by hand. But if a macro exists for that, it could be a solution. I do not want to write this macro myself because it would need to be kept in sync with the typeclass resolution algorithm.

[pcpthm]

I cannot imagine a situation where type class resolution is so complicated where it is not feasible to manually write that. Probably a #mwe is useful.

[Gabriel DORIATH DÖHLER]

Here is a minimal example (I didn't say small...).
The goal is to create a generic deriving framework.

• A type is represented by sums and products of units. This is done automatically from its definition by a macro.
• Instances for sums and products are given.
• They are then automatically combined and lifted to create an instance for any type that has a representation.

Here is an example for a binary operation typeclass and lists, but the mechanism has to remain general.
In particular, if instead of lists we used a recursive type that has a deeper functor, inlining by hand in painful.

universe u
variable (α β : Type u)

class Representation where
  to_repr : α → β
  from_repr : β → α
open Representation
open Sum (inl inr)
open Unit (unit)

-- This instance will be generated automatically from the definition of `List`.
-- List α ~ Sum Unit (Prod α (List α))
instance Representation.fromList : Representation (List α) (Sum Unit (Prod α (List α))) where
  to_repr x := match x with
    | [] => inl unit
    | h :: t => inr $ (h, t)
  from_repr x := match x with
    | inr (h, t) => h :: t
    | _ => []

-- A typeclass for binary operations.
class Binop where
  binop : α → α → α
open Binop

instance Binop.fromUnit : Binop Unit where
  binop _ _ := unit

instance Binop.fromProd [Binop α] [Binop β] : Binop (Prod α β) where
  binop a b := match a, b with
    | (x, y), (x', y') => (binop x x', binop y y')

instance Binop.fromSum [Binop α] [Binop β] : Binop (Sum α β) where
  binop a b := match a, b with
    | inl x, inl y => inl $ binop x y
    | inr x, inr y => inr $ binop x y
    | x, _ => x

-- Defining generic binop by lifting.
-- This will also be generated by macros from the typeclass definition.
def gbinop (β : Type u) [repr : Representation α β] [Binop β] (x : α) (y : α) : α :=
  @from_repr α β repr $ binop (to_repr x) (to_repr y)

-- This block would be generated by a macro from the representation type, the type and the typeclass.
mutual -- This block doesn't work.
def binopList : List α → List α → List α := @gbinop (List α) (Sum Unit (Prod α (List α))) _ _

instance Binop.ListT [Binop α] : Binop (List α) where
  binop := @gbinop _ (Sum Unit (Prod α (List α))) _ _
end

Intuitively, I define the Binop typeclass mutually for List α, Sum Unit (Prod α (List α)), and Prod α (List α).
I could define it using bare mutually recursive functions, as you proposed.
But, it would be long (and even more so if the functor is large) and writing a macro for it essentially reimplements typeclass resolution (because it cannot be hard coded for a particular datatype or typeclass).
I do not want to reimplement typeclass resolution, and would like to avoid having to modify it.

[Mario Carneiro]

Typeclass resolution constructs elements of structure types, by applying higher order functions of the form C α -> C (T α). Neither of those things plays well with mutual defs, which have to be function types and cannot call each other in a higher order way

[Mario Carneiro]

I would suggest you use W types explicitly in the repr macros, generating something like W (fun T => Sum Unit (Prod α T)) for the list type instead of an unfolding that still makes use of List A