Coq推理行为

Question

我试图用Coq编写以下Agda片段。

open import Data.Fin using (Fin; suc; zero)
open import Data.Nat using (ℕ; suc; zero)

thin : {n : ℕ} -> Fin (suc n) -> Fin n -> Fin (suc n)
thin zero    y       = suc y
thin (suc x) zero    = zero
thin (suc x) (suc y) = suc (thin x y)

我认为这可以直截了当地翻译为：

Inductive Fin : nat -> Type :=
  | fz {n : nat} : Fin (S n)
  | fs {n : nat} : Fin n -> Fin (S n).

Fixpoint thin {n : nat} (x : Fin (S n)) (y : Fin n) : Fin (S n) :=
  match x, y with
    | fz,      y' => fs y'
    | (fs x'), fz => fz
    | (fs x'), (fs y') => fs (thin x' y')
  end.

然而，这会导致以下错误：

Toplevel input, characters 171-173:
Error:
In environment
thin : forall n : nat, Fin (S n) -> Fin n -> Fin (S n)
n : nat
x : Fin (S n)
y : Fin n
n0 : nat
x' : Fin n0
n1 : nat
y' : Fin n1
The term "x'" has type "Fin n0" while it is expected to have type
 "Fin (S ?n1)".

我相信Coq应该能够计算出隐式参数n，所以我不知道发生了什么。我想我不知道Agda和Coq的类型系统之间的区别，因为以前的类型比较好。

Answer 1

当模式匹配与依赖类型匹配时，Coq通常不考虑上下文中的变量与分支中引入的变量之间的一些本质关系。

最简单的解决方案是在验证模式下定义函数，至少要了解正在发生的事情。

这意味着：

Fixpoint thin {n : nat} (x : Fin (S n)) (y : Fin n) : Fin (S n).
Proof.
  remember (S n) as n1. (* trick to keep the information when destructing *)
  destruct x; apply eq_add_S in Heqn1; subst n0.
  - apply fs. assumption.
  - destruct y.
    + apply fz.
    + apply fs. apply thin; assumption.
Defined. (* to create a transparent constant, as given by a classic Fixpoint *)

然后，您可以打印值并读取lambda术语，以了解如何直接定义它。这可能会使：

Fixpoint thin {n : nat} (x : Fin (S n)) (y : Fin n) : Fin (S n) :=
  match x as x0 in Fin k return k = S n -> Fin (S n) with
  | fz => fun _ => fs y
  | fs x' =>
      fun H => match y as y0 in Fin l return n = l -> Fin (S n) with
      | fz => fun _ => fz
      | fs y' => fun H' =>
          fs (eq_rec_r (fun x => Fin x)
                       (thin (eq_rec_r _
                                (eq_rec_r _ x' (eq_add_S _ _ (eq_sym H)))
                                (eq_sym H'))
                              y')
                       H')
      end eq_refl
  end eq_refl.

模式匹配的return子句用于解决上述问题:它们连接在分支中引入的变量和上下文中引入的变量。这里将对此进行更深入的讨论：http://adam.chlipala.net/cpdt/html/MoreDep.html。

还请注意，这种特殊的归纳类型是几周前在coq俱乐部邮件列表上讨论过的。见https://sympa.inria.fr/sympa/arc/coq-club/2016-03/msg00206.html。

Answer 2

如果您想坚持使用与Agda非常相似的语法，可以使用Sozeau的方程式插件。你可以写：

Require Import Equations.

Inductive Fin : nat -> Type :=
  | fz {n : nat} : Fin (S n)
  | fs {n : nat} : Fin n -> Fin (S n).

Lemma FinO_elim : Fin O -> False.
Proof.
inversion 1.
Qed.

Equations thin {n : nat} (x : Fin (S n)) (y : Fin n) : Fin (S n)
:= thin {n:=O}     _      y      :=! y (* y is uninhabited *)
;  thin fz     y      := fs y
;  thin (fs x) fz     := fz
;  thin (fs x) (fs y) := fs (thin x y)
.

You can also remove the first dead-code clause which is automatically inferred.