Defining mutually recursive fixpoints as (definitional) type class instances

[ifazk]

Version

8.8.0

Operating system

Linux

Description of the problem

Defining mutually recursive fixpoints as instances of definitional/singleton type classes is a little awkward right now. The following is an example that illustrates the problem.

Inductive bexp : Set :=
  | b_true : bexp
  | b_false : bexp
  | b_eq : aexp -> aexp -> bexp
with aexp : Set :=
     | a_of_bool : bexp -> aexp.

Class ContainsFalse (A : Set) :=
  contains_false : A -> bool.

Fixpoint bexp_ContainsFalse (b : bexp) :=
  match b with
  | b_true => false
  | b_false => true
  | b_eq a1 a2 => orb
                   (@contains_false aexp aexp_ContainsFalse a1)
                   (@contains_false aexp aexp_ContainsFalse a2)
  end with
aexp_ContainsFalse (a : aexp) :=
  match a with
  | a_of_bool b => (@contains_false bexp bexp_ContainsFalse b)
  end.

Instance BexpContainsFalse : ContainsFalse bexp := bexp_ContainsFalse.
Instance AexpContainsFalse : ContainsFalse aexp := aexp_ContainsFalse.

In the above code there are two awkward patterns. Firstly, I had to manually pass implicit parameters to contains_false, since I couldn't declare the instances a priori. Secondly, I had to rebind bexp_ContainsFalse and aexp_ContainsFalse to BexpContainsFalse and AexpContainsFalse so that I could declare them as instances.

Ideally I should be able to define instances with something like the following:

Fixpoint BexpContainsFalse (b : bexp) :=
  match b with
  | b_true => false
  | b_false => true
  | b_eq a1 a2 => orb (contains_false a1) (contains_false a2)
  end with
AexpContainsFalse (a : aexp) :=
  match a with
  | a_of_bool b => (contains_false b)
  end
with Instance BexpContainsFalse : ContainsFalse bexp
with Instance AexpContainsFalse : ContainsFalse aexp.

Could we extend coq's syntax for Fixpoint or Instance to support recursive singleton instances?

[SkySkimmer]

I don't think this has to do with the mutual in "mutual fixpoints", ie with

Inductive bexp : Set :=
  | b_true : bexp
  | b_false : bexp
  | b_eq : bexp -> bexp -> bexp.

Class ContainsFalse (A : Set) :=
  contains_false : A -> bool.

Fixpoint bexp_ContainsFalse (b : bexp) :=
  match b with
  | b_true => false
  | b_false => true
  | b_eq a1 a2 => orb
                   (@contains_false bexp bexp_ContainsFalse a1)
                   (@contains_false bexp bexp_ContainsFalse a2)
  end.

Instance BexpContainsFalse : ContainsFalse bexp := bexp_ContainsFalse.

you have to do the same kind of thing.

The issue is that we can't use a folded type for Fixpoint,ie if we could do something like

Fixpoint bexp_CF : ConstainsFalse bexp := fun b =>
  match b with 
  | b_true => false
  | b_false => true
  | b_eq a1 a2 => orb (contains_false a1) (contains_false a2)
  end.
Existing Instance bexp_CF.

it would be fine. (with attributes we could combine the Fixpoint and Existing Instance but I don't know how soon that's coming)

[SkySkimmer]

I don't think this has to do with the mutual in "mutual fixpoints"

OTOH with a single fixpoint you can use Instance bla := fix ... without having to repeat the fix body.

[Blaisorblade]

I also keep running into this issue, so 👍 from me.

Firstly, I had to manually pass implicit parameters to contains_false, since I couldn't declare the instances a priori.

I also did that, but @amintimany taught me this slightly better workaround:

Fixpoint bexp_ContainsFalse (b : bexp) :=
  let a := aexp_ContainsFalse : ContainsFalse aexp in
  match b with
  | b_true => false
  | b_false => true
  | b_eq a1 a2 => orb
                   (contains_false a1)
                   (contains_false a2)
  end with
aexp_ContainsFalse (a : aexp) :=
  let b := bexp_ContainsFalse : ContainsFalse bexp in
  match a with
  | a_of_bool b => (contains_false b)
  end.

[Blaisorblade]

Let me bump this issue, in particular @SkySkimmer's proposal for folded fixpoints #7913 (comment). The downside of the current workarounds is that they require Instance foo : T := bar (e.g. Instance AexpContainsFalse : ContainsFalse aexp := aexp_ContainsFalse.), but foo and bar are syntactically different and have syntactically different types.

And apparently, sometimes they don't even unify, depending on which unification is used — in my case, this involved #6170, so simple apply worked, but not the builtin simple apply used by typeclass inference.

And you're easily exposed to the "unexpected" instance bar — say, when you simplify foo using cbn, recursive calls necessarily use bar.*

*While simpl fails with operational typeclasses: the output will sometimes unfold TC methods like @contains_false and call instances directly.

[JasonGross]

The downside of the current workarounds is that they require Instance foo : T := bar (e.g. Instance AexpContainsFalse : ContainsFalse aexp := aexp_ContainsFalse.), but foo and bar are syntactically different and have syntactically different types.

And you're easily exposed to the "unexpected" instance bar — say, when you simplify foo using cbn, recursive calls necessarily use bar.*

You can fix this issue with a bit of reduction:

Inductive bexp : Set :=
  | b_true : bexp
  | b_false : bexp
  | b_eq : aexp -> aexp -> bexp
with aexp : Set :=
     | a_of_bool : bexp -> aexp.

Class ContainsFalse (A : Set) :=
  contains_false : A -> bool.

Module Import internal.
Local Fixpoint bexp_ContainsFalse (b : bexp) :=
  let _ : ContainsFalse aexp := aexp_ContainsFalse in
  match b with
  | b_true => false
  | b_false => true
  | b_eq a1 a2 => orb
                   (contains_false a1)
                   (contains_false a2)
  end with
aexp_ContainsFalse (a : aexp) :=
  let _ : ContainsFalse bexp := bexp_ContainsFalse in
  match a with
  | a_of_bool b => (contains_false b)
  end.
End internal.

Definition bexp_ContainsFalse : ContainsFalse bexp
  := Eval cbv [internal.aexp_ContainsFalse internal.bexp_ContainsFalse] in internal.bexp_ContainsFalse.
Definition aexp_ContainsFalse : ContainsFalse aexp
  := Eval cbv [internal.aexp_ContainsFalse internal.bexp_ContainsFalse] in internal.aexp_ContainsFalse.
Existing Instances aexp_ContainsFalse bexp_ContainsFalse.
Goal forall x, bexp_ContainsFalse (b_eq (id a_of_bool b_false) (id a_of_bool b_false)) = x.
  Set Printing Implicit.
  cbn [bexp_ContainsFalse].
  (*   forall x : bool,
  (@contains_false aexp aexp_ContainsFalse (@id (bexp -> aexp) a_of_bool b_false)
   || @contains_false aexp aexp_ContainsFalse (@id (bexp -> aexp) a_of_bool b_false))%bool = x
 *)

[Blaisorblade]

Cool trick! That cbn refolds the body of aexp_ContainsFalse to a call to aexp_ContainsFalse itself is nothing short of amazing (and terrifying), even if I suspect that's how cbn/simpl always work for mutual fixpoints...

[herbelin]

Wish granted in #19296.