Cubical Agda：我如何证明两件事不相等

Question

如何在 Cubical Agda 中证明两件事不相等？（v2.6.1，Cubical 回购版本acabbd9）

\n\n

具体来说，以下是作为更高归纳类型的整数：

\n\n

{-# OPTIONS --safe --warning=error --cubical --without-K #-}\n\nopen import Cubical.Core.Everything\nopen import Cubical.Foundations.Prelude\n\nmodule Integers where\n\ndata False : Set where\n\ndata \xe2\x84\x95 : Set where\n  zero : \xe2\x84\x95\n  succ : \xe2\x84\x95 \xe2\x86\x92 \xe2\x84\x95\n\n{-# BUILTIN NATURAL \xe2\x84\x95 #-}\n\ndata \xe2\x84\xa4 : Set where\n  pos : \xe2\x84\x95 \xe2\x86\x92 \xe2\x84\xa4\n  neg : \xe2\x84\x95 \xe2\x86\x92 \xe2\x84\xa4\n  congZero : pos 0 \xe2\x89\xa1 neg 0\n

\n\n

很容易表现出一些相当奇怪的等式，因为这里的“等式”实际上意味着一些与我们在非立方世界中习惯的东西不太一样的东西：

\n\n

oddThing2 : pos 0 \xe2\x89\xa1 congZero i1\noddThing2 = congZero\n

\n\n

我在https://github.com/Saizan/cubical-demo/blob/b112c292ded61b02fa32a1b65cac77314a1e9698/examples/Cubical/Examples/CTT/Data/Nat.agda发现了一个相当令人讨厌的证明，证明后继者非零：

\n\n

succNonzero : {a : \xe2\x84\x95} \xe2\x86\x92 succ a \xe2\x89\xa1 0 \xe2\x86\x92 False\nsuccNonzero {a} s = subst t s 0\n  where\n    t : \xe2\x84\x95 \xe2\x86\x92 Set\n    t zero = False\n    t (succ i) = \xe2\x84\x95\n

\n\n

有更好的证明吗？我无法succ a \xe2\x89\xa1 0再对证明进行模式匹配；在非立方 Agda 中，证明就是简单地oneNotZero ()识别不可能的模式。

\n\n

那么我如何证明以下内容（这是真的吗？）

\n\n

posInjective : {a b : \xe2\x84\xa4} \xe2\x86\x92 pos a \xe2\x89\xa1 pos b \xe2\x86\x92 a \xe2\x89\xa1 b\n

\n\n

可能很明显，我对 Cubical 完全是新手；但我过去曾大量使用过 Agda。

\n

Answer 1

因为posInjective你实际上可以做一个更简单的证明，

\n\n

fromPos : \xe2\x84\xa4 \xe2\x86\x92 \xe2\x84\x95\nfromPos (pos n) = n\nfromPos (neg _) = 0\nfromPos (congZero i) = refl\n

\n\n

然后posInjective = cong fromPos。

\n\n

更一般地，我们应该进行所谓的编码/解码证明（也称为无混淆证明），其中通过递归显式定义数据类型上的关系，然后证明它相当于路径相等。

\n\n

例如，这里有一个这样的证据List

\n\n

https://github.com/agda/cubical/blob/master/Cubical/Data/List/Properties.agda#L37

\n\n

从 的定义可以很容易地得出内射性和独特性Cover。

\n\n

这种证明的可能性实际上证明了 Agda 强大的归纳族模式匹配的可靠性。然而，HIT 构造函数通常既不是不同的也不是单射的，因此 Agda 是保守的，根本不将这些属性用于 HIT。

\n