証明チュートリアル

coq

随分遅れてcoqを少しやってみました。

それ何？

定理証明プログラムという奴です。僕の苦手なOcamlベースです＞＜
簡単なものならCoq内部だけで、複雑なら外部コマンドとして実行できます。

基本技

全ての技は . (ピリオド)で終わります。英語と一緒ですね。

Check
定理がwell-formedであるか調べます。実行すると (式) : (型）という形でレポートくれます
let ... in
思考を環境に閉じ込める檻ですね
fun =>
λλ... (トボトボ歩いている人、ではありません）
Definition ：=
思考を野に解き放つ呪文ですね
Print
野に放った思考を追跡するときに使います
Reset
ニューラライザーでピカッ!「あれー僕何してたんだっけー？」です
Eval compute in ...
絵に描いた餅を食べられるようにする呪文です

・・・・ごめんなさいごめんなさい

どんなかんじか

Eval compute in とか毎回打つのまんどいよーとか言ってはいけません。
超ミニマリストで bool演算するのにも 自然数(ちなみに０を含む)使うのにも以下のようなおまじないが必要です。

Require Import Bool.
Require Import Arith.

それでも「めんどくせー」とか言ってはいけません。 "With great power comes great responsibility"です。
めんどくせー大いなる責任以外はほとんどOcamlです。あの強力無比なパターンマッチも可能です。というかそれがないとなんもできないっぽい。
あと自然数は自然数としてだけでなく、いわゆるペアノの公理で S(Successor)で表現することもできます.

Definition is_zero (n:nat) :=
  match n with
    0 => true
  | S p => false
  end.

いや要するにめ＜秘匿事項＞
再帰関数だってちゃんとそう宣言してあげさえすれば！

Fixpoint sum_n n := 
  match n with
    0 => 0
  | S p => p + sum_n p
  end.

なんか let recとか嫌なものが見えてきます。しかもです。パターンマッチしたモノしか再帰呼び出しの引数に使えません。こゆーの構造的再帰なんだよこいつ。バカジャネーノんぎゃー。いや要するにめんど＜自主規制＞
しかもです

Coq < Eval compute in rec_bad 50000.
Warning: Stack overflow or segmentation fault happens when working with large
numbers in nat (observed threshold may vary from 5000 to 70000 depending on
your system limits and on the command executed).
Stack overflow.

てなくらいには弱者です。
要は道具は使いようということのようです。

しかし

萎えました。なんとなく手応えは見えてきたので、このまま進めますが今日はもうやめー