ほ…ほわぁ

相変わらずCoq書いてるけど進歩ないすなぁ。

Coqの特徴ってのはまあ、Inductive型が使えて帰納法ができてハッピーというアレなんだけど、あまりそこに到達していないとこがなんとも。
証明中にやりたくてもできないという知識的欠陥で、Arithmeticの周辺でライブラリとにらめっこでうじうじやってます。

といきなり言われてもナンノコッチャという話なのでちょっとCoqの紹介。
Coqについては…、まぁggrksということで割愛。
ちょっと基本的な証明晒す：

Section Minimal_Logic.
Lemma lem0 : forall A : Prop, A -> ~~A.
intros A H.
intro H1.
destruct H1.
apply H.
Qed.
End Minimal_Logic.

最小論理で二重否定導入の証明をしてます。
コードに出てくるコマンド(intro, destruct, apply)についてはロジック勉強したことある人に向けた言葉にすると、LKなどのシーケント計算の推論規則に対応してます。
まず二行目で証明する命題を宣言します。

______________________

- ∀A:Prop, A -> ~~A ... subgoal

証明の出口は普通subgoalと言われます。
ここに向かって証明を進めていくことになります。
次のintrosというのはCoqに搭載されている便利機能でGoalに出現する論理記号∀, ->などを自動で抜いてくれます。

A |- ~~A ... subgoal
______________________ (->導入則)

- A -> ~~A

______________________ (∀導入則 A)

- ∀A:Prop, A -> ~~A

Coqの標準ライブラリでは否定演算子"~X"は"X -> False"として定義されているのでもう一度introが使えます。

A, ~A |- False ... subgoal
______________________
A |- ~~A

destructで式の左に出現する否定を除去できます。えぇっと、まぁ細かいことは抜きで…。

A |- A ... subgoal
______________________ (~除去則)
A, ~A |- False

ここで、最後に残る"A |- A"はinitial sequentで公理式なので証明が完了しますが、Coqでは"apply 仮定"、"trivial"、"assumption"などの宣言をして証明を終えます。

Proof completed.

証明が終わったらQ.e.d.して証明を記録します。これでlem0が定義されました。

長々となりましたが、こんなこと趣味で始めました。てけとー

まぁそんなこんなで。。。

にゃんにゃん