CODEWITHSUNDEEP
typeclasscoq
jsinglet
jsinglet

Reputation: 1151

Fixpoint functions in Type Class Instances

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?

Upvotes: 1

Views: 70

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15424

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.

Upvotes: 2

Related Questions