Coq에서 보조 정리를 사용하는 방법? <code>Weak_A</code> :

Question

나는 하나 개의 파일 모듈 형 내가 예를 들어 WeakPairProps에 Lemma를 사용할 수있는 또 다른 파일 B.v을 정의하려면 다음

Module Type WeakPair. 
... 

End WeakPair. 

Module WeakPairProps (Import WP : WeakPair). 

Lemma Weak_A .... 

End WeakPairProps. 

A.v라고 정의했다. WeakPairProps은 모듈 유형이 아니기 때문에 WeakPairProps에서 보조 정리를 재사용 할 수있는 모듈을 작성하는 방법을 모르겠습니다.

Module WeakPairPropsInst := WeakPairProps(WeakPairImpl). 

은 이제 참조 할 수 있습니다 :

이제

Module WeakPairImpl <: WeakPair. 
(* stuff goes here *) 
End WeakPairImpl. 

당신이 펑 WeakPairProps를 인스턴스화 할 수 있습니다 :

Answer 1

먼저 당신이 구현 모듈 형 WeakPair 모듈을 정의해야 보조 정리 :

WeakPairPropsInst.lemma 

WeakPairPropsInst 정규화 된 이름을 사용하지 않으려면 가져올 수 있습니다.