私が持っているとしましょう
- T型
- 根拠のある関係 R: T->T->Prop
- 関数 F1: 引数を「小さく」する T->T
- 条件 C: T->R の「開始値」を記述するプロップ
- 関数 F2: 引数を「大きく」する T->T
次のような Fixpoint を作成するにはどうすればよいですか。
Fixpoint Example (n:T):X :=
match {C n} + {~C n} with
left _ => ... |
right _ => Example (F1 n)
end.
そして、戦術「誘導」（または同様のもの）の次の使用法をどのように可能にすることができますか：
Theorem ...
Proof.
...
induction n F.
(* And now I have two goals:
the first with assumption C n and goal P n,
the second with assumption P n and goal P (F2 n) *)
...
Qed.
タイプnzでそれをやろうとしました: {n:nat | n<>O} (Certified Programming with Dependent Types book の 7.1 章を参照) しかし、ここまでしか得られませんでした:
Require Import Omega.
Definition nz: Set := {n:nat | n<>O}.
Theorem nz_t1 (n:nat): S n<>O. Proof. auto. Qed.
Definition nz_eq (n m:nz) := eq (projT1 n) (projT1 m).
Definition nz_one: nz := exist _ 1 (nz_t1 O).
Definition nz_lt (n m:nz) := lt (projT1 n) (projT1 m).
Definition nz_pred (n:nz): nz := exist _ (S (pred (pred (projT1 n)))) (nz_t1 _).
Theorem nz_Acc: forall (n:nz), Acc nz_lt n.
Proof.
intro. destruct n as [n pn], n as [|n]. omega.
induction n; split; intros; destruct y as [y py]; unfold nz_lt in *; simpl in *.
omega.
assert (y<S n\/y=S n). omega. destruct H0.
assert (S n<>O); auto.
assert (nz_lt (exist _ y py) (exist _ (S n) H1)). unfold nz_lt; simpl; assumption.
fold nz_lt in *. apply Acc_inv with (exist (fun n0:nat=>n0<>O) (S n) H1). apply IHn.
unfold nz_lt; simpl; assumption.
rewrite <- H0 in IHn. apply IHn.
Defined.
Theorem nz_lt_wf: well_founded nz_lt. Proof. exact nz_Acc. Qed.
Lemma pred_wf: forall (n m:nz), nz_lt nz_one n -> m = nz_pred n -> nz_lt m n.
Proof.
intros. unfold nz_lt, nz_pred in *. destruct n as [n pn], m as [m pm]. simpl in *.
destruct n, m; try omega. simpl in *. inversion H0. omega.
Defined.
私には複雑すぎて、さらに何が起こるのか理解できませんでした。
PS私が見ているように、初心者向けのCoqの一般的な再帰と誘導に関する十分なチュートリアルはありません。少なくとも私は見つけることができました。:(