依赖记录类型的相等性

Question

一段时间以来，我一直在抨击这个问题：我有记录类型，有依赖字段，我想证明记录转换的相等性。我试图将问题的症结提炼成一个小例子。考虑以下记录类型Rec，它在字段之间具有依赖性：

module Bar where
open import Data.Nat
open import Relation.Binary.PropositionalEquality as PE
open import Relation.Binary.HeterogeneousEquality as HE

record Rec : Set where
  field val : ?
        inc : {n : ?} -> ?
        succ : inc {0} ? val

open Rec

该succ属性声明了其他两个字段之间的关系：即inc {0}返回val。以下函数incR定义了一个Rec转换器，该转换器将 value 和 incrementor 增加一个固定值m，这保留了它们的交互：

succPrf : {x : Rec} {m : ?} -> (inc x {0} + m) ? val x + m
succPrf {x} {m} rewrite (PE.cong (\x -> x + m) (succ x)) = refl

incR : Rec -> ? -> Rec
incR x m = record {
            val = val x + m
          ; inc = ?{n} -> inc x {n} + m
          ; succ = succPrf {x} {m} }

这里succPrf给出了inc/val关系成立的证明。

现在，我想证明以下几点：

incR0 : forall {x : Rec} -> incR x 0 ? x
incR0 {x} = {!!}

然而，由于记录内的依赖性，这变得相当困难。

我尝试将其分解为各个领域的个人平等，目的是使用一致将其重新组合在一起：似乎我可以走得很远：

postulate
  ext : {A : Set} {B : Set}
        {f g : {a : A} -> B} -> 
        (forall {n : A} -> f {n} ? g {n})
     -> (? {n : A} -> f {n}) ? (? {n : A} -> g {n})

  -- Trivial, but for tersity just postulated
  runit : {n : ?} -> n + 0 ? n

incRVal : forall {x : Rec} -> val (incR x 0) ? val x
incRVal {x} rewrite runit {val x} = refl

incRinc : forall {x : Rec} -> (?{n : ?} -> inc (incR x 0) {n}) ? (?{n : ?} -> inc x {n})
incRinc {x} rewrite ext (?{n : ?} -> runit {inc x {n}}) = refl

而在succ球场上，我们不得不诉诸异质平等

succIncR : {x : Rec} -> (inc (incR x 0) {0} ? val (incR x 0) + 0) 
               ? (inc x {0} ? val x)
succIncR {x} rewrite runit {inc x {0}} | runit {val x} | incRVal {x}     
  = refl

incRsucc : forall {x : Rec} -> succ (incR x 0) ? succ x
incRsucc {x} rewrite succIncR {x} | succ x | runit {val x}
  = HE.reflexive refl

但我正在努力将这些充分结合在一起。我真的需要 Pi 类型的某种一致性，以便我可以一次性插入incRinc并incRsucc组合在一起，但我未能构建它。我正处于看不到树木的森林的地步，所以尽管我会看到 SO 的想法。我在这里错过了一些简单的技术吗？

Answer 1

通常，sigma 等式等价于等式的 sigma：

?-?-intro :
  ? {? ?}{A : Set ?}{B : A ? Set ?}{a a' : A}{b : B a}{b' : B a'}
  ? (? (a ? a') ? p ? subst B p b ? b') ? (a , b) ? (a' , b')
?-?-intro (refl , refl) = refl

?-?-elim :
  ? {? ?}{A : Set ?}{B : A ? Set ?}{a a' : A}{b : B a}{b' : B a'}
  ? (a , b) ? (a' , b') ? ? (a ? a') ? p ? subst B p b ? b'
?-?-elim refl = refl , refl

我们可以将引入规则专门化和调整为Rec，也可以将其咖喱化并仅替换为实际的依赖项（我使定义更加明确和压缩，因为我的孔类型以这种方式更清晰）：

open import Data.Nat
open import Relation.Binary.PropositionalEquality

record Rec : Set where
  constructor rec
  field val : ?
        inc : ? -> ?
        succ : inc 0 ? val
open Rec

incR : Rec -> ? -> Rec
incR x m = rec (val x + m) (? n ? inc x n + m) (cong (_+ m) (succ x))

Rec-?-intro :
  ? {v v' : ?} {i i' : ? ? ?}{s : i 0 ? v}{s' : i' 0 ? v'}(p : v ? v')(q : i ? i')
  ? subst? (? v i ? i 0 ? v) p q s ? s'
  ? rec v i s ? rec v' i' s'
Rec-?-intro refl refl refl = refl

postulate
  ext : ? {? ?} ? Extensionality ? ? -- comes from PropositionalEquality
  runit : {n : ?} -> n + 0 ? n 

我们可以Rec-?-intro用来证明 上的等式Rec：

incR0 : ? x -> incR x 0 ? x
incR0 x = Rec-?-intro
  (runit {val x})
  (ext (? n ? runit {inc x n}))
  ?

剩下的洞有一个非常讨厌的类型，但我们基本上可以忽略它，因为 的等式证明?是命题的，即相同值之间的所有等式证明都是相等的。换句话说，?是一个集合：

?-set : {n m : ?}(p p' : n ? m) ? p ? p'
?-set refl refl = refl

incR0 : ? x -> incR x 0 ? x
incR0 x = Rec-?-intro
  (runit {val x})
  (ext (? n ? runit {inc x n}))
  (?-set _ _)

我相信这里的所有证明最终都必须使用一些等价于?-set（或公理 K；事实上，dochard 的解决方案仅适用于公理 K 启用），因为如果我们尝试一般地证明空洞义务，而不参考?，那么我们'需要一个在内涵 Martin-Löf 类型理论中无法证明的引理：

lem :
  ? {A : Set}{z : A}{f i : A ? A}(q? : f (i z) ? (i z))(q? : (? x ? f (i x)) ? i)
  ? subst? (? v i ? i z ? v) q? q? refl ? refl
lem q? q? = {!!}

在 MLTT 中对我来说似乎无法证明，因为我们可以在 HoTT 中找到反例。

如果我们假设公理 K，我们有证明无关性，可以在这里使用：

proof-irrelevance : ? {a} {A : Set a} {x y : A} (p q : x ? y) ? p ? q
proof-irrelevance refl refl = refl

lem :
  ? {A : Set}{z : A}{f i : A ? A}(q? : f (i z) ? (i z))(q? : (? x ? f (i x)) ? i)
  ? subst? (? v i ? i z ? v) q? q? refl ? refl
lem q? q? = proof-irrelevance _ _

但这有点傻，因为现在我们不妨填补我们原来的漏洞：

incR0 : ? x -> incR x 0 ? x
incR0 x = Rec-?-intro
  (runit {val x})
  (ext (? n ? runit {inc x n}))
  (proof-irrelevance _ _)