Coq
Menu Menu
Sequent Calculus
Sequent Calculus では、論理式を以下の形で使う。
仮定 |- 論理式
仮定は論理式で Context などと呼ばれる。
Γ |- Σ, P
というように左右に、任意の論理式が入ることもある。
推論規則
推論規則は、変形前と変形後の二つの式で表す。変形の条件が別にあることもある。
Γ |- Σ, P
---------------------
Γ |- Σ, P
なぜ、
|- Γ → Σ, P
ではだめなのかというと、だめなわけではなくて、
Γ |- Σ, P |- Γ → Σ, P
--------------------- ---------------------
|- Γ → Σ, P Γ |- Σ, P
という関係があります。deduction theorm などと呼ばれます。
Γ |- P Σ |- Q
--------------------- ∧ introduction
|- Γ,Σ → P ∧ Q
Γ |- P ∧ Q Γ |- P ∧ Q
------------------------ ------------------ ∧ elimnation (L,R)
Γ |- P Γ |- Q
Coq
Command line からなら、
/Applications/CoqIdE_8.4beta2.app/Contents/Resources/bin/coqtopCoq < Require Import ZArith.
period が最後に必要。
Prop.
Section で変数の宣言の準備をして、変数の宣言を行います。
Section hoge1. Variables (P Q R : Prop).: の後が型で、ここでは Prop 命題です。P Q R が Prop なことを Check で調べます。
Prop は Proposition (命題)という意味だけど、ここでは何かそういう名前の型。
Check P.P->Q なども Prop になります。命題論理式といいます。
Check P->Q. Check P->Q->P.P->Q->P は、P->(Q->P) のこと。3-2-1 が (3-2)-1 で、3-(2-1) とはならないのが普通だが、この場合は、この優先順位の方が便利だということがあとでわかる。
Coq のλ式
λ式は、変数を受け取ってなにか値を返す関数。
Variables (p:P) (q:Q).
Coq < Check (fun H:P => q).
fun _ : P => q
: P -> Q
fun H:P => q は、P という型を持つ値を変数Hで、(で、それを無視して) Q という型を持つ値 q を返す関数。
この場合の型を P->Q と書く。これは、命題論理式の形をしています。実際、これを命題論理式とみなして良いことが後でわかります。
実際に、この関数を評価したい時は、Eval compute in を使います。
Coq < Eval compute in (fun H:P => q) p.
= q
: Q
これを p に関数 (fun H:P=>q) を適用する(apply)と言います。
Curry 化
複数の引数を持つλ式は、以下のように書きます。
Coq < Check (fun (H:P) (H1:Q) => q).
fun (_ : P) (_ : Q) => q
: P -> Q -> Q
() は省略できないのが不思議ですが、この場合の型は P->Q->Q という式になります。
Coq < Eval compute in (fun (H:P) (H1:Q) => q) p q.
= q
: Q
引数を一つしか与えないと、
Coq < Eval compute in (fun (H:P) (H1:Q) => q) p .
= fun _ : Q => q
: Q -> Q
Q を受け取って q を返す関数を返します。
つまり、引数を複数持つ関数は、高階関数で表されるということなります。これを、Curry 化といいます。
高階関数はプログラミング言語では、closure で実現されることが多いです。
関数に名前を付ける
Coq < Definition f1 := fun (H:P) (H1:Q) => q .
f1 is defined
Coq < Check f1.
f1
: P -> Q -> Q
型を自分で与えることもできます。
Coq < Definition f2: P->Q->Q := fun (H:P) (H1:Q) => q .
f2 is defined
これを評価すると、
Coq < Eval compute in f2 p q.
= q
: Q
Coq < Eval compute in f2 p .
= fun _ : Q => q
: Q -> Q
となります。
Coq と命題論理
Coq では、証明はλ式に対応します。証明が終わると、それに対応するλ式が定義されます。証明するべき式を定義します。
Theorem hoge1 : P->Q->P.これを推論規則で変形していきます。変形には、tactics というコマンド使います。
intro
intro は、 以下の証明図に相当します。
Γ |- Σ, P
---------------------
|- Γ → Σ, P
Coq < Theorem hoge1 : P->Q->P.
1 subgoal
P : Prop
Q : Prop
R : Prop
============================
P -> Q -> P
hoge1 < intro.
1 subgoal
P : Prop
Q : Prop
R : Prop
H : P
============================
Q -> P
H というのが追加されて、P というのが仮定に入っていることがわかります。
もう一度、intro とすると、
hoge1 < intro.
1 subgoal
P : Prop
Q : Prop
R : Prop
H : P
H0 : Q
============================
P
となり、H0 に Q という仮定が入ります。残った P という goal は、H の仮定そのものです。仮定は、そのまま正しい。
---------------------
P, Σ |- P
そこで、仮定を使う assumption を入れると、
hoge1 < assumption.
No more subgoals.
これで証明が終わります。そこで、Qed とすると、証明が定義されます。
hoge1 < Qed.
intro.
intro.
assumption.
hoge1 is defined
Coq < Print hoge1.
hoge1 = fun (H : P) (_ : Q) => H
: P -> Q -> P
証明に対応するλ式
最後に定義された、
hoge1 = fun (H : P) (_ : Q) => H
: P -> Q -> P
は、fun (H : P) (_ : Q) => H が証明に対応しているλ式だということです。このように証明とλ式が対応しているのを、カーリーハワード対応と言います。
fun (H : P) (_ : Q) は、引数を二つ取り、最初の引数の型がP で、次の引数の型がQ だといういうことを表してます。H は引数の名前。_ は、とくに名前を付けない引数です。
戻り値は H ですが、これは P という型を持っています。
なので、このλ項は
P -> Q -> P
という型を持っています。そして、これが証明した式に対応します。なので、(型付)λ式の型は論式に対応します。
証明の例
Lemma hoge02 : (P->P)->(P->P).
intros.
assumption.
Qed.
この証明を
Print hoge02.
表示して得られるλ式は、
Eval compute in (hoge02 (fun H:P => p) p1).などと使うことができますが、それ自体には、特別な意味はありません。
intros と apply
Theorem hoge03: (P->Q)->(Q->R)->(P->R). intro H H' H''. intro H H'. intro H. intro . Undo. intros H H' H''.intros とすると、intro を複数適応してくれます。
使える assumption はありませんが、
1 subgoal
P : Prop
Q : Prop
R : Prop
p : P
q : Q
H : P -> Q
H0 : Q -> R
H1 : P
============================
R
H0: Q->R を使うと、Q という仮定が使えます。
apply H0. assumption. Qed.
例題
intro, intros, assumption, apply を使って、以下の式を証明し、対応するλ式を示せ。
Theorem imp_perm : (P->Q->R) -> (Q->P->R). Lemma ingore_Q : (P->R)->P->Q->R.
まとめ
Coq には Prop という型がある。
Section と Variable で変数を定義する。
fun でλ式を作る。
複数の引数を持つ関数をカーリー化で作る。
名前をつけた関数を定義する。
Check で型を調べる。
Eval compute で関数を適用する。
Theorem に intro, assumption , apply という tatctics を適用して証明する。
証明に対応するλ式を調べる。