主页 / coding / 问题 / 78971470
Accepted
ocaml_enthusiast123
Asked: 2024-09-11 06:11:42 +0800 CST

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

  • 772

作为 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

2 个回答

  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.
    • 1
  2. Best Answer

    您将需要依赖模式匹配才能对您的术语进行正确的类型检查。

    您的结构参数只能是，因为n这是您的的唯一参数Fixpoint。您的递归调用必须应用于的子项，n因此您需要在某处。matchn

    我赞成下面的解决方案，返回类型fin n -> fin (S n)，它更通用一些，但您可以fin (S n) -> fin (S (S n))稍后根据需要对其进行专门化：

    Fixpoint up {n} : fin n -> fin (S n) :=
  match n return fin n -> fin (S n) with 
  | 0   => fun p => match p with end
  | S n => fun p => match p with 
                    | None => None
                    | Some q => Some (up q)
                    end
  end.

Goal forall n, @up (S n) None = None.
Proof. reflexivity. Qed.

Goal forall n (p : fin n), @up (S n) (Some p) = Some (up p).
Proof. reflexivity. Qed.

Fixpoint fin2nat {n} : fin n -> nat :=
  match n with 
  | 0   => fun p => match p with end
  | S n => fun p => match p with
                    | None   => 0
                    | Some p => S (fin2nat p)
                    end
  end.

Eval compute in @fin2nat 8 (Some (Some (Some None))).
Eval compute in @fin2nat 20 (Some (Some (Some None))).

Fact up_correct {n} p : fin2nat (@up n p) = fin2nat p.
Proof.
  induction n as [ | n IHn ] in p |- *; destruct p; simpl fin2nat; trivial.
  f_equal; exact (IHn _).
Qed.
    • 1

相关问题