PFAD1章の最初のminfreeを定義するまで

PFAD1.agda

module PFAD1 where

open import Function
open import Coinduction
open import Data.Bool
open import Data.List
open import Data.Colist
open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym)

record Eq {x} (X : Set x) : Set x where
  field
    _==_ : X → X → Bool

Eq-ℕ : Eq ℕ
Eq-ℕ = record { _==_ = eq }
  where
    eq : ℕ → ℕ → Bool
    eq 0 0 = true
    eq 0 (suc _) = false
    eq (suc _) 0 = false
    eq (suc n) (suc m) = eq n m

elem : ∀{x} {X : Set x} → Eq X → X → List X → Bool
elem eq n xs = any (_==_ n) xs
  where
    open Eq {{...}}

notElem : ∀{x} {X : Set x} → Eq X → X → List X → Bool
notElem eq n xs = not $ elem eq n xs

-- [n..]
from : ℕ → Colist ℕ
from n = n ∷ ♯ from (suc n)

-- 無限Colistに対しては安全なhead,tailが定義できる
head×tail : ∀{x} {X : Set x} {xs : Colist X} → Infinite xs → X × Colist X
head×tail {_} {_} {[]} ()
head×tail {_} {_} {x ∷ xs} inf = (x , ♭ xs)

head : ∀{x} {X : Set x} {xs : Colist X} → Infinite xs → X
head {x} {X} {xs} = proj₁ ∘ head×tail {x} {X} {xs}

tail : ∀{x} {X : Set x} {xs : Colist X} → Infinite xs → Colist X
tail {x} {X} {xs} = proj₂ ∘ head×tail {x} {X} {xs}

max : ℕ → ℕ → ℕ
max n m with compare n m
max .n .(suc n + k) | less n k    = suc n + k
max .n .n           | equal n     = n
max .(suc n + k) .n | greater n k = suc n + k

_\\_ : List ℕ → List ℕ → List ℕ
xs \\ ys = filter (λ x → x ⟨ notElem Eq-ℕ ⟩ ys) xs

split_at : ∀{x}{X : Set x} → Colist X → ℕ → List X × Colist X
split_at [] n = ([] , [])
split_at xs 0 = ([] , xs)
split_at {x} {X} (x' ∷ xs) (suc n) = (x' ∷ proj₁ xs' , proj₂ xs')
  where
    xs' : List X × Colist X
    xs' = split_at {x} {X} (♭ xs) n

_\\\_ : Colist ℕ → List ℕ → Colist ℕ
xs \\\ [] = xs
xs \\\ (y ∷ ys) = fromList (proj₁ xys \\ (y ∷ ys)) Data.Colist.++ proj₂ xys
  where
    xys : List ℕ × Colist ℕ
    xys = split xs at $ suc $ foldl max y ys

-- [n..]は無限Colist
from_→∞ : ∀ n → Infinite (from n)
from n →∞ = n ∷ ♯ from suc n →∞

-- 無限Colist を 右append すると無限Colist
_++_∞→∞ : ∀{x} {X : Set x} (xs : Colist X) → {ys : Colist X} →
          Infinite ys → Infinite (xs Data.Colist.++ ys)
_++_∞→∞ [] {ys} ys∞ = ys∞
_++_∞→∞ (x ∷ xs) {ys} ys∞ = x ∷ ♯ _++_∞→∞ (♭ xs) {ys} ys∞

-- 無限Colist の tail も無限Colist
tail_∞→∞ : ∀{x}{X : Set x} → {xs : Colist X} →
           (xs∞ : Infinite xs) → Infinite (tail xs∞)
tail_∞→∞ {_} {_} {[]} ()
tail_∞→∞ {_} {_} {(.x ∷ .xs)} (_∷_ x {xs} inf) = ♭ inf

-- 無限Colist の split at n , proj₂ は無限Colist
split_∞at_₂→∞ : ∀{x} {X : Set x} →
                {xs : Colist X} → Infinite xs →
                (n : ℕ) → Infinite (proj₂ $ split xs at n)
split_∞at_₂→∞ {_} {_} {[]} () 0
split_∞at_₂→∞ {_} {_} {x ∷ xs} x∷xs∞ 0 = x∷xs∞
split_∞at_₂→∞ {_} {_} {[]} () (suc n)
split_∞at_₂→∞ {_} {_} {x ∷ xs} x∷xs∞ (suc n)= split_∞at_₂→∞ {_} {_} {♭ xs} (tail x∷xs∞ ∞→∞) n

-- 無限Colist \\\ List は無限Colist
_∞\\\_→∞ : ∀{xs} → Infinite xs → ∀ ys → Infinite (xs \\\ ys)
_∞\\\_→∞ {xs} xs∞ [] = xs∞
_∞\\\_→∞ {xs} xs∞ (y ∷ ys) = fromList (proj₁ xys \\ (y ∷ ys)) ++ split xs∞ ∞at m ₂→∞ ∞→∞
  where
    m = suc $ foldl max y ys
    xys = split xs at m

-- やっとminfree
minfree : List ℕ → ℕ
minfree xs = head (from 0 →∞ ∞\\\ xs →∞)

-- テスト
test-minfree1 : minfree [] ≡ 0
test-minfree1 = refl
test-minfree2 : minfree (0 ∷ []) ≡ 1
test-minfree2 = refl
test-minfree3 : minfree (1 ∷ []) ≡ 0
test-minfree3 = refl
test-minfree4 : minfree (0 ∷ 1 ∷ []) ≡ 2
test-minfree4 = refl
test-minfree5 : minfree (0 ∷ 2 ∷ []) ≡ 1
test-minfree5 = refl
test-minfree6 : minfree (1 ∷ 2 ∷ []) ≡ 0
test-minfree6 = refl
test-minfree7 : minfree (0 ∷ 4 ∷ 5 ∷ 3 ∷ 1 ∷ []) ≡ 2
test-minfree7 = refl

-- こっからminfreeの性質の証明をーって．疲れた
postulate
  minfree-is-free : ∀{xs} → elem Eq-ℕ (minfree xs) xs ≡ false
  minfree-is-min : ∀{xs} → minfree xs < minfree (minfree xs ∷ xs)