Agdaはじめました
あぐださん！あぐださんヤッホ！
Agda2に手を出してみた．とりあえずインストールし文法とかagda-modeとかをザックリとだが覚え，クイックソートを止められるあたりまで把握したので，練習としてData.Natに無さげだった速い冪乗を書いてみることに．
とりあえずの目標設定は，
- 速い冪乗(1/2してくやつ)を書く
- 遅い冪乗(1ずつ減らしてくやつ)と等価であることを示す
まず速い冪乗と遅い冪乗を書く．
module Power where
open import Data.Bool
open import Data.Nat
open import Induction.Nat
open import Data.Nat.Properties
import Induction.WellFounded as WF
open import Function
odd : ℕ → Bool
odd 0 = false
odd (suc n) = not (odd n)
even : ℕ → Bool
even = not ∘ odd
power' : ℕ → (n : ℕ) → <-Rec (λ _ → ℕ) n → ℕ
power' n 0 _ = 1
power' n 1 _ = n
power' n (suc (suc m)) rec = x * x * (if odd m then n else 1)
where
x = rec (suc ⌊ m /2⌋) (s≤′s (s≤′s (⌊n/2⌋≤′n m)))
-- 速い冪乗
_^_ : ℕ → ℕ → ℕ
n ^ m = <-rec (λ _ → ℕ) (power' n) m
where open WF.All <-well-founded
-- 遅い冪乗
_^^_ : ℕ → ℕ → ℕ
n ^^ 0 = 1
n ^^ suc m = n * n ^^ m
open import IO
open import Data.List
open import Data.Nat.Show
open import Data.Colist
main = run (IO.mapM (putStrLn ∘ show ∘ (λ m → 2 ^ m)) (fromList ls))
where ls : List ℕ
ls = 1 ∷ 4 ∷ 2 ∷ 3 ∷ 5 ∷ 0 ∷ []遅い冪乗は特にどうということもなく普通に1ずつ減らしながら掛け算すれば止まる．速い冪乗は普通に書くとAgdaさんがサーモンピンクになって「止まるかわからないよぅ」って泣きを入れるので整礎帰納法で止める．
で，ここまではよかったんだけど，速い冪乗と遅い冪乗が等価であることが示せなくて困る．使いそうな材料を用意だけして詰んだ．
open import Relation.Binary.PropositionalEquality as PropEq
using (_≡_; _≢_; refl; sym; cong;)
open PropEq.≡-Reasoning
-- +と*の結合則と交換則を取り出しておく
+-comm = IsCommutativeMonoid.comm
(IsCommutativeSemiring.+-isCommutativeMonoid
(CommutativeSemiring.isCommutativeSemiring commutativeSemiring))
where open import Algebra
open import Algebra.Structures
+-assoc = IsSemigroup.assoc
(IsCommutativeMonoid.isSemigroup
(IsCommutativeSemiring.+-isCommutativeMonoid
(CommutativeSemiring.isCommutativeSemiring commutativeSemiring)))
where open import Algebra
open import Algebra.Structures
*-comm = IsCommutativeMonoid.comm
(IsCommutativeSemiring.*-isCommutativeMonoid
(CommutativeSemiring.isCommutativeSemiring commutativeSemiring))
where open import Algebra
open import Algebra.Structures
*-assoc = IsSemigroup.assoc
(IsCommutativeMonoid.isSemigroup
(IsCommutativeSemiring.*-isCommutativeMonoid
(CommutativeSemiring.isCommutativeSemiring commutativeSemiring)))
where open import Algebra
open import Algebra.Structures
-- 使いそうな材料たち
⌊n/2⌋+⌈n/2⌉ : ℕ → ℕ
⌊n/2⌋+⌈n/2⌉ n = ⌊ n /2⌋ + ⌈ n /2⌉
⌊n/2⌋+⌈n/2⌉≡id : (n : ℕ) → ⌊n/2⌋+⌈n/2⌉ n ≡ n
⌊n/2⌋+⌈n/2⌉≡id 0 = refl
⌊n/2⌋+⌈n/2⌉≡id (suc n) =
begin
⌊n/2⌋+⌈n/2⌉ (suc n)
≡⟨ +-comm ⌊ suc n /2⌋ (suc ⌊ n /2⌋) ⟩
suc (⌊n/2⌋+⌈n/2⌉ n)
≡⟨ cong suc (⌊n/2⌋+⌈n/2⌉≡id n) ⟩
suc n
∎
_%2 : ℕ → ℕ
0 %2 = 0
1 %2 = 1
suc (suc n) %2 = n %2
⌊n/2⌋+n%2≡⌈n/2⌉ : (n : ℕ) → ⌊ n /2⌋ + n %2 ≡ ⌈ n /2⌉
⌊n/2⌋+n%2≡⌈n/2⌉ 0 = refl
⌊n/2⌋+n%2≡⌈n/2⌉ 1 = refl
⌊n/2⌋+n%2≡⌈n/2⌉ (suc (suc n)) = cong suc (⌊n/2⌋+n%2≡⌈n/2⌉ n)
2*⌊n/2⌋+n%2≡id : (n : ℕ) → 2 * ⌊ n /2⌋ + n %2 ≡ n
2*⌊n/2⌋+n%2≡id n =
begin
2 * ⌊ n /2⌋ + n %2
≡⟨ sym (cong (λ x → ⌊ n /2⌋ + x + n %2) (+-comm 0 ⌊ n /2⌋)) ⟩
⌊ n /2⌋ + ⌊ n /2⌋ + n %2
≡⟨ +-assoc ⌊ n /2⌋ ⌊ n /2⌋ (n %2) ⟩
⌊ n /2⌋ + (⌊ n /2⌋ + n %2)
≡⟨ cong (_+_ ⌊ n /2⌋) (⌊n/2⌋+n%2≡⌈n/2⌉ n) ⟩
⌊ n /2⌋ + ⌈ n /2⌉
≡⟨ ⌊n/2⌋+⌈n/2⌉≡id n ⟩
n
∎
n^^a*n^^b≡n^^a+b : (n a b : ℕ) → n ^^ a * n ^^ b ≡ n ^^ (a + b)
n^^a*n^^b≡n^^a+b n 0 b = +-comm (n ^^ b) zero
n^^a*n^^b≡n^^a+b n (suc a) b =
begin
n ^^ (suc a) * n ^^ b
≡⟨ *-assoc n (n ^^ a) (n ^^ b) ⟩
n * (n ^^ a * n ^^ b)
≡⟨ cong (_*_ n) (n^^a*n^^b≡n^^a+b n a b) ⟩
n ^^ (suc a + b)
∎
-- 本題
n^m≡n^^m : (n m : ℕ) → n ^ m ≡ n ^^ m
n^m≡n^^m n 0 = refl
n^m≡n^^m n 1 =
begin
n ^ 1
≡⟨ +-comm 0 n ⟩
1 * n
≡⟨ *-comm 1 n ⟩
n ^^ 1
∎
n^m≡n^^m n (suc (suc m)) =
begin
n ^ suc (suc m)
≡⟨ refl ⟩
power' n (suc ⌊ m /2⌋)
(WF.Some.wfRec-builder (λ x → ℕ) (power' n) (suc ⌊ m /2⌋)
(<-well-founded′ (suc (suc m)) (suc ⌊ m /2⌋)
(s≤′s (s≤′s (⌊n/2⌋≤′n m)))))
*
power' n (suc ⌊ m /2⌋)
(WF.Some.wfRec-builder (λ x → ℕ) (power' n) (suc ⌊ m /2⌋)
(<-well-founded′ (suc (suc m)) (suc ⌊ m /2⌋)
(s≤′s (s≤′s (⌊n/2⌋≤′n m)))))
* (if odd m then n else suc zero)
≡⟨ { }0 ⟩
{ }1
≡⟨ { }2 ⟩
n ^ (suc ⌊ m /2⌋) * n ^ (suc ⌊ m /2⌋) * (if odd m then n else suc zero)
≡⟨ { }3 ⟩
n ^^ (suc ⌊ m /2⌋) * n ^^ (suc ⌊ m /2⌋) * (if odd m then n else suc zero)
≡⟨ { }4 ⟩
n ^^ (suc ⌊ m /2⌋) * n ^^ (suc ⌊ m /2⌋) * n ^^ (m %2)
≡⟨ { }5 ⟩
n ^^ (suc ⌊ m /2⌋ + suc ⌊ m /2⌋ + m %2)
≡⟨ { }6 ⟩
n ^^ suc (suc m)
∎ここから先とりあえず，
<-well-founded′ (suc (suc n)) (suc ⌊ n /2⌋) (s≤′s (s≤′s (⌊n/2⌋≤′n n))) ≡ <-well-founded (suc ⌊ n /2⌋)
を教えてあげたいんだけど，なんだか混乱してきて止まってしまった．
