第5回講義

5月15日の内容です。前回の課題だった補題、
depth≤size : (t : Term) → (depth t ≤ size t)
を皆でやってみました。
プログラムにコメントを書き込める人はどんどん追記をお願いします。


授業で書いたプログラム(A先生ページより)


module A5 where

open import Data.Bool
open import Data.Nat
open import Data.Nat.Properties
open import Data.Fin hiding (_+_; _≤_)
open import Data.Vec
open import Relation.Binary.PropositionalEquality
open import Relation.Binary
open import Algebra.Structures

-------------------------------------------------------------------------

data Term : Set where
Num : ℕ → Term
 Add : Term → Term → Term

t1 : Term
t1 = Num 3

t2 : Term
t2 = Add (Num 3) (Num 2)

t3 : Term
t3 = Add (Num 2) (Add (Num 1) (Num 3))

size : Term → ℕ
size (Num x) = 1
size (Add t t₁) = suc (size t + size t₁)

depth : Term → ℕ
depth (Num x) = 1
depth (Add t t₁) = suc (depth t ⊔ depth t₁)


--ライブラリからtransの定義を引っ張ってくることに成功。詳しくは別途解説を用意しました。
≤-trans : Transitive _≤_
≤-trans = IsPreorder.trans (IsPartialOrder.isPreorder (IsTotalOrder.isPartialOrder (IsDecTotalOrder.isTotalOrder (DecTotalOrder.isDecTotalOrder decTotalOrder))))

⊔-comm = IsCommutativeMonoid.comm (IsSemiringWithoutOne.+-isCommutativeMonoid (IsCommutativeSemiringWithoutOne.isSemiringWithoutOne ⊔-⊓-0-isCommutativeSemiringWithoutOne))

≤-⊔R : (l m n : ℕ) → l ≤ m → l ⊔ n ≤ m ⊔ n
≤-⊔R zero zero n l≤m = n≤m+n zero n
≤-⊔R zero (suc m) n l≤m rewrite ⊔-comm (suc m) n = m≤m⊔n n (suc m) -- rewriteは置換するための命令らしい。しかし詳細は不明。別途解説。
≤-⊔R (suc l) .(suc n) zero (s≤s {.l} {n} l≤m) = s≤s l≤m
≤-⊔R (suc l) .(suc m) (suc n) (s≤s {.l} {m} l≤m) = s≤s (≤-⊔R l m n l≤m)

≤-⊔L : (l m n : ℕ) → l ≤ m → n ⊔ l ≤ n ⊔ m
≤-⊔L l m zero l≤m = l≤m
≤-⊔L zero m (suc n) l≤m = m≤m⊔n (suc n) m
≤-⊔L (suc l) .(suc m) (suc n) (s≤s {.l} {m} l≤m) = s≤s (≤-⊔L l m n l≤m)

m≤m+0 : (m : ℕ) → m ≤ m + 0
m≤m+0 zero = z≤n
m≤m+0 (suc m) = s≤s (m≤m+0 m)

m+suc-n≡suc-m+n : (m n : ℕ) → m + suc n ≡ suc (m + n)
m+suc-n≡suc-m+n zero n = refl
m+suc-n≡suc-m+n (suc m) n = cong suc (m+suc-n≡suc-m+n m n)

m⊔n≤m+n : (m n : ℕ) → m ⊔ n ≤ m + n
m⊔n≤m+n zero n = n≤m+n zero n
m⊔n≤m+n (suc m) zero = s≤s (m≤m+0 m)
m⊔n≤m+n (suc m) (suc n) rewrite m+suc-n≡suc-m+n m n =
s≤s (≤-trans (m⊔n≤m+n m n) (n≤1+n (m + n)))

depth≤size : (t : Term) → depth t ≤ size t
depth≤size (Num x) = s≤s z≤n
depth≤size (Add t t₁) =
s≤s (≤-trans (≤-⊔R (depth t) (size t) (depth t₁) (depth≤size t))
      (≤-trans (≤-⊔L (depth t₁) (size t₁) (size t) (depth≤size t₁))
               (m⊔n≤m+n (size t) (size t₁))))


rewriteの使い方


置換できると良いのにな、と思う場面で活躍します。
f(a) rewrite a≡b
と書くと、
f(b)
とみなしてくれるようです。

上のプログラムを例に説明します。該当箇所を抜粋。

≤-⊔R : (l m n : ℕ) → l ≤ m → l ⊔ n ≤ m ⊔ n
≤-⊔R zero zero n l≤m = n≤m+n zero n
≤-⊔R zero (suc m) n l≤m rewrite ⊔-comm (suc m) n = m≤m⊔n n (suc m) -- rewriteは置換するための命令らしい。しかし詳細は不明。別途解説。
≤-⊔R (suc l) .(suc n) zero (s≤s {.l} {n} l≤m) = s≤s l≤m
≤-⊔R (suc l) .(suc m) (suc n) (s≤s {.l} {m} l≤m) = s≤s (≤-⊔R l m n l≤m)

まず、
≤-⊔R zero (suc m) n l≤m
と書いた時点で、結果は
zero ⊔ n ≤ (suc m) ⊔ n
となります。
ここで、
n ≤ n ⊔ (suc m)
は既に示しているm≤m⊔nからいえるのに、今示したいのは左右逆じゃないか・・・!と思うと思います。

そこで、rewrite ⊔-comm (suc m) nを書いているわけ。

⊔-comm (suc m) n は (suc m) ⊔ n ≡ n ⊔ (suc m) です。
よって≤-⊔R zero (suc m) n l≤m rewrite ⊔-comm (suc m) n と書くことで、
(suc m) ⊔ n ≡ n ⊔ (suc m)を使って、
zero ⊔ n ≤ (suc m) ⊔ n を
zero ⊔ n ≤ n ⊔ (suc m) へと変換(?)することが可能となります。
こういう式だと思って良いなら、これはm≤m⊔nで示せるやつだよね、という感じでプログラムは続いています。

追記:rewriteに使う「a ≡ b」は\equivを使って自分で定義したもので良いんですね!(当たり前でしょうか。)
足し算のcommutativityを以下のように示してみました。
あまり綺麗ではありませんが、自分で作った「a ≡ b」を使ったサンプルとしておいておきます。
※わざわざ作らなくてもライブラリのどこかに埋まっているそうです。


足し算のcommutativity

-- 何かと使うので。ゼロの場合。
rightIdentity : (n : ℕ) -> n + 0 ≡ n
rightIdentity zero = refl
rightIdentity (suc n) = cong suc (rightIdentity n)

-- 名前が悪いですが。
succ : (n m : ℕ) → n + suc m ≡ suc (n + m)
succ zero m = refl
succ (suc n) m = cong suc (succ n m)

-- こちらは上のちょっと違うバージョン
succ2 : (n m : ℕ) → suc n + m ≡ suc (n + m)
succ2 n zero = refl
succ2 n (suc m) = cong suc refl

-- 自明な感じ。C-c C-rに頼って作りました。
trans≡ : (a b c : ℕ ) → a ≡ b → b ≡ c → a ≡ c
trans≡ .c .c c refl refl = refl

-- メイン。
comm : (n m : ℕ) → n + m ≡ m + n
comm zero zero = refl
comm zero (suc m) rewrite rightIdentity (suc m) = refl
comm (suc n) zero rewrite rightIdentity (suc n) = refl
comm (suc n) (suc m) rewrite succ (suc n) m = cong suc (trans≡ (suc (n + m)) (suc n + m) (m + suc n) (succ2 n m) (comm (suc n) m))


ライブラリから定義を取り出す方法


≦に関するtransitivityをどこからかもってきて使いたい、という状況を想定します。
≦のtransitivityはNat.agdaの中に見つかりました。


decTotalOrder : DecTotalOrder _ _ _
decTotalOrder = record
{ Carrier         = ℕ
 ; _≈_             = _≡_
 ; _≤_             = _≤_
 ; isDecTotalOrder = record
     { isTotalOrder = record
         { isPartialOrder = record
             { isPreorder = record
                 { isEquivalence = PropEq.isEquivalence
                 ; reflexive     = refl′
                 ; trans       = trans  
                 }
             ; antisym  = antisym
             }
         ; total = total
         }
     ; _≟_  = _≟_
     ; _≤?_ = _≤?_
     }
 }

これを取り出す方法が、
≤-trans : Transitive _≤_
≤-trans = IsPreorder.trans (IsPartialOrder.isPreorder (IsTotalOrder.isPartialOrder (IsDecTotalOrder.isTotalOrder (DecTotalOrder.isDecTotalOrder decTotalOrder))))
です。

transがどこにあるかを見てみると、まず、
decTotalOrderというレコードの中の、さらにisDecTotalOrderというフィールドの中にあることがわかります。
(DecTotalOrder.isDecTotalOrder decTotalOrder)
は、decTotalOrderの中のisDecTotalOrderのフィールドを参照しに行きます。
ここで、最初が大文字になっていることに注意して下さい。
(どうやらこういうルールになっているようです。)

その後を見ると、参照した先のフィールドはさらにレコードになっていて、
transはisTotalOrderというフィールドの中に埋まっているのが見えます。
そこを参照しにいっているのが
(IsDecTotalOrder.isTotalOrder (DecTotalOrder.isDecTotalOrder decTotalOrder))
です。
・・・・・というように、transにたどり着くまで潜っていきます。


ちなみに、すぐ下の⊔-commの例にあるのですが、
+-isCommutativeMonoid
というフィールド名で、最初を大文字にする余地がないぞ困ったな、という時。
単に記号を除いて、
IsCommutativeMonoid
とすれば良いようです。

別解1


depth t ≦ size t -> depth t ≦ size t + size t_1
depth t_1 ≦ size t_1 -> depth t_1 ≦ size t + size t_1
から、
(depth t ≦ size t + size t_1) -> (depth t_1 ≦ size t + size t_1) -> depth t ⊔ depth t_1 ≦ size t + size t_1
を示すという方針。
実際に成功した人は是非プログラムを貼って下さい:) => 貼っておきました

プログラム


lemma1 : {a b c : ℕ} -> a ≤ c -> b ≤ c -> a ⊔ b ≤ c
lemma1 z≤n z≤n = z≤n
lemma1 z≤n (s≤s h2) = s≤s h2
lemma1 (s≤s h1) z≤n = s≤s h1
lemma1 (s≤s h1) (s≤s h2) = s≤s (lemma1 h1 h2)

lemma2 : (a b c : ℕ) -> a ≤ b -> a ≤ b + c
lemma2 .0 b c z≤n = z≤n
lemma2 .(suc a) .(suc b) c (s≤s {a} {b} h) = s≤s (lemma2 a b c h)

lemma3 : (a b c : ℕ) -> a ≤ c -> a ≤ b + c
lemma3 .0 b c z≤n = z≤n
lemma3 .(suc a) b .(suc c) (s≤s {a} {c} h) = lemma3 (suc a) b (suc c) (s≤s h)

depth≤size : (t : Term) → depth t ≤ size t
depth≤size (Num x) = s≤s z≤n
depth≤size (Add t t₁) =
s≤s (lemma1 (lemma2 (depth t) (size t) (size t₁) (depth≤size t))
             (lemma3 (depth t₁) (size t) (size t₁) (depth≤size t₁)))

プログラム2

関数名が酷いことになっていますが、一応載せておきます。

mon+ : (a b c : ℕ) -> (a ≤ b) -> (a ≤ (b + c))
mon+ .0 b c z≤n = z≤n
mon+ .(suc m) .(suc n) c (s≤s {m} {n} l) = s≤s (mon+ m n c l)

lemma2 : (a b : ℕ) -> (a ≤ b) -> (a ≤ suc b)
lemma2 .0 b z≤n = z≤n
lemma2 .(suc m) .(suc n) (s≤s {m} {n} l) = s≤s (lemma2 m n l)

mon+2 : (a b c : ℕ) -> (a ≤ b) -> (a ≤ (c + b))
mon+2 .0 b c z≤n = z≤n
mon+2 .(suc m) .(suc n) zero (s≤s {m} {n} l) = s≤s l
mon+2 .(suc m) .(suc n) (suc c) (s≤s {m} {n} l) = s≤s (mon+2 m (suc n) c (lemma2 m n l))

lemma1 : (a b c : ℕ) -> (a ≤ c) -> (b ≤ c) -> (a ⊔ b ≤ c)
lemma1 .0 .0 c z≤n z≤n = z≤n
lemma1 .0 .(suc m) .(suc n) z≤n (s≤s {m} {n} m₁) = s≤s m₁
lemma1 .(suc m) .0 .(suc n) (s≤s {m} {n} l) z≤n = s≤s l
lemma1 .(suc m) .(suc m₁) .(suc n) (s≤s {m} {n} l) (s≤s {m₁} m₂) = s≤s (lemma1 m m₁ n l m₂)

depth≤size : (t : Term) → depth t ≤ size t
depth≤size (Num x) = s≤s z≤n
depth≤size (Add x x₁) = s≤s (lemma1 (depth x) (depth x₁) ((size x) + (size x₁))
                                  (mon+ (depth x) (size x) (size x₁) (depth≤size x)) 
                                   (mon+2 (depth x₁) (size x₁) (size x) (depth≤size x₁)))

  • 最終更新:2014-05-27 18:49:30

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

認証パスワード