坚持异构的证明

Question

我有一个二进制数表示形式，以及往返于Nat的一些转换：

open import Data.Nat
open import Data.Nat.Properties
open import Function
open import Relation.Binary.PropositionalEquality hiding (trans; cong; subst; sym)
open import Relation.Binary.HeterogeneousEquality
open import Data.Unit
open import Algebra
module CS = CommutativeSemiring commutativeSemiring 

data Bin : ? ? Set where
  zero  : Bin zero
  2*n   : ? {n} ? Bin n ? Bin (n + n)
  2*n+1 : ? {n} ? Bin n ? Bin (suc (n + n))

suc-lem : ? n ? suc (suc (n + n)) ? suc n + suc n
suc-lem zero = refl
suc-lem (suc n) rewrite 
    CS.+-comm n (suc n)
  | suc-lem n | CS.+-comm n (suc (suc n)) 
  | CS.+-comm n (suc n) = refl

inc : ? {n} ? Bin n ? Bin (suc n)
inc zero = 2*n+1 zero
inc (2*n b) = 2*n+1 b
inc (2*n+1 {n} b) rewrite suc-lem n = 2*n (inc b)

nat2bin : (n : ?) ? Bin n
nat2bin zero = zero
nat2bin (suc n) = inc (nat2bin n)

bin2nat : ? {n} ? Bin n ? ?
bin2nat {n} b = n

我想在这里证明事物需要异构的相等性，因为通常不明显两个Bin-s的Nat索引相等。不过，我对Agda缺乏经验，所以请告诉我这种方法是否被误导了。

我坚持以下几点：

lem : ? n ? 2*n+1 (inc (nat2bin n)) ? inc (inc (2*n+1 (nat2bin n)))
lem zero = refl
lem (suc n) = 
  subst
    (? b ? 2*n+1 (inc (inc (nat2bin n))) ? inc (inc b))
    (sym $ lem ?) ? 

显而易见的事情是插入n电源sym $ lem ?，但是这样会导致报错suc (n + n) != n + suc n。

我想知道为什么会发生这种情况或如何提供帮助。

Answer 1

进口：

open import Level hiding (zero; suc)
open import Function
open import Relation.Binary.HeterogeneousEquality
  renaming (sym to hsym; trans to htrans; cong to hcong; subst to hsubst)
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Fin hiding (_+_)
open import Algebra
open import Data.Nat.Properties
module ?plus = CommutativeSemiring commutativeSemiring

我重新整理inc了一下，以简化操作：

inc : ? {n} ? Bin n ? Bin (suc n)
inc zero = 2*n+1 zero
inc (2*n b) = 2*n+1 b
inc (2*n+1 {n} b) = subst (Bin ? suc) (?plus.+-comm n (suc n)) (2*n (inc b))

引理：

lem : ? n ? 2*n+1 (inc (nat2bin n)) ? inc (inc (2*n+1 (nat2bin n)))
lem zero = refl
lem (suc n) = {!!}

孔的类型是

2*n+1 (inc (inc (nat2bin n))) ?
      inc
      (subst ((? {.x} ? Bin) ? suc) (?plus.+-comm (suc n) (suc (suc n)))
       (2*n (inc (inc (nat2bin n)))))

因此，我们需要从standart库中将类似subst-removable的东西：

?-subst-removable : ? {a p} {A : Set a}
                    (P : A ? Set p) {x y} (eq : x ? y) z ?
                    P.subst P eq z ? z
?-subst-removable P refl z = refl

的类型

hsym $
  ?-subst-removable
    (Bin ? suc)
    (?plus.+-comm (suc n) (suc (suc n)))
    (2*n $ inc $ inc $ nat2bin n)

是

(2*n $ inc $ inc $ nat2bin n) ?
      subst ((? {.x} ? Bin) ? suc) (?plus.+-comm (suc n) (suc (suc n)))
      (2*n $ inc $ inc $ nat2bin n)

几乎我们需要的。现在我们要添加hcong inc，但是编译器拒绝它。这是实现cong：

cong : ? {a b} {A : Set a} {B : A ? Set b} {x y}
       (f : (x : A) ? B x) ? x ? y ? f x ? f y
cong f refl = refl

因此，x并且y必须是同一类型A，而我们subst更改类型。这是hcong我们需要的实现：

hcong' : {? ? ? : Level} {I : Set ?} {i j : I}
       -> (A : I -> Set ?) {B : {k : I} -> A k -> Set ?} {x : A i} {y : A j}
       -> i ? j
       -> (f : {k : I} -> (x : A k) -> B x)
       -> x ? y
       -> f x ? f y
hcong' _ refl _ refl = refl

最后的证明：

lem : ? n ? 2*n+1 (inc (nat2bin n)) ? inc (inc (2*n+1 (nat2bin n)))
lem zero = refl
lem (suc n) =
  hcong'
    (Bin ? suc)
    (?plus.+-comm (suc n) (suc (suc n)))
    inc
    $ hsym
      $ ?-subst-removable
          (Bin ? suc)
          (?plus.+-comm (suc n) (suc (suc n)))
          (2*n $ inc $ inc $ nat2bin n)

此外，我们可以合并subst-removable和cong：

?-cong-subst-removable : {? ? ? : Level} {I : Set ?} {i j : I}
                       -> (A : I -> Set ?) {B : {k : I} -> A k -> Set ?}
                       -> (e : i ? j)
                       -> (x : A i)
                       -> (f : {k : I} -> (x : A k) -> B x)
                       -> f (subst A e x) ? f x
?-cong-subst-removable _ refl _ _ = refl

lem' : ? n ? 2*n+1 (inc (nat2bin n)) ? inc (inc (2*n+1 (nat2bin n)))
lem' zero = refl
lem' (suc n) = hsym $
  ?-cong-subst-removable
    (Bin ? suc)
    (?plus.+-comm (suc n) (suc (suc n)))
    (2*n $ inc $ inc $ nat2bin n)
    inc

顺便说一句，我想Pierce就是这个数据类型：

data Bin : Set where
  zero  : Bin
  2*n   : Bin ? Bin
  2*n+1 : Bin ? Bin

顺便说一句，无需额外定义就可以证明您的人为示例：

contrived-example : {n : ?} {f : Fin (n + suc n)}
                  -> f ? from? (n + suc n)
                  -> f ? from? (suc n + n)
contrived-example {n} eq = htrans eq $ hcong from? $ ?-to-? $ ?plus.+-comm n (suc n)

BTW3，hsubst-ix1可以减少很多，因为您使用异构相等，并且不需要证明类型相等：

hsubst' : {C1 C2 : Set} {x : C1} {y : C2}
        -> (P : {C : Set} -> C -> Set)
        -> x ? y
        -> P x
        -> P y
hsubst' _ refl x = x

contrived-example' : 
  ? n
  ? (f : Fin (n + suc n)) 
  ? (from? (n + suc n) ? from? (suc n + n))
  ? (f ? from? (n + suc n))
  ? (f ? from? (suc n + n)) 
contrived-example' n f eq p = hsubst' (? f' ? f ? f') eq p