zyxwvの日記

Agda で挿入ソートする

Agda | 22:15 |

概要

Agda2 で挿入ソート関数を定義して、それがほんとにリストをソートすることを証明してみました。試すには Agda の標準ライブラリ(The Agda Wiki - Standard Library)が必要です。

冗長な証明になっている可能性は大いにあります。Agda のサンプルコードはあんまり見ない気がするので、誰かの参考になれば幸いです。

関数定義

インサート関数 insert と、リストをソートする関数 insertSort をごく普通に定義します。

"≤?" は Coq で言うところの SumBool 型の値を返す不等号演算子です。たぶん。こちらを使うと、条件分岐した先でその条件が仮定として使えるようになるので、後の証明がしやすくなります。

insert : ℕ → List ℕ → List ℕ
insert x [] = [ x ]
insert x (x' ∷ xs) with x ≤? x'
insert x (x' ∷ xs) | yes p = x ∷ x' ∷ xs
insert x (x' ∷ xs) | no ¬p = x' ∷ (insert x xs)

insertSort : List ℕ → List ℕ
insertSort  = 
insertSort (x ∷ xs) = insert x (insertSort xs)

ごく自然に ℕ とか使ってるあたりがきもいですね。標準ライブラリがそうなってるんだから仕方ないんです。ちなみに ℕ は agda-mode で \bn と入力すると打てます。

変な記号を打ちたい場合には id:mzp に教えてもらったサイト(Detexify LaTeX handwritten symbol recognition)もお使いください。

ゴール

まずは"ソート済み"という性質を表す sorted を定義します。

sorted : List ℕ → Set
sorted [] = ⊤
sorted (x ∷ []) = ⊤
sorted (x ∷ x' ∷ xs) = (x ≤ x') × (sorted (x' ∷ xs))

今回の証明の1つめのゴールは "ソート済みのリストに要素を insert してもソート済みのリストのままである" です。

{- 'insert' dosen't mess up the list -}
thmInsert : ∀ {x xs} → sorted xs → sorted (insert x xs)

2つめのゴールは "insertSort するとどんなリストもソート済みのリストになる" です。

{- 'insertSort' does sort the list -}
thmInsertSort : ∀ xs -> sorted (insertSort xs)

補題

"m が n 以下でない" ならば "n は m 以下である"

m≰n-n≤m : ∀ {x y} → (x ≤ y → ⊥) → y ≤ x
m≰n-n≤m {zero} {zero} p = z≤n
m≰n-n≤m {zero} {suc n} p = ⊥-elim (p z≤n)
m≰n-n≤m {suc n} {zero} p = z≤n
m≰n-n≤m {suc n} {suc n'} p = s≤s (m≰n-n≤m (λ x → p (s≤s x)))

"m が n 以下" であり "n が o 以下" であるなら "m は o 以下" である(不等号の推移律)

≤-trans : ∀ {m n o} → m ≤ n → n ≤ o → m ≤ o
≤-trans {zero} p q = z≤n
≤-trans {suc n} (s≤s m≤n) (s≤s m≤n') = s≤s (≤-trans m≤n m≤n')

ソート済みのリストの tail 部分はソート済みのリストである

leSubSorted : ∀ {x xs} → sorted (x ∷ xs) → sorted xs
leSubSorted {x} {[]} p = p
leSubSorted {x} {_ ∷ _} (_ , y) = y

自然数 x はリスト xs 内のどの自然数よりも小さいか等しい

_⊑_ : ∀ (x : ℕ) (xs : List ℕ) -> Set
x ⊑ [] = ⊤
x ⊑ (y ∷ xs) =  x ≤ y × x ⊑ xs

ソート済みのリスト xs の先頭に、xs 内のどの自然数よりも小さいか等しい自然数 x を追加したものは、ソート済みのリストである

leCons : ∀ x xs -> x ⊑ xs -> sorted xs -> sorted (x ∷ xs)
leCons x [] p q = p
leCons x (x' ∷ xs) (x0 , y) q = x0 , q

ソート済みのリストの先頭要素は、後ろのリスト内のどの自然数よりも小さいか等しい

leHeadIsMin : ∀ x xs -> sorted (x ∷ xs) -> x ⊑ xs
leHeadIsMin x [] p = p
leHeadIsMin x (x' ∷ xs) (x0 , y) =
            x0 , lemma {x} {x'} {xs} x0 (leHeadIsMin x' xs y)
  where lemma : ∀ {x y xs} -> x ≤ y -> y ⊑ xs -> x ⊑ xs
        lemma {x} {y} {[]} p q = q
        lemma {x} {y} {x' ∷ xs} p (x0 , y') =
          (≤-trans p x0) , (lemma {x} {y} {xs} p y')

"insert x x' xs" は、"x' ≤ x" の場合には "x' :: insert x xs" と評価される。このとき x' が xs に x をインサートしてできるリスト内のどの要素よりも小さい

leConsToInsertedList : ∀ x x' xs -> x' ≤ x -> x' ⊑ xs -> x' ⊑ (insert x xs)
leConsToInsertedList x x' [] p q = p , q
leConsToInsertedList x x' (x0 ∷ xs) p (x1 , y) with x ≤? x0
leConsToInsertedList x x' (x0 ∷ xs) p' (x1 , y) | yes p = p' , (x1 , y)
leConsToInsertedList x x' (x0 ∷ xs) p (x1 , y) | no ¬p = x1 , ih
  where ih = leConsToInsertedList x x' xs p y

証明

{- 'insert' dosen't mess up the list -}
thmInsert : ∀ {x xs} → sorted xs → sorted (insert x xs)
thmInsert {x} {[]} p = p
thmInsert {x} {x' ∷ xs} p with x ≤? x'
... | yes q = q , p
... | no ¬q = leCons x' (insert x xs)
                     (leConsToInsertedList x x' xs x'≤x (leHeadIsMin x' xs p)) ih
  where x'≤x = m≰n-n≤m ¬q
        ih = thmInsert {x} {xs} (leSubSorted {x'} {xs} p)

{- 'insertSort' does sort the list -}
thmInsertSort : ∀ xs -> sorted (insertSort xs)
thmInsertSort [] = tt
thmInsertSort (x ∷ xs) = thmInsert {x} {insertSort xs} (thmInsertSort xs)

感想

たかが挿入ソートですが、証明にはものすごい手間がかかりました。Agda に慣れていないというのが原因だとは思うのですが。ともあれ非常におもしろかったです。

あと Coq のタクティックのありがたみがわかりました :)

全ソース

続きを読む

tmiyaさんの練習問題をラムダ式で解いてみた

Agda | 21:24 |

2010-09-26 - にわとり小屋でのプログラミング日記 を見て同じ命題を Agda2 で証明してみた。

Functional Programming Memo: [Coq] Coq-99 : Part 1

agda-mode が証明するのを手伝ってくれるのでお気楽です。

module Practice1 where

data True : Prop where
  tt : True
data False : Prop where

data _∧_ (P Q : Prop) : Prop where
  ∧-intro : P → Q → P ∧ Q
∧-eliml : ∀ {P Q} → P ∧ Q → P
∧-eliml (∧-intro y y') = y
∧-elimr : ∀ {P Q} -> P ∧ Q -> Q
∧-elimr (∧-intro y y') = y'

data _∨_ (P Q : Prop) : Prop where
  ∨-introl : P -> P ∨ Q
  ∨-intror : Q -> P ∨ Q
∨-elim : ∀ {P Q R : Prop} -> (P ∨ Q) -> (P -> R) -> (Q -> R) -> R
∨-elim (∨-introl y) a b = a y
∨-elim (∨-intror y) a b = b y

~_ : Prop -> Prop
~ p = p -> False

infixl 10 _∧_
infixl 9  _∨_

lemma01 : ∀ (A B C : Prop) → (A → B → C) → (A → B) → A → C
lemma01 a b c d e f = d f (e f)

lemma02 : ∀ A B C → A ∧ (B ∧ C) → (A ∧ B) ∧ C
lemma02 a b c d = ∧-intro (∧-intro (∧-eliml d) (∧-eliml (∧-elimr d)))
                          (∧-elimr (∧-elimr d))

lemma03 : ∀ A B C D → (A → C) ∧ (B → D) ∧ A ∧ B → C ∧ D
lemma03 a b c d e = ∧-intro (∧-eliml (∧-eliml (∧-eliml e))
                                     (∧-elimr (∧-eliml e)))
                            (∧-elimr (∧-eliml (∧-eliml e)) (∧-elimr e))

lemma04 : ∀ A → ~(A ∧ (~ A))
lemma04 a b = ∧-elimr b (∧-eliml b)

lemma05 : ∀ A B C → A ∧ (B ∨ C) → (A ∨ B) ∨ C
lemma05 a b c d = ∨-introl (∨-introl (∧-eliml d))

lemma06 : ∀ A → ~(~(~ A)) → ~ A
lemma06 a b c = b (λ x → x c)

lemma07 : ∀ A B → (A → B) → ~ B → ~ A
lemma07 a b c d e = d (c e)

lemma08 :  ∀ (A B : Prop) → ((((A → B) → A) → A) → B) → B
lemma08 a b c = c (λ x → x (λ x' → c (λ _ -> x')))

lemma09 : ∀ A → ~(~(A ∨ (~ A)))
lemma09 a b = b (∨-intror (λ x → b (∨-introl x)))

とりあえず JapanTimes と NYTimes をクーリエ・ジャポンみたいに見るブックマークレット(超適当)

JavaScript | 18:19 |

iPad 買いました。おもしろいです。土日は iPad を持って外出してましたが、電池切れになることはありませんでした。あとは Evernote をプレミアムアカウントにしてローカルにファイルを保存できるようにすれば、今週は寮に MacBook を持ってく必要がないかもしれない！

で、iPad で JapanTimes とかを読んでみたのですが、僕は英語が苦手なので、画面いっぱいにアルファベットが表示されると読む気が失せてしまうのです。そこで前に感動したクーリエ・ジャポンの UI みたいなのを実現するブックマークレットを書いてみました。ブックマークレットを読み込むと本文の最初のパラグラフをハイライトして、暗い部分をタッチすると次のパラグラフにスクロールします。

ただ、ものっそい適当です。ハイライトのスクロールが遅いし、いろいろずれるし。まぁこれからしばらく使ってみて、いい感じなら改良していくことにします。

(function(){
   const db = {
      "search.japantimes.co.jp":"#mainbody > p",
      "www.nytimes.com":"#article p"
   };

   const duration = 0.4;
   const paragraphs =
      document.querySelectorAll(db[window.location.hostname]);

   function createCover(pos){
      var cover = document.createElement("div");
      cover.className = "couriercover";
      cover.style.position = "absolute";
      cover.style.left = "0px";
      cover.style.width = "100%";
      cover.style.zIndex = 65535;
      cover.style.backgroundColor = "black";
      cover.style.opacity = "0.5";
      if (pos == "upper") {
         cover.style.WebkitTransitionProperty = "height";
         cover.style.WebkitTransitionDuration = ""+duration+"s";
         cover.style.top = "0px";
         cover.style.height = "0px";
      } else if (pos == "lower") {
         cover.style.WebkitTransitionProperty = "top";
         cover.style.WebkitTransitionDuration = ""+duration+"s";
         cover.style.top = ""+(window.pageYOffset+window.innerHeight)+"px";
         cover.style.height =
            ""+(document.body.scrollHeight-
                (window.pageYOffset+window.innerHeight))+"px";
      }
      document.body.appendChild(cover);
      return cover;
   }

   var upperCover = createCover("upper");
   var lowerCover = createCover("lower");

   function getRect(element){
      function loop(element){
         var top = element.offsetTop;
         var left = element.offsetLeft;
         if (element.offsetParent) {
            var rect = loop(element.offsetParent);
            return {top:rect.top+top, left:rect.left+left};
         }
         return {top:top, left:left};
      }
      var rect = loop(element);
      rect.top = rect.top;
      rect.left = rect.left;
      rect.width = element.offsetWidth;
      rect.height = element.offsetHeight;
      rect.bottom = rect.top+rect.height;
      rect.right = rect.left+rect.width;
      return rect;
   }

   function smartScrollTo(element){
      var rect = getRect(element);
      if (rect.bottom > window.pageYOffset+window.innerHeight ||
          rect.top < window.pageYOffset) {
         window.scrollTo(0, rect.top-10);
      }
   }
   function forcusTo(element){
      smartScrollTo(element);
      var rect = getRect(element);
      upperCover.style.top = ""+window.pageYOffset+"px";
      upperCover.style.height = ""+(rect.top-window.pageYOffset)+"px";
      lowerCover.style.top = ""+rect.bottom+"px";
      setTimeout(function(){
         lowerCover.style.height =
            ""+(window.innerHeight-(rect.bottom-window.pageYOffset))+"px";
      }, duration*1000);
   }

   var counter = 0;
   function next(){
      if(counter<paragraphs.length)
         forcusTo(paragraphs[counter++]);
   }
   function prev(){
      if(counter>0)
         forcusTo(paragraphs[--counter]);
   }

   upperCover.addEventListener("touch",prev,false);
   upperCover.addEventListener("click",prev,false);
   lowerCover.addEventListener("touch",next,false);
   lowerCover.addEventListener("click",next,false);

   next();
})()

Project Euler: Problem23

C | 15:58 |

現在は工場実習中で毎日肉体労働をしてるので、休日くらいはプログラムを書きたくなります。というわけで超久しぶりに Project Euler をやってみたよ。

問題23。正の整数 n の約数の和が n をより大きいとき、 n を過剰数(abundant number)という。2つの過剰数の和で表すことができない正の整数の和を求めよ。ただし28123より大きい整数は2つの過剰数の和で表せることがわかっている。

Haskell で適当に書いたら止まらなかったので C で書き直した。

#include <stdio.h>
#define MAX 28123

int sumOfFactors(int n){
  int x,r;
  for (x=1,r=0;x<n;x++)
    if (n%x==0)
      r += x;
  return r;
}

int main(){
  char abundands[MAX];
  char result[MAX];
  unsigned int sum = 0;
  int i,j;

  for (i=0;i<MAX;i++)
    result[i] = 0;

  for (i=0;i<MAX;i++)
    abundands[i] = sumOfFactors(i) > i;

  for (i=0;i<MAX/2;i++)
    if (abundands[i])
      for (j=i;j+i<MAX;j++)
        if (abundands[j])
          result[i+j] = 1;

  for (i=0;i<MAX;i++)
    if (!result[i])
      sum += i;

  printf("%u\n", sum);
  return 0;
}

Project Euler: Problem27

C | 18:49 |

f(n) = n*n + an + b, |a|<1000, |b|<1000 である f に対し、 n に 0 から順に代入していったとき、素数が連続して最も長く出現するような a, b の値を求めよ。

こっちもがっちり C で。何も考えなくても Haskell より速い。素敵。

#include <stdio.h>
#define MAX 1000

int isPrime(int x){
  int i;
  for (i=2;i<x;i++)
    if (x%i==0)
      return 0;
  if (x<=1)
    return 0;
  return 1;
}
int euler(int a, int b, int n){
  return n*n+a*n+b;
}

int main(){
  int a,b,n;
  int max_a=0, max_b=0, max_n=0;

  for(a=-MAX+1;a<MAX;a++) {
    for(b=-MAX+1;b<MAX;b++) {
      for(n=0;;n++)
        if (!isPrime(euler(a,b,n)))
          break;
      if (n>max_n) {
        max_n = n;
        max_a = a;
        max_b = b;
      }
    }
  }
  printf("%d,%d:%d\n", max_a, max_b, max_n);

  return 0;
}

twitter.com を改善する拡張を書いた

Chrome | 19:56 |

背景

修論で追い詰められた学生が、「twitter クライアントはたくさんあるけど、実際ブラウザで十分なんじゃね。他の拡張と組み合わせれば、かえって操作性が上がるかもしれない。」と思いつき、嫌だ力を駆使して集中力が切れるたびに少しずつ書いた拡張機能です。

機能

今のところの機能は

• "in reply to" が付いてる tweet をクリックすると、一連のやりとりが表示される
• 自動再読み込みっぽいもの

だけです。そのうち適当なキーバインドを付けたいですね。

果たして修論が終わったあともやる気がでるかどうか！

インストール

一応公開しました。

https://chrome.google.com/extensions/detail/hobknpodnecnibpcepadfjfhfofjdjci

感想

• 他の拡張と組み合わせると、tweet 内のリンクを開いたりするのが便利
• 無事に卒業したい

LablGTK で遊ぶ

OCaml | 00:00 |

LablGTK(http://wwwfun.kurims.kyoto-u.ac.jp/soft/lsl/lablgtk.html) は、OCaml のための GUI ライブラリです。素敵です。

背景

• 研究のためにサンプルプログラムを書く必要があった
• マルチスレッドと GUI のライブラリが必要だった
• Haskell + wxHaskell でやってたけど、うまくいかなかった(たぶん僕のミス)
• じゃあ(嫌だ力を発揮して) OCaml でやってみるか
• 普通に動いたバロス

インストール

• Mac: MacPorts でインストールでき、コンパイルもできますが、ウィンドウが表示されません。頑張れば動くような感じ。
• Linux: Ubuntu なら aptitude でインストールでき、動作もかんぺき
• Windows: わかりません

ドキュメント

公式のドキュメントはLablGTKにあります。あとは、ホワット・ア・ワンダフル・ワールド LablGTK は素晴らしいからリンクをたどって参考にしました。いくつかサンプルを見て、あとは公式のドキュメントを睨めばなんとかなる。

ソースコード

やんごとなき事情により、研究用に書いたコードは事情を知らない人にはとっても読みにくいことに今気がついた。

でもここまで書いたのにざっくり消すのは悲しいので、とりあえず簡単なアプリケーションを書いてみた。

ボタンを交互に押し込むだけのもぐらたたきアプリケーションだ！

open Event
open GMain

let change_availavility obj b = obj#misc#set_sensitive b;;
let set_disable obj = change_availavility obj false;;
let set_enable obj = change_availavility obj true;;

let main _ = 
  (* レイアウト設定 *)
  let window = GWindow.window ~border_width:5 ~title: "mogura-tataki" () in
  let layout = GPack.vbox ~spacing:5 ~packing:window#add () in
  let text = GEdit.entry ~editable:false ~packing:layout#add () in
  let buttons = GPack.hbox ~packing:layout#add () in
  let mogura1 = GButton.button ~label:"(*-*)" ~packing:buttons#add () in
  let mogura2 = GButton.button ~label:"(*-*)" ~packing:buttons#add () in
    text#set_text "COUNT: 0";
    set_disable mogura2;

    let count = ref 0 in
    (* イベントハンドラ設定 *)
    window#connect#destroy ~callback:Main.quit;
    mogura1#connect#clicked
      ~callback:(fun _ ->
		   set_disable mogura1;
		   set_enable mogura2;
		   count := !count + 1;
		   text#set_text ("COUNT: "^string_of_int !count));
    mogura2#connect#clicked
      ~callback:(fun _ ->
		   set_disable mogura2;
		   set_enable mogura1;
		   count := !count + 1;
		   text#set_text ("COUNT: "^string_of_int !count));

    (* 開始 *)
    window#show ();
    Main.main ();;
let _ = Printexc.print main ()

マルチスレッドですらない…。

OMakefile

LablGTK を使うときには gtkInit.cmo をリンクしないといけません。普通に FILES[] とかに書いちゃうと、 omake さんは gtkInit.ml から gtkInit.cmo を作ろうと頑張ってしまうので、OCAML_BYTE_LINK_FLAGS に書きます。

# これで正しいのかはわからないのですが、とりあえず動いてます

USE_OCAMLFIND = true
OCAMLPACKS[] = unix threads lablgtk2
OCAMLINCLUDES += lablgkt2

NATIVE_ENABLED = $(not $(OCAMLOPT_EXISTS))
BYTE_ENABLED = $(OCAMLC_EXISTS)

OCAMLCFLAGS   += -thread -w -s -warn-error a
OCAML_BYTE_LINK_FLAGS += gtkInit.cmo

FILES[] = sampleapp
PROGRAM = sampleapp
OCAML_OTHER_LIBS += unix threads lablgtk

.DEFAULT: $(OCamlProgram $(PROGRAM), $(FILES))

Thread とか Event を使わない場合、 unix とか threads とかはいらないと思われ。

その他適当に

• コールバック関数はメインスレッドから呼ばれるので GUI の操作を安心して行えます
• vbox, hbox に add すると、垂直・水平に GUI オブジェクトを並べられる
• プログレスバーは GRange.progress_bar
• テキストボックスへのキー入力イベントの取り方

textbox#event#connect#key_release
   ~callback:(fun ev -> let key = GdkEvent.Key.string ev in ...);

感想

• コンパイル速い
• OCaml 素敵
• LablGTK 素敵
• Ubuntu 便利
• 無事に卒業したい

Google Chrome で migemo 検索

JavaScript, Chrome | 16:02 |

スクリーンショット

"nikki" で日記が検索できています！

内容

最近 Chrome の拡張を書くのがマイブームです。 Google Chrome で Hit a Hint - zyxwvの日記 で自分としてはだいぶ便利になったのですが、ページのどこかにある日本語のリンクをクリックしたいときには不便でした。

そこで Opera で Migemo 検索 with Opera Unite - mallowlabsの備忘録 にインスパイアされて Chrome で Migemo 検索をできるようにしてみました。というか、 id:mallowlabs さんに教えてもらった Opera UniteでOperaアドオン - もし高校野球の女子マネージャーがOpera Browserを使ったら - チーム俺等 を使っただけで、僕はコードを書いてません :)

インストール

安定(?)版

https://chrome.google.com/extensions/detail/jdfpnijdiejbhebabijgoibmnngiblhk

開発版

http://eva-lu-ator.net/~sho/

使い方

".","/" で migemo リンク検索、 Ctrl-g と Ctrl-Shift-g で前後のリンクを選択

"," で Hit-a-Hint

他におまけとして以下のキーが割り当てられています。いらないという人も多いと思うので、設定を変更できるような option ページを準備中です。

"Esc" で input からフォーカスを外す

"j","k","h","l"で前後左右に移動

Google Chrome で Hit a Hint

JavaScript, Chrome | 15:03 |

経緯

最近 Chrome を使っています。現状の Mac 版(4.0.245.0)だとブックマークの管理すらできず、ちょっと厳しいものがあるのですが、 windows でも linux でも動いて、簡単に拡張も書けるのでおすすめです。

で、拡張で遊んでみました。リンクをキーボードで選択できる "Hit a Hint" というやつです。

(追記)

リンク検索も追加してみました。

あと、 Hit-a-Hintブックマークレット2.0をリリースしたよ - by edvakf in hatena あたりを見て感動して、こいつを chrome でも使えるようにしてやるぜ！って感じでガーっと書いたんだけど、実は はじめてのGoogle Chrome拡張、オレオレChromeKeyconfig - by edvakf in hatena で chrome で使えるようになってました。どんまい。

インストール

Google Chrome で migemo 検索 - zyxwvの日記と統合しました。

使い方

","で hint を表示します。飛びたいリンクに振られた文字列をタイプしてリターンキーを力強く叩きます。

"." か "/" でリンク検索ができます。リンク間の移動は Ctrl+g と Ctrl+Shift+g です。

どちらも、シフトなどを押しながらリターンキーを叩けば、シフトなどを押しながらクリックしたのと同じ動作をします。このリンクをタブで開きたいぜ！っとかいうときに使うといいよ！

ご注意

ざっくりと書いただけなので誤動作などがもりもりあると思います。

無駄にアニメーションをいれてみました。 chrome 拡張だと CSS3 が安心して使えるのがいいですね。

オオカミとヤギとキャベツを移動させるやつ

Haskell | 23:19 |

研究室の一部の人が uppaal で解こうとしていた問題。

オオカミとヤギとキャベツを対岸に移動させたいけど、オオカミとヤギ、あるいはヤギとキャベツを残したまま人が対岸に行ってはダメ、というやつ。

最初は prolog でやってやろうとしたけど、くじけて Haskell でお茶を濁しました。 Snow Leopard で GHC が動かないのもあって、最近 Haskell のコードを書いてなかったからいいんです。

いつか、圏論を使って考えてみました！とか言いたい。(適当)

人とオオカミとヤギとキャベツの位置を Bool で表してます。Move0 は人が対岸に渡り、Move1 Move2 Move3 はそれぞれ、オオカミとヤギとキャベツが移動します。move 関数のガードは、人なしで勝手にキャベツなどが移動しないようにするために必要です。

import Control.Monad
import List

type Game = (Bool, Bool, Bool, Bool)
data Move = Move0 | Move1 | Move2 | Move3 deriving (Eq,Show)

move :: Move -> Game -> Maybe Game
move Move0 (h,x,y,z)        = Just (not h,x,y,z)
move Move1 (h,x,y,z) | h==x = Just (not h,not x,y,z)
move Move2 (h,x,y,z) | h==y = Just (not h,x,not y,z)
move Move3 (h,x,y,z) | h==z = Just (not h,x,y,not z)
move _     _                = Nothing

ok (True,False,False,_) = False
ok (True,_,False,False) = False
ok (False,True,True,_)  = False
ok (False,_,True,True)  = False
ok _                    = True

solved (_,False,False,False) = True
solved _                     = False

step :: (Game, [Move]) -> [(Game, [Move])]
step (state, ops) = do op <- [Move0,Move1,Move2,Move3]
                       case move op state of
                         Nothing     -> mzero
                         Just state' -> do guard (ok $ state')
                                           return (state', op:ops)

calc :: [(Game, [Move])] -> [Move]
calc states = let states' = concatMap step states in
              case find (solved . fst) states' of
                Nothing -> calc states'
                Just (_, moves) -> reverse moves

main = print $ calc [((True,True,True,True), [])]

$ runhaskell tmp.hs
[Move2,Move0,Move1,Move2,Move3,Move0,Move2]
$ 

CSS で画像を空間に散らしてみた

CSS | 18:32 |

起動時

拡大！

CSS でなんか作ってみた第二弾。画像を3次元空間に配置してぐるぐるさせることができます。例によって対応ブラウザは webkit 系だけです。-webkit-* を -moz-* にかえれば Firefox でもきっと動きます。

デモ: http://www.agusa.i.is.nagoya-u.ac.jp/person/shimo/3d/3d.html

マウスに追従して視線が動きます。クリックしながらマウスを動かすと、視点そのものが移動します。マウスホイールで拡大縮小ができます。

最新の Webkit で動作確認。 Safari でも動くみたい。

プログラマのための Coq

Coq | 01:24 |

CSS と Coq の記事が並ぶというシュールな展開ですが、これも嫌だ力のなせるわざです。今日の証明では SearchPattern とか eapply がでてくるよ！

本日のお題は、 filter 関数を2回適用しても結果のリストの長さが変わらないという性質 FilterLength の証明です。 filter 関数と FilterLength の定義は以下のようになってます。

Require Import List.

Fixpoint filter {a : Type} (f : a -> bool) (xs : list a) :=
  match xs with
    | nil => nil
    | (cons x xs) => if f x then cons x (filter f xs)
                            else filter f xs
  end.

Theorem FilterLength :
  forall {a:Type} (f : a -> bool) (xs : list a),
  length (filter f xs) <= length xs.

では、 coqtop で対話的に証明を行っていきましょう。

$ coqtop -l length.v
coqtop -l length.v
Welcome to Coq 8.2pl1 (September 2009)

FilterLength < Show.
Show.
1 subgoal
  
  ============================
   forall (a : Type) (f : a -> bool) (xs : list a),
   length (filter f xs) <= length xs

coqtop を起動したら、まずは証明すべき内容を確認しましょう。リスト操作関数の性質を検証したい場合、リストの構造に関する帰納法を使えばなんとかなります。たぶん。

FilterLength < induction xs.
induction xs.
2 subgoals
  
  a : Type
  f : a -> bool
  ============================
   length (filter f nil) <= length nil

subgoal 2 is:
 length (filter f (a0 :: xs)) <= length (a0 :: xs)

forall はできるだけ残しておくほうがいい、というアドバイスを id:yoshihiro503 さんからもらったので、 intros を行う前に induction を使ってみました。 今回の場合は xs の構造に関する場合分けなので、xs の前に書いてある仮定(a と f : a -> bool)が仮定に入ってしまいましたが、もし FilterLength の定義において xs が先頭に書いてあった場合は f に関してはゴールに残ります。やってみましょう。定理の引数の順番を変えた FilterLength2 を定義してみました。

FilterLength2 < Show.
Show.
1 subgoal
  
  ============================
   forall (a : Type) (xs : list a) (f : a -> bool),
   length (filter f xs) <= length xs

FilterLength2 < induction xs.
induction xs.
2 subgoals
  
  a : Type
  ============================
   forall f : a -> bool, length (filter f nil) <= length nil

subgoal 2 is:
 forall f : a -> bool, length (filter f (a0 :: xs)) <= length (a0 :: xs)

FilterLength2 < 

ゴールが "forall f : ..." の形をしています。この違いが後々証明で効いてくることもあるので引数の順番には注意が必要です。引数の順番を決める際の指針が欲しいですが、経験だそうです。

では、FilterLength の証明に戻ります。

2 subgoals
  
  a : Type
  f : a -> bool
  ============================
   length (filter f nil) <= length nil

subgoal 2 is:
 length (filter f (a0 :: xs)) <= length (a0 :: xs)

1つめの subgoal は簡単そうです。simpl で簡約します。

FilterLength < simpl.
simpl.
2 subgoals
  
  a : Type
  f : a -> bool
  ============================
   0 <= 0

subgoal 2 is:
 length (filter f (a0 :: xs)) <= length (a0 :: xs)

ゴールは明らかです。両辺が同じだから reflexivity で大丈夫かな？と思うわけですが、

FilterLength < reflexivity.
reflexivity.
Toplevel input, characters 0-11:
> reflexivity.
> ^^^^^^^^^^^
Error: Tactic failure: The relation le is not a declared reflexive relation. Maybe you need to require the Setoid library.

ダメでした。 reflexivity は等式にしか使えないそうです。SearchPattern で探してみます。

FilterLength < SearchPattern (_<=_).
SearchPattern (_<=_).
Gt.gt_S_le: forall n m : nat, S m > n -> n <= m
Gt.gt_le_S: forall n m : nat, m > n -> S n <= m
Le.le_refl: forall n : nat, n <= n
Le.le_trans: forall n m p : nat, n <= m -> m <= p -> n <= p
Le.le_O_n: forall n : nat, 0 <= n
...

長いので後半は省略しました。 Le.le_refl が求めるものですので、適用しましょう。

FilterLength < apply Le.le_refl.
apply Le.le_refl.
1 subgoal
  
  a : Type
  f : a -> bool
  a0 : a
  xs : list a
  IHxs : length (filter f xs) <= length xs
  ============================
   length (filter f (a0 :: xs)) <= length (a0 :: xs)

1つめの subgoal の証明が完了しました。やったね。

今回は律儀に定理を自分で探して適用しましたが、実はこれくらい簡単なゴールだと auto で証明できちゃったりします。やってみます。

FilterLength < Undo.
Undo.
2 subgoals
  
  a : Type
  f : a -> bool
  ============================
   0 <= 0

subgoal 2 is:
 length (filter f (a0 :: xs)) <= length (a0 :: xs)

FilterLength < auto.
auto.
1 subgoal
  
  a : Type
  f : a -> bool
  a0 : a
  xs : list a
  IHxs : length (filter f xs) <= length xs
  ============================
   length (filter f (a0 :: xs)) <= length (a0 :: xs)

素晴らしいですね。

続きまして帰納段階の証明です。まずは簡約してみます。

FilterLength < simpl.
simpl.
1 subgoal
  
  a : Type
  f : a -> bool
  a0 : a
  xs : list a
  IHxs : length (filter f xs) <= length xs
  ============================
   length (if f a0 then a0 :: filter f xs else filter f xs) <= S (length xs)

if 文が邪魔ですね。帰納法の仮定を睨むと、if 文の条件式が真でも偽でも、ゴールが証明できそうな気がします。いわゆる場合分けがしたいですね。

ここで新しいタクティック case を導入します。

FilterLength < case (f a0).
case (f a0).
2 subgoals
  
  a : Type
  f : a -> bool
  a0 : a
  xs : list a
  IHxs : length (filter f xs) <= length xs
  ============================
   length (a0 :: filter f xs) <= S (length xs)

subgoal 2 is:
 length (filter f xs) <= S (length xs)

case タクティックは、引数に取った式の場合分けを行ってサブゴールとしてくれます。 induction と似ています。

FilterLength < simpl.
simpl.
2 subgoals
  
  a : Type
  f : a -> bool
  a0 : a
  xs : list a
  IHxs : length (filter f xs) <= length xs
  ============================
   S (length (filter f xs)) <= S (length xs)

subgoal 2 is:
 length (filter f xs) <= S (length xs)

帰納法の仮定をみると、明らかな気もしますが、両辺の頭に S がついています。"n <= m -> S n <= S m" は需要の多そうな定理だと思うので、探してみます。

FilterLength < SearchPattern (S _ <= S _).
SearchPattern (S _ <= S _).
Le.le_n_S: forall n m : nat, n <= m -> S n <= S m

そのまんまありました。適用します。

FilterLength < apply Le.le_n_S.
apply Le.le_n_S.
2 subgoals
  
  a : Type
  f : a -> bool
  a0 : a
  xs : list a
  IHxs : length (filter f xs) <= length xs
  ============================
   length (filter f xs) <= length xs

subgoal 2 is:
 length (filter f xs) <= S (length xs)

帰納法の仮定そのままですね。

FilterLength < apply IHxs.
apply IHxs.
1 subgoal
  
  a : Type
  f : a -> bool
  a0 : a
  xs : list a
  IHxs : length (filter f xs) <= length xs
  ============================
   length (filter f xs) <= S (length xs)

さて、どうしよう。よく見ると、ゴールの左辺と IHxs の左辺が同じですね。で、この共通の式 "length (filter f xs)" は "length xs" 以下であるというのが仮定に入っている。さらに、ゴールの右辺である "S (length xs)" は明らかに "(length xs)" よりも大きいです。

ということで、 "length (filter f xs) <= length xs -> length xs <= S (length xs) -> length (filter f xs) <= S (length xs)" という流れで証明をしたいです。いわゆる推移律ですね。

自然数の推移律は明らかだし需要がありそうなので、きっと標準ライブラリに入ってるだろうということで、探してみます。

FilterLength < SearchPattern (_ <= _ -> _ <= _ -> _ <= _ ).
SearchPattern (_ <= _ -> _ <= _ -> _ <= _ ).
Error: The pattern is not simple enough.

探せませんでした。残念。推移律みたいな定理をどうやって探したらいいのかわかりませんが、とりあえず "SearchPattern (_ <= _)" としてやると一応でてきます。

FilterLength < SearchPattern (_ <= _).
...
Le.le_trans: forall n m p : nat, n <= m -> m <= p -> n <= p
...

ちょっと反則っぽいですが、求める定理 Le.le_trans が見つかりました。適用してみます。

FilterLength < apply Le.le_trans.
apply Le.le_trans.
Toplevel input, characters 0-17:
> apply Le.le_trans.
> ^^^^^^^^^^^^^^^^^
Error: Unable to find an instance for the variable m.

だめでした。まぁ、明らかにゴールと形が違うからね。coq は、ゴールが "n <= p" の形だから n と p はマッチできるけど m がよくわからん、と言っています。そんなあなたに eapply 。

FilterLength < eapply Le.le_trans.
eapply Le.le_trans.
2 subgoals
  
  a : Type
  f : a -> bool
  a0 : a
  xs : list a
  IHxs : length (filter f xs) <= length xs
  ============================
   length (filter f xs) <= ?11

subgoal 2 is:
 ?11 <= S (length xs)

Le.le_trans の m のところに謎の変数 "?11" が導入されました。 Le.le_trans は "n <= m -> m <= p -> n <= p" という形で、 "n <= p" の部分がゴールにマッチしたので、あとは "n <= m" と "m <= p" がそれぞれ証明できればいいです。そういうわけでゴールが2つになりました。

あとは ?11 という変数に証明できそうなちょうどいい式を与えてやればいいです。上で見たように ?11 に length xs を与えるのが簡単そうです。今回の場合は帰納法の仮定をそのまま適用してやれば、 ?11 が length xs になります。

FilterLength < apply IHxs.
apply IHxs.
1 subgoal
  
  a : Type
  f : a -> bool
  a0 : a
  xs : list a
  IHxs : length (filter f xs) <= length xs
  ============================
   length xs <= S (length xs)

明らかなので横着します。

FilterLength < auto.
auto.
Proof completed.

やったぜ！

FilterLength < Qed.
Qed.
induction xs.
 simpl in |- *.
 auto.
 
 simpl in |- *.
 case (f a0).
  simpl in |- *.
  apply Le.le_n_S.
  apply IHxs.
  
  eapply Le.le_trans.
   apply IHxs.
   
   auto.
   
FilterLength is defined

お疲れ様でした。