先に結論を書いておく: change (~ P) もしくは change (?p -> False) with (~ p) を使えばよい
Coq で、~P というのは、not P の notation である。
not は以下のように定義される。
Definition not := fun A : Prop => A -> False
というわけで、~P というのは not を展開すれば P -> False になる。
Variable P : Prop. Goal ~P. (* ~ P *) unfold not. (* P -> False *)
さて、P -> False を ~P に戻すにはどうしたらいいか。 型検査では P -> False と ~P は同等に扱われるのでどちらでも関係ないが、他の文脈では ~P でないと困ることがある。 先日は実数 Reals についての証明を書いていて、 discrR tactic をつかったら、 1 = 2 -> False という形の命題を扱えなくて、1 <> 2 に変える必要があった。(1 <> 2 は not (1 = 2) の notation である) そういうことがあるので、この変形はときに必要になる。
unfold の逆だから fold だろうというのはダメで、以下のようにゴールは変わらない
Goal P -> False. (* P -> False *) fold not. (* P -> False *)
これが動かないというのはマニュアルにExample: fold doesn't always undo unfoldという例で説明されている。 この例では、fold を動かすためには pattern を使うと書いてある。
Goal P -> False. (* P -> False *) pattern P. (* (fun P0 : Prop => P0 -> False) P *) fold not. (* ~ P *)
しかし、tactic を 2回使うのは大げさだし、P を書かなければならないのも気になる。 上の例のように P が 1文字とか短ければいいのだが、命題が長くなると、それをコピーして証明が長くなってしまう。
だいたい、P を書いていいのであれば、change を使えばいいのである。
Goal P -> False. (* P -> False *) change (~P). (* ~ P *)
では、P を書かないで済ます方法はないかと考えて、change で変数を使えばいいではないかと思いついた。
Goal P -> False. (* P -> False *) change (?p -> False) with (~ p). (* ~ P *)
うむ、ちゃんと動く。
まぁ、ちょっと長いので、短い命題については change (~ P) を使えばいいだろう。 とくに、P が x = y なら change (x <> y) と書けばいいとか、より直接的な記述が可能なこともある。
なお、定理を探すと、neg_false というのが見つかった。
neg_false: forall A : Prop, ~ A <-> (A <-> False)
ただ、<-> を 2重に使っているので使うのは面倒くさい。 SSReflect を使って以下のように書けるのは確認したが、長いし、証明項も大きくなるし、使い道はないだろうな。 (change の場合は証明項は増えない)
From mathcomp Require Import all_ssreflect. Variable P : Prop. Goal P -> False. (* P -> False *) apply: (iffLR ((iffLR (neg_false _)) _)). (* ~ P *)
[latest]