Erreur: application illégale (construction non-fonctionnelle)

Question

J'essaye de travailler quelques preuves des diverses lois deMorgans en utilisant les constructeurs de type/éliminateurs du livre HoTT. J'avais sauté pour choisir https://mdnahas.github.io/doc/Reading_HoTT_in_Coq.pdf pour les choses pertinentes et vider tout dans un fichier texte .v. J'ai besoin de règles d'élimination/d'introduction pour le produit, le co-produit et un moyen d'établir la négation. Jusqu'à présent, j'ai,

Definition idmap {A:Type} (x:A) : A := x. 

Inductive prod {A B:Type} : Type := pair : A -> B -> @prod A B. 

Notation "x * y" := (prod x y) : type_scope. 

Section projections. 
    Context {A : Type} {B : Type}. 
    Definition fst (p: A * B) := 
    match p with 
     | (x , y) => x 
    end. 

    Definition snd (p:A * B) := 
    match p with 
     | (x , y) => y 
    end. 
End projections. 

L'erreur sur "Définition fst (p: A * B): =" est

Error: Illegal application (Non-functional construction): 
The expression "prod" of type "Type" 
cannot be applied to the term 
"A" : "Type" 

J'ai essayé la recherche dans la liste d'erreurs sur le site Coq, mais n » Je ne trouve rien.

Answer 1

Il y a deux problèmes avec votre code:

• prod sont déclarés de deux Type arguments implicites

En conséquence, la notation "x * y" correspond à prod {_} {_} x y qui conduit toujours à des mauvais termes tapés: prod {_} {_} est un Type et en tant que tel, il n'a pas de sens d'appliquer quelque chose.

Le correctif est de transformer ces deux arguments implicites dans les explicites:

Inductive prod (A B:Type) : Type := pair : A -> B -> @prod A B. 

• La notation (x , y) n'a pas été déclaré

Une fois que vous avez fixé la définition de prod, la définition ne sais pas encore parce que Coq ne sait pas ce que vous voulez dire par le modèle (x, y). Vous pouvez le déclarer comme une nouvelle notation avant Section projections comme ceci:

Notation "x , y" := (pair _ _ x y) (at level 10).