anarchy proofのAgda版作った

全国一億三千万のAgdarの皆様に送る Agda Challenge

最近chaton haskellがchaton agdaと化していたりすることもあり,anarchy proofがうらやましくてAgda版が欲しい人いっぱいいるのではないかと思って作ってみた.開発中にステージング環境を作り近くの数人にアナウンスしたけど何故か誰も試してみてくれないという悲しい事態を経たりしたのでもう公開する.きっと恥ずかしがりやさん達だったのだろう.

個人的にyesodとその周辺に関する知識をアップデートする目的があってyesodを採用している.デザインはあまり弄る気が起きずほぼ素のyesod 1.2のまま.あなごる・あなぷるでは採用してないが,認証系まわりも使ってみるためにOAuth認証を付けている.現在Twitterのみ.

使い方は大体あなぷると同じというかトップページの文面からして殆ど丸パクである.kikさんごめんなさい.

問題を作るときはDefinitions.agda(必要なら),Theorem.agda,Verifier.agdaを作って投稿する.Theoremは(あれば)Definitionsをimportし,証明すべきものをpostulateしておく.Verifierは(あれば)DefinitionsとTheoremをimportし,Theoremでpostulateしたものを使った検証用コードを書いておく.作成時はいずれも--safeオプション無しで検証される.

問題を投稿するときは(あれば)Definitions.agdaとTheorem.agdaをダウンロードし,Theorem.agda内のpostulateを消して証明したものを投稿する.投稿時はDefinitionsだけ--safeオプション無し,他は--safeオプション付きで検証される.

別段ゴルフがメインではないのだが,Agda Golferなる生物が万が一にも生息しているかもわからないので,念のためあなごる・あなぷる同様コードサイズを出すようにした.ただし,コードサイズの定義がそれらとは少し違っており,Unicode文字を多用するAgdaに合わせてbyteカウントではなく文字カウントとし,また証明の可読性に配慮する余地を残すため改行('\r','\n')と空白(' ')をカウントしないようにしている.

Agdarが増えるよ!!やっt(ry