Coq에서 동형 클래스 정의하기

Question

Coq에서 동형 클래스를 정의하는 방법?

가정하자 나는 기록 ToyRec 있습니다

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

그리고 전단 사 함수 f를가 존재하는 경우이 객체의 T1 및 T2는 동형 것을 주장 유형 ToyRec 두 개체 사이의 isomorphisms의 정의 :. T1을 (X) -> T2. (X)는 매핑 된 요소의 레이블을 유지합니다.

Definition Isomorphic{Labels:Set} (T1 T2 : @ToyRec Labels) : Prop := 
exists f:T1.(X)->T2.(X), (forall x1 x2:T1.(X), f x1 <> f x2) /\ 
         (forall x2:T2.(X), exists x1:T1.(X), f x1 = f x2) /\ 
         (forall x1:T1.(X) T1.(r) x1 = T2.(r) (f x1)). 

는 지금은 T1 동형 모든 객체를 포함한 세트 을 객체 T1을 받아 반환하는 함수를 정의하고 싶습니다.

g(T1) = {T2 | Isomorphic T1 T2} 

어떻게 이런 일을 coq에서합니까? 나는 이론적으로도 이론적으로이 논리를 가지고 있을지도 모른다는 것을 알고있다. 그러나 동형체 클래스의 올바른 유형의 이론적 인 개념은 무엇인가? 아니면 더 근본적으로, 어떻게 주어진 속성을 만족하는 모든 엘레 넷의 집합 (또는 유형)을 정의 할 수 있을까요?

Answer 1

정말로 당신이 무엇을하고 싶은지에 달려 있습니다. Coq에서 은이며, 을 만족하는 모든 요소 x이 T 인 모든 유형의 유형 인 이해 유형 {x : T | P x}입니다. 그러나 유형입니다. 즉, 다른 용어를 분류하는 데 사용되며 데이터 구조이 아니라 전통적인 의미로 계산할 수 있습니다. 따라서 예를 들어, P을 만족하는 요소에서만 작동하는 T에 함수를 작성할 수 있습니다.이 경우 함수의 유형은 {x : T | P x} -> Y이고, Y이 결과 유형입니다. T의 요소 중 몇 개가 P을 만족시키는 지 계산하는 함수를 작성하는 데 사용하십시오.

이 세트로 계산하려면 일이 좀 더 복잡해집니다. P은 결정하기 쉬운 속성이므로 좀 더 쉽게 작업 할 수 있다고 가정 해 보겠습니다. T이 유한 유형이면 이해 연산자가있는 데이터 구조를 설정할 수 있습니다 (예 : Ssreflect 라이브러리 참조). 그러나 이것은의 경우 무한대 인 T 일 때 중단됩니다. Vinz가 말했듯이이 집합을 데이터 구조로 건설적으로 구축하는 일반적인 방법은 없습니다.

아마도이 유형으로하고 싶은 것을 설명했다면 완전한 대답을하는 것이 더 쉬울 것입니다.