Unexpected definition of `mrec_fix`

[Mbodin]

I find the current definition of mrec_fix quite surprising: https://github.com/DeepSpec/InteractionTrees/blob/master/theories/Interp/Recursion.v#L103 It has two parameters A and B that are unused. Furthermore the notation mrec-fix defined below is putting a wildcard for the type T, which is typically needed for mutually recursive definitions.

Here is a proof script to illustrate my point.

The definition odd_even_1 is made using mrec and works. Note the importance of using the argument T (which why I was so surprised to find a wildcard in mrec-fix).

The natural definition odd_even_2 is failing because of the wildcard. The definition odd_even_3 suggests a fix.

From ITree Require Import ITree ITreeFacts.

Inductive odd_evenE : Type -> Type :=
  | odd : nat -> odd_evenE bool
  | even : nat -> odd_evenE bool
  .

Definition odd_even_1 : odd_evenE ~> itree void1 :=
  mrec (fun T (d : odd_evenE T) =>
    match d with
    | odd 0 => ret false
    | odd (S m) => trigger (even m)
    | even 0 => ret true
    | even (S m) => trigger (odd m)
    end).

Fail Definition odd_even_2 : odd_evenE ~> itree void1 :=
  mrec-fix odd_even d :=
    match d in odd_evenE T return itree (odd_evenE +' void1) T with
    | odd 0 => ret false
    | odd (S m) => odd_even _ (even m)
    | even 0 => ret true
    | even (S m) => odd_even _ (odd m)
    end.

Local Notation endo T := (T -> T).

Definition mrec_fix2 {D E : Type -> Type}
           (ctx : endo (D ~> itree (D +' E)))
  : D ~> itree E
  := mrec (ctx trigger_inl1).

Notation "'mrec-fix2' f d := g" :=
  (let D := _ in
   mrec_fix2 (D := D) (fun (f : forall T, D T -> _) T (d : D T) => g))
  (at level 200, f ident, d pattern).

Definition odd_even_3 : odd_evenE ~> itree void1 :=
  mrec-fix2 odd_even d :=
    match d in odd_evenE T return itree (odd_evenE +' void1) T with
    | odd 0 => ret false
    | odd (S m) => odd_even _ (even m)
    | even 0 => ret true
    | even (S m) => odd_even _ (odd m)
    end.

[Lysxia]

Rather than the wildcard, it seems the trouble comes from inferring the event type D for the "mutually recursive" events. Maybe it should be annotated explicitly? That would avoid the let trick...

[Mbodin]

I agree that annotating D explicitly in the notation feels like a good idea. It may also prevent the in odd_evenE T return itree (odd_evenE +' void1) T pattern-matching annotation.

I also think that it would be worth instantiating the mrec-fix notation for some specific numbers of mutually recursive functions. rec-fix is already an instance for one function, using the callE construct. I think that it would also make sense to define a rec-fix f x := f_body with g y := g_body notation, based on a call2E or something like that: defining two function mutually recursive is a very common use-case. What do you think?

[Lysxia]

That sounds great! I'm definitely in favor of all of that. I would welcome a PR for it :)