眠気と戦う日々

眠気と戦いながらいろいろと書くブログ

内部でFixpointの関数を呼ぶ関数を定義した時にsimplだと証明できない

Coq

はい、表題のとおりです。
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が何やっているのか全然わからず。

Twitterで教えて頂いた感じだと複数のtacticを組み合わせたもののようです。

各種リンク

ソフトウェアの基礎