将值从一种 fintype 转换为另一种 fintype？

Question

作为 Coq 新手，我被这个问题困扰了。希望有人可以帮忙！

Coq 中有限类型的编码如下 -

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

是否可以定义一个将值从

fin (S n)

提升到

fin (S (S n))

的函数。我想写这个-

Fixpoint up {n:nat} : fin (S n) -> fin (S (S n)) :=
fun p => match p with 
         | None => None 
         | Some p' => Some (up p)

但是被拒绝了。直觉上我明白这是可能的，因为 -

fin 2 - None, Some None

的成员是

fin 3 - None, Some None, Some (Some None)

的成员，依此类推。但我无法为其编写函数。我怀疑它是因为递归定义必须处理

@up 0

，其中应该有一个空匹配，但我不知道如何编写这种情况。任何帮助将不胜感激！谢谢

Answer 1

一种有用的调试方法是用其对应的证明模式替换您的定义，以查看发生了什么：

Fixpoint up {n:nat} : fin (S n) -> fin (S (S n)).
cbn in *. intro p; destruct p as [p' |].
- (* case Some *)
- (* case None *)

如果你这样做，你会发现你正在尝试构建一个

option (option (fin n))

类型的术语，并且知道：

up: forall n : nat,
     option (fin n) ->
     option (option (fin n))
n: nat
p': fin n
--------------------------------
option (option (fin n))

很明显

up p

没有输入检查

但其实你想多了，这里不需要归纳，

fin (S n)

就是

option n

，所以你可以将

up {n} : fin n -> fin (S n)

定义为

Some

：

Definition up {n:nat} : fin n -> fin (S n) := Some.