Coq: Ошибка в определении принуждении

Question

Можно ли исправить ошибку:

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".*) 

Я получаю ту же ошибку, когда я беру термин из

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

Answer 1

Частичный ответ: Ваш fun t => @proj1 (x u) (y u /\ z u) t член имеет type x u /\ y u /\ z u -> x /\ u. Вы хотите, чтобы все принуждение имело тип x u, поэтому вам нужно подать свою функцию на срок x u /\ y u /\ z u, чтобы получить x u.

Я думаю, что вы получили путаницу из-за fun t => proj1 t. Чтобы избежать путаницы, вы можете переименовать эту переменную со свежим именем, например fun foobar => proj1 foobar, и вы увидите, что никогда не используете свой аргумент t.

Таким образом, весь срок: (fun t => @proj1 (x u) (y u /\ z u) t) t, и он работает для Definition. Но в случае Coercion я получаю следующее сообщение:

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

Error: Cannot find the target class.