概要 Agda2 で挿入ソート関数を定義して、それがほんとにリストをソートすることを証明してみました。試すには Agda の標準ライブラリ(The Agda Wiki - Standard Library)が必要です。 冗長な証明になっている可能性は大いにあります。Agda のサンプルコード…

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 da…

Agda というか依存型が(主に自分の周りで)流行っている。id:yoshihiro503 さんが Agda にはまっていて頼もしい感じなのでいろいろ教えてもらえればと思います。

どうやら Agda2 はまだ主流じゃない(?)ような感じなので、まずは Agda1 を触ってみようと思った。こっちならチュートリアルとかも少しはあるし。というかそもそもの動機の論文では Agda1 を使ってるし…。(最初に気づいとけよ)

Agda2 まじわかんない。心折れそう。とりあえず agda-mode で使い方がわかったやつを適当 メモ。そのうち追加します。 C-c C-x C-l agda で証明を開始。 ? 証明がよくわからないところは ? で埋める。 assoc x y z = ? これで C-c C-x C-l とすると ? がゴー…

なときに、である証明。よくわかってない。まず filter の定義。 filter : forall {a} -> (a -> Bool) -> [ a ] -> [ a ] filter p [] = [] filter p (x ∷ xs) with p x ... | true = x ∷ filter p xs ... | false = filter p xs で、証明。 mod…

Agda を勉強中です。いわゆる初心者マークです。どこぞのチュートリアルに載ってたこのコードが通らないので困る。最後の odd k の型が合わないらしい。 あと dotted pattern っていうのもいまいち理解に自信がない。型から値がわかるような仮引数につけるっ…

summer school library っていうのを使ったら動きました。あとでライブラリのコードを読まねば。 module Views where open import Data.Nat data Parity : ℕ -> Set where even : (k : ℕ) -> Parity (k * 2) odd : (k : ℕ) -> Parity (1 +…

あまりわかってないけど、とりあえずいくつか適当な関数を書いたのでメモ。依存型うける(気がする)。 agda2 の emacs モードが使いこなせないのと関数を実行する方法がわからんのが問題である。 module NList where data Nat : Set where zero : Nat succ : …

今 Agda 的な論文を読んでて、Agda はなかなかおもしろそうだなと思った。Coq よりは情報系の人に優しい気がするし(僕は情報系ですらないという噂も。Oops!)。というわけで日記に Agda タグを作ってみた。依存型とかうけるし。