Предположим, что у меня есть
- тип Т
- обоснованное отношение R: T-> T-> Prop
- функция F1: T-> T, которая делает аргумент «меньше»
- условие C: T-> Prop, которое описывает "начальные значения" 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} (смотрите главу 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.
Я не мог понять, что происходит дальше, потому что это было слишком сложно для меня.
P.S. На мой взгляд, нет достаточно хорошего учебника по общей рекурсии и индукции в Coq для начинающих. По крайней мере, я смог найти. :(
