Coq: Définition d'une fonction par appariement de motif sur l'arité de son argument

Question

Je souhaite définir une fonction dont le comportement dépend de son argument (au moins) d'une fonction n-place. Un rudimentaire (échec) tentative

Definition rT {y:Type}(x:y) := ltac: (match y with 
| _ -> _ -> _ => exact True 
| _ => exact False end). 

Check prod: Type -> Type -> Type. 
Compute rT prod. (*= False: Prop*) 
Print rT. (*rT = fun (y : Type) (_ : y) => False: forall y : Type, y -> Prop*) 

Comme vous le voyez, les cartes rT tout pour False. Pourquoi? Le résultat reste le même si je remplace y dans la clause de correspondance w/type of x

Answer 1

La fonction que vous voulez ne peut pas exister dans Gallina au type que vous attendez.

Votre fonction est acceptée, mais si vous l'imprimez, vous pouvez voir son corps est:

rT = fun (y : Type) (_ : y) => False 

Gallina n'a aucun moyen de match -ment sur un Type. Il existe des moyens de traiter les fonctions n-aires, de telle sorte que vous pouvez inspecter leur arité, mais cela implique des types dépendants pour capturer statiquement l'arité. Par exemple, pour les fonctions de n-aire uniformes:

https://coq.inria.fr/library/Coq.Numbers.NaryFunctions.html