Coq: приведение / подтип между сложными выражениями

Question

У меня сложилось впечатление, что это невозможно в Coq. Например

Parameter Arg: Type.
Parameter F X XP: Arg.
Parameter S P I PLS PI: Arg -> Type.
Parameter tree car: P X.
Parameter mary john: PLS XP.
Parameter c: PLS XP -> P XP.
Coercion c: PLS XP >-> P XP. (*Syntax error: '>->' expected after [vernac:class_rawexpr] (in [vernac:gallina_ext]).*)

Так что не только типы выражений должны быть рядом с >-> быть установленным, набирать или поддерживать, сами выражения также должны быть синтаксически элементарными ("rawexpressions" по-галлински?)? Как обойти это; я могу сформировать принуждение между сложным выражением? Есть ли другой способ определить подтип в Coq, который будет работать с сложными выражениями? Могу ли я сделать лучше, чем

Let nui := PLS XP.
Let hui := P XP.
Parameter c: nui -> hui.
Coercion c: nui >-> hui.
Parameter st: P XP -> Type.
Check st (c mary). (*st mary : Type*)
Check st mary. (*Error: The term "mary" has type "PLS XP" while it is expected to have type "P XP".*)

Answer 1

Попробовав это, то и еще, решение оказалось на удивление легким. Было два шага, в которых мой вопрос отсутствовал:

1. Вы можете привести функции друг к другу, т.е. Coercion c: PLS >-> P работает
2. Чтобы не нарушать "условие единообразного наследования", вы должны определить функцию, которую вы хотите превратить в приведение в ее общей ("forall") форме

В сумме:

Parameter Arg: Type.
Parameter F X XP: Arg.
Parameter S P I PLS PI: Arg -> Type.
Parameter tree car: P X.
Parameter mary john: PLS XP.
Parameter c: forall x:Arg, PLS x -> P x.
Coercion c: PLS >-> P.
Check mary:P XP.

Answer 2

IMVHO, установка проблемы выглядит очень сложной; Я не уверен, что этот метод моделирования будет эффективным (в смысле эффективности).

Если вы действительно хотите пойти по этому пути, обратите внимание, что у Принуждений есть очень специфические правила; если вы хотите их использовать, вам необходимо ознакомиться с главой 18 руководства. В частности, я думаю, что параметры нельзя сделать исходным классом, поэтому вам придется добавить некоторые обертки:

Parameter Arg: Type.
Parameter F X XP: Arg.
Parameter S P I PLS PI: Arg -> Type.
Parameter tree car: P X.
Parameter mary john: PLS XP.
Parameter c: PLS XP -> P XP.

Inductive p_wrap := p_wrap_C : PLS XP -> p_wrap.
Coercion u_cast x := match x with | p_wrap_C u => u   end.
Coercion c_cast x := match x with | p_wrap_C u => c u end.

Parameter st: P XP -> Type.
Definition Mary := p_wrap_C mary.
Check st (c Mary).
Check st Mary.

YMMV. Обратите внимание, что общее subType class в ssreflect doc может предоставить некоторую помощь в том, как создать общую структуру принуждения.