Fonctions Fixpoint dans les instances de classe de type

Question

J'essaie d'utiliser une fonction de style point de repère dans le contexte d'une instance de classe de type, mais cela ne semble pas fonctionner. Y a-t-il quelque chose de plus que je dois faire pour que cela fonctionne? Pour l'instant, j'ai utilisé un hack pour déplacer la fonction en dehors de la classe de type et la déclarer explicitement Fixpoint. Cela semble horrible, cependant.

Voici l'exemple court:

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 
    }. 

Cela échoue avec:

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

?Propable : "Propable cexp" 

Que doit-on faire pour faire ce travail?

Answer 1

Vous pouvez utiliser fix pour le faire:

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 
    }. 

Permettez-moi d'illustrer comment on peut venir avec elle. Prenons le morceau de code suivant:

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

Fixpoint ici est une commande vernaculaire qui rend la définition un peu plus facile sur les yeux, mais il cache ce qui se passe ici. Il se trouve que ce Coq ne fait quelque chose comme ceci:

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

Vous pouvez le vérifier en utilisant Print silly. après la définition.