10

この戦術を使用してdestruct、場合によってステートメントを証明したいと思います。オンラインでいくつかの例を読みましたが、混乱しています。誰かがそれをよりよく説明できますか？

以下に小さな例を示します (解決する方法は他にもありますが、 を使用してみてくださいdestruct)。

 Inductive three := zero 
                  | one 
                  | two.
 Lemma has2b2: forall a:three, a<>zero /\ a<>one -> a=two.

現在、オンラインのいくつかの例では、次のことを提案しています。

intros. destruct a.

その場合、次のようになります。

3 subgoals H : zero <> zero /\ zero <> one
______________________________________(1/3) 
zero = two

______________________________________(2/3) 
one = two

______________________________________(3/3) 
two = two

そこで、最初の 2 つのケースが不可能であることを証明したいと思います。しかし、マシンはそれらをサブゴールとしてリストし、私にそれらを証明することを望んでいます... これは不可能です.

まとめ: 不可能なケースを正確に破棄するには?

使用例をいくつか見inversionましたが、手順がわかりません。

最後に、補題がいくつかの帰納型に依存していて、それでもすべてのケースをカバーしたい場合はどうなりますか?

4

2 に答える 2

10

不可能なゴールを見つけた場合、2 つの可能性があります。証明戦略を間違えたか (おそらく補題が間違っている)、仮説が矛盾しています。

仮説が矛盾していると思われる場合は、目標を に設定してFalse、少し複雑にすることができます。elimtype Falseこれを達成します。多くの場合、False命題Pとその否定を証明することによって証明し~Pます。タクティックはとabsurd Pから任意のゴールを推測します。矛盾する特定の仮説がある場合は、目標を に設定します。仮説が否定の場合、目標は(よりも強力ですが、通常はより便利です) になります。特定の仮説が明らかに矛盾している場合、または目的を証明するだけの場合。P~Pcontradict H~H~AA~ ~Acontradiction Hcontradiction

帰納型の仮説を含む多くの戦術があります。どちらを使用するかを判断することは、ほとんど経験の問題です。主なものは次のとおりです (ただし、ここで取り上げていないケースにもすぐに遭遇します)。

  • destruct仮説をいくつかの部分に分解するだけです。依存関係と再帰に関する情報が失われます。典型的な例はdestruct HwhereHが接続詞であり、タイプとの 2 つの独立した仮説にH : A /\ B分割されます。または二重に、どこに論理和があり、証明を 2 つの異なる部分証明に分割します。1 つは仮説を持ち、もう 1 つは仮説を持ちます。HABdestruct HHH : A \/ BAB
  • case_eqに似てdestructいますが、仮説が他の仮説と持っている接続を保持しています。たとえば、destruct nwheren : natは証明を 2 つのサブ証明 ( に対して 1 つと に対して 1 つ) に分割n = 0しn = S mます。が他の仮説で使用されている場合n(つまり、 を持っている場合)、破棄した はこれらの仮説で使用されているものと同じH : P nであることを覚えておく必要があります。nncase_eq n
  • inversion仮説のタイプについてケース分析を実行します。destructこれは、忘れる仮説の型に依存関係がある場合に特に役立ちます。通常case_eq、仮説 in Set(等式が関連する場合) およびinversion仮説 in Prop(非常に依存する型を持つ) で使用します。このinversion戦術は多くの等式を置き去りにしsubst、仮説を単純化するためにしばしば使用されます。このinversion_clear戦術は単純な代替手段inversion; substですが、少し情報が失われます。
  • inductionは、与えられた仮説について帰納法 (= 再帰) によってゴールを証明しようとしていることを意味します。たとえば、induction nwhereは、整数帰納法を実行し、基本ケース ( で置換) と帰納ケース ( で置換)n : natを証明することを意味します。n0nm+1

あなたの例は、「ケース分析によって明らか」であることを証明できるほど単純ですa。

Lemma has2b2: forall a:three, a<>zero/\a<>one ->a=two.
Proof. destruct a; tauto. Qed.

destructしかし、タクティックによって生成されたケースを見てみましょうintros; destruct a.。( is のケースaはone対称です。最後のケースaistwoは再帰性によって明らかです。)

H : zero <> zero /\ zero <> one
============================
 zero = two

目標は不可能に見えます。これを Coq に伝えると、ここで矛盾を自動的に見つけることができます (zero=zeroは明らかで、残りはタクティクスによって処理される 1 次トートロジーtautoです)。

elimtype False. tauto.

実際tautoには、Coq にゴールを気にしないように指示しtauto、最初のものなしで書いたとしてもelimtype False機能します (IIRC は以前のバージョンの Coq ではそうではありませんでした)。tautoと書くことで、タクティックで Coq が何をしているかを見ることができますinfo tauto。Coq は、タクティックが生成した証明スクリプトを教えてくれますtauto。従うのは簡単ではないので、このケースの手動証明を見てみましょう。まず、仮説 (接続詞) を 2 つに分割しましょう。

destruct H as [H0 H1].

現在、2 つの仮説があり、そのうちの 1 つは ですzero <> zero。これは明らかに偽であり、その否定zero = zeroは明らかに真です。

contradiction H0. reflexivity.

contradiction戦術が何をするかをさらに詳しく見ることができます。（info contradictionシーンの下で何が起こっているかを明らかにしますが、これも初心者向けではありません）。仮説が矛盾しているため、目標が真であると主張し、何でも証明できます。それでは、中間目標を に設定しましょうFalse。

assert (F : False).

実際にが意味として定義されている表記法であるred in H0.ことを確認するために実行します。の結論も同様です:zero <> zero~(zero=zero)zero=zero -> FalseFalseH0

apply H0.

そして今zero=zero、それを証明する必要があります。

reflexivity.

これで、 の主張が証明されましたFalse。False残っているのは、それが私たちの目標を意味することを証明することです. まあ、Falseそれはその定義です（Falseはゼロケースの誘導型として定義されています）。

destruct F.
于 2011-07-26T18:40:00.940 に答える
10

不可能なケースをどのように破棄しますか? 確かに、最初の 2 つの義務を証明することは不可能ですが、矛盾する仮定 (zero <> zeroとone <> one、それぞれ ) があることに注意してください。したがって、これらの目標を証明することができますtauto(興味がある場合は、トリックを実行するより原始的な戦術もあります)。

inversiondestruct のより高度なバージョンです。インダクティブを「破壊」することに加えて、(必要な場合がある)いくつかの等値を生成することがあります。それ自体は の単純なバージョンでありinduction、さらに帰納仮説を生成します。

目標に帰納型が複数ある場合は、destruct/invertそれらを 1 つずつ指定できます。

より詳細なウォークスルー:

Inductive three := zero | one | two .

Lemma test : forall a, a <> zero /\ a <> one -> a = two.
Proof.
  intros a H.
  destruct H. (* to get two parts of conjunction *)
  destruct a. (* case analysis on 'a' *)
(* low-level proof *)
  compute in H. (* to see through the '<>' notation *)
  elimtype False. (* meaning: assumptions are contradictory, I can prove False from them *)
  apply H.
  reflexivity.
(* can as well be handled with more high-level tactics *)
  firstorder.
(* the "proper" case *)
  reflexivity.
Qed.
于 2011-07-26T10:10:14.800 に答える