Coq, Pattern matching an Axiom with a wildcard

Question

I was working with Coq, and I ran into some trouble trying to pattern match objects constructed with Axiom using a wildcard. I have created a minimal Coq program which demonstrates my problem.

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.

Fundamentally, I require MyFunction C to evaluate to 1. It seems to me that Coq is expanding my wildcard _ to B, and it is failing when I attempt to apply the function on this nonsensical object C. I would appreciate advice into how one works around this issue.

Answer 1

When you do:

Axiom C : MyType.

You do not extend the inhabitants of the inductively-defined type MyType. You merely postulate the existence of an element of MyType, binding it to the name C. That is, C has to either be an A or a B.

I believe you will not be able to extend a type like this a posteriori. After their definition, inductive types are set in stone, with all their constructors known, and it would be unsafe to allow their extension (since existing proofs would become false).

Unless you tell us more about what you're trying to achieve, it will be hard to help you further.