Fixpoint functions in Type Class Instances

Question

I am trying to use a fixpoint style function in the context of a type class instance but it doesn't seem to work. Is there something extra I have to do to make this work? For the time being I've used a hack of moving the function outside the type class and explicitly declaring it Fixpoint. This seems awful, however.

Here's the short example:

Inductive cexp : Type :=
| CAnd :  cexp -> cexp -> cexp
| COr  :  cexp -> cexp -> cexp
| CProp : bool -> cexp.  

Class Propable ( A : Type ) := { compile : A -> Prop }.

Instance: Propable cexp :=
  { compile c :=
      match c with
      | CAnd x y => (compile x) /\ (compile y)
      | COr x y => (compile x) \/ (compile y)
      | CProp _ => False
      end
  }.

This fails with:

Error: Unable to satisfy the following constraints:
In environment:
c, x, y : cexp

?Propable : "Propable cexp"

What does one have to do to make this work?

score 2 · Accepted Answer · answered Jun 19 '17 at 06:09

2

You can use fix to do that:

Instance: Propable cexp :=
  { compile := fix compile c :=
      match c with
      | CAnd x y => (compile x) /\ (compile y)
      | COr x y => (compile x) \/ (compile y)
      | CProp _ => False
      end
  }.

Let me illustrate how one can come up with it. Let's take the following piece of code:

Fixpoint silly n :=
  match n with
  | 0 => 0
  | S n => silly n
  end.

Fixpoint here is a vernacular command which makes the definition a little bit easier on the eyes, but it conceals what is going on here. It turns out that what Coq actually does is something like this:

Definition silly' :=
  fix self n :=
    match n with
    | 0 => 0
    | S n => self n
    end.

You can verify it by using Print silly. after the definition.

answered Jun 19 '17 at 06:09

Anton Trunov

15,074
2
23
43

this works, however I am noticing that when I apply the "simpl" tactic, I get a huge unruly fix point definition instead of just a simple formula with identifiers. Is there a way to tell Coq to cook up better looking identifiers rather than printing the entire function inline? – jsinglet Jun 19 '17 at 21:08
This is a frequent issue. These questions might provide some insight: [1](https://stackoverflow.com/q/39355817/2747511), [2](https://stackoverflow.com/q/28432187/2747511), [3](https://stackoverflow.com/q/41404337/2747511). `fold` may help (but rarely does), maybe you need a better control on where the reduction happens. If those won't help, send me a link to the actual code -- I'll try to look into it. – Anton Trunov Jun 20 '17 at 08:51

Fixpoint functions in Type Class Instances

1 Answers1