第7回講義
5月29日の内容です。
前回定義したindNを使って、数学的帰納法で何か示してみよう!という回でした。
示したいのは、おなじみの「nまでの自然数の和」です。(割り算したくないので、実際は2倍したものを示しました。)
結構すごいスピードで進んだので、メモが不足しています。是非加筆をお願いします:)
プログラム
module A7 where
open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality.≡-Reasoning
-- どうしてopenなのかは不明 -- どんどん≡でつなげていきたいときに、そういう証明をさせてくれる。
open import Data.Nat.Properties
--isCommutativeSemiringのレコードを読み込んだことになっている。
open import Algebra.Structures
-- IsCommutativeSemiringの型定義を読み込んだ。
private module M = IsCommutativeSemiring
-- なぜかこれで上手くいく。
assoc = M.+-assoc
--これでassocが使えるようになる。 --いつでもこのやり方で良いのかはまだ分からない。 -- C-c C-o Mとやると、モジュールMの中身が確認できるので便利。
----------------------------------------------------------------
-- 折角recursionを定義したので、帰納法で何か証明してみよう。 -- sum n = 1 + 2 + ... + n -- 2 (sum n) = n(n + 1)
-- ℕのelimination rule
recN : {C : Set} → C → (ℕ → C → C) → (ℕ → C)
recN z s zero = z
recN z s (suc n) = s n (recN z s n)
sum : ℕ → ℕ
sum zero = zero
sum (suc n) = suc n + sum n
sum2 : ℕ → ℕ
sum2 n = recN zero (λ n c → suc n + c) n
-- zeroから初めて、λ n c → suc n + cという関数をn回繰り返す、と読むこともできる -- recNの中で、sは1つ小さい数(n)で呼び出されているので、 -- sum2の中では、ちゃんとsuc nを足すようにしている。(1つ小さい数で呼び出されても、ちゃんと元の数になるように。)
test1 : ℕ
test1 = sum2 (suc (suc zero))
test2 : ℕ
test2 = sum (suc (suc zero))
-- ℕのinduction principle
indN : {C : ℕ → Set} → C zero → ((n : ℕ) → C n → C (suc n)) → ((n : ℕ) → C n)
indN z s zero = z
indN z s (suc n) = s n (indN z s n)
-- lemma1 実際に証明してみる。 -- まずはindNを使わずに書いてみる。 -- いきなりやらずに、まずは手で証明しよう!重要。 -- 方針。以下のように変形していけると考える。 -- 2 * (sum (suc n)) -- = 2 * (suc n + sum n) -- = 2 * (suc n) + 2 * sum n -- = 2 * (suc n) + n * (n + 1) -- = 2 * (n + 1) + n * (n + 1) -- = (2 + n) * (n + 1) -- = (2 + n) * (1 + n) -- = (1 + n) * (2 + n) -- = suc n * (1 + suc n) -- = suc n * (suc n + 1)
lemma1 : (n : ℕ) → 2 * (sum n) ≡ n * (n + 1)
lemma1 zero = refl
lemma1 (suc n) =
-- ≡をどんどんつなげて書く書き方。transを何回やっても良いが、こちらのほうが楽? begin 2 * (sum (suc n)) ≡⟨ refl ⟩ -- \<と\> ここに使った規則を書く 2 * ((suc n) + sum n) ≡⟨ proj₁ (M.distrib isCommutativeSemiring) 2 (suc n) (sum n) ⟩ --どのSemiringのdistributionのproof termを取ってくるか、を指定してやる必要がある。 --こんかいはisCommutativeSemiringのdistributionがほしい。 -- proj₁は組の第一要素を取り出す操作。事情はもう少し先に書きました。 2 * (suc n) + 2 * (sum n) ≡⟨ cong (_+_ (2 * suc n)) (lemma1 n) ⟩ -- congに渡しているやつは特殊な見た目だが、これは足し算の右側だけを取り替えたいので。 -- lemm1 n の結果の両辺に、2 * suc nを足したら今欲しい命題がえられるから、congでそういうのを与える。 2 * (suc n) + n * (n + 1) ≡⟨ cong (λ x → 2 * x + n * (n + 1)) {suc n} {n + 1} (M.+-comm isCommutativeSemiring 1 n) ⟩ -- {suc n} {n + 1}はimplicitに何がλ xのxであるかをいってやっている。 2 * (n + 1) + n * (n + 1) ≡⟨ sym (M.distribʳ isCommutativeSemiring (n + 1) 2 n) ⟩ --ʳ \^r -- ただのdistribは、定義を見ると、ペアを返すらしい。右バージョンと左バージョンがあるので、上ではproj₁を用いた。 -- distribʳは始めから右バージョンらしいので、このままつかう。 (2 + n) * (n + 1) ≡⟨ cong (λ x → (2 + n) * x) {n + 1} {1 + n} (M.+-comm isCommutativeSemiring n 1) ⟩ (2 + n) * (1 + n) ≡⟨ (M.*-comm isCommutativeSemiring (2 + n) (1 + n)) ⟩ (1 + n) * (2 + n) ≡⟨ refl ⟩ suc n * (1 + suc n) ≡⟨ cong (_*_ (suc n)) (M.+-comm isCommutativeSemiring 1 (suc n)) ⟩ suc n * (suc n + 1) ∎ -- \qed
-- こちらは、indNを使った定義。
lemma2 : (n : ℕ) → 2 * (sum n) ≡ n * (n + 1)
lemma2 = indN
refl (λ n IH → begin 2 * sum (suc n) ≡⟨ refl ⟩ 2 * (suc n + sum n) ≡⟨proj₁ (M.distrib isCommutativeSemiring) 2 (suc n) (sum n) ⟩ 2 * suc n + 2 * sum n ≡⟨ cong (_+_ (2 * suc n)) IH⟩ 2 * suc n + n * (n + 1) ≡⟨ cong (λ x → 2 * x + n * (n + 1)) {suc n} {n + 1} (M.+-comm isCommutativeSemiring 1 n)⟩ 2 * (n + 1) + n * (n + 1) ≡⟨ sym (M.distribʳ isCommutativeSemiring (n + 1) 2 n) ⟩ (2 + n) * (n + 1) ≡⟨ cong (λ x → (2 + n) * x) {n + 1} {1 + n} (M.+-comm isCommutativeSemiring n 1)⟩ (2 + n) * (1 + n) ≡⟨ M.*-comm isCommutativeSemiring (2 + n) (1 + n) ⟩ (1 + n) * (2 + n) ≡⟨ refl ⟩ suc n * (1 + suc n) ≡⟨ cong (_*_ (suc n)) (M.+-comm isCommutativeSemiring 1 (suc n)) ⟩ (suc n * (suc n + 1)) ∎ ) -- 型をみてみると、indNを使うことにするとかなり数学の証明っぽい流れになっている -- 帰納法の仮定はIHと書けば使えるらしい。 -- (λ n IH →...の後にかくのはlemma1で示したものを「ほぼ」そのまま書いている。。 --※唯一の違いは: --再帰はしなくていいので、(lemma1 n)と書いていた部分はIHで良くなった。
Reasoningでの「?」について
Reasoningの途中で「?」を使おうと思ったのにエラーが出ちゃった!という声を聞きました。
よくある間違いみたいなので書いておきます。
大事なのは
・begin以降のインデント
・最後をqedで閉じていること
・スタートの式とゴールの式が(示したいものと)あっていること。
【間違い例】
lemma1 : (n : ℕ) → 2 * (sum n) ≡ n * (n + 1)
lemma1 zero = refl
lemma1 (suc n) =
begin 2 * (sum (suc n)) ≡⟨ ? ⟩ n * (n + 1) ∎
というように、
begin スタートの式 ≡⟨ ? ⟩ ゴールの式 ∎
と書けば、「?」が効くはずなのに、全体が真っ赤になってしまってエラーが表示されるぞ?!と思っていませんか?
この場合、エラーはたとえばこんな風にでます。
n * (n + 1) != suc (n + 1 + n * (suc n + 1)) of type ℕ
when checking that the expression
begin 2 * sum (suc n) ≡⟨ ? ⟩ (n * (n + 1) ∎) has type
2 * sum (suc n) ≡ suc n * (suc n + 1)
よーく読むと、一番最後に「どういう型を持っていないといけないか」が書いてあります。
そこで自分の書いたプログラムを読むと、ゴールとして書いている式が「suc n」のときのバージョンでないことがわかります。
この場合、ゴールの式を「(suc n) * (suc n + 1)」と書き直せば、ちゃんと「?」がききます。
証明の際は、この間を埋めるように途中過程を書き足していくとスムーズです。
課題
「2^0 + 2^1 + 2^2 + ... + 2^(n-1) = 2^n -1」を示すこと。
- 最終更新:2014-06-12 16:53:25