24 December, 2010

[Coq] How to Find Unreachable Nodes

不正な状態遷移を見つけるアルゴリズム @ kencobaの日記経由。

答えを出すだけならこんなのでもOK? 元の問題の規模が判らないが、この程度に小さな問題なら auto で探索出来る。

Axiom O A B C D E F G H I:Prop.
Axiom OA : O -> A.
Axiom AB : A -> B.
Axiom BC : B -> C.
Axiom CB : C -> B.
Axiom CA : C -> A.
Axiom DB : D -> B.
Axiom DH : D -> H.
Axiom HD : D -> H.
Axiom EF : E -> F.
Axiom FG : F -> G.
Axiom GF : G -> F.
Axiom GE : G -> E.
Axiom II : I -> I.

Hint Resolve OA AB BC CB CA DB DH HD EF FG GF GE II.

Goal O -> A. info auto. Qed.
Goal O -> B. info auto. Qed.
Goal O -> C. info auto. Qed.


Goal O -> D.などはauto.で証明出来ないので、path が無いと判る。

[Coq] Coq Advent Calender : reflexivity (25 of 25)

 Coq でよく使われる tactic の紹介も今回で最後。最終回は reflexivity を紹介します。

 reflexivity はゴールが等式で、左辺と右辺の値が等しい時に使います。内容的には apply refl_equal. と同じです。refl_equal はこんな公理。

Inductive eq (A : Type) (x : A) : A -> Prop := refl_equal : x = x

 左辺と右辺が全く同じ形をしていないと等式は成り立ちません(が、reflexivity は内部的に simpl を実行しているので simpl で簡単化して等しくなる物は成立します)。

 ところで、同じ形というのはどこまで同じならば = が成り立つかというのは良く解らないので色々試してみました。

Coq < Definition f : nat -> nat := fun x => x.
Coq < Definition h : nat -> nat := fun y => y .
Coq < Goal f = h.
1 subgoal

============================
f = h

Unnamed_thm < simpl.
1 subgoal

============================
f = h

Unnamed_thm < unfold f.
1 subgoal

============================
(fun x : nat => x) = h

Unnamed_thm < unfold h.
1 subgoal

============================
(fun x : nat => x) = (fun y : nat => y)

Unnamed_thm < reflexivity.
Proof completed.

Unnamed_thm < Qed.

 これを見ると、(fun x : nat => x) = (fun y : nat => y) は成立するようです。同様に、

Coq < Goal forall P:nat->Prop, (forall n, P n) = (forall m, P m).
Unnamed_thm0 < intros P.
Unnamed_thm0 < reflexivity.
Proof completed.

 これを見ると、(forall n : nat, P n) = (forall m : nat, P m) も成立。

 上記の f, h の場合はreflexivityで等しい事が示せましたが、一般には関数が等しい事を reflexivity で証明する事は出来ません。 
 f, g : nat -> nat について、f = g ⇔ ∀n:nat, f n = g n. を以て等しいとする場合は、こんな感じで証明します。

Coq < Definition f : nat -> nat := fun x => x.

Coq < Fixpoint g(x:nat):nat :=
Coq < match x with
Coq < | O => O
Coq < | S n' => S (g n')
Coq < end.

Coq < Require Import Logic.FunctionalExtensionality.

Coq < Lemma Sample_of_reflexivity : f = g.
1 subgoal

============================
f = g

Sample_of_reflexivity < extensionality n.
1 subgoal

n : nat
============================
f n = g n

Sample_of_reflexivity < unfold f.
1 subgoal

n : nat
============================
n = g n

Sample_of_reflexivity < induction n.
2 subgoals

============================
0 = g 0

subgoal 2 is:
S n = g (S n)

Sample_of_reflexivity < reflexivity.
1 subgoal

n : nat
IHn : n = g n
============================
S n = g (S n)

Sample_of_reflexivity < simpl.
1 subgoal

n : nat
IHn : n = g n
============================
S n = S (g n)

Sample_of_reflexivity < rewrite <- IHn.
1 subgoal

n : nat
IHn : n = g n
============================
S n = S n

Sample_of_reflexivity < reflexivity.
Proof completed.

Sample_of_reflexivity < Qed.


 他にも、= を同値関係を以て定義する場合は Setoid というものを使って考える(Coqの型理論には集合論の商集合が無いので、代わりに = を同値関係で置き換えた物を使う)とか有るらしいのですが、そっちはちょっと調べきれませんでした。

ーーーーー

★後書き★

 Coq Advent Calender を始めるにあたっては、Coq Partyでのmaeda_さんの発表に有った「tactic使用例が有ると嬉しい」と「coqでの人気tactic」という話題からネタを頂きました。
 25個もあると自分では使った事の無いtacticとかもあって結構使い方を調べたり、あるいは適当な証明課題を探したりなど、それなりに大変で、何度か挫けそうになりましたがなんとか最後まで書けて良かったです。
 Coq を学ぶ人の参考になると良いなぁ。

23 December, 2010

[Coq] Coq Advent Calender : exact (24 of 25)

 Coq でよく使われる tactic の24番目は exact です。

 現在のゴールが、仮定のどれか、あるいは既存の定理にマッチする時に exact H?. とか exact my_theorem. とかするとゴールが証明されます。前者の場合は assumption. で済みますし、exact ではなく apply でもOKなんで、無理に使う必要は無いですが、ゴールと同じ物があったという意図を多少は示せるのかも。

 exact を使って書いてみました。

Coq < Lemma Sample_of_exact : forall n m, n + m = m + n.
1 subgoal

============================
forall n m : nat, n + m = m + n

Sample_of_exact < intros.
1 subgoal

n : nat
m : nat
============================
n + m = m + n

Sample_of_exact < induction n.
2 subgoals

m : nat
============================
0 + m = m + 0

subgoal 2 is:
S n + m = m + S n

Sample_of_exact < simpl.
2 subgoals

m : nat
============================
m = m + 0

subgoal 2 is:
S n + m = m + S n

Sample_of_exact < exact (plus_n_O m).
1 subgoal

n : nat
m : nat
IHn : n + m = m + n
============================
S n + m = m + S n

Sample_of_exact < simpl.
1 subgoal

n : nat
m : nat
IHn : n + m = m + n
============================
S (n + m) = m + S n

Sample_of_exact < rewrite IHn.
1 subgoal

n : nat
m : nat
IHn : n + m = m + n
============================
S (m + n) = m + S n

Sample_of_exact < exact (plus_n_Sm m n).
Proof completed.

Sample_of_exact < Qed.

22 December, 2010

[Link] Formal Methods Forum

 東京でほぼ毎月開催している形式手法の勉強会、Formal Methods Forum ですが、FMFのGoogle groupに登録して頂くと開催案内や開催日程相談のメールが配信されます。
 ATNDで告知しているのですが、Google groupに登録して頂いた方がより確実だと思います。

 活動内容ですが11月分についてはkencobaさんの日記なんかも参考にして頂けるといいかと。

[Coq] Coq Advent Calender : specialize (23 of 25)

 Coq でよく使われる tactic の23番目は specialize です。

 公理とかライブラリにある定理とか証明済み補題とかに特定の引数を適用した物を仮定に使いたい事があります。forall n, P n. みたいな補題Lのnに特定の値 n0 を代入した P n0 が仮定にあると良いなぁ、とか。
 勿論、assert(H:P n0)とかcut (P n0)とか書いても良いのですが、specialize (L n0). と書けば cut (P n0)してapply (L n0) するのと同じになり、証明が短く判りやすくなります。

replaceの説明の時と同じ定理を、replaceを使わず、specializeとrewriteを使って証明してみます。証明の前提と成る公理は replace の回を参照して下さい。

Coq < Theorem inv_r : forall a:G, a * (inv a) = 1.
1 subgoal

============================
forall a : G, a * inv a = 1

inv_r < intros.
1 subgoal

a : G
============================
a * inv a = 1

inv_r < specialize (id_l (a * inv a)).
1 subgoal

a : G
============================
1 * (a * inv a) = a * inv a -> a * inv a = 1

specializeすると、公理 id_l に (a * inv a) を適用した物が得られますので、intro して書き換えて消去します。あとは同様に。

inv_r < intro H; rewrite <- H; clear H.
1 subgoal

a : G
============================
1 * (a * inv a) = 1

inv_r < specialize (inv_l (inv a)); intro H; rewrite <- H; clear H.
1 subgoal

a : G
============================
inv (inv a) * inv a * (a * inv a) = inv (inv a) * inv a

inv_r < specialize (assoc (inv (inv a)) (inv a) (a * inv a)); intro H; rewrite H; clear H.
1 subgoal

a : G
============================
inv (inv a) * (inv a * (a * inv a)) = inv (inv a) * inv a

inv_r < specialize (assoc (inv a) a (inv a)); intro H; rewrite <- H; clear H.
1 subgoal

a : G
============================
inv (inv a) * (inv a * a * inv a) = inv (inv a) * inv a

inv_r < specialize (inv_l a); intro H; rewrite H; clear H.
1 subgoal

a : G
============================
inv (inv a) * (1 * inv a) = inv (inv a) * inv a

inv_r < specialize (id_l (inv a)); intro H; rewrite H; clear H.
1 subgoal

a : G
============================
inv (inv a) * inv a = inv (inv a) * inv a

inv_r < reflexivity.
Proof completed.

inv_r < Qed.

21 December, 2010

[Coq] Coq Advent Calender : left, right (21,22 of 25)

 Coqでよく使われる tactic の21,22番目は left と right です。
 最初に25個と決めて、でもよく考えると12/24で終了すべき。都合が良いのでここで2つ紹介して帳尻を合わせます。

 left は constructor 1 、right は constructor 2 の意味で、実は goal が A \/ B の場合に限らず、コンストラクタが2通りあってどちらかを明示的に指定したい時に使えます。
 大抵そういう場合は左右と対応している訳ですが、例えば nat とかも left が O を指すはず。同様に n:nat に対して destruct n ではなく split とかも使えるはず。単に他人に判りにくいだけですが。

 今回は sumbool について left, right を使う例です。やはり左右に対応しています。

Coq < Lemma Sample_of_left_right : forall n:nat, {n = 0} + {n <> 0}.
1 subgoal

============================
forall n : nat, {n = 0} + {n <> 0}

Sample_of_left_right < induction n.
2 subgoals

============================
{0 = 0} + {0 <> 0}

subgoal 2 is:
{S n = 0} + {S n <> 0}

Sample_of_left_right < left.
2 subgoals

============================
0 = 0

subgoal 2 is:
{S n = 0} + {S n <> 0}

Sample_of_left_right < reflexivity.
1 subgoal

n : nat
IHn : {n = 0} + {n <> 0}
============================
{S n = 0} + {S n <> 0}

Sample_of_left_right < right.
1 subgoal

n : nat
IHn : {n = 0} + {n <> 0}
============================
S n <> 0

Sample_of_left_right < intro.
1 subgoal

n : nat
IHn : {n = 0} + {n <> 0}
H : S n = 0
============================
False

Sample_of_left_right < inversion H.
Proof completed.

Sample_of_left_right < Qed.

20 December, 2010

[Coq] Coq Advent Calender : generalize (20 of 25)

 Coqでよく使われる tactic の20番目は generalize です。

 generalize は intro の逆で、具体的な値の term を、"forall t" のような形に戻します。
 簡単な使用例は下記の様なものです。

Coq < Lemma sample_of_generalize : forall x y, 0 <= x + y + y.
1 subgoal

============================
forall x y : nat, 0 <= x + y + y

sample_of_generalize < intros.
1 subgoal

x : nat
y : nat
============================
0 <= x + y + y

sample_of_generalize < generalize (x + y + y).
1 subgoal

x : nat
y : nat
============================
forall n : nat, 0 <= n

sample_of_generalize < Require Import Arith.Le.

sample_of_generalize < apply le_O_n.
Proof completed.

sample_of_generalize < Qed.


 単純に generalize で戻せない場合は、generalize dependent t のような形で使います。例えば下記の証明(TAPLの練習問題の証明)で使っています。よほど明らかな場合以外は、generalize dependentの形で使う事が多い様に思います。
 まず証明の前提の定義を幾つか。

Inductive term : Set :=
| TmTrue : term
| TmFalse : term
| TmIf : term -> term -> term -> term
| TmZero : term
| TmSucc : term -> term
| TmPred : term -> term
| TmIszero : term -> term.

Inductive nvalue : term -> Prop :=
| NvZero : nvalue TmZero
| NvSucc : forall t, nvalue t -> nvalue (TmSucc t).

Inductive bvalue : term -> Prop :=
| BvTrue : bvalue TmTrue
| BvFalse : bvalue TmFalse.

Definition value(t:term) : Prop := bvalue t \/ nvalue t.

Inductive eval : term -> term -> Prop :=
| EvIfTrue : forall t2 t3, eval (TmIf TmTrue t2 t3) t2
| EvIfFalse : forall t2 t3, eval (TmIf TmFalse t2 t3) t3
| EvIf : forall t1 t1' t2 t3, eval t1 t1' -> eval (TmIf t1 t2 t3) (TmIf t1' t2 t3)
| EvSucc : forall t1 t1', eval t1 t1' -> eval (TmSucc t1) (TmSucc t1')
| EvPred : forall t1 t1', eval t1 t1' -> eval (TmPred t1) (TmPred t1')
| EvPredZero : eval (TmPred TmZero) TmZero
| EvPredSucc : forall nv, nvalue nv -> eval (TmPred (TmSucc nv)) nv
| EvIszeroZero : eval (TmIszero TmZero) TmTrue
| EvIszeroSucc : forall nv, nvalue nv -> eval (TmIszero (TmSucc nv)) TmFalse
| EvIszero : forall t1 t1', eval t1 t1' -> eval (TmIszero t1) (TmIszero t1').

Notation "t1 --> t2" := (eval t1 t2) (at level 80, no associativity).

Definition normal_form (t : term) : Prop := ~ exists t', eval t t'.

 ここで下記の定理を証明します。intros を下記の様にすると予めdestructした形で intros 可能です。

Coq < Lemma value_is_normal_form : forall v, value v -> normal_form v.
1 subgoal

============================
forall v : term, value v -> normal_form v

value_is_normal_form < intros v [bv|nv] [t vEt].
2 subgoals

v : term
bv : bvalue v
t : term
vEt : v --> t
============================
False

subgoal 2 is:
False

value_is_normal_form < destruct bv; inversion vEt.
1 subgoal

v : term
nv : nvalue v
t : term
vEt : v --> t
============================
False

ここで t をgeneralize dependentします。(generalize t だと、forall t:term, にならずうまくいかない。)

value_is_normal_form < generalize dependent t.
1 subgoal

v : term
nv : nvalue v
============================
forall t : term, v --> t -> False

value_is_normal_form < induction nv.
2 subgoals

============================
forall t : term, TmZero --> t -> False

subgoal 2 is:
forall t0 : term, TmSucc t --> t0 -> False

value_is_normal_form < intros t zEt.
2 subgoals

t : term
zEt : TmZero --> t
============================
False

subgoal 2 is:
forall t0 : term, TmSucc t --> t0 -> False

value_is_normal_form < inversion zEt.
1 subgoal

t : term
nv : nvalue t
IHnv : forall t0 : term, t --> t0 -> False
============================
forall t0 : term, TmSucc t --> t0 -> False

value_is_normal_form < intros t0 stEt0.
1 subgoal

t : term
nv : nvalue t
IHnv : forall t0 : term, t --> t0 -> False
t0 : term
stEt0 : TmSucc t --> t0
============================
False

value_is_normal_form < inversion stEt0.
1 subgoal

t : term
nv : nvalue t
IHnv : forall t0 : term, t --> t0 -> False
t0 : term
stEt0 : TmSucc t --> t0
t1 : term
t1' : term
H0 : t --> t1'
H : t1 = t
H1 : TmSucc t1' = t0
============================
False

value_is_normal_form < elim (IHnv t1').
1 subgoal

t : term
nv : nvalue t
IHnv : forall t0 : term, t --> t0 -> False
t0 : term
stEt0 : TmSucc t --> t0
t1 : term
t1' : term
H0 : t --> t1'
H : t1 = t
H1 : TmSucc t1' = t0
============================
t --> t1'

value_is_normal_form < exact H0.
Proof completed.

value_is_normal_form < Qed.

19 December, 2010

[Coq] Coq Advent Calender : inversion (19 of 25)

 Coq でよく使われる tactic の19番目は inversion です。
 inversion は仮定に対して帰納的な定義を適用し、その仮定が成立する為の前提を導き出すか、あるいはそもそもそのような前提が存在しない(=仮定が間違っている)ので証明終了、を導いてくれます。ある種の証明では inversion を使うと証明が非常に簡単なのですが、中で何をしているのかは簡単には説明するのは難しいです。

 inversionの使用例というと典型的にはこの関数を定義することになっています。

Coq < Inductive even : nat -> Prop :=
Coq < | EvenO : even O
Coq < | EvenSS : forall n, even n -> even (S (S n)).
even is defined
even_ind is defined

偶数である事を、上記の様に帰納的に定義します。

 では3が偶数でない事を証明しましょう。こういう定理の証明の時にはinversionが有用です。今回はinversionの中で何をしているかみたいのでinfo inversionとして使っています。

Coq < Lemma Sample_of_inversion : ~(even 3).
1 subgoal

============================
~ even 3

Sample_of_inversion < intro.
1 subgoal

H : even 3
============================
False

Sample_of_inversion < info inversion H.
== assert (H0:3 = 3 -> False).
refine match H in (even n) return (n = 3 -> False) with
| EvenO => _
| EvenSS x x0 => _ x x0
end.
intro H0; refine ((_:0 = 3 -> False) H0); clear H0;
intro H0; cut False;[intro H1|idtac].
refine ((_:False -> False) H1); clear H1; intro H1;
exact (False_ind False H1).

exact (eq_ind 0
(fun e : nat => match e with
| 0 => True
| S _ => False
end) I 3 H0).

intro n; intro H0; intro H1; refine ((_:even n -> False) H0);
clear H0; refine ((_:S (S n) = 3 -> even n -> False) H1);
clear H1; intro H1;
cut (n = 1);[intro H0|idtac].
refine ((_:n = 1 -> even n -> False) H0); clear H0;
intro H0;
refine (eq_ind 1 (fun n : nat => even n -> False) _ n _).
clear H1; intro H1; dependent move H1 after H0.

refine (sym_eq _);
exact H0.

exact (f_equal
(fun e : nat =>
match e with
| 0 => n
| 1 => n
| S (S n) => n
end) H1).

refine (H0 _); change (3 = 3); exact (refl_equal 3).

1 subgoal

H : even 3
n : nat
H1 : even 1
H0 : n = 1
============================
False

 H: even 3の前提にH1: even 1が前提である事が判りました。このH1について再度inversionを使います。

Sample_of_inversion < info inversion H1.
== assert (H2:1 = 1 -> False).
refine match H1 in (even n) return (n = 1 -> False) with
| EvenO => _
| EvenSS x x0 => _ x x0
end.
intro H2; refine ((_:0 = 1 -> False) H2); clear H2;
intro H2; cut False;[intro H3|idtac].
refine ((_:False -> False) H3); clear H3; intro H3;
exact (False_ind False H3).

exact (eq_ind 0
(fun e : nat => match e with
| 0 => True
| S _ => False
end) I 1 H2).

intro n0; intro H2; intro H3; refine ((_:even n0 -> False) H2);
clear H2; refine ((_:S (S n0) = 1 -> even n0 -> False) H3);
clear H3; intro H3;
cut False;[intro H2|idtac].
refine ((_:False -> even n0 -> False) H2); clear H2;
intro H2;
exact (False_ind (even n0 -> False) H2).

exact (eq_ind (S (S n0))
(fun e : nat =>
match e with
| 0 => False
| 1 => False
| S (S _) => True
end) I 1 H3).

refine (H2 _); change (1 = 1); exact (refl_equal 1).

Proof completed.

Sample_of_inversion < Qed.

H1を成立させる前提が無いので、証明完了になります。

 あと、inversionが役に立つ例というとsmall-stepの決定性の証明とかです。


Coq < Inductive term : Set :=
Coq < | TmTrue : term
Coq < | TmFalse : term
Coq < | TmIf : term -> term -> term -> term.
term is defined
term_rect is defined
term_ind is defined
term_rec is defined


Coq < Inductive eval : term -> term -> Prop :=
Coq < | EvIfTrue : forall t2 t3, eval (TmIf TmTrue t2 t3) t2
Coq < | EvIfFalse : forall t2 t3, eval (TmIf TmFalse t2 t3) t3
Coq < | EvIf : forall t1 t1' t2 t3, eval t1 t1' ->
Coq < eval (TmIf t1 t2 t3) (TmIf t1' t2 t3).
eval is defined
eval_ind is defined

上記の様にsmall-stepの規則を定義して、下記を証明します。

Coq < Theorem eval_deterministic : forall t t' t'', (eval t t') -> (eval t t'') -> (t' = t'').
1 subgoal

============================
forall t t' t'' : term, eval t t' -> eval t t'' -> t' = t''

eval_deterministic < intros t t' t'' tEt' tEt''.
1 subgoal

t : term
t' : term
t'' : term
tEt' : eval t t'
tEt'' : eval t t''
============================
t' = t''

まず tEt' について induction で場合分けをします。

eval_deterministic < induction tEt' as [t2 t3|t2 t3|t1 t1' t2 t3 t1Et1'] in t'', tEt'' |-*.
3 subgoals

t'' : term
t2 : term
t3 : term
tEt'' : eval (TmIf TmTrue t2 t3) t''
============================
t2 = t''

subgoal 2 is:
t3 = t''
subgoal 3 is:
TmIf t1' t2 t3 = t''

最初の場合は、t' = TmIf TmTrue t2 t3 の場合です。ここで tEt'' については induction ではなくinversion を使うと、tEt'' が成立するような t'' の場合分けを自動で行ってくれます。

eval_deterministic < inversion tEt'' as [t2_ t3_| t2_ t3_| t1_ t1'_ t2_ t3_ t1Et1'_].
4 subgoals

t'' : term
t2 : term
t3 : term
tEt'' : eval (TmIf TmTrue t2 t3) t''
t2_ : term
t3_ : term
H0 : t2_ = t2
H1 : t3_ = t3
H2 : t2 = t''
============================
t'' = t''

subgoal 2 is:
t2 = TmIf t1'_ t2 t3
subgoal 3 is:
t3 = t''
subgoal 4 is:
TmIf t1' t2 t3 = t''

eval_deterministic < reflexivity.
3 subgoals

t'' : term
t2 : term
t3 : term
tEt'' : eval (TmIf TmTrue t2 t3) t''
t1_ : term
t1'_ : term
t2_ : term
t3_ : term
t1Et1'_ : eval TmTrue t1'_
H : t1_ = TmTrue
H1 : t2_ = t2
H2 : t3_ = t3
H0 : TmIf t1'_ t2 t3 = t''
============================
t2 = TmIf t1'_ t2 t3

subgoal 2 is:
t3 = t''
subgoal 3 is:
TmIf t1' t2 t3 = t''

 ここでinversion t1Et1'_を行います。TmTrueが何かにevalされる規則はevalに無いので、仮定が不成立となり、goalの証明が終わります。

eval_deterministic < inversion t1Et1'_.
2 subgoals

t'' : term
t2 : term
t3 : term
tEt'' : eval (TmIf TmFalse t2 t3) t''
============================
t3 = t''

subgoal 2 is:
TmIf t1' t2 t3 = t''

 t' = TmIfFalse t2 t3 の場合は同様の証明をすればOKです。

eval_deterministic < inversion tEt'' as [t2_ t3_| t2_ t3_| t1_ t1'_ t2_ t3_ t1Et1'_].
eval_deterministic < reflexivity.
eval_deterministic < inversion t1Et1'_.
1 subgoal

t'' : term
t1 : term
t1' : term
t2 : term
t3 : term
t1Et1' : eval t1 t1'
tEt'' : eval (TmIf t1 t2 t3) t''
IHt1Et1' : eval t1 t'' -> t1' = t''
============================
TmIf t1' t2 t3 = t''

 最後は、t' = TmIf t1 t2 t3 の場合についてです。やはりtEt''についてinversionします。

eval_deterministic < inversion tEt'' as [t2_ t3_| t2_ t3_| t1_ t1'_ t2_ t3_ t1Et1'_].
3 subgoals

t'' : term
t1 : term
t1' : term
t2 : term
t3 : term
t1Et1' : eval t1 t1'
tEt'' : eval (TmIf t1 t2 t3) t''
IHt1Et1' : eval t1 t'' -> t1' = t''
t2_ : term
t3_ : term
H0 : TmTrue = t1
H1 : t2_ = t2
H2 : t3_ = t3
H3 : t2 = t''
============================
TmIf t1' t'' t3 = t''

subgoal 2 is:
TmIf t1' t2 t'' = t''
subgoal 3 is:
TmIf t1' t2 t3 = TmIf t1'_ t2 t3

 ここでも、H0とt1Et1'から、eval TmTrue t1'を作ってinversionして仮定が成立しない事を使って証明します。

eval_deterministic < rewrite <- H0 in t1Et1'.
3 subgoals

t'' : term
t1 : term
t1' : term
t2 : term
t3 : term
t1Et1' : eval TmTrue t1'
tEt'' : eval (TmIf t1 t2 t3) t''
IHt1Et1' : eval t1 t'' -> t1' = t''
t2_ : term
t3_ : term
H0 : TmTrue = t1
H1 : t2_ = t2
H2 : t3_ = t3
H3 : t2 = t''
============================
TmIf t1' t'' t3 = t''

subgoal 2 is:
TmIf t1' t2 t'' = t''
subgoal 3 is:
TmIf t1' t2 t3 = TmIf t1'_ t2 t3

eval_deterministic < inversion t1Et1'.
2 subgoals

t'' : term
t1 : term
t1' : term
t2 : term
t3 : term
t1Et1' : eval t1 t1'
tEt'' : eval (TmIf t1 t2 t3) t''
IHt1Et1' : eval t1 t'' -> t1' = t''
t2_ : term
t3_ : term
H0 : TmFalse = t1
H1 : t2_ = t2
H2 : t3_ = t3
H3 : t3 = t''
============================
TmIf t1' t2 t'' = t''

subgoal 2 is:
TmIf t1' t2 t3 = TmIf t1'_ t2 t3

 同様にして、TmFalse の場合も証明出来ます。

eval_deterministic < rewrite <- H0 in t1Et1'.
eval_deterministic < inversion t1Et1'.
1 subgoal

t'' : term
t1 : term
t1' : term
t2 : term
t3 : term
t1Et1' : eval t1 t1'
tEt'' : eval (TmIf t1 t2 t3) t''
IHt1Et1' : forall t'' : term, eval t1 t'' -> t1' = t''
t1_ : term
t1'_ : term
t2_ : term
t3_ : term
t1Et1'_ : eval t1 t1'_
H0 : t1_ = t1
H1 : t2_ = t2
H2 : t3_ = t3
H3 : TmIf t1'_ t2 t3 = t''
============================
TmIf t1' t2 t3 = TmIf t1'_ t2 t3

最後はIHt1Et1'のt''をt1'_にして、t1Et1'_と組み合わせてゴールを導きます。

eval_deterministic < rewrite (IHt1Et1' t1'_ t1Et1'_).
eval_deterministic < reflexivity.
Proof completed.

eval_deterministic < Qed.

18 December, 2010

[Coq] Coq Advent Calender : clear (18 of 25)

 Coq でよく使われる tactic の18番目は clear です...って使わないと思うけどなぁ。

 clear Hとすると、仮定 H が消えます。下記の様な感じです。

Coq < Lemma Sample_of_clear : forall A B C, (A->B->C)->(A->B)->A->C.
1 subgoal

============================
forall A B C : Type, (A -> B -> C) -> (A -> B) -> A -> C

Sample_of_clear < intros A B C abc ab a.
1 subgoal

A : Type
B : Type
C : Type
abc : A -> B -> C
ab : A -> B
a : A
============================
C

Sample_of_clear < apply abc; clear abc.
2 subgoals

A : Type
B : Type
C : Type
ab : A -> B
a : A
============================
A

subgoal 2 is:
B

Sample_of_clear < exact a.
1 subgoal

A : Type
B : Type
C : Type
ab : A -> B
a : A
============================
B

Sample_of_clear < apply ab; clear ab.
1 subgoal

A : Type
B : Type
C : Type
a : A
============================
A

Sample_of_clear < exact a.
Proof completed.

Sample_of_clear < Qed.

 使い終わって不要になった仮定をclearで消すと多少見通しが良くなる事もありますが、あまり使わないのではないかなぁ。

 むしろ、各種 tactic の中で内部的に使われる事が多い様な気がします。例えば下記の簡単な tactic の swap の中で使われています。apply して一回使った仮定は不要なので clear で消しているようです。

Ltac swap H :=
idtac "swap is OBSOLETE: use contradict instead.";
intro; apply H; clear H.

 これを使った証明です。

Coq < Lemma Sample_of_claer : forall P, ~~~P -> ~P.
1 subgoal

============================
forall P : Prop, ~ ~ ~ P -> ~ P

Sample_of_claer < intros.
1 subgoal

P : Prop
H : ~ ~ ~ P
============================
~ P

Sample_of_claer < swap H.
swap is OBSOLETE: use contradict instead.
1 subgoal

P : Prop
H0 : P
============================
~ ~ P

Sample_of_claer < swap H.
swap is OBSOLETE: use contradict instead.
1 subgoal

P : Prop
H0 : P
============================
P

Sample_of_claer < exact H0.
Proof completed.

Sample_of_claer < Qed.
intros.
swap H.
swap ipattern:H.
exact H0.

Sample_of_claer is defined

Coq <

17 December, 2010

[Coq] Coq Advent Calender : elim (17 of 25)

 Coq でよく使われる tactic の17番目は elim です。

 elim はほとんど induction と同じ事が出来ます。例えばこんな感じ。帰納法の仮定を自分で intro する必要があるのが違います。

Coq < Lemma Sample_of_elim : forall n, n + 0 = n.
1 subgoal

============================
forall n : nat, n + 0 = n

Sample_of_elim < intros.
1 subgoal

n : nat
============================
n + 0 = n

Sample_of_elim < elim n.
2 subgoals

n : nat
============================
0 + 0 = 0

subgoal 2 is:
forall n0 : nat, n0 + 0 = n0 -> S n0 + 0 = S n0

Sample_of_elim <


 ただこうやって帰納法で使うときはinductionする方が多い様にも思います。(golfだとelimが有利なのかな?)

 下記の様にゴールが False で、仮定が ~P の形をしている時は、私は習慣で他のタクティックではなく elim を使います。こんな感じ。

Coq < Lemma Sample_of_elim' : forall P, ~~(P \/ ~P).
1 subgoal

============================
forall P : Prop, ~ ~ (P \/ ~ P)

Sample_of_elim' < intros.
1 subgoal

P : Prop
============================
~ ~ (P \/ ~ P)

Sample_of_elim' < intro npnp.
1 subgoal

P : Prop
npnp : ~ (P \/ ~ P)
============================
False

Sample_of_elim' < elim npnp.
1 subgoal

P : Prop
npnp : ~ (P \/ ~ P)
============================
P \/ ~ P

Sample_of_elim' < right.
1 subgoal

P : Prop
npnp : ~ (P \/ ~ P)
============================
~ P

Sample_of_elim' < intro p.
1 subgoal

P : Prop
npnp : ~ (P \/ ~ P)
p : P
============================
False

Sample_of_elim' < elim npnp.
1 subgoal

P : Prop
npnp : ~ (P \/ ~ P)
p : P
============================
P \/ ~ P

Sample_of_elim' < left.
1 subgoal

P : Prop
npnp : ~ (P \/ ~ P)
p : P
============================
P

Sample_of_elim' < exact p.
Proof completed.

Sample_of_elim' < Qed.
intros.
intro npnp.
elim npnp.
right.
intro p.
elim npnp.
left.
exact p.

Sample_of_elim' is defined

Coq <

16 December, 2010

[Coq] Coq Advent Calender : ring (16 of 25)

 Coq でよく使われる tactic の16番目は ring です。

 ring は可換な半環 ( 演算 +, * があって、それぞれ単位元 0, 1 があって、それぞれ交換則と結合則が成り立って、分配法則があってな数学的構造)での計算を行ってくれます。基本的には多項式の掛け算を展開し、標準形に直して比較するようなことをします。
 使用するにはRequire Import Ring.が必要です。

 下記で色々試してみましたが、適宜 rewrite, replace なども併用しないとうまくいきませんでした。


Coq < Require Import ZArith Ring.

Coq < Open Scope Z_scope.

Coq < Lemma Sample_of_ring : forall a b:Z, a + b = 7 -> a * b = 12 -> a^2 + b^2 = 25.
1 subgoal

============================
forall a b : Z, a + b = 7 -> a * b = 12 -> a ^ 2 + b ^ 2 = 25

Sample_of_ring < intros a b H1 H2.
1 subgoal

a : Z
b : Z
H1 : a + b = 7
H2 : a * b = 12
============================
a ^ 2 + b ^ 2 = 25

Sample_of_ring < replace (a^2 + b^2) with ((a+b)^2 - 2*a*b) by ring.
1 subgoal

a : Z
b : Z
H1 : a + b = 7
H2 : a * b = 12
============================
(a + b) ^ 2 - 2 * a * b = 25

Sample_of_ring < rewrite H1.
1 subgoal

a : Z
b : Z
H1 : a + b = 7
H2 : a * b = 12
============================
7 ^ 2 - 2 * a * b = 25

Sample_of_ring < replace (2*a*b) with (2*12) by ring [H2].
1 subgoal

a : Z
b : Z
H1 : a + b = 7
H2 : a * b = 12
============================
7 ^ 2 - 2 * 12 = 25

Sample_of_ring < reflexivity.
Proof completed.

Sample_of_ring < Qed.

15 December, 2010

[Coq] Coq Advent Calender : case (15 of 25)

 Coq でよく使われる tactic の15番目は case です。

 帰納的な型について自動で場合分けをしてくれるという意味では、13番目のinductionと同じですが、inductionと違って単に場合分けを行うだけで帰納法の仮定とかは作ってくれません。

 今回は3値論理を定義してみます。帰納的な bool3 という型を定義し、それらに対する否定、論理積、論理和を定義します。

Coq < Inductive bool3 : Set := yes | maybe | no.
bool3 is defined
bool3_rect is defined
bool3_ind is defined
bool3_rec is defined

Coq < Definition not3(b:bool3) :=
Coq < match b with
Coq < | yes => no
Coq < | maybe => maybe
Coq < | no => yes
Coq < end.
not3 is defined

Coq < Definition and3(a b:bool3) :=
Coq < match a,b with
Coq < | yes,yes => yes
Coq < | no, _ => no
Coq < | _, no => no
Coq < | _,_ => maybe
Coq < end.
and3 is defined

Coq < Definition or3(a b:bool3) :=
Coq < match a,b with
Coq < | no,no => no
Coq < | yes,_ => yes
Coq < | _,yes => yes
Coq < | _,_ => maybe
Coq < end.
or3 is defined

Coq <

 では、bool3 における簡単な証明をしてみます。a, b についての場合分けを行うのに case タクティックを使用します。下記の例では case でゴールが増えるのを示したいので個別に case を使っていますが、普通は
case a; case b; reflexivity.
で一行で9通りの場合分けを実施して終了とするでしょう。

Coq < Lemma Sample_of_case : forall a b:bool3,
Coq < not3 (or3 a b) = and3 (not3 a) (not3 b).
1 subgoal

============================
forall a b : bool3, not3 (or3 a b) = and3 (not3 a) (not3 b)

Sample_of_case < intros a b.
1 subgoal

a : bool3
b : bool3
============================
not3 (or3 a b) = and3 (not3 a) (not3 b)

Sample_of_case < case a.
3 subgoals

a : bool3
b : bool3
============================
not3 (or3 yes b) = and3 (not3 yes) (not3 b)

subgoal 2 is:
not3 (or3 maybe b) = and3 (not3 maybe) (not3 b)
subgoal 3 is:
not3 (or3 no b) = and3 (not3 no) (not3 b)

Sample_of_case < case b.
5 subgoals

a : bool3
b : bool3
============================
not3 (or3 yes yes) = and3 (not3 yes) (not3 yes)

subgoal 2 is:
not3 (or3 yes maybe) = and3 (not3 yes) (not3 maybe)
subgoal 3 is:
not3 (or3 yes no) = and3 (not3 yes) (not3 no)
subgoal 4 is:
not3 (or3 maybe b) = and3 (not3 maybe) (not3 b)
subgoal 5 is:
not3 (or3 no b) = and3 (not3 no) (not3 b)

Sample_of_case < reflexivity.
4 subgoals

a : bool3
b : bool3
============================
not3 (or3 yes maybe) = and3 (not3 yes) (not3 maybe)

subgoal 2 is:
not3 (or3 yes no) = and3 (not3 yes) (not3 no)
subgoal 3 is:
not3 (or3 maybe b) = and3 (not3 maybe) (not3 b)
subgoal 4 is:
not3 (or3 no b) = and3 (not3 no) (not3 b)

Sample_of_case < reflexivity.
3 subgoals

a : bool3
b : bool3
============================
not3 (or3 yes no) = and3 (not3 yes) (not3 no)

subgoal 2 is:
not3 (or3 maybe b) = and3 (not3 maybe) (not3 b)
subgoal 3 is:
not3 (or3 no b) = and3 (not3 no) (not3 b)

Sample_of_case < reflexivity.
2 subgoals

a : bool3
b : bool3
============================
not3 (or3 maybe b) = and3 (not3 maybe) (not3 b)

subgoal 2 is:
not3 (or3 no b) = and3 (not3 no) (not3 b)

Sample_of_case < case b; reflexivity.
1 subgoal

a : bool3
b : bool3
============================
not3 (or3 no b) = and3 (not3 no) (not3 b)

Sample_of_case < case b; reflexivity.
Proof completed.

Sample_of_case < Qed.

14 December, 2010

[Coq] Coq Advent Calender : split (14 of 25)

 Coq でよく使われる tactic の14番目は split です。...そんなに使うかなぁ?

 split はゴールが P /\ Q の形をしている時に、二つのゴール P, Q に分割します。あとはそれぞれを別々に証明すればOKです。

 簡単な例を下記に示します。

Coq < Lemma Sample_of_split : forall A B C:Prop, A /\ (B /\ C) -> (A /\ B) /\ C.
1 subgoal

============================
forall A B C : Prop, A /\ B /\ C -> (A /\ B) /\ C

Sample_of_split < intros A B C abc.
1 subgoal

A : Prop
B : Prop
C : Prop
abc : A /\ B /\ C
============================
(A /\ B) /\ C

Sample_of_split < destruct abc as [a [b c]].
1 subgoal

A : Prop
B : Prop
C : Prop
a : A
b : B
c : C
============================
(A /\ B) /\ C

Sample_of_split < split.
2 subgoals

A : Prop
B : Prop
C : Prop
a : A
b : B
c : C
============================
A /\ B

subgoal 2 is:
C

Sample_of_split < split.
3 subgoals

A : Prop
B : Prop
C : Prop
a : A
b : B
c : C
============================
A

subgoal 2 is:
B
subgoal 3 is:
C

Sample_of_split < assumption.
2 subgoals

A : Prop
B : Prop
C : Prop
a : A
b : B
c : C
============================
B

subgoal 2 is:
C

Sample_of_split < assumption.
1 subgoal

A : Prop
B : Prop
C : Prop
a : A
b : B
c : C
============================
C

Sample_of_split < assumption.
Proof completed.

Sample_of_split < Qed.

13 December, 2010

[Coq] Coq Advent Calender : induction (13 of 25)

 Coq でよく使われる tactic の13番目は induction です。

 Coq は帰納的な型を定義すると、その型に対する帰納法を自動で定義してくれます。例えば

Inductive nat : Set :=
O : nat
| S : nat -> nat

という自然数natに対して、

forall P : nat -> Prop,
P 0 ->
(forall n : nat, P n -> P (S n)) ->
forall n : nat, P n

というnat_indを定義してくれます。これを使って、自然数nについての帰納法の証明の時に、

  • n=0 の場合のゴール
  • nの時成り立つという仮定IHnと、S nの場合のゴール

を作ってくれます。同様にリストであれば、nilとconsの場合などです。

 今までにも何度か induction を使った証明を示してきましたが、今回も簡単な例を。

Coq < Lemma plus_comm : forall n m, n + m = m + n.
1 subgoal

============================
forall n m : nat, n + m = m + n

plus_comm < induction n.
2 subgoals

============================
forall m : nat, 0 + m = m + 0

subgoal 2 is:
forall m : nat, S n + m = m + S n

plus_comm < intro m.
2 subgoals

m : nat
============================
0 + m = m + 0

subgoal 2 is:
forall m : nat, S n + m = m + S n

plus_comm < simpl.
2 subgoals

m : nat
============================
m = m + 0

subgoal 2 is:
forall m : nat, S n + m = m + S n

plus_comm < erewrite <- plus_n_O.
2 subgoals

m : nat
============================
m = m

subgoal 2 is:
forall m : nat, S n + m = m + S n

plus_comm < reflexivity.
1 subgoal

n : nat
IHn : forall m : nat, n + m = m + n
============================
forall m : nat, S n + m = m + S n

plus_comm < intro m.
1 subgoal

n : nat
IHn : forall m : nat, n + m = m + n
m : nat
============================
S n + m = m + S n

plus_comm < simpl.
1 subgoal

n : nat
IHn : forall m : nat, n + m = m + n
m : nat
============================
S (n + m) = m + S n

plus_comm < erewrite <- plus_n_Sm.
1 subgoal

n : nat
IHn : forall m : nat, n + m = m + n
m : nat
============================
S (n + m) = S (m + n)

plus_comm < erewrite IHn.
1 subgoal

n : nat
IHn : forall m : nat, n + m = m + n
m : nat
============================
S (m + n) = S (m + n)

plus_comm < reflexivity.
Proof completed.

plus_comm < Qed.

12 December, 2010

[Coq] Coq Advent Calender : replace (12 of 25)

Coq でよく使われる tactic の12番目は replace です。

 replace t1 with t2 とすると、t2 = t1 という等式をsubgoalに追加し、t2 = t1 を用いてゴールの書き換えを行います。書き換え規則 t2 = t1 の証明を先送りにすることで本筋の証明の見通しがよくなります。また、simpl, unfold, rewriteを使う場合とかで、「ゴールのこの部分だけ書き換えたいのだが別のところも書き換えられてしまう」と悩む場面もありますが、そういうときは replace でとりあえず部分的に書き換え、あとでその箇所の書き換えを証明すると楽です。

 replace を多用するのは、等式変形を繰り返す場合です。今回はそういう例を。
 下記の様に群 G を定義してみます。

Coq < Axiom G : Set. (* 群G *)
Coq < Axiom G_dec : forall a b:G, {a=b} + {a <> b}. (* 単位元や逆元の一意性とかを示す時に必要 *)
Coq < Axiom mult : G -> G -> G. (* 乗法 *)
Coq < Notation "a * b" := (mult a b). (* 記号 * で書ける様にする *)
Coq < Axiom assoc : forall a b c:G, (a * b) * c = a * (b * c). (* 結合則 *)
Coq < Axiom G1 : G. (* 単位元 *)
Coq < Notation "1" := G1. (* 記号 1 で書ける様にする *)
Coq < Axiom id_l : forall a:G, 1 * a = a. (* 左単位元である *)
Coq < Axiom inv : G -> G. (* 逆元 *)
Coq < Axiom inv_l : forall a:G, (inv a) * a = 1. (* 左逆元 *)


 では、左逆元は右逆元でもあることを証明してみます。長くなるのでゴールを示すのは要所要所だけです。replaceを使うと、subgoalが増えているのが判ります。

Coq < Theorem inv_r : forall a:G, a * (inv a) = 1.
inv_r < intros.
1 subgoal

a : G
============================
a * inv a = 1

inv_r < replace (a * inv a) with (1 * a * inv a).
2 subgoals

a : G
============================
1 * a * inv a = 1

subgoal 2 is:
1 * a * inv a = a * inv a

inv_r < replace (1 * a * inv a) with ((inv (inv a) * (inv a)) * a * inv a).
3 subgoals

a : G
============================
inv (inv a) * inv a * a * inv a = 1

subgoal 2 is:
inv (inv a) * inv a * a * inv a = 1 * a * inv a
subgoal 3 is:
1 * a * inv a = a * inv a

inv_r < replace (inv (inv a) * inv a * a * inv a) with (inv (inv a) * (inv a * a) * inv a).
4 subgoals

a : G
============================
inv (inv a) * (inv a * a) * inv a = 1

subgoal 2 is:
inv (inv a) * (inv a * a) * inv a = inv (inv a) * inv a * a * inv a
subgoal 3 is:
inv (inv a) * inv a * a * inv a = 1 * a * inv a
subgoal 4 is:
1 * a * inv a = a * inv a

inv_r < rewrite inv_l. (* ここからは replace を使わなくても rewrite で簡単に変形出来る *)
inv_r < rewrite assoc.
inv_r < rewrite id_l.
inv_r < rewrite inv_l.
4 subgoals

a : G
============================
1 = 1

subgoal 2 is:
inv (inv a) * (inv a * a) * inv a = inv (inv a) * inv a * a * inv a
subgoal 3 is:
inv (inv a) * inv a * a * inv a = 1 * a * inv a
subgoal 4 is:
1 * a * inv a = a * inv a

inv_r < reflexivity. (* メインゴールの証明完了。残りは replace の書き換えの証明 *)
3 subgoals

a : G
============================
inv (inv a) * (inv a * a) * inv a = inv (inv a) * inv a * a * inv a

subgoal 2 is:
inv (inv a) * inv a * a * inv a = 1 * a * inv a
subgoal 3 is:
1 * a * inv a = a * inv a

inv_r < rewrite <- assoc; reflexivity.
2 subgoals

a : G
============================
inv (inv a) * inv a * a * inv a = 1 * a * inv a

subgoal 2 is:
1 * a * inv a = a * inv a

inv_r < erewrite inv_l; reflexivity.
1 subgoal

a : G
============================
1 * a * inv a = a * inv a

inv_r < rewrite assoc; rewrite id_l; reflexivity.
Proof completed.

inv_r < Qed.
intros.
replace (a * inv a) with (1 * a * inv a) .
replace (1 * a * inv a) with (inv (inv a) * inv a * a * inv a) .
replace (inv (inv a) * inv a * a * inv a) with
(inv (inv a) * (inv a * a) * inv a) .
rewrite inv_l in |- *.
rewrite assoc in |- *.
rewrite id_l in |- *.
rewrite inv_l in |- *.
reflexivity.

rewrite <- assoc in |- *; reflexivity.

erewrite inv_l in |- *; reflexivity.

rewrite assoc in |- *; rewrite id_l in |- *; reflexivity.

inv_r is defined

Coq <

11 December, 2010

[Coq] Coq Advent Calender : exists (11 of 25)

 Coq でよく使われる tactic の11番目は exists です。
 証明のゴールが exists x, P x とか { n:nat | isPrime n } とか、ある性質を満たす要素が存在することを求めている時に、「具体的に」その要素を与えてゴールを変形します。

 下記は exists を使う簡単な例です。mの具体的な値としてS n = n+1 を与えています。具体的なmを何か与えないとomegaでの自動証明は通りません。

Coq < Require Import Omega.

Coq < Lemma Sample_of_exists : forall n, exists m, n < m.
1 subgoal

============================
forall n : nat, exists m : nat, n < m

Sample_of_exists < intros.
1 subgoal

n : nat
============================
exists m : nat, n < m

Sample_of_exists < exists (S n).
1 subgoal

n : nat
============================
n < S n

Sample_of_exists < omega.
Proof completed.

Sample_of_exists < Qed.
intros.
exists (S n).
omega.

Sample_of_exists is defined
Coq <

10 December, 2010

[TAPL][OCaml] Untyped Lambda Calculus Interpreter

 TAPLのChap.5を読むのに型無しλ計算のインタプリタが無いかなと探していたところ下記を見つけました。(...まぁそもそもそのくらい自分で作れよ、という話はあるんだが)

http://www.cs.ru.nl/~freek/notes/lambda.ml

ページの内容を lambda.ml として保存し、

$ ocaml
# #use "lambda.ml";;

で読み込まれるので、あとは下記の様に試すだけ。

# nf "(^x.fx)a";;
- : term = term "fa"
# nf "(KISS)(KISS)";;
- : term = term "^yzz'.zz'(yzz')"
# red_gk all "SKK";;
- : term list =
[term "SKK"; term "(^yz.Kz(yz))K"; term "^z.(^y.z)(Kz)"; term "^z.z"]
# red 7 "(^x.xx)(^x.xx)";;
- : term list =
[term "(^x.xx)^x.xx"; term "(^x.xx)^x.xx"; term "(^x.xx)^x.xx";
term "(^x.xx)^x.xx"; term "(^x.xx)^x.xx"; term "(^x.xx)^x.xx";
term "(^x.xx)^x.xx"; term "..."]
#

手計算に自信が無い時に使うといいかなー。

[Coq] Coq Advent Calender : unfold (10 of 25)

 Coq でよく使われる tactic の10番目は unfold です。unfold は関数定義を展開します。
 unfold だけで使う場合も有りますが、fold と組み合わせて使う事もあります。fold は展開された関数を元に戻します。unfold して、simpl とか rewrite とかして、また fold して戻すと式が良い具合に変形されている場合があります。ここではそういう例を見てみましょう。

 まず、sum n := 1 + 2 + ... + nという関数を定義します。

Coq < Fixpoint sum n :=
Coq < match n with
Coq < | O => O
Coq < | S n' => S n' + sum n'
Coq < end.
sum is recursively defined (decreasing on 1st argument)

 次に、sum n = 1/2 * n * (n + 1) であることを証明したいのですが、割り算が入ると面倒ですから、次の定理を証明する事にします。今回は環に関する自動証明器の ring を使いたいのでArithとRingをImportしておきます。
 nに関する帰納法で、n=0の場合はさらっと証明を流すことにします。

Coq < Require Import Arith Ring.

Coq < Lemma Sample_of_unfold : forall n, 2 * sum n = n * (n + 1).
1 subgoal

============================
forall n : nat, 2 * sum n = n * (n + 1)

Sample_of_unfold < induction n.
2 subgoals

============================
2 * sum 0 = 0 * (0 + 1)

subgoal 2 is:
2 * sum (S n) = S n * (S n + 1)

Sample_of_unfold < reflexivity.
1 subgoal

n : nat
IHn : 2 * sum n = n * (n + 1)
============================
2 * sum (S n) = S n * (S n + 1)

 ここで、sum を unfold して、fold すると式が少し変形されます。

Sample_of_unfold < unfold sum.
1 subgoal

n : nat
IHn : 2 * sum n = n * (n + 1)
============================
2 *
(S n +
(fix sum (n0 : nat) : nat :=
match n0 with
| 0 => 0
| S n' => S n' + sum n'
end) n) = S n * (S n + 1)

Sample_of_unfold < fold sum.
1 subgoal

n : nat
IHn : 2 * sum n = n * (n + 1)
============================
2 * (S n + sum n) = S n * (S n + 1)

 ここでreplaceを使ってちょっと左辺を書き換えます。書き換えて良い証明はsubgoal 2と後回しです。


Sample_of_unfold < replace (2 * (S n + sum n)) with (2 * S n + 2 * sum n).
2 subgoals

n : nat
IHn : 2 * sum n = n * (n + 1)
============================
2 * S n + 2 * sum n = S n * (S n + 1)

subgoal 2 is:
2 * S n + 2 * sum n = 2 * (S n + sum n)

 ここでIHnを用いて書き換えて式変形を ring で自動証明します。後回しにしたものもringで一発です。


Sample_of_unfold < rewrite IHn.
2 subgoals

n : nat
IHn : 2 * sum n = n * (n + 1)
============================
2 * S n + n * (n + 1) = S n * (S n + 1)

subgoal 2 is:
2 * S n + 2 * sum n = 2 * (S n + sum n)

Sample_of_unfold < ring.
1 subgoal

n : nat
IHn : 2 * sum n = n * (n + 1)
============================
2 * S n + 2 * sum n = 2 * (S n + sum n)

Sample_of_unfold < ring.
Proof completed.

Sample_of_unfold < Qed.

09 December, 2010

[Coq] Coq Advent Calender : simpl (9 of 25)

 Coq でよく使われる tactic の9つ目は simpl です。simpl はβι簡約(beta, iota)をして式を簡単にします。βι簡約が何かについては「言語ゲーム」の記事が判りやすいです。β簡約は関数適用で、ι簡約だと再帰的に関数が適用される、と考えると良いです。

 予め、足し算の定義を示しておきます。plus を含んだ式を simpl すると、一つ目の変数 n について再帰的にパターンマッチして式を変形してくれます。

Coq < Print plus.
plus =
fix plus (n m : nat) : nat := match n with
| 0 => m
| S p => S (plus p m)
end
: nat -> nat -> nat

Argument scopes are [nat_scope nat_scope]

 では足し算を使った simpl の使用例です。

Coq < Lemma Sample_of_simpl : forall n m, n + m = m + n.
1 subgoal

============================
forall n m : nat, n + m = m + n

Sample_of_simpl < intros n m.
1 subgoal

n : nat
m : nat
============================
n + m = m + n

Sample_of_simpl < induction n.
2 subgoals

m : nat
============================
0 + m = m + 0

subgoal 2 is:
S n + m = m + S n

Sample_of_simpl < simpl.
2 subgoals

m : nat
============================
m = m + 0

subgoal 2 is:
S n + m = m + S n

simpl を使うと左辺の0 + mnに簡約されますが、右辺は変化がありません。ここは別途証明しておいた(というか標準ライブラリにはいっている)定理のplus_n_Oを使って書き換える事にします。

Sample_of_simpl < Check plus_n_O.
plus_n_O
: forall n : nat, n = n + 0

Sample_of_simpl < erewrite <- plus_n_O.
2 subgoals

m : nat
============================
m = m

subgoal 2 is:
S n + m = m + S n

Sample_of_simpl < reflexivity.
1 subgoal

n : nat
m : nat
IHn : n + m = m + n
============================
S n + m = m + S n

帰納法の後半も simpl を使い、別の補題plus_n_Smを使います。

Sample_of_simpl < simpl.
1 subgoal

n : nat
m : nat
IHn : n + m = m + n
============================
S (n + m) = m + S n

Sample_of_simpl < Check plus_n_Sm.
plus_n_Sm
: forall n m : nat, S (n + m) = n + S m

Sample_of_simpl < erewrite <- plus_n_Sm.
1 subgoal

n : nat
m : nat
IHn : n + m = m + n
============================
S (n + m) = S (m + n)

Sample_of_simpl < erewrite IHn.
1 subgoal

n : nat
m : nat
IHn : n + m = m + n
============================
S (m + n) = S (m + n)

Sample_of_simpl < reflexivity.
Proof completed.

Sample_of_simpl < Qed.

08 December, 2010

[Coq] Coq Advent Calender : intro (8 of 25)

 Coq でよく使われる tactic の8つ目は intro です。基本的には前に説明したintrosと同じで、introsと違って一度に1つしかintro出来ないのが違います。
 あと、introsと違ってintroの場合は、~Pの形のゴールを、Pという仮定と、Falseというゴールに変形出来ます。~PP->Falseなのですが、intros.では~P~Pのままです。

 intro.を使った例です。

Coq < Lemma Sample_of_intro : forall P, ~~~P -> ~P.
1 subgoal

============================
forall P : Prop, ~ ~ ~ P -> ~ P

Sample_of_intro < intro P.
1 subgoal

P : Prop
============================
~ ~ ~ P -> ~ P

Sample_of_intro < intro nnnp.
1 subgoal

P : Prop
nnnp : ~ ~ ~ P
============================
~ P

Sample_of_intro < intro p.
1 subgoal

P : Prop
nnnp : ~ ~ ~ P
p : P
============================
False

Sample_of_intro < elim nnnp.
1 subgoal

P : Prop
nnnp : ~ ~ ~ P
p : P
============================
~ ~ P

Sample_of_intro < intro np.
1 subgoal

P : Prop
nnnp : ~ ~ ~ P
p : P
np : ~ P
============================
False

Sample_of_intro < elim np.
1 subgoal

P : Prop
nnnp : ~ ~ ~ P
p : P
np : ~ P
============================
P

Sample_of_intro < exact p.
Proof completed.

Sample_of_intro < Qed.

07 December, 2010

[Coq] Coq Advent Calender : assert (7 of 25)

 Coq でよく使われる tactic の7つ目は assert です。

 1つ目のapplyのところで書いた様に、Coqの証明は最初にゴールがあって、それを仮定と逆に戻して行く格好になっています。しかし証明する人間は仮定からゴールを考える方が楽な場合、つまり証明途中で適当な補題を作りたくなる場合があります。
 補題はある程度汎用性があるならば、予め切り出して証明しておいた方が良いと思いますが、使い捨て的な補題は assert を使うと、証明内証明みたいに作る事ができます。例えば下記の例で、

Coq < Lemma Sample_of_assert : forall P Q, (P /\ P) -> (Q /\ Q) -> (P /\ Q).
1 subgoal

============================
forall P Q : Prop, P /\ P -> Q /\ Q -> P /\ Q

Sample_of_assert < intros P Q pp qq.
1 subgoal

P : Prop
Q : Prop
pp : P /\ P
qq : Q /\ Q
============================
P /\ Q


 ここまで証明した段階で、forall X, X /\ X -> Xという補題があれば、ppからPを、qqからQを取り出せて便利そうだと考えました。そこでassertを使います。すると現在の証明課題より先に、まずこの補題が証明課題になります。

Sample_of_assert < assert(H: forall X, X /\ X -> X).
2 subgoals

P : Prop
Q : Prop
pp : P /\ P
qq : Q /\ Q
============================
forall X : Prop, X /\ X -> X

subgoal 2 is:
P /\ Q

Sample_of_assert < intros X xx.
2 subgoals

P : Prop
Q : Prop
pp : P /\ P
qq : Q /\ Q
X : Prop
xx : X /\ X
============================
X

subgoal 2 is:
P /\ Q

Sample_of_assert < destruct xx as [x _].
2 subgoals

P : Prop
Q : Prop
pp : P /\ P
qq : Q /\ Q
X : Prop
x : X
============================
X

subgoal 2 is:
P /\ Q

Sample_of_assert < exact x.
1 subgoal

P : Prop
Q : Prop
pp : P /\ P
qq : Q /\ Q
H : forall X : Prop, X /\ X -> X
============================
P /\ Q

 assertで設定した補題 H の証明が終わると、以後は仮定 H としてそれを使う事が出来ます。

Sample_of_assert < split.
2 subgoals

P : Prop
Q : Prop
pp : P /\ P
qq : Q /\ Q
H : forall X : Prop, X /\ X -> X
============================
P

subgoal 2 is:
Q

Sample_of_assert < apply (H P).
2 subgoals

P : Prop
Q : Prop
pp : P /\ P
qq : Q /\ Q
H : forall X : Prop, X /\ X -> X
============================
P /\ P

subgoal 2 is:
Q

Sample_of_assert < exact pp.
1 subgoal

P : Prop
Q : Prop
pp : P /\ P
qq : Q /\ Q
H : forall X : Prop, X /\ X -> X
============================
Q

Sample_of_assert < apply (H Q).
1 subgoal

P : Prop
Q : Prop
pp : P /\ P
qq : Q /\ Q
H : forall X : Prop, X /\ X -> X
============================
Q /\ Q

Sample_of_assert < exact qq.
Proof completed.

Sample_of_assert < Qed.

06 December, 2010

[Coq] Coq Advent Calender : omega (6 of 25)

 Coq でよく使われる tactic の6つ目は omega です...ってanarchy proofは課題が数学寄りに偏っているから、順序が6つ目というのはあまり気にしないで下さい。

 omega タクティックはforallとかexistsとかを含まない形のPresburger算術 (Wikipedia)の式を自動証明してくれます。端的に言うと、

  • 割り算無し

  • 変数と変数の掛け算が入っているものはNG、変数と定数(2, 3などの具体的な整数)の掛け算はOK

みたいな感じの等式 or 不等式を証明します。
 Coqがよく使われる理由は、この手の数式関係の自動証明が便利に使えるからだと思います。整数の等式不等式に関する公理定理を組み合わせて証明するとか大変ですからね。

簡単な例はこんなのです。使い方は簡単で、Require Import Omega して、introsとかして、omega と入力するだけ。

Coq < Require Import Omega.

Coq < Lemma Sample_of_omega : forall x:nat, x > 1 -> 3 * x > x + 2.
1 subgoal

============================
forall x : nat, x > 1 -> 3 * x > x + 2

Sample_of_omega < intros.
1 subgoal

x : nat
H : x > 1
============================
3 * x > x + 2

Sample_of_omega < omega.
Proof completed.


 内部で実行された自動証明を見てみると、こんな感じらしい。

Sample_of_omega < Undo.
1 subgoal

x : nat
H : x > 1
============================
3 * x > x + 2

Sample_of_omega < info omega.
== refine (Decidable.dec_not_not (3 * x > x + 2) (dec_gt (3 * x) (x + 2)) _);
intro H0;
refine ((_:3 * x <= x + 2 -> False) (not_gt (3 * x) (x + 2) H0));
clear H0; intro H0;
refine ((_:(Z_of_nat x > Z_of_nat 1)%Z -> False) (inj_gt x 1 H));
change ((Z_of_nat x > 1)%Z -> False); clear H;
intro H;
refine ((_:(Z_of_nat (3 * x) <= Z_of_nat (x + 2))%Z -> False)
(inj_le (3 * x) (x + 2) H0));
refine ((fun (P : Z -> Prop) (H : P (Z_of_nat 3 * Z_of_nat x)%Z) =>
eq_ind_r P H (inj_mult 3 x))
(fun x0 : Z => (x0 <= Z_of_nat (x + 2))%Z -> False) _);
change ((3 * Z_of_nat x <= Z_of_nat (x + 2))%Z -> False);
refine ((fun (P : Z -> Prop) (H : P (Z_of_nat x + Z_of_nat 2)%Z) =>
eq_ind_r P H (inj_plus x 2))
(fun x0 : Z => (3 * Z_of_nat x <= x0)%Z -> False) _);
change ((3 * Z_of_nat x <= Z_of_nat x + 2)%Z -> False);
clear H0; intro H0; refine (ex_ind _ (intro_Z x));
intro Zvar2; intro Omega11; refine (and_ind _ Omega11);
clear Omega11; intro Omega8; intro Omega11;
refine ((_:(0 <= Z_of_nat x + -1 + - (1))%Z -> False)
(Zgt_left (Z_of_nat x) 1 H)); clear H;
refine ((fun (P : Z -> Prop) (H : P Zvar2) => eq_ind_r P H Omega8)
(fun x : Z => (0 <= x + -1 + - (1))%Z -> False) _);
change ((0 <= Zvar2 + -1 + -1)%Z -> False);
refine (fast_Zplus_assoc_reverse Zvar2 (-1)
(-1) (fun x : Z => (0 <= x)%Z -> False) _);
change ((0 <= Zvar2 + -2)%Z -> False);
refine (fast_Zred_factor0 Zvar2
(fun x : Z => (0 <= x + -2)%Z -> False) _);
intro Omega10;
refine ((_:(0 <= Z_of_nat x + 2 + - (3 * Z_of_nat x))%Z -> False)
(Zle_left (3 * Z_of_nat x) (Z_of_nat x + 2) H0));
clear H0;
refine ((fun (P : Z -> Prop) (H : P Zvar2) => eq_ind_r P H Omega8)
(fun x0 : Z => (0 <= x0 + 2 + - (3 * Z_of_nat x))%Z -> False)
_);
refine ((fun (P : Z -> Prop) (H : P Zvar2) => eq_ind_r P H Omega8)
(fun x : Z => (0 <= Zvar2 + 2 + - (3 * x))%Z -> False) _);
refine (fast_Zmult_comm 3 Zvar2
(fun x : Z => (0 <= Zvar2 + 2 + - x)%Z -> False) _);
refine (fast_Zopp_mult_distr_r Zvar2 3
(fun x : Z => (0 <= Zvar2 + 2 + x)%Z -> False) _);
change ((0 <= Zvar2 + 2 + Zvar2 * -3)%Z -> False);
refine (fast_Zplus_comm (Zvar2 + 2) (Zvar2 * -3)
(fun x : Z => (0 <= x)%Z -> False) _);
refine (fast_Zplus_assoc (Zvar2 * -3) Zvar2 2
(fun x : Z => (0 <= x)%Z -> False) _);
refine (fast_Zred_factor3 Zvar2 (-3)
(fun x : Z => (0 <= x + 2)%Z -> False) _);
change ((0 <= Zvar2 * Zneg (3 - 1) + 2)%Z -> False);
intro Omega9;
cut ((Zvar2 * -2 + 2)%Z = ((Zvar2 * -1 + 1) * 2 + 0)%Z);[intro H|idtac].
refine ((_:(Zvar2 * -2 + 2)%Z = ((Zvar2 * -1 + 1) * 2 + 0)%Z -> False) H);
clear H; intro auxiliary;
refine ((_:(0 <= (Zvar2 * -1 + 1) * 2 + 0)%Z -> False)
(OMEGA1 (Zvar2 * -2 + 2) ((Zvar2 * -1 + 1) * 2 + 0)
auxiliary Omega9)); clear auxiliary Omega9;
intro Omega9;
cut (2 > 0)%Z;[intro H|idtac].
refine ((_:(2 > 0)%Z -> False) H); clear H;
cut (2 > 0)%Z;[intro H|idtac].
refine ((_:(2 > 0)%Z -> (2 > 0)%Z -> False) H);
clear H; intro auxiliary_1; intro auxiliary_2;
refine ((_:(0 <= Zvar2 * -1 + 1)%Z -> False)
(Zmult_le_approx 2 (Zvar2 * -1 + 1) 0 auxiliary_1
auxiliary_2 Omega9));
clear auxiliary_1 auxiliary_2 Omega9; intro Omega9;
refine ((_:(0 <= Zvar2 * 1 + -2 + (Zvar2 * -1 + 1))%Z -> False)
(OMEGA2 (Zvar2 * 1 + -2) (Zvar2 * -1 + 1) Omega10 Omega9));
refine (fast_OMEGA13 Zvar2 (-2) 1 1 (fun x : Z => (0 <= x)%Z -> False)
_); change ((0 <= Zneg (2 - 1))%Z -> False);
change ((0 ?= Zneg (2 - 1))%Z <> Gt -> False);
change (Gt <> Gt -> False); intro H; refine (False_ind False _);
cut (Gt = Gt);[intro H0|idtac].
refine ((_:Gt = Gt -> False) H0); clear H0;
cut (Gt <> Gt);[intro H0|idtac].
refine ((_:Gt <> Gt -> Gt = Gt -> False) H0); clear H0;
intro H0; intro H1; exact (H0 H1).

exact H.

change (Gt = Gt); exact (refl_equal Gt).

change ((2 ?= 0)%Z = Gt); change (Gt = Gt); change (Gt = Gt);
exact (refl_equal Gt).

change ((2 ?= 0)%Z = Gt); change (Gt = Gt); change (Gt = Gt);
exact (refl_equal Gt).

refine (fast_OMEGA11 Zvar2 (-1) 1 0 2
(fun x : Z => (Zvar2 * -2 + 2)%Z = x) _);
change ((Zvar2 * -2 + 2)%Z = (Zvar2 * -2 + 2)%Z);
change ((Zvar2 * -2 + 2)%Z = (Zvar2 * -2 + 2)%Z);
exact (refl_equal (Zvar2 * -2 + 2)%Z).

Proof completed.

Sample_of_omega <

05 December, 2010

[Coq] Coq Advent Calender : intros (5 of 25)

 Coq でよく使われる tactic の5つ目は intros です。

 実は過去4回の記事でも毎回 intros を使用していました。forall とかで定義された変数や -> の左の式とかを仮定に持って行く為に使います。introの複数形なので、introを必要な回数繰り返してもOKです。
 intros. だけでも勝手に適当に名前(仮定は通常 H? みたいな名前)を付けてくれますが、判りやすさを考えると自分で適切な名前を付けた方が良いと思います。

Coq < Lemma Sample_of_intros : forall A B C:Prop, (A->B->C) -> (A->B) -> A -> C.
1 subgoal

============================
forall A B C : Prop, (A -> B -> C) -> (A -> B) -> A -> C

Sample_of_intros < intros A B C abc ab a.
1 subgoal

A : Prop
B : Prop
C : Prop
abc : A -> B -> C
ab : A -> B
a : A
============================
C

Sample_of_intros < apply abc.
2 subgoals

A : Prop
B : Prop
C : Prop
abc : A -> B -> C
ab : A -> B
a : A
============================
A

subgoal 2 is:
B

Sample_of_intros < exact a.
1 subgoal

A : Prop
B : Prop
C : Prop
abc : A -> B -> C
ab : A -> B
a : A
============================
B

Sample_of_intros < apply ab; exact a.
Proof completed.

Sample_of_intros < Qed.
intros A B C abc ab a.
apply abc.
exact a.

apply ab; exact a.

Sample_of_intros is defined

Coq <

04 December, 2010

[Coq] Coq Advent Calender : destruct (4 of 25)

 Coq でよく使われる tactic の4つ目は destruct です。

 destruct は基本的にはある項を場合分けする時使うのですが、仮定の中にある /\ とか \/ とか exists とかを分解するのに使うのに便利です。(それ以外のときは induction とか case_eq とか使う事が多い様にも思います。)
 下記の例では仮定 abc を分解して仮定 a, b, c を作っています。 


Coq < Lemma Sample_of_destruct : forall A B C:Prop,
Coq < A /\ (B /\ C) -> (A /\ B) /\ C.
1 subgoal

============================
forall A B C : Prop, A /\ B /\ C -> (A /\ B) /\ C

Sample_of_destruct < intros A B C abc.
1 subgoal

A : Prop
B : Prop
C : Prop
abc : A /\ B /\ C
============================
(A /\ B) /\ C

Sample_of_destruct < destruct abc as [a [b c]].
1 subgoal

A : Prop
B : Prop
C : Prop
a : A
b : B
c : C
============================
(A /\ B) /\ C

Sample_of_destruct < split; [split|]; assumption.
Proof completed.

Sample_of_destruct < Qed.
intros A B C abc.
destruct abc as (a, (b, c)).
split; [ split | idtac ]; assumption.

Sample_of_destruct is defined

Coq <

[Coq] Coq Advent Calender : rewrite (3 of 25)

 Coq でよく使われる tactic の3つ目は rewrite です。

 rewrite は仮定にある等式を使ってゴールを書き換えます。下記の例では、リスト xs について帰納法を用いて証明していますが、ゴールの中に含まれるlength (xs ++ ys)を、帰納法の仮定IHxsを用いてrewriteすることでlength xs + length ysに書き換えています。


Coq < Lemma Sample_of_rewrite : forall (A:Set)(xs ys:list A),
Coq < length (xs ++ ys) = length xs + length ys.
1 subgoal

============================
forall (A : Set) (xs ys : list A),
length (xs ++ ys) = length xs + length ys

Sample_of_rewrite < intros A xs ys.
1 subgoal

A : Set
xs : list A
ys : list A
============================
length (xs ++ ys) = length xs + length ys

Sample_of_rewrite < induction xs.
2 subgoals

A : Set
ys : list A
============================
length (nil ++ ys) = length nil + length ys

subgoal 2 is:
length ((a :: xs) ++ ys) = length (a :: xs) + length ys

Sample_of_rewrite < reflexivity.
1 subgoal

A : Set
a : A
xs : list A
ys : list A
IHxs : length (xs ++ ys) = length xs + length ys
============================
length ((a :: xs) ++ ys) = length (a :: xs) + length ys

Sample_of_rewrite < simpl.
1 subgoal

A : Set
a : A
xs : list A
ys : list A
IHxs : length (xs ++ ys) = length xs + length ys
============================
S (length (xs ++ ys)) = S (length xs + length ys)

Sample_of_rewrite < rewrite IHxs.
1 subgoal

A : Set
a : A
xs : list A
ys : list A
IHxs : length (xs ++ ys) = length xs + length ys
============================
S (length xs + length ys) = S (length xs + length ys)

Sample_of_rewrite < reflexivity.
Proof completed.

Sample_of_rewrite < Qed.
intros A xs ys.
induction xs.
reflexivity.

simpl in |- *.
rewrite IHxs in |- *.
reflexivity.

Sample_of_rewrite is defined

Coq <

[Coq] Coq Advent Calender : auto (2 of 25)

 Coq でよく使われる tactic の2つ目は auto です。

 Coq は簡単な証明は自動的に証明してくれる機能が幾つかありますが、auto はよく使われます。autoが何をやっているか知りたい場合は、autoの代わりにinfo autoと入力すると、autoの中で何をしてるかが判ります。Coqの初学者にはinfoは便利ですよ。


Coq < Lemma Sample_of_auto : forall A B:Prop, ((((A->B)->A)->A)->B)->B.
1 subgoal

============================
forall A B : Prop, ((((A -> B) -> A) -> A) -> B) -> B

Sample_of_auto < auto.
Proof completed.

Sample_of_auto < Qed.
auto.

Sample_of_auto is defined

Coq <

[Coq] Coq Advent Calender : apply (1 of 25)

 技術的 Advent Calender という概念を知らなかったのですが、面白そうなので遅ればせながら始めてみました。という訳で12/1から開始出来なかったのはご容赦下さい。
 先日のCoq Party絡みで集計されたCoqでよく使われるtacticのリストの順に、そのtacticが使われている証明例を書いてみます。

 最初は apply です。
 「この仮定(下記の例では pq)を使うとゴール(下記の例では Q)が出て来る」という時に、apply pq とすると、ゴール Q が変化します。学校で習う普通の証明の順序と違って、Coqの証明はゴールを一歩一歩、仮定に戻して行きます。その時使うのが apply です。


Coq < Lemma Sample_of_apply : forall P Q:Prop, P -> (P->Q) -> Q.
1 subgoal

============================
forall P Q : Prop, P -> (P -> Q) -> Q

Sample_of_apply < intros P Q p pq.
1 subgoal

P : Prop
Q : Prop
p : P
pq : P -> Q
============================
Q

Sample_of_apply < apply pq.
1 subgoal

P : Prop
Q : Prop
p : P
pq : P -> Q
============================
P

Sample_of_apply < exact p.
Proof completed.

Sample_of_apply < Qed.
intros P Q p pq.
apply pq.
exact p.

Sample_of_apply is defined

Coq <