はい、表題のとおりです。
Coqを勉強していたらよくわからない挙動にぶつかったのでメモ。
問題のコード
Fixpoint evenb (n:nat) : bool := match n with | O => true | S O => false | S (S n') => evenb n' end. Definition oddb (n:nat) : bool := negb (evenb n).
そこまで難しいもんじゃないです。 要するに偶数判定関数をFixpointの再帰関数として定義し、それを内部で呼ぶ奇数判定関数をDefinitionで定義しています。 これだけ見ると何の問題もないのですが……。
simplで証明できない
Example test_oddb1 : (oddb (S O)) = true. Proof. simple.
とまあこんな感じで証明を行おうとすると、
oddb 1 = true
のまま動かない。 一旦動かすようにしてみます。
幾つかパターンが有ります。
oddbをFixpointで定義する
先ほどのDefinitionで定義していたoddbをFixpointで定義することでsimplが使えるようになります。
Fixpoint oddb (n: nat) : bool := negb (evenb n). Example test_oddb1 : (oddb (S O)) = true. Proof. simpl. reflexivity. Qed.
unfold oddbをsimplの前に実行する
関数名を定義に置き換えるunfoldを使うことで、simplが使えるようになります。
Proof. unfold oddb. simpl. reflexivity. Qed.
computeをsimplの代わりに使う
Proof. compute. reflexivity. Qed.
終わりに
computeが何やっているのか全然わからず。
@zakky_dev 確かcbv beta delta iota zetaの別名です。http://t.co/UmeDBpI9yT
— コスモ (@cosmo__) 2014, 8月 5
Twitterで教えて頂いた感じだと複数のtacticを組み合わせたもののようです。