Coq例: n + 0 = n でいろいろ
証明戦略unfoldとfoldの練習です。
Coq < Lemma pluszero: forall n:nat, plus n 0 = n. 1 subgoal ============================ forall n : nat, n + 0 = n pluszero < intros. 1 subgoal n : nat ============================ n + 0 = n
pluszero < induction n. 2 subgoals ============================ 0 + 0 = 0 subgoal 2 is: S n + 0 = S n
まずnをnatの定義から帰納的に場合わけすると、nが0の場合とS mの場合とに分かれる。
Coq < Print nat. Inductive nat : Set := O : nat | S : nat -> nat For S: Argument scope is [nat_scope]
つづけます。
pluszero < unfold plus. 2 subgoals ============================ 0 = 0 subgoal 2 is: S n + 0 = S n pluszero < reflexivity. 1 subgoal n : nat IHn : n + 0 = n ============================ S n + 0 = S n
0+0をplusの定義で展開してみます。
plusの定義は、
Coq < Print plus.
plus =
fix plus (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p => S (p + m)
end
: nat -> nat -> nat
Argument scopes are [nat_scope nat_scope]0 + 0で、plusを展開すると、matchのうち、+の左の0のパターンによりm、このmが+の右の0になって、=の左辺が0になり、0 = 0で同値reflexivityでサブゴールが終了。
pluszero < unfold plus.
1 subgoal
n : nat
IHn : n + 0 = n
============================
S
((fix plus (n0 m : nat) {struct n0} : nat :=
match n0 with
| 0 => m
| S p => S (p + m)
end) n 0) = S n
pluszero < fold plus.
1 subgoal
n : nat
IHn : n + 0 = n
============================
S (n + 0) = S n
前のゴール同様に、左辺のplus (S n) 0 をplusの定義で展開すると、S側のS (p + m)にマッチして展開されるが、unfldでp+m中の再帰的なplusまでも展開してしまう。そこでそのplusの展開をfold plusに書き戻すことで、S (n + 0)となります。
- unfold f: fの定義で展開し、パターン簡約(beta iota reduction)する
- fold f: fの定義をfに置き換える
( http://coq.inria.fr/doc/Reference-Manual010.html#htoc212 より)
pluszero < rewrite IHn. 1 subgoal n : nat IHn : n + 0 = n ============================ S n = S n pluszero < reflexivity. Proof completed.
IHnの等式の左辺側で置き換え、同値で証明終了。
pluszero < Qed. intros. induction n. unfold plus in |- *. reflexivity. unfold plus in |- *. fold plus in |- *. rewrite IHn in |- *. reflexivity. pluszero is defined
一応、どんなコードが生成されるか。
Coq < Print pluszero.
pluszero =
fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) (refl_equal 0)
(fun (n0 : nat) (IHn : n0 + 0 = n0) =>
eq_ind_r (fun n1 : nat => S n1 = S n0) (refl_equal (S n0)) IHn) n
: forall n : nat, n + 0 = n
Argument scope is [nat_scope]わけわかりませんが、_indや_equalがinduction,reflexivityにより生成されるものであることから、なんとなくあのへんがunfoldやfoldになってそうという気はしそうです。
実のところ、この証明はautoで可能。その場合は、
Coq < Lemma bar: forall n:nat, plus n 0 = n. 1 subgoal ============================ forall n : nat, n + 0 = n bar < intros. 1 subgoal n : nat ============================ n + 0 = n bar < auto. Proof completed. bar < Qed. intros. auto. bar is defined
そのコードは。
Coq < Print bar.
bar = fun n : nat => sym_eq (plus_n_O n)
: forall n : nat, n + 0 = n
Argument scope is [nat_scope]
同様のplus_n_0: n=n+0がすでにnatで定義されていました。
