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

IMVHO、問題の設定が非常に複雑に見えています。私はこのモデリング方法が効果的であるとは確信していません。

実際にそのルートに行きたい場合、強制は非常に特別なルールがあります。それらを使用する場合は、マニュアルのchapter 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：特に、私はあなたには、いくつかの包装を追加する必要がありますので、パラメータはソースクラスを作ることができないと思います。 ssreflect docにある一般的なsubTypeクラスは、ジェネリック強制フレームワークを作成する方法についていくつかの助けを与えるかもしれないことに注意してください。

Answer 2

これを試してみると、解決策は驚くほど簡単でした。

は

1. あなたは機能、あなたは強制でにしたい関数を定義する必要があります"uniform inheritance condition"を破る避けるために
2. を作品Coercion c: PLS >-> Pすなわち、互いの方へを強制することができます：二つのステップ、私の質問が欠落していましたがありましたその一般的な（ "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.