하위 집합 유형에서 Z를 "추출하는 방법"{z : Z | z> 0}

Question

함수가 Z을 인수로 취하면 Z의 하위 집합도 가져올 수 있어야합니다. 맞습니까? 예를 들어, Zmod은 Z 2 개를 취하고 Z을 반환합니다. 이 메소드를 구현하지 않고 부분 집합 유형으로 개선 할 수 있습니까?

내가이 원하는 :

Definition Z_gt0 := {z | z > 0}. 

Definition mymod (n1 n2 : Z_gt0) := 
    Zmod n1 n2. 

을하지만 COQ는 n1 is expected to have type Z 물론 뿌려줍니다. Z_gt0에서 어떻게 작동합니까? 강제? Random nat stream and subset types in Coq

편집 :

이 질문은 여기 내 다른 하나는 관련이 proj1_sig 트릭을 할 수 있습니다, 감사 COQ IRC 채널!

Answer 1

proj1_sig은 일반적인 방법입니다. 또 다른 해결책은 패턴 일치하는 것입니다

match z1 with 
    exist _ z hz => ... 
end 

z은 투사 될 것이며, hz는 z > 0 그 증거 일 것이다. 나는 보통 z : Z을 알고 있기 때문에 첫 번째 매개 변수를 익명으로 남겨 둡니다.

Definition Zmod_gt0 (z1 z2: Z_gt0) : Z := 
    let (a, _) := z1 in 
    let (b, _) := z2 in 
    Zmod a b. 

:

내가 COQ의 최신 버전은 (sig 단 하나의 생성자를 유도하기 때문에) let를 사용하여, 그것을 할 수있는 또 다른 방법이있다