어떻게 보편적 인 정량화에서 매개 변수를 캡처하는

Question

내가 가장 COQ의 상황에 이런 종류의 처리하는 방법을 궁금 오전 (모듈을 사용하여 섹션?) :

은 가정하자 내가 정의하고 임의의 구조에 대한 여러 가지를 증명해야을 (이 토론의 목적을 위해 이진 관계가있는 집합을 가정 해 봅시다). 물론, 나는 각 정의/증명에 대한 인수로서 집합과 관계를 항상 제공 할 수 있습니다.

Inductive star (X : Set) (R : X -> X -> Prop) := ... 

Lemma star_trans (X : Set) (R : X -> X -> Prop) : ... 

당연히 이것은 다소 시간이 걸립니다. 정의와 정리는,이 코드 영역 외부에 사용할 경우, X을 캡처 할 수있는 방식으로

Parameter X : Set. 
Parameter R : X -> X -> Prop. 

Inductive star := ... 
Lemma star_trans : ... 

: 내가 뭘하고 싶은 로컬 그래서 같은 코드의 일부 경계가 지역 내에서 매개 변수로 X 및 R을 가지고있다 및 R을 보편적 인 정량화 (universal quantification)하에 사용하여 적절한 유형을 제공하십시오. 예를 들어 Check star은 star : forall X : Set, (X -> X -> Prop) -> X -> X -> Prop입니다.

나는이 모듈이 필요한 것일 수도 있다고 생각했지만,이 상황에서 어떻게 사용하는지 알아낼 수는 없다.

Answer 1

"섹션 ​​메커니즘"과 정확히 같습니다 : https://coq.inria.fr/distrib/current/refman/Reference-Manual004.html#Section 참조.

Section rel_star. 

Variables (X : Set) (R : X -> X -> Prop). 

Inductive star := ... 
Lemma star_trans: ... 

End rel_star.