我正在做一个关于使用子集类型编写经过认证的函数的简单练习。想法是先写一个前驱函数
pred : forall (n : {n : nat | n > 0}), {m : nat | S m = n.1}.
然后使用这个定义给定一个函数
pred2 : forall (n : {n : nat | n > 1}), {m : nat | S (S m) = n.1}.
我对第一个没有问题。这是我的代码
Program Definition pred (n : {n : nat | n > 0}) : {m : nat | S m = n.1} :=
match n with
| O => _
| S n' => n'
end.
Next Obligation. elimtype False. compute in H. inversion H. Qed.
但我无法解释第二个定义。我试图写出这些定义
Program Definition pred2 (n : {n : nat | n > 1}) : {m : nat | S (S m) = n.1}
:= pred (pred n).
我设法证明了前两个义务
Next Obligation. apply (gt_trans n 1 0). assumption. auto. Qed.
Next Obligation.
destruct pred.
simpl.
simpl in e.
rewrite <- e in H.
apply gt_S_n in H; assumption.
Qed.
但对于最后一项义务,我陷入了困境,因为当我尝试对 pred 的返回类型进行案例分析时,新的假设并未在目标中重写。
我尝试了以下策略但没有结果。
destruct (pred (n: pred2_obligation_1 (n ; H))).
destruct (pred (n; pred2_obligation_1 (n ; H))) eqn:?.
rewrite Heqs.
我知道我可以直接编写 pred2,但想法是使用和组合函数 pred。