types - 判断平等

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 的声明被定义为 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