Coq, Axiom과 와일드 카드 패턴 일치

Question

나는 Coq와 함께 작업 중이었고 와일드 카드를 사용하여 Axiom으로 구성된 일치 개체를 패턴 화하려고 할 때 약간의 문제가 발생했습니다. 내 문제를 보여주는 최소한의 Coq 프로그램을 만들었습니다.

Inductive MyType : Set := 
| A 
| B. 

Definition MyFunction (n:MyType) : nat := 
match n with 
| A => 0 
| _ => 1 
end. 

Eval compute in MyFunction A. 
Eval compute in MyFunction B. 

Axiom C : MyType. 

Eval compute in MyFunction C. 

기본적으로, 나는 1로 평가 MyFunction C을 필요로 COQ가 B 내 와일드 카드 _을 확대하고 나에게 것, 그리고 내가 것이 무의미한 객체 C.에 함수를 적용 할 때 그것은 실패 이 문제를 해결하는 방법에 대한 조언을 주셔서 감사합니다.

Answer 1

당신이 할 경우 :

Axiom C : MyType. 

당신은 유도 정의 유형 MyType의 주민을 연장하지 않습니다. MyType이라는 요소의 존재를 가정하고 이름을 C으로 바인딩합니다. 즉, C은 A 또는 B이어야합니다.

나는 이런 종류의 후천을 늘릴 수 없다고 생각합니다. 정의 후에는 유도 형이 돌에 설정되며 생성자는 모두 알려져 있으므로 확장을 허용하는 것은 안전하지 않습니다 (기존의 교정본이 거짓이 될 수 있기 때문에).

달성하려는 목표에 대해 자세히 알려주지 않는 한 더 이상 도움을 줄 수 없습니다.