Coq: 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
~~~coq
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
~coq
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 https://github.com/coq/coq/issues/7913#issuecomment-399866519. 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.