判断平等

Question

TL;DR:在Agda中，给定a : A和proof : A == B，我能获得一个元素a : B吗？

在我不断尝试学习Agda的过程中，我创建了以下Prime : nat -> Set数据类型，这是一个自然的原始性的见证。

Prime zero = False
Prime (succ zero) = False
Prime (succ (succ n)) = forall {i : nat} -> divides i p -> i <N p -> zero <N i -> i == (succ zero)
  where
    p = succ (succ n)

在此：

• False是一种没有构造函数的数据类型；
• divides a b是一种数据类型，它包含见证k的事实，即a * k = b；
• a <N b是一种数据类型，它包含见证k的事实，即a + k = b；
• ==是相等类型，只有一个构造函数refl；
• 自然数是用zero : nat和succ : nat -> nat以明显的方式定义的。

我成功地展示了Prime (succ (succ zero))的一个成员，并证明了Prime (succ (succ (succ (succ zero)))))语句暗示了False。

现在我试图证明素数比一个素数更大：

primesAreGreaterThanOne : (p : Sg nat Prime) -> (succ zero <N value p)

哪里

• Sg A pred是依赖对(p, pred(p))，其中p : A；
• value : Sg A pred -> A提取值并丢弃证明。

我已经证明了顺序的三分法:对于所有的a, b来说，无论是a <N b，还是a == b，还是b <N a，都是正确的。(我希望这个引理能帮助我们避免任何被排除在外的中间问题。)因此，通过研究succ zero和value p之间的排序关系，我简化为有p == zero的证明和Prime p的证明，以及Prime zero被定义为假的陈述。

当然，这些说法是矛盾的:因为我有p == zero的证据，所以我可以展示一个Prime p == Prime zero类型的居民，因此我有一个Prime p == False的居住者。

但是，我如何将元素proof : Prime p (p : Sg nat Prime的第二个组件的证明)“转换”到False的元素中呢？这些类型在命题上是相等的，但在判断上不是平等的。

Answer 1

我想就这个专题指出一些理论背景。

Agda的核心是Martin L f的逻辑框架(LF)，它是一种最小依赖类型的lambda演算，它给我们提供了依赖函数等。从总体上讲，Agda是基于内涵ML型理论的。

在LF中，有一个叫做类型转换规则的规则，它声明

 Γ ⊢ t : A     Γ ⊢ A = B
--------------------------
        Γ ⊢ t : B

这沿类型相等强制项。其中，由计算(beta)和扩展性(eta)确定的两种类型在定义上相等。

编辑澄清:在意旨中，判断平等和命题平等是分开的，命题平等不给你评判。如果您希望一条给出两个命题相等条件的规则在判断上也是平等的，那么您将处于扩展TT中，这通常是不可取的，因为它使类型检查无法判定。因此，在意向性TT中，这并不总是正确的。

Answer 2

这很容易，只需做(tm)就行了。

typeCast : {a : _} {A : Set a} {B : Set a} (el : A) (pr : A == B) -> B
typeCast {a} {A} {.A} elt refl = elt