■
δ-reduction
δ-reduction は変数をその定義で置き換える。
まず何か定義して、
Coq < Definition hoge := fun x:nat => 2+x. hoge is defined
cbvを実行してみる。
Coq < Eval cbv delta [hoge] in (hoge 3).
= (fun x : nat => 2 + x) 3
: natこの場合は「hoge」だけを展開する。
さらに「plus」も展開してみる。
Coq < Eval cbv delta [hoge plus] in (hoge 3).
= (fun x : nat =>
(fix plus (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p => S (p + m)
end) 2 x) 3
: nat全部の定義を展開したい場合は[]はいらない。
β-reduction
β-reduction は
(fun x:T, t) a
を
t{a/x}に変換する。ここで{a/x}はtの中に含まれるxをaに置き換える操作。
Coq < Eval cbv delta [hoge] beta in (hoge 3).
= 2 + 3
: natさらにplusも展開すると
Coq < Eval cbv delta beta in (hoge 3).
= (fix plus (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p => S (p + m)
end) 2 3
: nat
ι-reduction
ι-reduction は再帰的な定義を展開する。fixpointもできるだけ計算してくれる。
まず、ちっとも計算できない場合。
Coq < Eval cbv delta beta iota in plus.
= fix plus (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p => S (p + m)
end
: nat -> nat -> natこれは n が分からないので、これ以上進まない。ひとつ引数を与えると
Coq < Eval cbv delta beta iota in (plus 2).
= fun m : nat => S (S m)
: nat -> natと、完全に計算してくれる。
ζ-reduction
let で定義した変数を定義で置き換える。δと似てるがなぜか違う名前がついている。
cbv, lazy
cbv と lazy は指定した reduction ルールをできるだけ適用する tactic。
ふたつの違いは call-by-value か call-by-need のどっちを使うかどうか。
red
red はゴールの頭の変数だけを展開する。
hnf
red をひたすら適用するんだと思う。
simpl
δを一回だけ使い、βιする？
unfold qualid
指定した変数を展開する。
fold term
unfold の逆。
pattern term
βの逆。たとえば、ゴール
Q x y z
に
lt_wf_ind : forall n (P:nat -> Prop), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
この定理を「n := y」として適用したいとする。ということは「P := fun n => Q x n z」ということになる。
そこで、pattern y とすると
(fun n => Q x n z) y
となって apply しやすくなる。ただこの場合は pattern しなくても、apply が正しくパターンマッチに成功するので、もっと複雑な場合で失敗したらこの方法を思い出すとよい。
■
change term
ゴールとtermが変換可能なときに、ゴールをtermで置き換える tacic。
simpl とかを適当に使った結果、やりすぎていらんとこまで置き換えてしまった場合とか、逆に何をどう使えばもっと簡単に置き換えることができるのか分からない場合に使うとよいかも。
例えば、simpl の結果
============================ x = match y with | 0 => 0 | Zpos y' => Zpos (xO y') | Zneg y' => Zneg (xO y') end + x
というわけのわからない式になっちまったが、よく考えると「x = 2 * y + x」じゃねーかってときに
< change (x = 2 * y + x).
とすればよい。
absurd term
仮定に矛盾がありそうなときはこれを使う。termと~termを証明すれば、ゴールを証明したことになる。
普通はtermか~termのどちらかが仮定にそのまま入ってる。すでに両方とも入ってる場合は contradiction を使うとよい。
contradiction
これは tauto でも証明できる。
cbv系
さっぱりわからん。あとで書く。
■
assert form
ゴールを直接の証明が簡単には書けないので、とりあえず簡単に証明できる中間結果を教えるtactic。
ringとかomegaで一発で証明するには複雑すぎるときに、問題を二つに分けるとよいことがある。
中間結果 form を指定すると、サブゴールにformが追加されて、元のゴールにはformが仮定として追加される。
< Goal forall x y: Z, x>=0 -> x*x>y*y -> x-y>0. < intros. 1 subgoal x : Z y : Z H : x >= 0 H0 : x * x > y * y ============================ x - y > 0
ここで、定理 Zgt_square_simpl を使いたいわけだが、この定理は「x-y>0」ではなく「x>y」を導くものなので、直接は適用できない。そこで、assert を使って
Unnamed_thm < assert (x>y); auto with zarith. 1 subgoal x : Z y : Z H : x >= 0 H0 : x * x > y * y ============================ x > y
これで定理が使える形になったので、apply Zgt_square_simpl すれば証明が終わる。
assert (identifier:=term)
これは assert と exact を続けて実行したのと同じだが、論理式を書くのが億劫な場合に便利。
仮定に forall があって、それを例化した仮定を後でたくさん使いたいときに使うとよい。
H : forall x : nat, P x -> Q x -> R x y : nat ============================
たとえば上のような場合で、「P y -> Q y -> R y」は導けるので
H : forall x : nat, P x -> Q x -> R x y : nat Hy : P y -> Q y -> R y ============================
としておけば、後で Hy を何度も使う場合は便利である。この状態にもっていくのに普通の assert を使うと
< assert (Hy: P y -> Q y -> R y); auto.
と書かないといけないが、こっちの形式で書くと
< assert (Hy := H y).
と書くだけでよい。
cut form
これは基本的に assert と同じであるが、できあがるサブゴールの並び順が逆になる。
apply term in ident
assert のところに書いたことを、apply 一発で済ませられる tactic。
仮定に「H: T -> U」があって、定理「th: U->V->W」があったとすると、
apply th in H.
を実行すると、T と V を証明すれば W が仮定に追加できる状態になる。例えば、
x : Z y : Z H : x >= 0 H0 : y = 1 -> x * x > y * y ============================
で、
apply Zgt_squre_simpl in H0.
とすれば、「x >= 0」と「y = 1」を証明すれば「x > y」を使えるようになる。
Zgt_squre_simpl の前提は「n >= 0」と「n * n > m * m」なので、H に対して適用してもよいのだが
apply Zgt_squre_simpl in H.
では、「m」を何にして定理を適用するのか不明なのでだめで、
apply Zgt_squre_simpl with (m:=y) in H.
と書かないといけない。
この方法で適用できる定理を見つけるのは面倒なので、使えそうな定理を知ってるときにしか使えないと思う。
■
assumption
この tactic は忘れてもよい。仮定の中に結論と一致しているものがある場合に使うと一発で証明が終わる。でも、auto を使えば同じことができる。
intro
この tactic はチュートリアルで普通に理解できる以上の機能はない。
結論が「forall x:T, U」の場合と「T->U」の場合にしか使わない。「U」が新しい結論になって、「x:T」が新たに仮定に追加される。それ以外の場合は「red」を勝手に実行してくれる。なので
Goal ~A. intro.
とすれば、「not」を勝手に展開してくれて
H: A ====== False
となる。
intro ident
「intro」に引数を与えると、追加される仮定の名前を設定できる。チュートリアルに載ってるからみんな知ってるよね。
apply term
「apply」はゴールに辿り着くために最後に適用する仮定または定理を教えてあげる tactic。
適用できる定理は「forall」と「->」でゴールまでつながっている形で無ければならない。
例えばゴールが「A /\ B」のときは
th1: forall A B: Prop, A -> B -> A/\ B.
は適用できる定理であり、
apply th1.
とすれば、残った証明すべきことは「A」と「B」なので、ゴールはこの二つとなる。
ゴールに「forall」とか「->」含まれていてもよくて、「~A->~B」がゴールだとすると
th2: forall X Y: Prop, (X->Y)->~Y->~X
もうまくパターンマッチしてくれる。
パターンマッチングで決定できなかった変数は指定しなければならない。次の定理を適用することを考えよう
th3: forall (X: Set) (x y z: X), x = y -> y = z -> x = z.
証明したいのは
Goal 1+3 = 2+2.
だとする。どちらも「4」に等しいことを使って証明しよう
apply th3.
こうすると「1+3 = 2+2」が「x = z」とパターンマッチされて、「x = 1+3」と「z = 2+2」となる。
ついで、「X = nat」であることがわかる。しかし、「y」が何になるか分からないので、この apply はエラーになる。
「y」には「4」を指定したかったので、
apply th3 with 4.
とするか
apply th3 with (y := 4).
とすればよい。ここで上の形式は使いにくくて、この例で「X = nat」が決まることに気づかずに
apply th3 with nat 4.
なんて書いてしまうと、とんでもなく不親切なエラーメッセージが表示される。
下の形式だと、余分に指定した
apply th3 with (X := nat) (y := 4).
も通るので、初心者向きである。
もちろん
apply (th3 nat (1+3) 4 (2+2)).
のように全部自分で指定してもよい。
■
Coqでの証明はtacticと呼ばれるコマンドを並べて次々に実行ことによって行われる。
このtacticの語彙が多いほど証明の記述は楽になる。
しかし、語彙を増やすようなドキュメントはオンラインに見つからないので、書きやすいところから書いてみる。
exact term
「exact」は最もプリミティブなtacticで、現在のゴールの証明を直接記述する。
直接記述する形式は Print コマンドを使えば知ることができる。
Variables A B C:Prop. Lemma ex1: (A->B->C)->(A->B)->A->C. auto. Qed.
このように簡単な定理を証明したとして、証明の内容を Print コマンドを使って表示すると
Print ex1.
ex1 =
fun (H : A -> B -> C) (H0 : A -> B) (H1 : A) => H H1 (H0 H1)
: (A -> B -> C) -> (A -> B) -> A -> Cとなり、この中で証明にあたる部分は
fun (H : A -> B -> C) (H0 : A -> B) (H1 : A) => H H1 (H0 H1)
である。まったく同じ定理を証明しようと思ったら、
Lemma ex2: (A->B->C)->(A->B)->A->C. exact (fun X Y Z => X Z (Y Z)). Qed.
のように同じ関数を記述すればよい。型は指定しなくても勝手に推論してくれる。
定理の証明を行ったら毎回 Print を実行して、どのような証明が行われたかを確認するとよい。
初めて見る関数に出会えたり、より簡単な証明を思いついたりできる。
慣れてくれば「->」しかでてこない定理は exact でも簡単に証明できる。
否定がまじってる場合も同様である。否定の定義は
not A := A -> False.
であるから、これを展開すれば同様にできる。結論に False が現れる場合は仮定のどこかに False が入っていなければ証明できない。最も単純な場合は
Lemma ex3: A -> ~A -> False.
は「A である」と「A ではない」を仮定して結論「False」を導きたいので、仮定に入っている「False」を探すことになる。
否定の定義を思い出すと証明したいことは
A -> (A -> False) -> False.
なので、一発で証明できて
exact (fun isA notA => notA isA).
となる。
「notA isA」が False になるのは覚えておくべき基本事項。
もっと複雑な例
Lemma ex4: (A -> B) -> (~B -> ~A).
こういう場合は、括弧と優先順位からintros したときにどこまでが仮定になるのかを考えて、「A->B」と「~B」と「A」が仮定で「False」が結論であることに気づけば、「A->B」と「A」から「B」を導いて、「~B」とぶつけてやれば「False」が得られることが分かるので、
exact (fun AimplB notB isA => notB (AimplB isA)).
で証明できる。
■
Coqにおける等号は「Leibniz Equality」というもので、
(forall P: Prop, P x -> P y) <-> x = y.
つまり「任意の命題に関して、同じ結論を与えるなら二つは等しい」というのが等しいの定義らしい。
等しくないことを示すにはどうすればよいかというと、結果が等しくならない命題を作ってやればいいわけだ。
たとえば Inductive で
Inductive X : Set := a | b.
とした場合は当然「a <> b」であって欲しいわけなのだが、「a」と「b」で結論が違うものをどうやって構成するかというと、奇妙なことに
Definition eq_a (x:X) := match x with a => True | b => False end.
でできるのである。この関数「eq_a」は「match」を使って引数が「a」だったら真を返し、「b」だったら偽を返す。
これを使って「a <> b」を証明する。
Lemma a_ne_b : a <> b. unfold not; intros. absurd (eq_a a). rewrite H. auto. unfold eq_a. trivial. Qed.
というわけで、Inductiveの場合はmatchが二つのコンストラクタを必ず区別するということから、等しくないことを証明できた。
一般の場合も、二つを区別する述語が存在すれば等しくないことを証明できる。
Variable Y : Set. Lemma neq : forall x y: Y, (exists P: Y->Prop, P x /\ ~P y) -> x <> y. intros. elim H. intros. unfold not. elim H0. intros. absurd (x0 x). rewrite H3. auto. auto. Qed.
というふうにだいたい上のと同じ。
Leibniz Equality の重要な性質は「x=y」を仮定すれば、ほかのところに現れる「x」を勝手に「y」に置き換えてもよいということである。
最初の証明は実は「inversion」を使えば勝手にできる。
