Coq 添加一个新变量而不是使用正确的变量

Question

我正在 Coq 中自己实现向量，运行遇到了一个奇怪的问题。

到目前为止，这是我的代码：

Inductive Fin : nat -> Type :=
  |FZ : forall n, Fin (S n)
  |FS : forall n, Fin n -> Fin (S n).

Definition emptyf(A : Type) : Fin 0 -> A.
  intro e; inversion e.
Defined.

Inductive Vec(A : Type) : nat -> Type :=
  |Nil  : Vec A 0
  |Cons : forall n, A -> Vec A n -> Vec A (S n).

Definition head(A : Type)(n : nat)(v : Vec A (S n)) : A :=
  match v with
  |Cons a _ => a
  end.

Definition tail(A : Type)(n : nat)(v : Vec A (S n)) : Vec A n :=
  match v with
  |Cons _ w => w
  end.

Fixpoint index(A : Type)(n : nat) : Vec A n -> Fin n -> A :=
  match n as n return Vec A n -> Fin n -> A with
  |0   => fun _ i => emptyf _ i
  |S m => fun v i => match i with
                     |FZ _ => head v
                     |FS j => index (tail v) j
                     end
  end.

tail 之前的所有内容都可以正常编译，但是当我尝试编译 index 时，我收到以下错误：

Error:
In environment
index : forall (A : Type) (n : nat), Vec A n -> Fin n -> A
A : Type
n : nat
m : nat
v : Vec A (S m)
i : Fin (S m)
n0 : nat
j : Fin n0
The term "j" has type "Fin n0" while it is expected to have type "Fin m".

显然，罪魁祸首是 Coq 引入了新变量 n0 而不是将 j 分配给类型 Fin m，即使这是 [=15= 的唯一可能类型] ] 这将导致从 j 构建 i。知道为什么会发生这种情况吗？我该如何解决这个问题？

Answer 1

我发现 Vec 和 Fin 通常很难使用，所以我最近使用 math-comp 中的 'I_n 和 n.-tuples T，它们只是自然物和附有无关证据的清单。但是，如果你想继续复杂模式匹配的乐趣，你可以尝试定义一个更强的模式匹配原则：

Definition fin_case T m (i : Fin m) : T -> (Fin (pred m) -> T) -> T :=
  match i with
  | FZ _   => fun fn fz => fn
  | FS _ j => fun fn fz => fz j
  end.

一旦你有了 fin_case，你的函数定义就可以工作了：

Fixpoint index (A : Type) (n : nat) : Vec A n -> Fin n -> A :=
  match n as n return Vec A n -> Fin n -> A with
  | 0   => fun _ i => emptyf _ i
  | S m => fun v i => fin_case i (head v) (index (tail v))
  end.

Answer 2

当您使用 match 时，您可能会丢失信息。我使用 convoy pattern 将信息返回到上下文中。

    match i in Fin (S n0) return n0 = m  -> A with 
      ... => fun H : n0 = m => ...
    end  eq_refl

使 Coq 能够将信息 n0 = m 放入上下文中。它作为函数参数发送到匹配子句中。为了在类型检查中使用它，我使用 (match H with ... end) 以便 Coq 理解 Fin n0 = Fin m。这就是解决方案。

Fixpoint index(A : Type)(n : nat) : Vec A n -> Fin n -> A :=

  match n as n return Vec A n -> Fin n -> A with
  |0   => fun _ i => emptyf _ i
  |S m => fun v i =>
           match i in Fin (S n') return n' = m  -> A with
             |FZ _ => fun _ => head _ _ v
             |FS _ j => fun H => index (tail v) (match H with eq_refl _  => j end)
           end eq_refl
  end.

当类型检查无法理解两件事是否相等时，护送模式通常可以帮助您将该信息放入上下文中。我还建议使用 refine 来逐步构建术语。它让你看到上下文中有什么信息。

Answer 3

请注意，您不需要针对 n 进行模式匹配，而只需针对 Fin n 类型的参数进行模式匹配。生成的定义更简单。

Fixpoint index {A:Type} {n:nat} (i:Fin n) : Vec A n -> A :=
  match i in Fin n0 return Vec A n0 -> A with
  | FZ => fun v => head v
  | FS j => fun v => index j (tail v)
  end.

Coq 实际上很聪明，可以猜出注释。

Fixpoint index {A:Type} {n:nat} (i:Fin n) : Vec A n -> A :=
  match i with
  | FZ => fun v => head v
  | FS j => fun v => index j (tail v)
  end.

Answer 4

只是添加到其他答案中，一个基于策略的解决方案：

Fixpoint index (A : Type) (n : nat) (v : Vec A n) (i : Fin n) : A.
  destruct v as [| n h tl].
  - exact (emptyf A i).
  - inversion i as [ | ? i'].
    + exact h.
    + exact (index _ _ tl i').
Defined.

inversion 策略负责 "information loss"。如果你尝试 Print index. 结果不会很好，但 Coq 本质上使用了@larsr 提到的护航模式。

请注意，此方法不在 n 上使用模式匹配。相反，它在向量参数上进行模式匹配，这就是为什么它不需要 head 和 tail 函数的原因。

Coq 添加一个新变量而不是使用正确的变量

Coq adding a new variable instead of using the correct one

coq