【发布时间】：2013-09-14 11:58:24
【问题描述】：
假设我有
- 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 | nO}（查看 Certiified Programming with Dependent Types 的第 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.
我无法理解接下来会发生什么，因为这对我来说太复杂了。
附：正如我所看到的——对于初学者来说，关于 Coq 中的一般递归和归纳的教程还不够好。至少我能找到。 :(
【问题讨论】：