종속 유형 인스턴스 간의 평등성 입증

Question

대수적 구조 (예 : 모든 단일체 클래스)에 해당하는 클래스를 형식화하려고 시도하면 자연스러운 설계는 필요한 모든 모델을 모델 유형으로 monoid (a:Type)을 생성하는 것입니다 필드 (요소 e:a, 운영자 app : a -> a -> a, 모노로이드 법칙이 충족됨을 증명 함). 이렇게하면지도 monoid: Type -> Type이 생성됩니다. 이 접근법의 단점은 monoid m:monoid a (지원 유형이 a 인 모노 가드)과 m':monoid b (monoid wih 지원 유형 b)이 주어지면 유형이 잘못되었으므로 m = m' 항을 쓸 수 없다는 것입니다 . 대안 설계는 유형이 monoid 인 지원 유형이 다른 필드 인 a:Type을 작성하는 것입니다. 따라서 m m':monoid이 주어진다면 m = m'인지 여부는 항상의 L가 있습니다. 어쨌든, m과 m'에 동일한 지원 (a m = a m)이 있고 연산자가 같음 (app m = app m', 일부 확장형 평등 공리 덕분에 달성 될 수 있음)과 증명 필드는 중요하지 않다고 주장하고 싶습니다. 어떤 증거 부적합 공리) 등등 다음 m = m'. 잘못 입력하기 때문에 불행하게도, 우리는 이벤트가 문제를 단순화하기 위해 ...

을 평등 app m = app m'을 표현할 수없는, 우리가 있다고 가정

이

Inductive myType : Type := 
| make : forall (a:Type), a -> myType. 
. 

나는 형태의 결과를 가지고 싶다 :

forall (a b:Type) (x:a) (y:b), a = b -> x = y -> make a x = make b y. 

이 문장은 입력 할 수 없으므로 입력 할 수 없습니다.

나는 공리는 나에게 두 가지 유형 a 및 b가 동일 함을 입증 할 수있을 수 있습니다, 나는 x과 y도 실제로 동일하다는 것을 보여줄 수 있습니다,하지만 난 내가 결론 할 수있는 도구를 갖고 싶어 make a x = make b y. 어떤 제안이라도 환영합니다.

Answer 1

제공되는 동등성을 사용하여 수동 유형 캐스트를 삽입하는 것이 가장 낮은 방법입니다. 즉, 가정이 x = y 인 대신 가정은 (CAST q x) = y입니다. 아래에 명시 적으로 일치 항목으로 캐스트를 작성하지만 수행 할 함수를 정의하여보다 멋지게 만들 수도 있습니다.

Inductive myType : Type := 
| make : forall (a:Type), a -> myType. 

Lemma ex : forall (a b:Type) (x:a) (y:b) (q: a = b), (match q in _ = T return T with eq_refl => x end) = y -> make a x = make b y. 
Proof. 
    destruct q. 
    intros q. 
    congruence. 
Qed. 

도 JMeq로 알려진 "이종 평등"을 사용하여이 기계의 대부분을 숨길 수있는 더 좋은 방법이있다. 자세한 소개는 the Equality chapter of CPDT을 권장합니다. 이 특정 정리 공리없이 증명 될 수 있지만 귀하의 예는이 스타일의 형식화를 할 경우 평등에 대한 공리없이 COQ 입증 할 수없는 목표를 발생할 가능성이 있으며, 일반적으로

Require Import Coq.Logic.JMeq. 

Infix "==" := JMeq (at level 70, no associativity). 

Inductive myType : Type := 
| make : forall (a:Type), a -> myType. 

Lemma ex : forall (a b:Type) (x:a) (y:b), a = b -> x == y -> make a x = make b y. 
Proof. 
    intros. 
    rewrite H0. 
    reflexivity. 
Qed. 

된다. 특히, 이런 종류의 종속 기록에 대한 분사 성은 증명할 수 없다. JMEq 라이브러리는 이기종 평등에 대한 공리를 자동으로 사용합니다. 매우 편리합니다.