読者です 読者をやめる 読者になる 読者になる

Agdaはじめました

あぐださん!あぐださんヤッホ!


Agda2に手を出してみた.とりあえずインストールし文法とかagda-modeとかをザックリとだが覚え,クイックソートを止められるあたりまで把握したので,練習としてData.Natに無さげだった速い冪乗を書いてみることに.

とりあえずの目標設定は,

  1. 速い冪乗(1/2してくやつ)を書く
  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' : &#8469; → (n : &#8469;)  → <-Rec (λ _ → &#8469;) n → &#8469;
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 &#8970; m /2&#8971;) (s&#8804;′s (s&#8804;′s (&#8970;n/2&#8971;&#8804;′n m)))

-- 速い冪乗
_^_ : &#8469; → &#8469; → &#8469;
n ^ m = <-rec (λ _ → &#8469;) (power' n) m
  where open WF.All <-well-founded

-- 遅い冪乗
_^^_ : &#8469; → &#8469; → &#8469;
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 &#8728; show &#8728; (λ m → 2 ^ m)) (fromList ls))
  where ls : List &#8469;
        ls = 1 &#8759; 4 &#8759; 2 &#8759; 3 &#8759; 5 &#8759; 0 &#8759; []

遅い冪乗は特にどうということもなく普通に1ずつ減らしながら掛け算すれば止まる.速い冪乗は普通に書くとAgdaさんがサーモンピンクになって「止まるかわからないよぅ」って泣きを入れるので整礎帰納法で止める.

で,ここまではよかったんだけど,速い冪乗と遅い冪乗が等価であることが示せなくて困る.使いそうな材料を用意だけして詰んだ.

open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; _&#8802;_; 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

-- 使いそうな材料たち
&#8970;n/2&#8971;+&#8968;n/2&#8969; : &#8469; → &#8469;
&#8970;n/2&#8971;+&#8968;n/2&#8969; n = &#8970; n /2&#8971; + &#8968; n /2&#8969;

&#8970;n/2&#8971;+&#8968;n/2&#8969;≡id : (n : &#8469;) → &#8970;n/2&#8971;+&#8968;n/2&#8969; n ≡ n
&#8970;n/2&#8971;+&#8968;n/2&#8969;≡id 0 = refl
&#8970;n/2&#8971;+&#8968;n/2&#8969;≡id (suc n) =
  begin
    &#8970;n/2&#8971;+&#8968;n/2&#8969; (suc n)
  ≡&#10216; +-comm &#8970; suc n /2&#8971; (suc &#8970; n /2&#8971;) &#10217;
    suc (&#8970;n/2&#8971;+&#8968;n/2&#8969; n)
  ≡&#10216; cong suc (&#8970;n/2&#8971;+&#8968;n/2&#8969;≡id n) &#10217;
    suc n
  &#8718;

_%2 : &#8469; → &#8469;
0 %2 = 0
1 %2 = 1
suc (suc n) %2 = n %2

&#8970;n/2&#8971;+n%2≡&#8968;n/2&#8969; : (n : &#8469;) → &#8970; n /2&#8971; + n %2 ≡ &#8968; n /2&#8969;
&#8970;n/2&#8971;+n%2≡&#8968;n/2&#8969; 0 = refl
&#8970;n/2&#8971;+n%2≡&#8968;n/2&#8969; 1 = refl
&#8970;n/2&#8971;+n%2≡&#8968;n/2&#8969; (suc (suc n)) = cong suc (&#8970;n/2&#8971;+n%2≡&#8968;n/2&#8969; n)

2*&#8970;n/2&#8971;+n%2≡id : (n : &#8469;) → 2 * &#8970; n /2&#8971; + n %2 ≡ n
2*&#8970;n/2&#8971;+n%2≡id n =
  begin
    2 * &#8970; n /2&#8971; + n %2
  ≡&#10216; sym (cong (λ x → &#8970; n /2&#8971; + x + n %2) (+-comm 0 &#8970; n /2&#8971;)) &#10217;
    &#8970; n /2&#8971; + &#8970; n /2&#8971; + n %2
  ≡&#10216; +-assoc &#8970; n /2&#8971; &#8970; n /2&#8971; (n %2) &#10217;
    &#8970; n /2&#8971; + (&#8970; n /2&#8971; + n %2)
  ≡&#10216; cong (_+_ &#8970; n /2&#8971;) (&#8970;n/2&#8971;+n%2≡&#8968;n/2&#8969; n) &#10217;
    &#8970; n /2&#8971; + &#8968; n /2&#8969;
  ≡&#10216; &#8970;n/2&#8971;+&#8968;n/2&#8969;≡id n &#10217;
    n
  &#8718;

n^^a*n^^b≡n^^a+b : (n a b : &#8469;) → 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
  ≡&#10216; *-assoc n (n ^^ a) (n ^^ b) &#10217;
    n * (n ^^ a * n ^^ b)
  ≡&#10216; cong (_*_ n) (n^^a*n^^b≡n^^a+b n a b) &#10217;
    n ^^ (suc a + b)
  &#8718;

-- 本題
n^m≡n^^m : (n m : &#8469;) → n ^ m ≡ n ^^ m
n^m≡n^^m n 0 = refl
n^m≡n^^m n 1 =
  begin
    n ^ 1
  ≡&#10216; +-comm 0 n &#10217;
    1 * n
  ≡&#10216; *-comm 1 n &#10217;
    n ^^ 1
  &#8718;
n^m≡n^^m n (suc (suc m)) =
  begin
    n ^ suc (suc m)
  ≡&#10216; refl &#10217;
    power' n (suc &#8970; m /2&#8971;)
      (WF.Some.wfRec-builder (λ x → &#8469;) (power' n) (suc &#8970; m /2&#8971;)
       (<-well-founded′ (suc (suc m)) (suc &#8970; m /2&#8971;)
        (s&#8804;′s (s&#8804;′s (&#8970;n/2&#8971;&#8804;′n m)))))
      *
      power' n (suc &#8970; m /2&#8971;)
      (WF.Some.wfRec-builder (λ x → &#8469;) (power' n) (suc &#8970; m /2&#8971;)
       (<-well-founded′ (suc (suc m)) (suc &#8970; m /2&#8971;)
        (s&#8804;′s (s&#8804;′s (&#8970;n/2&#8971;&#8804;′n m)))))
      * (if odd m then n else suc zero)
  ≡&#10216; { }0 &#10217;
    { }1
  ≡&#10216; { }2 &#10217;
    n ^ (suc &#8970; m /2&#8971;) * n ^ (suc &#8970; m /2&#8971;) * (if odd m then n else suc zero)
  ≡&#10216; { }3 &#10217;
    n ^^ (suc &#8970; m /2&#8971;) * n ^^ (suc &#8970; m /2&#8971;) * (if odd m then n else suc zero)
  ≡&#10216; { }4 &#10217;
    n ^^ (suc &#8970; m /2&#8971;) * n ^^ (suc &#8970; m /2&#8971;) * n ^^ (m %2)
  ≡&#10216; { }5 &#10217;
    n ^^ (suc &#8970; m /2&#8971; + suc &#8970; m /2&#8971; + m %2)
  ≡&#10216; { }6 &#10217;
    n ^^ suc (suc m)
  &#8718;

ここから先とりあえず,

<-well-founded′ (suc (suc n)) (suc &#8970; n /2&#8971;) (s&#8804;′s (s&#8804;′s (&#8970;n/2&#8971;&#8804;′n n))) ≡ <-well-founded (suc &#8970; n /2&#8971;)

を教えてあげたいんだけど,なんだか混乱してきて止まってしまった.