Coq - 레코드에 매개 변수 전달

Question

동일한 레코드 유형의 두 가지 별개 인스턴스에 속한 세트 요소를 비교하는 데 문제가 있습니다. 다음 기록을 고려하십시오.

Record ToyRec := { 
    X:Set; 
    Labels:Set; 
    r:X->Labels 
} 

는 두 개체 T1 입력 ToyRec의 T2가 같은 레이블 T2.(X)의 요소가 존재 T1.(X)의 모든 요소에 대한 경우 좋은 쌍을 형성 말한다.

Definition GoodPair(T1 T2:ToyRec):Prop := 
forall x1:T1.(X), exists x2:T2.(X), T1.(r) x1 = T2.(r) x2. 

문제

내가 T1.(r) x1 유형 X1.(Labels), 이며 T2.(r) x2 유형 X2.(Labels)입니다 없다는 오류를 얻을 수 있다는 것입니다.

나는이 문제를 이해하고, 어쨌든 레이블 집합을 레코드 외부에 선언하고 매개 변수로 전달하면 해결할 수 있다고 상상한다. Coq에서이를 수행 할 수있는 방법이 있습니까? 또는 내가 원하는 레코드를 정의하는 의 가장 우아한 방법은 무엇이며 속성은 GoodPair입니까?

Answer 1

나는 그의 다음 코드에서 가져온 가장 가까운 것은 :

Record ToyRec {Labels : Set} := { 
    X:Set; 
    r:X->Labels 
}. 

Definition GoodPair {Labels:Set} (T1 T2 : @ToyRec Labels) : Prop := 
    forall x1: X T1, exists x2: X T2, r T1 x1 = r T2 x2. 

ToyRec에 대한 종속성으로 Labels을 가짐으로써 당신이 두 기록은 동일한 유형을 사용하고 있는지 확신 할 수 있습니다.

추신 : (Labels : Set) 대신 {Labels : Set}을 사용하여이 인수가 암시 적이며 가능한 경우 유추되어야한다고 지정했습니다.