4

私が抱えている問題を示すために、このサンプルタイプを作成しました。

Inductive foo : nat -> Prop :=
| foo_1 : forall n, foo n
| foo_2 : forall n, foo n.

明らかfoo_1 0 <> foo_2 0になりましたが、これを証明することはできません:

Lemma bar : foo_1 0 <> foo_2 0.
Proof. unfold not. intros H. discriminate H.

これはエラーを返します

差別可能な平等ではありません。

inversion Hコンテキストをまったく変更しません。奇妙なことに、 をfooからPropに変更するとType証明は通りますが、他の場所で問題が発生するため、実際のコードでこれを行うことはできません。

どうすればこの証明を通過させることができますか? そして、そもそもなぜこれが問題なのですか？

4

2 に答える 2

5

Coq の根底にあるロジックは、与えられた任意の 2 つの証明Propは等しいという「証明の無関係」の公理と互換性があります。結果として、あなたが定式化した声明を証明することは不可能です。

2 つのコンストラクターを区別できるようにしたい場合は、ではなくfoo帰納的にする必要があります。その後、有効な証拠として受け入れられます。TypePropbar

Inductive foo : nat -> Type :=
| foo_1 : forall n, foo n
| foo_2 : forall n, foo n.

Lemma bar : foo_1 0 <> foo_2 0.
Proof. unfold not. intros H. discriminate H. Qed.
于 2016-10-27T19:16:22.167 に答える