pattern-matching - 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 C1 に評価する必要があります。Coq は私のワイルドカードを に拡張しているように思え_ますB。この無意味なオブジェクト C に関数を適用しようとすると失敗します。この問題を回避する方法についてアドバイスをいただければ幸いです。

Answer 1

あなたがするとき：

Axiom C : MyType.

帰納的に定義された type の住民を拡張しませんMyType。の要素の存在を前提としてMyType、それを名前にバインドするだけCです。つまり、または のCいずれかでなければなりません。AB

このようなタイプを事後的に拡張することはできないと思います。定義後、帰納型は固定され、すべてのコンストラクターが既知であり、それらの拡張を許可することは安全ではありません (既存の証明が false になるため)。

あなたが達成しようとしていることについてもっと教えてくれなければ、それ以上あなたを助けることは難しいでしょう.