时间戳

首页 > 解决方案 > Gallina 中是否有任何未键入但有效的术语？

types - Gallina 中是否有任何未键入但有效的术语？

问题描述

我认为 Gallina 语言的每个有效术语都有一个相关的类型。但是是否有任何术语被 Coq 接受，而没有被输入？

这主要是关于一些翻译的事情，但（我认为）也是一件有趣的事情。

标签： typescoq

解决方案

正如 Yves 和gallais 所说，除了系统中的错误之外，Coq 接受的每个 Gallina 术语都有一个类型。这几乎是根据定义；说一个术语t被 Coq 接受就是说它Check t不会失败，我们可以观察到它Check t总是会打印一个t. 现在，可能是Check t自己打印的类型是错误类型的，但这又是系统中的一个错误，我从未见过它发生过（只要符号不妨碍印刷的可逆性）。

但是，有几件事与您的要求相近，您可能会感兴趣。

宇宙

在 Coq 中，我们可以写

Universe i.
Check Type@{i}.

然而，虽然i是一个有效的全域，但Check i失败了，并且i没有类型，就像 Gallina 术语有类型一样。

请注意，在 Agda 中，我们可以写

postulate foo : (i : Level) → Set i

Agda 检查器接受这一点，但如果我们写

bar = (i : Level) → Set i

我们收到错误消息Setω is not a valid type。Coq 没有这个问题，因为 Universe 在 Coq 中不是术语，而 Coq 中的 Universe 多态性是 prenex。

主题减少的损失

Coq 有一些极端情况（可能也称为错误），其中主题减少丢失。也就是说，当您减少它们时，有一些类型良好的术语会变成错误类型。参见例如bug #6768，它给出了代码

CoInductive I := C : I -> I.
CoFixpoint infty := C infty.
Definition unfold : infty = C infty :=
  match infty as x return match x with C n => x = C n end with
  | C n => eq_refl (C n)
  end.
Fail Definition nf_unfold : infty = C infty := Eval lazy in unfold.

请注意，即使没有类型注释，我们也会得到这样的错误，例如使用

Axiom id : forall {T}, T -> T.
Definition nf_unfold := Eval lazy in id unfold.
(*Error: Illegal application:
The term "@id" of type "forall T : Type, T -> T"
cannot be applied to the terms
 "(cofix infty : I := C infty) = C (cofix infty : I := C infty)" : "Prop"
 "eq_refl"
   : "C (cofix infty : I := C infty) = C (cofix infty : I := C infty)"
The 2nd term has type
 "C (cofix infty : I := C infty) = C (cofix infty : I := C infty)"
which should be coercible to
 "(cofix infty : I := C infty) = C (cofix infty : I := C infty)".
*)

这不完全是您要问的，但似乎相关。

自引用类型

所有术语都有类型，但并非所有术语都具有您想要的类型。例如，给定A : Typeand B : A -> Type，您可能想写下具有类型的术语f的类型

forall b : bool, if b then A else B (f true)

当然，这不被 Coq 接受，但我们可以定义具有这种类型的术语。例如，给定A、B和x : @sigT A B，Coq 接受

Definition f := fun b : bool => if b return if b then _ else _
                                then projT1 x else projT2 x.
Check f : forall b : bool, if b then A else B (f true).

不能陈述的定理的证明

早在 Coq 有明确的全域变量之前，我想证明函数外延性是向下封闭的。也就是说，我想证明这个定理

Set Universe Polymorphism.
Definition funext_at@{i} := forall (A B : Type@{i}) (f g : A -> B),
    (forall x, f x = g x) -> f = g.
Universes i j.
Constraint j <= i.
Theorem funext_downward_closed : funext_at@{i} -> funext_at@{j}.

然而，没有办法陈述这个定理。我只能写

Theorem funext_downward_closed : funext -> funext.

不过，我仍然设法证明了这个定理（参见HoTT/HoTT库中的这个提交和这个提交以及这个问题），但是，通过写下证明项，然后检查这个定理，看看宇宙约束是否正确。我开玩笑说我已经证明了一个不可言说的定理。

推荐阅读