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)

我认为这可以直接翻译为Coq：

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-club邮件列表上讨论了这种特殊的归纳类型。见https://sympa.inria.fr/sympa/arc/coq-club/2016-03/msg00206.html。

Answer 2

如果你想坚持与Agda相似的语法，你可以使用Sozeau的equations插件。你可以写：

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.