agda - 立方 Agda : how do I prove two things not equal

Question

如何证明 Cubical Agda 中的两件事不相等？ (v2.6.1, Cubical repo 版本 acabbd9 )

具体来说，这里是作为更高归纳类型的整数:

{-# OPTIONS --safe --warning=error --cubical --without-K #-}

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude

module Integers where

data False : Set where

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

data ℤ : Set where
  pos : ℕ → ℤ
  neg : ℕ → ℤ
  congZero : pos 0 ≡ neg 0

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

oddThing2 : pos 0 ≡ congZero i1
oddThing2 = congZero

我在 https://github.com/Saizan/cubical-demo/blob/b112c292ded61b02fa32a1b65cac77314a1e9698/examples/Cubical/Examples/CTT/Data/Nat.agda 找到了一个相当难看的证明，证明后继者非零。 :

succNonzero : {a : ℕ} → succ a ≡ 0 → False
succNonzero {a} s = subst t s 0
  where
    t : ℕ → Set
    t zero = False
    t (succ i) = ℕ

有更好的证明吗？我无法对 succ a ≡ 0 的证明进行模式匹配没有了；在非立方 Agda 中，证明只是 oneNotZero () ，识别不可能的模式。

那么我如何证明以下内容(它甚至是真的吗？)

posInjective : {a b : ℤ} → pos a ≡ pos b → a ≡ b

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

Answer 1

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

fromPos : ℤ → ℕ
fromPos (pos n) = n
fromPos (neg _) = 0
fromPos (congZero i) = refl

然后 posInjective = cong fromPos .

更一般地，人们应该进行所谓的编码/解码证明(也称为 NoConfusion 证明)，其中通过递归明确定义数据类型的关系，然后证明它等效于路径相等。

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

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

从 Cover 的定义很容易得出单射性和独特性.

这种证明的可能性其实就是Agda强大的归纳族模式匹配的合理性的证明。然而，HIT 的构造函数通常既不是独特的也不是单射的，因此 Agda 是保守的，根本不使用这些属性来进行 HIT。