主页 / user-23260401

ocaml_enthusiast123's questions

Martin Hope
ocaml_enthusiast123
Asked: 2024-09-11 06:11:42 +0800 CST
  • 5

作为 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))，同时保持值不变。因此，我希望有以下等式，例如 -

@up 2 (None : fin 2) = (None : fin 3)

@up 2 (Some None : fin 2) = (Some None : fin 3)

我想写这个 -

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应该有一个空匹配的地方，但我不确定如何编写这种情况。任何帮助都将不胜感激！谢谢

coq