3

事例による証明を使用して証明したい単純な定理があります。以下に例を示します。

目標 forall ab : 設定、a = b \/ a <> b.
証拠
  イントロ a b.
  ...

これを解決するにはどうすればよいでしょうか。そして、等値の 2 つの可能な値 (True または False) を使用してケースごとに証明を正確に定義するにはどうすればよいでしょうか?

どんな助けでも大歓迎です。ありがとう、

4

2 に答える 2

7

SetCoq では s の等価性が決定できないことは確かです。理由は (私の限られた理解では) 帰納的に定義されたセットではないため (したがって、ケース分析はありません...)、閉じたセットでもないためです: 新しいデータ型を定義するたびに、の住民の新しい家族を作成しますSet。したがって、表示する目標を証明した用語は、これらの新しい住民を反映するように更新する必要があります。

@hardmath がコメントで述べているように、Classical仮定を使用して目標を証明できます ( Axiom classic : forall P:Prop, P \/ ~ P.)。

@Robin Green がここのコメントで言及しているように、決定的に等しい型に対してこの種の目標を証明できます。この目的のために、decide equality戦術から助けを得たいと思うかもしれません。参照: http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#@tactic121

于 2013-03-05T15:22:27.503 に答える
4

Propあなたの質問は、Coq の興味深い側面に触れています。それは、命題 (つまり、のメンバー) とブール値 (つまり、のメンバー)の違いboolです。この違いを詳しく説明するのはやや技術的すぎるため、特定の例に焦点を当ててみます。

大雑把に言えば、PropCoqの aは、通常のブール値のようにTrueまたはに評価されるものではありません。False代わりに、事実を推論するために組み合わせることができるProp推論規則があります。それらを使って、命題が成り立つことを示したり、矛盾していることを示したりできます。物事を微妙にしているのは、3 つ目の可能性、つまり命題を証明することも反論することもできないということです。これは、Coq が建設的なロジックであるためです。これの最もよく知られた結果の 1 つは、除外された中間( forall P : Prop, P \/ ~ P) として知られるおなじみの推論原理が Coq で証明できないことですP \/ ~ P。P~ P. どちらが正しいかを知らずして、これを主張することはできません。

いくつかの命題については、それがP \/ ~ P成り立つことを示すことができることがわかりました。たとえば、表示するのは難しくありませんforall n m : nat, n = m \/ n <> m。上記の注意に従って、これは、自然数のすべてのペアに対して、それらが等しいことの証明またはそれらが等しくないことの証明を生成できることを意味します。

一方、あなたの例のように に変更natするとSet、定理を証明することはできなくなります。その理由を理解するにはSet nat * nat、自然数のペアの を考えてみましょう。あなたの定理を証明できれば、それはnat = nat * nat \/ nat <> nat * nat. nat = nat * nat繰り返しますが、上記の発言により、これは、またはを証明できることを意味しますnat <> nat * nat。ただし、両型の間には全単射があるので、 と仮定することが矛盾しているとは言えませんnat = nat * natが、型は構文的に同じではないので、異なると仮定しても問題ありません。技術的に言えば、命題の妥当性はCoq の論理nat = nat * natとは無関係です。

あなたが言及した事実が本当に必要な場合は、除外された中間を公理 ( Axiom classical : forall P, P \/ ~ P.)としてアサートする必要があり\/ます。次に、例の定理を次のようなもので証明できます

イントロ a b. 破壊する (古典的な (a = b))。
  左。予測。
  右。予測。

お役に立てれば。

于 2013-03-08T06:54:49.040 に答える