Software Foundations その

(1)

「計算と論理」

Software Foundations その 2

五十嵐淳

[email protected]

京都大学

October 22, 2013

(2)

今日のメニュー

Induction.v

場合分けに名前をつける

(Case

_{タクティック}

)

数学的帰納法による証明

(induction

_{タクティック}

)

証明中の証明

(assert

_{タクティック}

)

(3)

場合分けに名前をつける

場合分けの証明は読みにくい

▶

どこまでが「ひとつの場合」なの

!?

⇒

コメント・インデントをつける？

▶

今どの場合を証明しようとしているか

(

_特にコメントが画面の外に流れると

)

わかりにくい

⇒ Case

タクティック

!

▶

この教科書の著者謹製

▶

教科書をこの部分まで読み込むと使えるように

なる

(4)

Case を使って書き直した証明

Theorem plus_1_neq_0 : forall n : nat, beq_nat (n + 1) 0 = false.

Proof.

intros n. destruct n as [| n’].

Case "n = 0".

reflexivity.

Case "n = S n’".

reflexivity.

Qed.

デモ

:

単なるコメントとの違い

andb_true_elim1

の証明

(5)

Case _{タクティック}

Case

の使用は強制ではないが強く推奨

▶

後で読み返してわかる証明を書こう

!

▶ (Case

に限らず，一行の長さとかも気をつけよう

!)

場合分けが入れ子になる時のための

SCase, SSCase, . . .

▶ SCase = subcase

(6)

今日のメニュー

Induction.v

場合分けに名前をつける

(Case

_{タクティック}

)

数学的帰納法による証明

(induction

_{タクティック}

)

証明中の証明

(assert

_{タクティック}

)

(7)

帰納法による証明

定理 : 0 は足し算の右単位元

Theorem plus_0_r : forall n:nat, n + 0 = n.

詰まる証明

Proof.

intros n. simpl. (* Does nothing! *)

(8)

「こういう時は場合分けでしょ？」

またもや詰まる証明

Proof.

intros n. destruct n as [| n’].

Case "n = 0".

reflexivity. (* so far so good... *) Case "n = S n’".

simpl. (*

また同じようなゴールが…

orz *)

場合分けをいくら続けてもキリがない

!

n

より

1

小さい

n’

について

plus_0_r

が成り立って

いれば…

⇒

^{数学的帰納法}

(9)

数学的帰納法

P(n)

を自然数

n

の性質について述べた命題とする

数学的帰納法の原理

「任意の自然数

n

について

P(n)

」は以下と同値

P(0)

_かつ

任意の自然数

n^′

_について

P(n^′)

_ならば

P(S n^′)

単なる場合分けと違って，

P(S n^′)

_{を示すのに，ひと} つ小さい数では

P

が成立していること

(

つまり

P(n^′))

を仮定してよい

P(n^′)

を「帰納法の仮定」

(induction hypothesis, IH)

と呼ぶ

(10)

数学的帰納法の妥当性

個々の具体的な数

(

例えば

4)

について

P

が成立することが，

P(0)

かつ

任意の自然数

n^′

について

P(n^′)

ならば

P(S n^′)

を組み合わせて導き出せる

(11)

数学的帰納法を使った証明

Theorem plus_0_r : forall n:nat, n + 0 = n.

Proof.

intros n. induction n as [| n’].

Case "n = 0". reflexivity.

Case "n = S n’".

simpl. rewrite -> IHn’. reflexivity. Qed.

基本的な使い方は

destruct

と同じ

intro

_パターン

IHn’

が帰納法の仮定

(Coq

_{が勝手に名前をつける}

)

(12)

数学的帰納法を使った証明 (2)

Theorem minus_diag : forall n, minus n n = 0.

(13)

今日のメニュー

Induction.v

場合分けに名前をつける

(Case

_{タクティック}

)

数学的帰納法による証明

(induction

_{タクティック}

)

証明中の証明

(assert

_{タクティック}

)

(14)

証明中の証明

以前に証明した定理は他の定理の証明中で使える証明中でも「サブ定理」を宣言・証明できる

⇒ assert

タクティック

(15)

Theorem mult_0_plus’ : forall 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.

Case

は，読み易さのため

assert 0 + n = n as H

と書いてもよい

(16)

assert の挙動

新たなサブゴールとして

assert

された命題が追加される

前のゴールの文脈には

assert

された命題が仮定と

して追加されている

(17)

assert の応用

そこじゃない !

Theorem plus_rearrange_firsttry : forall n m p q : nat,

(n + m) + (p + q) = (m + n) + (p + q).

Proof.

intros n m p q.

(* n

と

m

を入れ替えればいいんでしょ？

*) rewrite

→

plus_comm.

(18)

assert の応用

Theorem plus_rearrange : forall 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).

(* n

と

m

の交換に特化

*) Case "Proof of assertion".

rewrite -> plus_comm. reflexivity.

rewrite -> H. reflexivity. Qed.

(

こうしなきゃいけないのはどうかと思うが…

)

(19)

宿題： 10/29 _午前 10:30 _締切

Exercise

の

basic_induction, double_plus, beq_nat_refl

Software Foundations その

「計算と論理」