一般に、定理証明者のケース分析を行うと、多くのケースが「起こり得ない」ということになります。たとえば、整数に関する事実を証明している場合は、整数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はyについてはfalseになり、おそらく真とは言えません）。だからあなたは自由に唯一のもの（つまりH）で目標を叩き、新しい目標はfalse = andb false cです。
あなたは不条理な目標を達成しようとするばかばかしい仮説を適用します。そして、あなたが実際に反射的に示すことのできるもので終わるのを見てください。 Qed。
更新日正に、ここでは何が起こっているのですか。
Coqのすべての帰納的定義には誘導原理があることを想起してください。
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の証拠を与えた場合と言う私は、：ここでは平等とFalse命題のための誘導の原則の種類は（タイプboolの用語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
あなたはブールbに依存して、いくつかの命題P(b)で始まり、そしてあなたがP(false)の証拠を持っているのであれば、その後、falseに等しく、他のブールyのために、あなたが証拠を持っていますP(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 = trueの証明を与えれば、どんな命題も証明できます。
so back to andb_true_elim1。仮説Hはfalse = trueです。そして私たちはある種の目標を証明したいと思っています。上に示したように、false = trueの証明をあなたが望むものの証明に変える証明項が存在します。したがって、特にHはfalse = trueという証明であるため、あなたが望む目標を証明できるようになりました。
戦術は基本的に証明用語を構成する機械です。
あなたは['discriminate']（http://www.fing.edu.uy/inco/grupos/mf/man/Coq/node.1.2.8.html）を試してみることができます。 （私はそれが古い投稿だと思う） – guest