Coq: Problème avec correspondance de motif dépendant

Question

Je me demande s'il est possible de retirer cette correspondance de motif dépendant. Comme vous le voyez, j'essaie de mapper plusieurs valeurs à nul (et d'indiquer à la sortie d'avoir le type requis avec une clause return). Type N est un éboueur, je suis tout simplement essayer de se débarrasser de toutes les valeurs après

| P, c => phy 
| P, b => phy 
| Ii, b => inf 

(Dans ce contexte particulier, en utilisant un type option semblait très difficile à manier.) Notez que si Coercion est impossible ici, Je serais aussi heureux w/Definition

Inductive R := P | Ii | S | N. 
Parameter rp:> R -> Prop. 
Inductive X: Type := | c {z:P} :> X | b {z:P} {y:Ii} :> X. 
Parameter (phy:P) (inf:Ii) (sen:S) (nul:N). 

Check phy: id P. 
Fail Coercion xi(y:R)(x:X): id y := match y, x with 
| P, c => phy 
| P, b => phy 
| Ii, b => inf 
| _, _ => match _ return N with _ => nul end end. 
(* The term "nul" has type "rp N" while it is expected to have type "rp Ii". *) 

Answer 1

Une solution plus courte w/a définition renvoyant un « match »:

Inductive R := P | Ii | S | N. Fail Check N: Type. 
Parameter rp:> R -> Prop. Check N: Type. 
Inductive X: Type := | c {z:P} :> X | b {z:P} {y:Ii} :> X. 
Parameter (phy:P) (inf:Ii) (sen:S) (nul:N). 

Definition xi (y:R) := match y return (match y with (P|Ii) => y | _ => N end) with 
    | P => phy 
    | Ii => inf 
    | _ => nul end. 

Eval hnf in xi S. (* = nul *) 

trouvé l'idée here

Answer 2

Vous dites: « Je suis tout simplement essayer de se débarrasser de toutes les valeurs après ... », et je suis un peu inquiet d'avoir plusieurs valeurs par défaut sans caractéristiques distinctives, et je soupçonne que votre code ne fera pas ce que vous pensez qu'il va, mais vous pouvez le faire:

Inductive R := P | Ii | S | N. 
Parameter rp:> R -> Prop. 
Inductive X: Type := | c {z:P} :> X | b {z:P} {y:Ii} :> X. 
Parameter (phy:P) (inf:Ii) (sen:S) (nul:N). 

Check phy: id P. 
Definition xi(y:R)(x:X): id y 
    := match y, x with 
    | P, c => phy 
    | P, b => phy 
    | Ii, b => inf 
    | Ii, _ => inf 
    | S, _ => sen 
    | N, _ => nul 
    end. 

Notez que vous pouvez aussi bien faire:

Definition xi(y:R)(x:X): id y 
    := match y with 
    | P => phy 
    | Ii => inf 
    | S => sen 
    | N => nul 
    end. 

Vous ne pouvez pas faire une contrainte parce qu'il n'y a aucun moyen de déduire y de x.

---

Si ce que vous aimez sont les valeurs, plutôt que les types, vous pouvez utiliser les types dépendants pour obtenir le type de retour que vous voulez dans chaque cas:

Inductive R := P | Ii | S | N. 
Parameter rp:> R -> Prop. 
Inductive X: Type := | c {z:P} :> X | b {z:P} {y:Ii} :> X. 
Parameter (phy:P) (inf:Ii) (sen:S) (nul:N). 

Check phy: id P. 
Definition xi_type(y:R)(x:X) 
    := match y, x return Type with 
    | P, c 
    | P, b 
    | Ii, b 
     => y 
    | _, _ 
     => N 
    end. 
Definition xi(y:R)(x:X): xi_type y x 
    := match y, x return xi_type y x with 
    | P, c => phy 
    | P, b => phy 
    | Ii, b => inf 
    | _, _ => nul 
    end.