修行失敗

割と良く分からないなーって感じになって、ググるとさかいさんの記事が出て来たので、依存和使っててすごいというか、なんで依存和使ってるか分からん感じだったんですけれども、実際やってみると少し分かりました。

http://www.tom.sfc.keio.ac.jp/~sakai/d/?date=20070810#p02

Id型の使いどころが面白くて

data Id {X : Set0} : X -> X -> Set0 where
  id : (x : X) -> Id x x

みたいな感じで定義出来て、これどうやって使うねん　という感じだと思うんですが

same_val1 : Id (succ (succ zero)) (succ zero + succ zero)
same_val1 = id (succ (succ zero))

とか、これはまぁリテラルであからさま過ぎて、こういうあからさまなヤツにはAgda2さんは頑張ってしまうのでもうちょっとキツいヤツでもなんとかやってくれるんですけど、filterのproofの中だとあんまりキツいやつ使うと負けちゃうので・・・。

あと、このIdと依存和組み合わせた時は、これまた何か知らないんですけれどもfilterのproofの中でするする言っちゃうので、謎過ぎる・・・。

取りあえずAgda2で書き直したコードをべだり゛

module QSort4 where

open import Bool
open import Nat
open import List
open import ValueHolder

length : {A : Set0} -> List A -> Nat
length [] = zero
length (x :: xs) = succ (length xs)

-- 場合分けを避ける為に非常に簡単なfilterにしています
filter : {A : Set0} -> (A -> Bool) -> List A -> List A
filter p [] = []
filter p (x :: xs) = filter p xs

data Id {X : Set0} : X -> X -> Set0 where
  id : (x : X) -> Id x x

record Sum (X : Set0) (Y : X -> Set0) : Set0 where
  field
    pi1 : X
    pi2 : Y pi1

Exist : {D : Set0} -> (D -> Set0) -> Set0
Exist {Type} p = Sum Type p

LE : Nat -> Nat -> Set0
LE n m = Exist (λ x -> Id (x + n) m)

Smaller : {X : Set0} -> List X -> List X -> Set0
Smaller xs ys = LE (length xs) (length ys)

-- 安易に準公理を持って来ている私の頭の悪さ
postulate p_succId : {x : Nat} {y : Nat} -> Id x y -> Id (succ x) (succ y)
postulate tranId : {X : Set0} {a b c : X} -> Id a b -> Id b c -> Id a c

infixl 5 _<=>_

_<=>_ : {X : Set0} {x y z : X} -> Id x y -> Id y z -> Id x z
id1 <=> id2 = tranId id1 id2

filterproof : (p : Nat -> Bool) -> (xs : List Nat) -> Smaller (filter p xs) xs
filterproof p [] = record { pi1 = zero ; pi2 = id zero }
filterproof p (x :: xs') = record { pi1 = fst ; pi2 = snd }
  where
    hypo : Smaller (filter p xs') xs'
    hypo = filterproof p xs'
    n : Nat
    n = Sum.pi1 hypo
    fst : Nat
    fst = succ n
    lem1 : Id (n + length (filter p xs')) (length xs') -- まずこれが言えるっていう時点で...
    lem1 = Sum.pi2 hypo
    --lem1' : Id (n + length (filter p xs')) (length xs')
    --lem1' = -- id (length xs') -- id (n + length (filter p xs')) -- これらは出来ないらしい。面白い
    lem2 : Id ((succ n) + length (filter p (x :: xs'))) ((succ n) + length (filter p xs')) 
    lem2 = id ((succ n) + length (filter p xs'))
    lem3 : Id ((succ n) + length (filter p xs')) (succ (n + length (filter p xs')))
    lem3 = id (succ (n + length (filter p xs')))
    lem4 : Id (succ (n + length (filter p xs'))) (succ (length xs'))
    lem4 = p_succId lem1 -- (succId lem1) -- mapId succ lem1 -- p_succId lem1 -- (succId lem1)
    lem5 : Id (succ (length xs')) (length (x :: xs'))
    lem5 = id (length (x :: xs'))
    -- 全部くっ付ける
    snd : Id ((succ n) + length (filter p (x :: xs'))) (length (x :: xs'))
    snd = (id ((succ n) + length (filter p (x :: xs')))) <=>
          (id ((succ n) + length (filter p xs'))) <=>
          (id (succ (n + length (filter p xs')))) <=>
          (p_succId lem1) <=> (id (length (x :: xs')))
    
sort : List Nat -> List Nat
sort [] = []
sort (x :: xs) = sort first -- 残念です
  where
    pred1 : (Nat -> Bool)
    pred1 = (λ v -> x < v)
    first : List Nat
    first = filter pred1 xs
    useproof : Smaller (first) xs
    useproof = filterproof pred1 xs
    n : Nat
    n = Sum.pi1 useproof
    lem1 : Id (n + length first) (length xs)
    lem1 = Sum.pi2 useproof

「かなり」簡単にしていて、filterとかsortとか名ばかりな感じですけれども、これでもダメっていわれるので、Idと依存和の絶妙な辺を読み解いたらこの修行は辞めます。

これやった所で、結局「filterしたリストの長さは、元のリストの長さより短い」としか言えてなくて、多分なんかsortに長さ方向の制約付ければ出来るんじゃないかなぁ。出来ないかなぁ。

多分filterしたリストが、元のリストの出現位置の順序関係を含んだ部分集合であるとか書いても無駄だと思うのでうーん・・・。

この記事 (http://d.hatena.ne.jp/yoshihiro503/20080308) を見ると、Coqのmeasureキーワードさん凄いなーって感じですけど入る前はどうやってたんだろう・・・。

他参考
http://joshkos.blogspot.com/2007/11/qsort-in-agda.html

分かった

lem1 : Id (n + length (filter p xs')) (length xs') -- まずこれが言えるっていう時点で...
lem1 = Sum.pi2 hypo
--lem1' : Id (n + length (filter p xs')) (length xs')
--lem1' = -- id (length xs') -- id (n + length (filter p xs')) -- これらは出来ないらしい。面白い

ここんとこが割と肝で、Sum.pi2 hypoだと良いのにーみたいなのは、結局これが出来るって事はid ?が出来なければ成らないって事を頭の中でさっと考えてlem1'を私が書いちゃったと思うんですけれども、そもそもLEの定義で(λ v -> Id _ _)みたく成ってるので、当然と言えば当然という感じになってるんですね。

もっとも、ここから綺麗に

Id ((succ n) + length (filter p (x :: xs'))) (length (x :: xs'))

を言って、最終的に、リストの大きさの差であるSum.pi2をなんとか言い切ったという所が凄いと思うんですけど言い切る大変さがあってもAgdaさんはなんかそれを上手く利用出来てないので、余りにも悲しいんじゃないでしょうかみたいな・・・。

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.AOPA
AOPAのExampleの中に500行近くかけて証明(してるのか分かりませんが)やってるのはあって、まぁ読む気には成りませんし・・・。