CoqのtacticやコマンドとAgda上操作の対応

この記事は Theorem Prover Advent Calendar 2013 1日目の記事です．
注意事項がひとつあります．本記事にはAgdaコードを含めようとしていますが，記事内でちゃんと書けてない文字があるかもしれません．だが私は悪くねぇ！

　　 　 　 ﾊヽ／::::ヽ.ヘ===ｧ
　　 　 　 {::{/≧=＝=≦V:/
　　 　 　 >:´:::::::::::::::::::::::::｀ヽ、
　　　 γ:::::::::::::::::::::::::::::::::::::::::ヽ
　 _／/::::::::::::::::::::::::::::::::::::::::::::::ﾊ　　　　　　私知ってるよ
.　| ll ! :::::::l::::::/|ハ::::::::∧::::i :::::::i　　　　　 みんなCoqの記事ばっか書くってこと
　 ､ヾ|:::::::::|:::/｀ト-:::::/ _,X:j:::/:::l
　　 ヾ:::::::::|≧ｚ　!Ｖ　ｚ≦　/::::/
　　　 ∧::::ト “　 　 　 　 “ ﾉ:::/!
　 　 /::::（＼　　 ー'　 　/￣）　 |
　　　 　 |　｀`ー――‐''|　　ヽ、.|
　　　　　 ゝ　ノ　　　　 ヽ　 ノ　|
￣￣￣￣￣￣￣￣￣￣￣￣￣￣￣￣￣￣ 　　　　　　　

なので，出バナでCoq-erをAgdaに誘導(特にAgda Challengeに誘導)する記事出そうという方針で1日目を取る．あとネタ被りされると私のような定理証明弱者はネタが無くて死ぬのでそれを避ける意味でも．

レガシーCoqの基本的なtacticとかコマンドなどアレコレを，Software Foundationsに出てくる順とかに見ていってAgdaにマッピングするとだいたいのところagda-modeのどんな操作とかどんなコードに対応するかという話をしよう．ちなAgda標準ライブラリ有りでザックリと．

match ... with ... end.

いきなりtacticじゃないけどまあよく使うのでパターンマッチあたりから．

とりあえずHaskellとかと同じ．

even : ℕ → Bool
even 0 = true
even 1 = false
even (suc (suc n)) = even n

もしくは，Function.case_of_などを使って．

even' : ℕ → Bool
even' n = case n of λ
  { 0 → true
  ; 1 → false
  ; (suc (suc n)) → even' n
  }

まぁコレもパターンマッチ付きのラムダ使ってるから最初のとあまり変わり無いと言えば無いんだけど，停止性がわかんなくなることがあるらしいのでちょい注意．

reflexivity tactic

Relation.Binary.PropositionalEquality.reflとか等価性が定められるものには大体reflがあるからそれ使えばいい．

A≡A : ∀ {a} {A : Set a} → A ≡ A
A≡A = refl

simpl tactic

特に何かあるわけではなく適宜実行されてる？みたい．

0+0≡0 : 0 + 0 ≡ 0
0+0≡0 = refl

Inductive Data Type

これもtacticじゃないけどInductiveは普通の(=#や♭を使わない)データ定義．

data nat : Set where
  zero : nat
  suc : nat → nat

Haskellと同じカンジだけど，こっちは依存型バリバリだから常にGADTとかそのへんがONになってる状態と思ってもらえば．

Eval simpl in ~

Eval simpl in ~ は agda-mode の c-c c-n に対応している．
c-c c-n すると "Expression: [∏]"と式の入力を促され，式を入力してEnterで式の評価結果が表示される．
また，ゴール内で式を書いて c-c c-n すると，そのゴール内に書いた式がそのゴールの環境において評価されて表示される．

Admitted

Admittedはpostulateに対応．

たとえば，直観主義では証明できないPeirce's lawを定義しておくには以下のようになる．

postulate
  peirce : (P Q : Set) → ((P → Q) → P) → P

Check

Check は agda-mode の c-c c-d に対応している
c-c c-d すると "Expression: [∏]"と式の入力を促され，入力してEnterで式の型が表示される
また，ゴール内で式を書いて c-c c-d すると，そのゴール内に書いた式の型そのゴールの環境において評価されて表示される．

Notation

Notationに相当する機能は無い．というかprefix/suffix/mixfix operatorとそれらの結合優先度が使えるから必要性がほぼ無い．

intro/intros tactic

intro/introsはゴールのλ抽象を1から数段外して仮定に加えるということをするだけ．

0+n≡n : ∀ n → 0 + n ≡ n
0+n≡n = ?

に対して，ゴール?の型は(n : ℕ) → 0 + n ≡ nなので，そのまま証明した証明オブジェクトは

0+n≡n = λ n → refl

だが，intro/intros相当の書き換え(=λ抽象を1から数段外し)をすると

0+n≡n n = ?

を証明することになり，ゴール?の型が0 + n ≡ nになるので，証明オブジェクトは

0+n≡n n = refl

ということになる．

rewrite tactic

rewrite tactic は rewrite pattern もしくは Relation.Binary.PropositionalEquality.Core.subst が対応する．

n≡m→n+n≡m+m : ∀ n m → n ≡ m → n + n ≡ m + m
n≡m→n+n≡m+m n m n≡m
  rewrite n≡m
        = refl -- このときゴールの型は m + m ≡ m + m

rewrite H はこれでいいが，逆方向の書き換え rewrite ← H については，Relation.Binary.PropositionalEquality.Core.sym を使う．

n≡m→n+n≡m+m : ∀ n m → n ≡ m → n + n ≡ m + m
n≡m→n+n≡m+m n m n≡m
  rewrite sym n≡m
        = refl -- このときゴールの型は n + n ≡ n + n

destruct tactic

agda-mode の c-c c-c に対応しており，これは対象の変数に対し，その変数部分の網羅的なパターンマッチに展開する．

b∧c≡t→b≡t : ∀ b c → b ∧ c ≡ true → b ≡ true
-- b∧c≡t→b≡t b c b∧c≡t = ? まで書いて c-c c-l
-- b∧c≡t→b≡t b c b∧c≡t = { }0 となるので，このゴールの中で c-c c-c
-- すると "pattern variables to case:   [∏]"となるので対象の変数bを入れEnter
-- b∧c≡t→b≡t true c b∧c≡t = { }0
-- b∧c≡t→b≡t false c b∧c≡t = { }1
-- のようにbについて場合分けされる．
-- b∧c≡t→b≡t true c b∧c≡t = { }0 のほうのゴールはtrue ≡ true なので refl
b∧c≡t→b≡t true c b∧c≡t = refl
-- b∧c≡t→b≡t false c b∧c≡t = { }1 のほうのゴールはfalse ≡ true なので ⊥ になるはず，
-- このとき仮定b∧c≡tがもう成立していないハズなので．さらに c-c c-c で b∧c≡t すると．
b∧c≡t→b≡t false c ()
-- と仮定が空(⊥)にマッチして証明完了．

ゴールに対象の変数を書いてから c-c c-c でもよい．また，複数の変数を同時に展開することもできる．

b∧c≡t→b≡t' : ∀ b c → b ∧ c ≡ true → b ≡ true
-- b∧c≡t→b≡t' b c b∧c≡t = ? まで書いて c-c c-l
-- b∧c≡t→b≡t' b c b∧c≡t = { }0 となるので，このゴールの中に次のように書き，
-- b∧c≡t→b≡t' b c b∧c≡t = {b b∧c≡t }0 そして c-c c-lすると，
-- b∧c≡t→b≡t' true .true refl = { }
-- b∧c≡t→b≡t' false c ()
-- と場合分けされ後者のケースは即終わる．前者はrefl入れて終わり．
b∧c≡t→b≡t' true .true refl = refl
b∧c≡t→b≡t' false c ()

イントロパターンに相当するものは無いのでAgdaが適当に変数名を補完する．気に入らなければ展開後に直せばいい．先にやるか後でやるかの違い程度．

induction tactic

induction は destruct と同じくc-c c-c で展開し，その変数が再帰的なデータ型であれば， 証明オブジェクトが構造再帰関数となるだけ．

n+0≡n : ∀ n → n + 0 ≡ n
-- c-c c-c で n について場合分け
-- これが base case
n+0≡n zero = refl
-- こっちが step case
n+0≡n (suc n)
  rewrite n+0≡n n -- nについて再帰したものは使ってOK(=使っても停止することはわかっている)
        = refl

assert tactic

assertは着目したい部分だけwhere節などで取り出したりするだけ．
やはりイントロパターンに相当するものは無いが，どのみち適当に名付けないと本筋で使えないのでどうでもいい．

replace tactic

replace t with u は rewrite (仮定等から t ≡ u を作る式) に対応．

remember tactic

Relation.Binary.PropositionalEquality.inspect による．

eqℕ : ℕ → ℕ → Bool
eqℕ zero zero = true
eqℕ zero (suc b) = false
eqℕ (suc a) zero = false
eqℕ (suc a) (suc b) = eqℕ a b

3or5 : ℕ → Bool
3or5 n with eqℕ n 3
3or5 n | true = true
3or5 n | false = eqℕ n 5

odd : ℕ → Bool
odd zero = false
odd (suc n) = not (odd n)

eqℕ-a-b→odd-a≡odd-b : ∀ a b → eqℕ a b ≡ true → odd a ≡ odd b
eqℕ-a-b→odd-a≡odd-b zero zero p = refl
eqℕ-a-b→odd-a≡odd-b zero (suc b) ()
eqℕ-a-b→odd-a≡odd-b (suc a) zero ()
eqℕ-a-b→odd-a≡odd-b (suc a) (suc b) p = cong not (eqℕ-a-b→odd-a≡odd-b a b p)

3or5-odd : ∀ n → 3or5 n ≡ true → odd n ≡ true
-- eqℕの定義に従い，まずはeqℕ n 3の結果で場合分けするが，
-- eqℕ n 3をどちらに評価したかも使うのでinspectで覚えさせる
3or5-odd n p with eqℕ n 3 | inspect (eqℕ n) 3
3or5-odd n p | true | [ eq ] = eqℕ-a-b→odd-a≡odd-b n 3 eq
-- eqℕの定義に従い，次にeqℕ n 5の結果で場合分けするが，
-- eqℕ n 5をどちらに評価したかも使うのでinspectで覚えさせる
3or5-odd n p | false | [ eq ] with eqℕ n 5 | inspect (eqℕ n) 5
3or5-odd n p | false | [ eq₁ ] | true | [ eq ] = eqℕ-a-b→odd-a≡odd-b n 5 eq
3or5-odd n () | false | [ eq₁ ] | false | [ eq ]

inversion tactic

absurd pattern matching で矛盾引き出して終わり．

ring tactic

Data.Nat.PropertiesのRingSolverによる．

環上の多項式のequalityを示すには

f : ∀ x a b → x * x + (a + b) * x + a * b ≡ (x + a) * (x + b)
-- 式をRingSolver用の構造(_:*_;  _:+_; _:+_)で書き直す
f = solve 3 (λ x a b → x :* x :+ (a :+ b) :* x :+ a :* b := (x :+ a) :* (x :+ b)) refl
-- 3は式内の変数のarity，reflはまぁ，おやくそく的に

リフレクションを使えば構造を自分で書き直している部分を自動化したものを定義することもできる．

まぁ，他にもいろいろあるだろうけどとりあえずこのくらいで．