我正在尝试在 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 的类型系统之间的区别,因为前者的类型检查很好。
最佳答案
在与依赖类型进行模式匹配时,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 .
关于types - Coq 推理行为,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/36996020/