30

[これがスタック オーバーフローに適しているかどうかはわかりませんが、ここには他にも多くの Coq に関する質問があるので、誰かが助けてくれるかもしれません。]

私はhttp://www.cis.upenn.edu/~bcpierce/sf/Basics.html#lab28 (Case が導入されている場所のすぐ下) から次の作業を行っています。私はこれの完全な初心者であり、自宅で作業していることに注意してください-私は学生ではありません.

Theorem andb_true_elim1 : forall b c : bool,
  andb b c = true -> b = true.
Proof.
  intros b c H.
  destruct b.
  Case "b = true".
    reflexivity.
  Case "b = false".
    rewrite <- H. reflexivity.
Qed.

そして、私は書き換えが何をするかを見ています:

  Case := "b = false" : String.string
  c : bool
  H : andb false c = true
  ============================
   false = true

次にrewrite <- H.適用されます。

  Case := "b = false" : String.string
  c : bool
  H : andb false c = true
  ============================
   false = andb false c

そして、証明がどのように成功するかは明らかです。

機械的な方法でシンボルを操作するという観点から、どのように証明に到達しているのかがわかります。それはいいです。しかし、私は「意味」に悩まされています。false = true特に、証明の途中でどうやって持つことができますか?

何か矛盾した議論をしているようですが、よくわかりません。やみくもにルールに従っていて、どういうわけかナンセンスなタイピングをしているように感じます。

私は上で何をしていますか？

質問が明確であることを願っています。

4

4 に答える 4

24

一般に、定理証明者で場合分けを行うと、多くの場合は「あり得ない」という結果になります。たとえば、整数に関する何らかの事実を証明する場合、整数iが正、ゼロ、または負のいずれであるかについてケース分析を行う必要がある場合があります。しかし、あなたの文脈、またはおそらくあなたの目標の一部には、ケースの1つと矛盾する他の仮説が横たわっている可能性があります. たとえば、以前の主張から、それiが決して否定的ではないことを知っているかもしれません。

ただし、Coq はそれほどスマートではありません。したがって、矛盾する 2 つの仮説をくっつけて不条理を証明し、それによって定理を証明できることを実際に示すメカニズムをまだ確認する必要があります。

コンピュータプログラムのように考えてください:

switch (k) {
  case X:
    /* do stuff */
    break;
  case Y:
    /* do other stuff */
    break;
  default:
    assert(false, "can't ever happen");
}

目標は「false = true決して起こらないこと」です。しかし、Coq で自分のやり方を主張することはできません。実際には、証明項を書き留める必要があります。

上記のように、ばかげたゴールを証明する必要がありますfalse = true。そして、あなたが働かなければならない唯一のものは、仮説H: andb false c = trueです。少し考えてみれば、実際にはこれがばかげた仮説であることがわかります (なぜなら、andb false yはすべてに対して false に還元されy、したがっておそらく true になることはあり得ないからです)。したがって、自由に使える唯一のもの (つまりH) でゴールを叩くと、新しいゴールは になりますfalse = andb false c。

だから、ばかげた目標を達成しようとして、ばかげた仮説を適用します。そして見よ、あなたは実際に再帰性によって示すことができる何かに行き着く. Qed。

更新 正式には、これが起こっていることです。

Coq のすべての帰納的定義には、帰納原理が付属していることを思い出してください。等号と命題の誘導原理の型を次に示します( typeFalseの項とは対照的に):falsebool

Check eq_ind.
eq_ind
  : forall (A : Type) (x : A) (P : A -> Prop),
    P x -> forall y : A, x = y -> P y
Check False_ind.
False_ind
 : forall P : Prop, False -> P

の帰納原理Falseは、あなたが の証明を私に与えてくれれば、私Falseはあなたに任意の命題の証明を与えることができると言っていますP。

の誘導原理eqはもっと複雑です。に限定して考えてみましょうbool。そして具体的にはfalse。それは言います：

Check eq_ind false.
eq_ind false
 : forall P : bool -> Prop, P false -> forall y : bool, false = y -> P y

したがってP(b)、ブール値 に依存する命題から始めbて、 の証明がある場合、に等しいP(false)他のブール値については、 の証明があります。yfalseP(y)

これはそれほどエキサイティングに聞こえませんが、必要な命題に適用できますP。そして、私たちは特に厄介なものを望んでいます。

Check eq_ind false (fun b : bool => if b then False else True).
eq_ind false (fun b : bool => if b then False else True)
 : (fun b : bool => if b then False else True) false ->
   forall y : bool,
   false = y -> (fun b : bool => if b then False else True) y

少し単純化すると、これはTrue -> forall y : bool, false = y -> (if y then False else True).

したがって、これは証明が必要でTrueあり、次に選択できるブール値yが必要です。では、そうしましょう。

Check eq_ind false (fun b : bool => if b then False else True) I true.
eq_ind false (fun b : bool => if b then False else True) I true
 : false = true -> (fun b : bool => if b then False else True) true

そして、ここにいます: false = true -> False.

の帰納原理について私たちが知っていることと組み合わせると、次のことがわかりFalseますfalse = true。

に戻りandb_true_elim1ます。という仮説Hがありfalse = trueます。そして、ある種の目標を証明したいと考えています。上で示したように、証明を必要なものの証明に変える証明項が存在しfalse = trueます。特にHは の証明なfalse = trueので、任意のゴールを証明できます。

戦術は基本的に、証明項を構築する機械です。

于 2011-11-01T14:21:36.450 に答える
8

true = falseは、2 つの異なるブール値を等しくするステートメントです。これらの値は異なるため、このステートメントは明らかに証明できません (空のコンテキストでは)。

あなたの証明を考えると、あなたは目標が である段階に到達するfalse = trueので、明らかにそれを証明することはできません. これは、たとえば、ケース分析を行い、ケースの 1 つが他の仮定と矛盾する場合によく発生します。

于 2011-11-01T14:35:15.937 に答える