判断平等

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 zeroand之间的排序关系逐案工作value p，我已经简化为我有一个证明p == zero和证明的情况Prime p以及陈述Prime zero被定义为 False。

现在，当然，这些陈述是矛盾的：因为我有证据表明p == zero，我可以展示 类型的居民Prime p == Prime zero，因此我有 的居民Prime p == False。

但是我怎样才能把我的元素proof : Prime p（证明是 的第二个组成部分p : Sg nat Prime）并将它“投射”到 的元素False？类型在命题上相等，但在判断上不相等。

Answer 1

事实证明这很容易；就去做吧（tm）。

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