[n] = [m]

情報科学概論
第4回
1
Poly
〜多相性と高階関数〜
2
多相性
3
単相的 vs 多相的なリスト
Inductive natlist : Type :=
| nil : natlist
| cons : nat
→
natlist
→
natlist.
Inductive boollist : Type :=
| bool_nil : boollist
| bool_cons : bool
→
boollist
→
boollist.
：
：
Inductive list (X:Type) : Type :=
| nil : list X
| cons : X
list
→
list X
→
list X.
は，型 X を取り帰納的な定義を返す関数と考えるとよい
4
多相的なコンストラクタ
Check nil.
(* ===> nil : ∀X : Type, list X *)
Check cons.
(* ===> cons : ∀X : Type, X -> list X -> list X *)
Check (cons nat 2 (cons nat 1 (nil nat))).
5
多相的な関数の例
Fixpoint length (X:Type) (l:list X) : nat :=
match l with
| nil => 0
| cons h t => S (length X t)
end.
型の注釈は
あってはならない
適切な型を
引数に与える
Example test_length1 :
length nat (cons nat 1 (cons nat 2 (nil nat))) = 2.
Example test_length2 :
length bool (cons bool true (nil bool)) = 1.
前回のリスト上の関数も再定義できる
6
型推論
Fixpoint app (X : Type) (l1 l2 : list X)
: (list X) :=
match l1 with
| nil => l2
| cons h t => cons X h (app X t l2)
end.
型の注釈を省略
Fixpoint app' X l1 l2 : list X :=
match l1 with
| nil => l2
| cons h t => cons X h (app' X t l2)
end.
app と app' は同じ型
forall X : Type,
list X -> list X -> list X
7
引数の合成と暗黙的引数
Definition list123 :=
cons nat 1 (cons nat 2 (cons nat 3 (nil nat))).
合成
Definition list123' :=
cons _ 1 (cons _ 2 (cons _ 3 (nil _))).
Arguments nil {X}. 暗黙的引数
Arguments cons {X} _ _.
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y []) ..).
Definition list123''' := [1, 2, 3].
8
練習：多相型リスト
Fixpoint repeat (X : Type)
(n : X) (count : nat) : list X :=
match count with
| 0 => []
| S count' => n :: repeat _ n count'
end.
9
その他の多相的なデータ型(自習)
• 組
• オプション
10
データとしての関数
11
高階関数
1. 引数として渡せる
2. 結果として返せる
3. データ構造に格納できる
• Coqでは、関数が第1級の市民
• 高階関数：他の関数を処理する関数
Definition doit3times {X:Type} (f:X→X) (n:X) : X :=
f (f (f n)).
Example test_doit3times: doit3times minustwo 9 = 3.
Example test_doit3times': doit3times negb true = false.
12
部分適用
Check plus.
(* ==> nat -> nat -> nat *)
Definition plus3 := plus 3.
適用の結果は
関数
13
高階関数の例：フィルタ
Fixpoint filter {X:Type} (test: X→bool) (l:list X)
: (list X) :=
match l with
| [] => []
| h :: t => if test h then h :: (filter test t)
else filter test t
end.
Example test_filter1: filter evenb [1,2,3,4] = [2,4].
偶数か？
14
無名関数
Example test_anon_fun':
doit3times (fun n => n * n) 2 = 256.
無名関数
• 高階関数の引数には一度しか使わない関数が頻出する
• 一度しか使わない関数には無名関数を使うと良い
15
高階関数の例：map
Fixpoint map {X Y:Type} (f:X→Y) (l:list X)
: (list Y) :=
match l with
| [] => []
| h :: t => (f h) :: (map f t)
end.
Example test_map1:
map (plus 3) [2,0,2] = [5,3,5].
16
練習：flat_map
flat_map (fun n => [n,n+1,n+2]) [1,5,10]
= [1, 2, 3, 5, 6, 7, 10, 11, 12].
Fixpoint concat {X : Type} (l:list (list X))
: (list X) :=
match l with
| [] => []
| h :: t => app h (concat t)
end.
Fixpoint flat_map {X Y:Type} (f:X→list Y) (l:list X)
: (list Y) :=
concat (map f l).
17
高階関数の例：fold
cf. Google's
map/reduce
Fixpoint fold {X Y:Type}
(f: X→Y→Y) (l:list X) (b:Y) : Y :=
match l with
| nil => b
| h :: t => f h (fold f t b)
end.
fold plus [1,2,3,4] 0
→ 1 + (2 + (3 + (4 + 0)))
18
関数を構築する関数
定数関数
Definition constfun {X: Type} (x: X) : nat→X :=
fun (k:nat) => x.
常にtrue
Definition ftrue := constfun true.
Example constfun_example1 : ftrue 0 = true.
Example constfun_example2 : (constfun 5) 99 = 5.
19
関数を構築する関数
Definition override {X: Type}
通常は f
(f: nat→X) (k:nat) (x:X) : nat→X:=
fun (k':nat) => if beq_nat k k' then x else f k'.
引数が k のときは
何もしない
Definition fmostlytrue :=
override (override ftrue 1 false) 3 false.
Example
Example
Example
Example
override_example1
override_example2
override_example3
override_example4
:
:
:
:
fmostlytrue
fmostlytrue
fmostlytrue
fmostlytrue
0
1
2
3
=
=
=
=
true.
false.
true.
false.
20
練習：何を表しているか
Theorem override_example : ∀(b:bool),
(override (constfun b) 3 true) 2 = b.
• 引数が 3 のときはtrue を返す
• そうでないときは引数に constfun b を適用する
(bを返す)
21
Coq をさらに詳しく
22
apply タクティック
Theorem silly1 : ∀(n m o p : nat),
n = m →
[n,o] = [n,p] →
[n,o] = [m,p].
Proof.
intros n m o p eq1 eq2.
rewrite ← eq1.
(* これまでと同様に "rewrite → eq2. reflexivity."
で終えられる。
しかし、同じ結果が apply タクティック１つで得られる *)
apply eq2.
Qed.
23
unfold タクティック
Theorem unfold_example : ∀m n,
3 + n = m →
plus3 n + 1 = m + 1.
Proof.
Coq は自動で
intros m n H.
plus3 を展開しない
unfold plus3.
rewrite → H.
reflexivity. Qed.
24
Inversion タクティック
Inductive nat : Type :=
| O : nat
| S : nat → nat.
• コンストラクタSは単射
• O と S は disjoint
25
Inversion タクティック
仮定のひとつ
c a1 a2 ... an = d b1 b2 ... bm
• c = d のとき，
a1 = b1, a2 = b2, ... を仮定に追加
• c <> d のとき，仮定が false
26
Inversion タクティックの例
Theorem eq_add_S :
∀(n
m : nat),
S n = S m →
n = m.
Proof.
intros n m eq. inversion eq. reflexivity. Qed.
∀(n
→
Theorem silly4 :
m : nat),
[n] = [m]
n = m.
Proof.
intros n o eq. inversion eq. reflexivity. Qed.
27
練習：Inversion
Example sillyex1 :
∀(X : Type) (x y z : X) (l j : list X),
x :: y :: l = z :: j →
y :: l = x :: j →
x = y.
Proof.
intros X x y z l j ex1 ex2.
inversion ex1. inversion ex2.
rewrite H0. reflexivity.
Qed.
28
IHの工夫
Theorem beq_nat_eq_FAILED :
∀n
m,
true = beq_nat n m → n = m.
Proof.
intros n m H. induction n as [| n'].
Case "n = 0".
destruct m as [| m'].
SCase "m = 0". reflexivity.
SCase "m = S m'". simpl in H. inversion H.
Case "n = S n'".
destruct m as [| m'].
SCase "m = 0". simpl in H. inversion H.
SCase "m = S m'".
apply eq_remove_S.
(* 手詰まり．．．IHが特殊な m について言及 *)
Admitted.
29
IHの工夫
true = beq_nat n' m → n' = m .
ある m について
∀ m : nat, true = beq_nat n' m → n' = m
任意の m について
30
IHの工夫
Theorem beq_nat_eq :
∀n
→
m,
true = beq_nat n m
n = m.
m は文脈に移動しない
Proof.
intros n. induction n as [| n'].
Case "n = 0".
intros m. destruct m as [| m'].
SCase "m = 0". reflexivity.
SCase "m = S m'". simpl. intros contra. inversion
contra.
Case "n = S n'".
intros m. destruct m as [| m'].
SCase "m = 0". simpl. intros contra. inversion
contra.
SCase "m = S m'". simpl. intros H.
apply eq_remove_S. apply IHn'. apply H. Qed.
31
仮定にタクティックを使う
simpl in H ：仮定 H を単純化
apply L in H ：仮定 H に条件文 L を適用
L1 → L2 ： L1 を L2 に書換え
32
その他のタクティック
• 複合式の上に destruct を用いる
• remember
• apply ... with ...
33
復習
34
• これまで見たタクティック
– intros, reflexivity, apply, apply... in H, apply...
with..., simpl, simpl in H, rewrite, rewrite ... in H,
symmetry, symmetry in H, unfold, unfold... in H,
destruct... as..., induction... as..., inversion,
remember (e) as x, assert (e) as H
– 大体のことが可能
• 今後，導入するタクティック
– それほど多くない量
– automationタクティック
35
Gen
〜IHの一般化〜
36
IHの選定
Theorem double_injective_FAILED :
∀n
m,
double n = double m →
n = m.
うまくいかない
Proof.
intros n m. induction n as [| n'].
Case "n = O"...
P n = "if double n = double m, then n =
m"
•P O (i.e., "if double O = double m then O =
m")
•P n → P (S n) (i.e., "if double n = double m
then n = m" implies "if double (S n) = double
m then S n = m").
37
IHの選定
Theorem double_injective_FAILED :
∀n
m,
double n = double m →
n = m.
うまくいく
Proof.
intros n. induction n as [| n'].
Case "n = O"...
P n = "for any m, if double n = double m, then n =
m"
•P O (i.e., "if double O = double m then O = m")
•P n → P (S n) (i.e., "for any m, if double n = double m
then n = m" implies "for any m, if double (S n) = double
m then S n = m").
38
IHの選定（今度はmで）
Theorem double_injective_take2_FAILED :
m, double n = double m → n = m.
Proof.
intros n m. induction m as [| m'].
Case "m = O"...
うまくいかない
∀n
P n = "if double n = double m, then n =
m"
•P O (i.e., "if double O = double m then O =
m")
•P m → P (S n) (i.e., "if double n = double m
then n = m" implies "if double (S n) = double
m then S n = m").
39
IHの一般化
Theorem double_injective_take2 :
∀n
m, double n = double m
Proof.
intros n m.
generalize dependent n.
induction m as [| m'].
Case "m = O"...
→
n = m.
うまくいく
40

Download Report