第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

このWIKIを編集するにはパスワード入力が必要です

認証パスワード