如何在Coq中将fin(S n)类型值提升至fin(S(S n))并保留原值？

给定fin类型的递归定义：

Fixpoint fin (n : nat) : Type :=
  match n with
  | 0 => False
  | S m => option (fin m)
  end.

我们需要定义函数up，将fin (S n)类型的值映射到fin (S (S n))且保留原值结构。你之前的定义被拒绝，核心问题是未处理n=0的基础情况，且递归调用的参数逻辑有误。

正确的up函数定义 #

Fixpoint up (n : nat) : fin (S n) -> fin (S (S n)) :=
match n with
| 0 => fun p => match p with None => None end
| S m => fun p => match p with
                  | None => None
                  | Some p' => Some (up m p')
                  end
end.

定义说明 #

• 基础情况（n=0）：此时fin (S 0) = fin 1 = option False，该类型仅含元素None（False无构造子），直接返回None : fin (S (S 0)) = fin 2即可。
• 递归情况（n=S m）：
  • 若输入为None : fin (S (S m))，直接返回None : fin (S (S (S m)))
  • 若输入为Some p'（p' : fin (S m)），递归调用up m将p'提升至fin (S (S m))，再用Some包裹得到目标类型的值。

验证期望等式 #

• @up 2 (None : fin 2)：进入n=2=S1分支，输入为None，直接返回None : fin 3，符合要求。
• @up 2 (Some None : fin 2)：进入n=2=S1分支，输入为Some p'（p'=None : fin1），递归调用up1 p'返回None : fin2，最终得到Some None : fin3，符合要求。

内容的提问来源于stack exchange，提问作者ocaml_enthusiast123