pptx

情報科学概論
第5回
1
Prop
〜命題と根拠〜
2
再帰的に定義された命題
3
命題 beautiful
•
•
•
•
Rule b_0: The number 0 is beautiful.
Rule b_3: The number 3 is beautiful.
Rule b_5: The number 5 is beautiful.
Rule b_sum: If n and m are both beautiful,
then so is their sum.
4
推論規則の例
前提条件がない
ものは公理
前提条件
結論
5
証明木の例
----------- (b_3)
----------- (b_5)
beautiful 3
beautiful 5
------------------------------- (b_sum)
beautiful 8
証明木は
一意でない
----------- (b_5)
----------- (b_3)
beautiful 5
beautiful 3
------------------------------- (b_sum)
beautiful 8
6
Coqにおけるbeautifulの定義
命題
Proposition
Inductive beautiful : nat
b_0 : beautiful 0
| b_3 : beautiful 3
| b_5 : beautiful 5
| b_sum :
∀n
→
Prop :=
→
m →
m, beautiful n
beautiful
beautiful (n+m).
7
ある特定の数はbeautiful
Theorem three_is_beautiful: beautiful 3.
Proof.
(* 公理 b_3 より自明 *)
apply b_3.
Qed.
Theorem eight_is_beautiful: beautiful 8.
Proof.
(* 規則 b_sum でCoqに n と m を具体化する方法を伝える *)
apply b_sum with (n:=3) (m:=5).
(* b_sum によって生成されたサブゴールを解くため，
beautiful 3 と beautiful 5 の根拠を与えなければならない．
ここでは公理で充分． *)
apply b_3.
apply b_5.
Qed.
8
証明対象
9
美の根拠はデータ構造と見なせる
同じ
キーワード
Inductive beautiful : nat
b_0 : beautiful 0
| b_3 : beautiful 3
| b_5 : beautiful 5
| b_sum :
∀n
→
Prop :=
→
m →
m, beautiful n
beautiful
beautiful (n+m).
is a proof of
(has typeであった)
10
Curry-Howard同型対応
論理の世界
命題
根拠
計算の世界
型
データ
計算の世界のことばで
論理の世界を解釈できる
11
Inductive beautiful : nat → Prop :=
b_0 : beautiful 0
| b_3 : beautiful 3
命題（型）
| b_5 : beautiful 5
| b_sum :
∀n
→
m →
m, beautiful n
beautiful
根拠（データ）
beautiful (n+m).
命題（型）
b_sum 3 5 b_3 b_5 : beautiful 8
12
【参考】
同型 isomorphism
一般に，1つの与えられた構造を持つ2つ
の集合 X, Y の間の全単射φ:XYが構造を保
つとき，φを(与えられた構造における)同型
写像といい，X, Yは(互いに)同型であるとい
われる．．．．
青本ら(編集): 岩波数学入門辞典，岩波書店 (2005).
13
コンストラクタ b_sum の解釈
b_sum :
∀n
m,
beautiful n
→
beautiful m
→
beautiful (n+m).
データ
コンストラクタ
14
型「beautiful 8」の式を書けるか？
b_sum 3 5 b_3 b_5
書ける
この考え方を
用いて別証明
Theorem eight_is_beautiful': beautiful 8.
Proof.
apply (b_sum 3 5 b_3 b_5).
Qed.
根拠を構築する
式を与える
15
証明スクリプトと証明対象
Theorem eight_is_beautiful'': beautiful 8.
Proof.
apply b_sum with (n:=3) (m:=5).
apply b_3.
apply b_5.
Qed.
Definition eight_is_beautiful''' : beautiful 8 :=
b_sum 3 5 b_3 b_5.
根拠を構築する
式を与える
16
6は美しい
Theorem six_is_beautiful :
beautiful 6.
Proof.
apply b_sum with (n:=3) (m:=3).
apply three_is_beautiful.
apply three_is_beautiful.
Qed.
Definition six_is_beautiful' : beautiful 6 :=
b_sum 3 3 b_3 b_3.
17
9は美しい
Theorem nine_is_beautiful :
beautiful 9.
Proof.
apply b_sum with (n:=3) (m:=6).
apply three_is_beautiful.
apply six_is_beautiful.
Qed.
Definition nine_is_beautiful' : beautiful 9 :=
b_sum 6 3 (b_sum 3 3 b_3 b_3) b_3.
18
含意と関数
Theorem b_plus3:
Proof.
intros n H.
apply b_sum.
apply b_3.
apply H.
Qed.
∀n,
beautiful n
→
beautiful (3+n).
プリミティブ
でない含意
Definition b_plus3' : ∀n, beautiful n
fun n => fun H : beautiful n =>
b_sum 3 n b_3 H.
→
beautiful (3+n) :=
Definition b_plus3'' (n : nat) (H : beautiful n)
: beautiful (3+n) :=
b_sum 3 n b_3 H.
19
証明対象の上の帰納法
• 根拠のコンストラクタ：
根拠を構築する唯一の方法
• 例
根拠 E が beautiful n の正しさを説明
→ E は b_0(n=O), b_3(n=3), b_5(n=5) ,
もしくは b_sum n1 n2 E1 E2 (n=n1+n2,
E1,E2はn1,n2がそれぞれbeauifulである
ことの根拠).
20
偶数の判定
Definition even (n:nat) : Prop :=
evenb n = true.
｢n は偶数｣を
｢関数evenbがnに適用されたときtrueを返却｣と定義
Inductive ev : nat → Prop :=
| ev_0 : ev O
| ev_SS : ∀n:nat, ev n → ev (S (S n)).
数が偶数である根拠を与える2つの方法
1. 0は偶数 ← ev_0
2. mは偶数 ← (もし m = S (S n) かつ n が偶数である
根拠eがあったならば) ev_SS n e
21
Inverting Evidence
根拠に inversion を適用
22
根拠の上で場合分け
例：偶数の判定
Theorem ev_minus2: ∀n,
ev n → ev (pred (pred n)).
Proof.
根拠の上で
intros n E.
destruct E as [| n' E']. 場合分け
Case "E = ev_0". simpl. apply ev_0.
Case "E = ev_SS n' E'". simpl. apply E'.
Qed.
23
根拠の上で場合分けの限界
Theorem SSev_ev_firsttry : ∀n,
ev (S (S n)) → ev n.
Proof.
intros n E.
destruct E as [| n' E'].
(* 証明できないサブゴール！ *)
Admitted.
n : nat
=======
ev n
S (S n)が０であることが忘れられている
24
忘れないよう remember
Theorem SSev_ev_secondtry : ∀n,
ev (S (S n)) → ev n.
Proof.
intros n E. remember (S (S n)) as n2.
destruct E as [| n' E'].
Case "n = 0". inversion Heqn2.
Case "n = S n'". inversion Heqn2.
rewrite ← H0. apply E'.
Qed.
25
帰納的に定義された命題
ev (S (S n)) に inversion
※inversionの新しい使い方
Theorem SSev__even : ∀n,
ev (S (S n)) → ev n.
Proof.
intros n E. inversion E as [| n' E'].
apply E'.
Qed.
再掲
Inductive ev : nat → Prop :=
| ev_0 : ev O
| ev_SS : ∀n:nat, ev n → ev (S (S n)).
26
inversion の練習
Theorem SSSSev__even : ∀n,
ev (S (S (S (S n)))) → ev n.
Proof.
intros n E.
inversion E as [| n' E'].
inversion E' as [| n'' E''].
apply E''.
Qed.
27
命題を用いたプログラミング
28
命題の例
Prop 型
Check (2 + 2 = 4).
(* ===> 2 + 2 = 4 : Prop *)
Check (ble_nat 3 2 = false).
(* ===> ble_nat 3 2 = false : Prop *)
Check (beautiful 8).
(* ===> beautiful 8 : Prop *)
29
言明である ≠ 証明可能である
Check (2 + 2 = 5).
(* ===> 2 + 2 = 5 : Prop *)
Check (beautiful 4).
(* ===> beautiful 4 : Prop *)
証明できない
言明
30
命題の使われ方
• 証明の宣言における使用
Theorem plus_2_2_is_4 : 2 + 2 = 4.
Proof. reflexivity. Qed.
• 定義中で使用
Definition plus_fact : Prop := 2 + 2 = 4.
Check plus_fact.
(* ===> plus_fact : Prop *)
• 定義されたものを証明の宣言で使用
Theorem plus_fact_is_true :
Proof. reflexivity. Qed.
plus_fact.
31
命題の使われ方（続き）
Definition strange_prop1 : Prop :=
(2 + 2 = 5) → (99 + 26 = 42).
計算式から
等式の
命題を作る
2つの命題から
新命題を作る
Definition strange_prop2 :=
∀n, (ble_nat n 17 = true) → (ble_nat n 99 = true).
命題から量子化により
新命題を作る
32
パラメータ化された命題
Check even.
(* ===> even : nat -> Prop *)
Check (even 4).
(* ===> even 4 : Prop *)
Check (even 3).
(* ===> even 3 : Prop *)
even の型 nat→Prop の読み方
1. 数から命題への関数
2. 数nを添え字とする命題の族
3. 数の性質
33
Coqでは命題は第１級の市民
復習：
第1級の市民であるための
3つの要件は何であったか
34
帰納法による証明
35
帰納的に定義された型の
帰納法の考え方
• Inductiveデータ型 t を宣言
→ 型tのIP(t_ind)を含む公理が生成
• 例．自然数のIP
Check nat_ind.
(* ===> nat_ind :
forall P : nat -> Prop,
P 0 ->
(forall n : nat, P n -> P (S n))
forall n : nat, P n *)
->
36
Basicsの復習
Theorem mult_0_r : ∀n:nat,
n * 0 = 0.
Proof.
intros n. induction n as [| n'].
Case "n = 0". reflexivity.
Case "n = S n'".
rewrite -> IHn'. reflexivity.
Qed.
37
nat_indを用いた場合
Theorem mult_0_r' : ∀n:nat,
n * 0 = 0.
introsが
Proof.
あってはならない
apply nat_ind.
Case "O". reflexivity.
introsが必要
Case "S". simpl. intros n IHn.
rewrite → IHn. reflexivity.
Qed.
自動的に
名前付けがされる
38
帰納法の仮定
∀ P : nat → Prop,
P 0 →
(∀ n : nat, P n → P (S n))
∀ n : nat, P n
→
Definition P_m0r (n:nat) : Prop :=
n * 0 = 0.
Theorem mult_0_r'' : ∀n:nat,
========================
P_m0r n.
forall n : nat,
Proof.
P_m0r n -> P_m0r (S n)
apply nat_ind.
Case "n = O". reflexivity.
Case "n = S n'".
unfold P_m0r. simpl. intros n' IHn'.
apply IHn'. Qed.
39
Prop〜命題と根拠〜
まとめ
• 再帰的に定義された命題
• 証明対象
• 命題を用いたプログラミング
• 帰納法による証明
40

Download Report