Кубическая Агда: как мне доказать две вещи не равные - PullRequest
Новая
       81

Кубическая Агда: как мне доказать две вещи не равные

1 голос
/ 26 апреля 2020

Как я могу доказать, что две вещи не равны в Кубической Агде? (v2.6.1, версия кубического репо 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; в не кубической Агде доказательство будет просто oneNotZero (), идентифицирующее невозможный образец.

Тогда как я могу доказать следующее (это даже верно?) 

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

Это, вероятно, ясно, что я новичок в Cubical; но я использовал Агду нетривиальное количество в прошлом.

Ответы [ 2 ]

4 голосов
/ 27 апреля 2020

Для 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.

Возможность такого рода доказательств на самом деле является оправданием обоснованности Агды. эффективное сопоставление с образцом на индуктивных семействах Однако конструкторы HIT в целом не являются ни различными, ни инъективными, поэтому Agda консервативна и вообще не использует эти свойства для HIT.

1 голос
/ 26 апреля 2020

Ну, у меня очень странный ответ, которого я совсем не понимаю. 

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))
...