pptx

情報科学概論
第3回
1
帰納法
〜帰納法による証明〜
2
場合分けに名前をつける
3
Caseタクティック:
場合分けに名前をつける
1 ...
2 ...
3 ...
4 ...
5 ...
• 場合分けが多いと分かりにくい
• 字下げ，コメントも理解の助けだが．．
Theorem andb_true_elim1 : ∀b c : bool,
andb b c = true → b = true.
1 ...
2 ...
3 ...
4 ...
5 ...
6 ...
7 ...
Proof.
intros b c H.
destruct b.
Case "b = true". (* <----- here *)
reflexivity.
Case "b = false". (* <---- and here *)
rewrite ← H.
reflexivity. Qed.
4
推奨するコーディングスタイル
• 必ず字下げをする
• 必要に応じてコメントをつける
• Caseタクティックを使う
– サブケースは SCase
– サブサブケースは SSCase
– ...
• 一行の長さは，長すぎず短すぎず
– 1行80文字以内を目安
5
単純化による証明の限界
Theorem plus_0_r_firsttry :
n + 0 = n.
∀n:nat,
第一引数で
再帰
Fixpoint plus (n m : nat) : nat :=
match n with
| O => m
| S n' => S (plus n' m)
end.
6
場合分けによる証明の限界
Theorem plus_0_r_secondtry : ∀n:nat,
n + 0 = n.
Proof.
intros n. destruct n as [| n'].
Case "n = 0".
reflexivity. (* ここまではよいが... *)
Case "n = S n'".
simpl. (* ...ここで止まってしまう *)
Admitted.
7
帰納法（高校の復習）
∀n. P(n)
⇔
• P(0)
• ∀n'. P(n') ⇒ P(S(n'))
こちらを証明すれば，
上が言えたことに
帰納法の仮定
(IH: Induction Hypothesis)
8
帰納法の例
∀n. n + 0 = n
⇔
• 0+0=0
• ∀n'. n' + 0 = n' ⇒ S n' + 0 = S n'
0+0=0
(+の定義)
S n' + 0 = S (n' + 0) (+の定義)
= S n'
(∵IH)
9
帰納法による証明
Theorem plus_0_r : ∀n:nat, n + 0 = n.
Proof.
intros n. induction n as [| n'].
intro
Case "n = 0". reflexivity.
パターン
Case "n = S n'".
simpl. rewrite
Qed.
→
IHn'. reflexivity.
帰納法の
仮定
10
証明中の証明
• 先に証明した定理を使用できる
• 証明中で"小定理"が必要なことがある
– ほぼ自明
– 命名しても他で使用されない
⇒ assert タクティックが便利
11
assert タクティック
Theorem mult_0_plus' : ∀n m : nat,
(0 + n) * m = n * m.
Proof.
intros n m.
assert (H: 0 + n = n).
Case "Proof of assertion". reflexivity.
rewrite → H.
reflexivity.
Qed.
読みやすくなるし，
assert の証明の
完了も明確に
12
rewrite タクティックの難点
Theorem plus_rearrange_firsttry :
∀n
m p q : nat,
(n + m) + (p + q) = (m + n) + (p + q).
Proof.
intros n m p q.
(* (n + m) を (m + n) に書き換えたいだけ...
plus_comm でうまくいきそう! *)
rewrite
→
plus_comm.
(* いかない...Coq は中央の + を書き換える! *)
Admitted.
13
assert タクティックによる解決
Theorem plus_rearrange : ∀n m p q : nat,
(n + m) + (p + q) = (m + n) + (p + q).
Proof.
intros n m p q.
assert (H: n + m = m + n).
Case "Proof of assertion".
→ plus_comm. reflexivity.
→ H. reflexivity. Qed.
rewrite
rewrite
14
証明
非形式的 vs 形式的
• 「アルゴリズム」
• 「コード」
• アイデアを
効率的に伝達可
• 機械的に正しさの
チェック可能
• 人間のみ
• Coqでも！
15
形式的証明の例：+ は結合的
Theorem plus_assoc' : ∀n m p : nat,
n + (m + p) = (n + m) + p.
Proof.
intros n m p.
induction n as [| n']. reflexivity.
simpl. rewrite
→
IHn'. reflexivity. Qed.
• 複雑 →人間は理解が大変
• Coqの問題ではない
16
非形式的証明の例
定理: 任意の n, m, p について
n + (m + p) = (n + m) + p である．
証明： n についての帰納法を行う．
• n = 0 とする．+ の定義より
0 + (m + p) = (0 + m) + p である．
• n = S n' として n' + (m + p) = (n' + m) + p を帰
納法の仮定とする．+ の定義と帰納法の仮定よ
り (S n') + (m + p) = ((S n') + m) + p は，
S (n' + (m + p)) = S ((n' + m) + p) に変形できる．
☐
17
リスト
〜構造化データの処理〜
18
自然数の組
例： Inductive による型定義
• 引数なし： true, O
• 引数1つ： S
• 引数2つ：
Inductive natprod : Type :=
pair : nat
→
nat
→
natprod.
2引数に適用，またその方法でのみ構成
（コンストラクト）
19
要素の取り出し
first
Definition fst (p : natprod) : nat :=
match p with
| pair x y => x
end.
second
Definition snd (p : natprod) : nat :=
match p with
| pair x y => y
end.
Eval simpl in (fst (pair 3 5)).
(* ===> 3 *)
20
pair x y を (x,y) と表記する
Notation "( x , y )" := (pair x y).
Definition fst' (p : natprod) : nat :=
match p with
| (x,y) => x
end.
パターン
Definition swap_pair (p : natprod) :
natprod :=
match p with
| (x,y) => (y,x)
end.
式
21
組の性質の証明
Theorem surjective_pairing' : ∀(n m : nat),
(n,m) = (fst (n,m), snd (n,m)).
Proof.
reflexivity. Qed.
より自然な表現の場合．．．
Theorem surjective_pairing : ∀(p
: natprod),
p = (fst p, snd p).
Proof.
intros p. destruct p as (n,m). simpl.
reflexivity. Qed.
置き換えを
行う
22
自然数のリスト
cons 1 (cons 3 (cons 5 nil))
1
3
5
23
自然数のリストの
構築子(コンストラクタ)
cons nat natlist
数
nil
数のリスト
24
自然数のリスト
自然数のリスト：
• 空リスト，もしくは
• 自然数と自然数のリストの組
• 以上で構成されるものだけ
Inductive natlist : Type :=
| nil : natlist
| cons : nat
→
natlist
→
natlist.
例：
Definition mylist :=
cons 1 (cons 2 (cons 3 nil)).
25
リスト表記
以下は同じリスト
cons の中置記法
Definition mylist1 := 1 :: (2 :: (3 :: nil)).
Definition mylist2 := 1 :: 2 :: 3 :: nil.
Definition mylist3 := [1,2,3].
:: は右結合
列挙の表記
26
リスト処理関数(1)
Fixpoint repeat (n count : nat) : natlist :=
match count with
| O => nil
| S count' => n :: (repeat n count')
end.
[n, n, ..., n] を返す
count 個
27
リスト処理関数(2)：
リストの長さ
Fixpoint length (l:natlist) : nat :=
match l with
| nil => O
| h :: t => S (length t)
end.
28
リスト処理関数(3)：
リストの連結
Fixpoint app (l1 l2 : natlist) : natlist :=
match l1 with
| nil => l2
| h :: t => h :: (app t l2)
end.
appの中置記法
Example test_app1: [1,2,3] ++ [4,5] = [1,2,3,4,5].
Example test_app2: nil ++ [4,5] = [4,5].
Example test_app3: [1,2,3] ++ nil = [1,2,3].
29
リスト処理関数(4)：
先頭と先頭以外のリスト
Definition hd (default:nat) (l:natlist) : nat :=
match l with
| nil => default
空リストの
| h :: t => h
場合に返す値
end.
Definition tail (l:natlist) : natlist :=
match l with
| nil => nil
| h :: t => t
end.
Example test_hd1: hd 0 [1,2,3] = 1.
Example test_hd2: hd 0 [] = 0.
Example test_tail: tail [1,2,3] = [2,3].
30
リストによるバッグ(多重集合)の実現
• 集合：各要素は１回しか現れない
• バッグ：各要素が複数回現れても良い
• リストを用いて実装する
Definition bag := natlist.
31
count v s:
バッグ s 中の要素 v の出現回数
Fixpoint count (v:nat) (s:bag) : nat :=
match s with
| []
=> 0
| h :: t => match beq_nat v h with
| true => S (count v t)
| false => count v t
end
end.
count 1 [1,2,3,1,4,1]  3
count 6 [1,2,3,1,4,1]  0
32
再帰は不要
sum a b:
バッグ a，b の和
Definition sum : bag → bag → bag :=
app.
count 1 (sum [1,2,3] [1,4,1])  3
33
add v s: バッグ s に要素 v を追加
Definition add (v:nat) (s:bag) : bag :=
v :: s.
count 1 (add 1 [1,4,1])  3
count 5 (add 1 [1,4,1])  0
34
member v s:
バッグ s 中の要素 v の有無
Definition member (v:nat) (s:bag) : bool :=
blt_nat O (count v s).
member 1 [1,4,1]  true
member 2 [1,4,1]  false
35
リストに関する論証
36
単純化による証明
Theorem nil_app : ∀l:natlist,
[] ++ l = l.
Proof. reflexivity. Qed.
自然数のときと同様に
単純化のみでOK
37
場合分けによる証明
Theorem tl_length_pred : ∀l:natlist,
pred (length l) = length (tail l).
Proof.
intros l. destruct l as [| n l'].
Case "l = nil".
reflexivity.
自然数のときと同様に
Case "l = cons n l'".
場合分けが必要
reflexivity. Qed.
tail nil = nil
38
リスト上の帰納法
∀l. P(l)
⇔
• P(nil)
• ∀n∀l'. P(l') ⇒ P(n :: l')
こちらを証明すれば，
上が言えたことに
帰納法の仮定
(IH: Induction Hypothesis)
39
++ の結合律
Theorem app_ass : ∀l1 l2 l3 : natlist,
(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof.
intros l1 l2 l3. induction l1 as [| n l1'].
Case "l1 = nil".
reflexivity.
Case "l1 = cons n l1'".
simpl. rewrite → IHl1'. reflexivity. Qed.
40
非形式的な証明
定理
任意の l1, l2, l3 について
l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3
である
l1 についての帰納法で証明する．
• l1 = [] とする. ++ の定義より
[] ++ (l2 ++ l3)=([] ++ l2) ++ l3
である．
41
非形式的な証明（続き）
• l1 = n :: l1′ であるとする．ただし，
l1′ ++ (l2 ++ l3) = (l1′ ++ l2) ++ l3 (*)
であるとする．
• (n::l1′) ++ (l2 ++ l3)
= n:: (l1′ ++ (l2 ++ l3))
++の定義より
= n::((l1′ ++ l2) ++ l3)
(*)より
= (n::(l1′ ++ l2)) ++ l3
++の定義より
= ((n::l1′) ++ l2) ++ l3
++の定義より
☐
42
SearchAbout
• 証明には，以前証明した定理を使用可
• 定理の名前を覚えるのは困難
• SearchAbout
(EmacsではC-cC-aC-a,
C-cC-;で結果を貼り付け)
SearchAbout rev.
revに関する
定理を表示
43
オプション
44
リストの n 番目の要素
（オプションなし）
Fixpoint index_bad (n:nat) (l:natlist) : nat :=
match l with
| nil => 42 (* 何か必要! *)
| a :: l' => match beq_nat n O with
| true => a
| false => index_bad (pred n) l'
end
end.
45
リストの n 番目の要素
（オプションあり）
Inductive natoption : Type :=
| Some : nat → natoption
| None : natoption.
Fixpoint index (n:nat) (l:natlist) : natoption :=
match l with
| nil => None (* 何か *)
| a :: l' => match beq_nat n O with
| true => Some a
| false => index (pred n) l'
end
end.
46
リストの n 番目の要素
（オプションあり）
Inductive natoption : Type :=
| Some : nat → natoption
| None : natoption.
Fixpoint index' (n:nat) (l:natlist) : natoption :=
match l with
| nil => None (* 何か *)
| a :: l' => if beq_nat n O
then Some a
else index (pred n) l'
end.
条件式
47
Example test_index1
Proof. reflexivity.
Example test_index2
Proof. reflexivity.
Example test_index3
Proof. reflexivity.
: index 0 [4,5,6,7] = Some 4.
Qed.
: index 3 [4,5,6,7] = Some 7.
Qed.
: index 10 [4,5,6,7] = None.
Qed.
Definition option_elim (d : nat) (o : natoption) : nat :=
match o with
| Some n' => n'
| None => d
end.
48
デフォルト値のない hd
Definition hd_opt (l : natlist) : natoption :=
match l with
| nil
=> None
| a :: _ => Some a
end.
Example test_hd_opt1 : hd_opt [] = None.
Proof. reflexivity. Qed.
Example test_hd_opt2 : hd_opt [1] = Some 1.
Proof. reflexivity. Qed.
Example test_hd_opt3 : hd_opt [5,6] = Some 5.
Proof. reflexivity. Qed.
49
ディクショナリー
50
データ型 dictionary
Inductive dictionary : Type :=
| empty : dictionary
| record : nat
→
nat
dictionary
キー
→
→
dictionary.
値
51
dictionary へキーと値の追加
Definition insert (key value : nat)
(d : dictionary) : dictionary :=
(record key value d).
52
dictionary へキーと値の追加
Fixpoint find (key : nat)
(d : dictionary) : natoption :=
match d with
| empty => None
key が見つからないとき
| record k v d' =>
if beq_nat key k then
Some v
key が見つかったとき
else
find key d'
end.
53
練習問題1
Theorem dictionary_invariant1' :
∀(d
: dictionary) (k v: nat),
(find k (insert k v d)) = Some v.
Proof.
intros d k v.
simpl.
rewrite <- beq_nat_refl.
reflexivity.
Qed.
54
練習問題2
Theorem dictionary_invariant2' :
∀(d
: dictionary) (m n o: nat),
(beq_nat m n) = false → (find m d)
= (find m (insert n o d)).
Proof.
intros d m n o.
intros H.
simpl.
rewrite H.
reflexivity.
Qed.
55
付録
56
代数データ型
1
4
1
3
9
5
7
3
5
57

Download Report