Coq, шаблон, сопоставляющий аксиому с подстановочным знаком

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. 

Фундаментально, я требую MyFunction C оценить 1. Мне кажется, что Coq расширяет свои подстановочные _ к B, и он терпит неудачу при попытке применить функцию на этом бессмысленном объекте C. Я бы оцените совет, как это работает вокруг этой проблемы.

Answer 1

Когда вы делаете:

Axiom C : MyType. 

Вы не продлевают жителей индуктивно определенный тип MyType. Вы просто постулируете существование элемента MyType, привязывая его к имени C. То есть C должен быть либо A, либо B.

Я считаю, что вы не сможете расширить тип, подобный этому posteriori. После их определения индуктивные типы задаются в камне, причем все их конструкторы известны, и было бы небезопасно допускать их расширение (поскольку существующие доказательства станут ложными).

Если вы не сообщите нам больше о том, чего вы пытаетесь достичь, вам будет сложно помочь вам дальше.