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.