fixタクティック
fixタクティックについて。
ふつう、Coqの証明モードで構造帰納法を回したい場合は inductionタクティックを使いますが、 fix は、帰納法のためのよりプリミティブなタクティックのようです(項の場合分けをやらない)．
This tactic is a primitive tactic to start a proof by induction. In general, it is easier to rely on higher-level induction tactics such as the ones described in Section 8.7.
In the syntax of the tactic, the identifier ident is the name given to the induction hypothesis. The natural number num tells on which premise of the current goal the induction acts, starting from 1 and counting both dependent and non dependent products. Especially, the current lemma must be composed of at least num products.
...
ちょっとこの説明はわかりづらいですが， 要するに "fix 仮定の名前 引数の位置." という風に書きます．例えば，
============================ forall (x : T1) (y : T2), P x y
というゴールがあるとき，
fact < fix IH 1.
とやれば x の構造に関する帰納法になります．ここで IHが帰納法の仮定になります．また，
fact < fix IH 2.
とやれば y の構造に関する帰納法になります．
「どの引数について帰納法を回すか」を考えるのをサボりたい場合は refine (fix fact x y := _). とかやれば，いけるかもしれない．
どの場合でも、ゴールは
IH : forall (x : T1) (y : T2), P x y ============================ forall (x : T1) (y : T2), P x y
になります． IHを使う場合は、構造的により小さい引数を第1 (もしくは2) 引数に与えます．
使ってみる
関数 fact : nat -> nat と lt : nat -> nat -> bool を わざわざ証明モードで定義して，その途中で fixタクティックを使ってみます．
ふつう関数はGallinaで定義するので特に意味はありませんが、良い例題がうかばなかったので…
Coq < Definition fact : nat -> nat. 1 subgoal ============================ nat -> nat fact < fix fact 1. 1 subgoal fact : nat -> nat ============================ nat -> nat fact < intro x. 1 subgoal fact : nat -> nat x : nat ============================ nat fact < case x. 2 subgoals fact : nat -> nat x : nat ============================ nat subgoal 2 is: nat -> nat fact < apply (S O). (* x=O のとき 1 *) 1 subgoal fact : nat -> nat x : nat ============================ nat -> nat fact < intro y. 1 subgoal fact : nat -> nat x : nat y : nat ============================ nat fact < apply (x * fact y). (* x=y+1 のとき x * fact y *) Proof completed. fact < Qed. fix fact 1. intro x. case x. apply 1. intro y. apply (x * fact y). fact is defined
ちゃんと定義できていると思います(カリーハワード的に考えて)．
一応チェック．
Coq < Print fact. fact = fix fact (x : nat) : nat := match x with | 0 => 1 | S y => x * fact y end : nat -> nat Argument scope is [nat_scope] Coq <
次は < ．こんどは2番目の引数について回してみましょう．ここで定義しているのはbool型を返す関数で，Prop型をもつ述語とは違うので注意．紛らわしくてスイマセン．
Coq < Definition lt : nat -> nat -> bool. 1 subgoal ============================ nat -> nat -> bool lt < fix lt 2. 1 subgoal lt : nat -> nat -> bool ============================ nat -> nat -> bool lt < intros x y. 1 subgoal lt : nat -> nat -> bool x : nat y : nat ============================ bool lt < case y. (* yについて場合分け *) 2 subgoals lt : nat -> nat -> bool x : nat y : nat ============================ bool subgoal 2 is: nat -> bool lt < apply false. (* y=0のときfalse *) 1 subgoal lt : nat -> nat -> bool x : nat y : nat ============================ nat -> bool lt < intro y1. (* y=y1+1のとき *) 1 subgoal lt : nat -> nat -> bool x : nat y : nat y1 : nat ============================ bool lt < case x. (* xについて場合分け *) 2 subgoals lt : nat -> nat -> bool x : nat y : nat y1 : nat ============================ bool subgoal 2 is: nat -> bool lt < apply true. (* x=0のとき true *) 1 subgoal lt : nat -> nat -> bool x : nat y : nat y1 : nat ============================ nat -> bool lt < intro x1. (* x=x1+1 のとき *) 1 subgoal lt : nat -> nat -> bool x : nat y : nat y1 : nat x1 : nat ============================ bool lt < apply (lt x1 y1). (* 帰納法の仮定を使う，というか再帰 *) Proof completed. lt < Qed. fix lt 2. intros x y. case y. apply false. intro y1. case x. apply true. intro x1. apply (lt x1 y1). lt is defined Coq < Print lt. lt = fix lt (x y : nat) : bool := match y with | 0 => false | S y1 => match x with | 0 => true | S x1 => lt x1 y1 end end : nat -> nat -> bool Argument scopes are [nat_scope nat_scope] Coq <
証明モードで作った証明が，カリーハワード同型で対応する Gallinaのプログラムになっています．大丈夫っぽいです．
