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

Question

如何在 Cubical Agda 中证明两个事物不相等？（v2.6.1，Cubical 回购版本 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

很容易显示一些相当奇怪的等式，因为 "equality" 这里实际上意味着一些与我们在非立方世界中习惯的东西不完全相同的东西：

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

好吧，我有一个很奇怪的答案，我根本不明白。

decr : ℤ → ℤ
decr (pos zero) = neg 1
decr (pos (succ x)) = pos x
decr (neg x) = neg (succ x)
decr (congZero i) = neg 1

-- "Given a proof that `pos (succ a) = pos (succ b)`, transport it back along `decr`."
posDecr : {a b : ℕ} → pos (succ a) ≡ pos (succ b) → pos a ≡ pos b
posDecr {a} {b} pr = cong decr pr

posInjective : {a b : ℕ} → pos a ≡ pos b → a ≡ b
posInjective {zero} {zero} x = refl
posInjective {zero} {succ b} x = subst t x (succ b)
  where
    t : ℤ → Set
    t (pos zero) = ℕ
    t (pos (succ x)) = zero ≡ succ b
    t (neg x) = ℕ
    t (congZero i) = ℕ
posInjective {succ a} {zero} x = subst t x (succ a)
  where
    t : ℤ → Set
    t (pos zero) = succ a ≡ zero
    t (pos (succ x)) = ℕ
    t (neg x) = succ a ≡ zero
    t (congZero i) = succ a ≡ zero
posInjective {succ a} {succ b} x = cong succ (posInjective (posDecr x))

Answer 2

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

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

然后 posInjective = cong fromPos。

更一般地说，应该做一个所谓的 encode/decode 证明（也称为 NoConfusion 证明），其中通过递归明确定义数据类型上的关系，然后证明它等同于路径相等性。

例如这里有一个关于 List

的证据

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

根据 Cover.

的定义很容易得出内射性和区别性

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

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

Cubical Agda: how do I prove two things not equal

agda

cubical-type-theory