Coq: Erreur dans la définition de la contrainte

Question

Pouvez-vous corriger l'erreur:

Parameter Arg: Type. 
Parameter F X XP: Arg. 
Parameter Sen Phy Leg Inf: Arg -> Prop. 
Parameter tree car: Phy X. 
Parameter mary john: Phy XP /\ Leg XP /\ Sen XP. 
Fail Coercion c (u:Arg) (x y z: Arg -> Prop) (t:x u /\ y u /\ z u): x u := fun t => @proj1 (x u) (y u /\ z u) t. 
(*The type of this term is a product while it is expected to be "x u".*) 

Je reçois la même erreur quand je prends le terme de

Coercion f (u:Arg) (x y z: Arg -> Prop) (t:x u /\ y u /\ z u): x u. tauto. Defined. Print f. 

Answer 1

réponse partielle: votre fun t => @proj1 (x u) (y u /\ z u) t terme est tapez x u /\ y u /\ z u -> x /\ u. Vous voulez que toute la coercition ait le type x u, vous devez donc alimenter votre fonction avec un terme de type x u /\ y u /\ z u afin d'obtenir un x u.

Je pense que vous avez eu de la confusion à cause du fun t => proj1 t. Pour éviter toute confusion, vous pouvez renommer cette variable avec un nouveau nom, comme fun foobar => proj1 foobar, et vous verrez que vous n'utilisez jamais réellement votre argument t. Par conséquent, le terme entier est (fun t => @proj1 (x u) (y u /\ z u) t) t, et il fonctionne pour Definition. Mais dans le cas d'un Coercion, je reçois le message suivant:

c is defined 
Warning: c does not respect the uniform inheritance condition 

Error: Cannot find the target class.