依赖记录类型的平等

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} returns val。下面的函数 incR 定义了一个 Rec 转换器，它将值和增量器递增一个固定值 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

很抱歉自己回答，但我破解了它。我不知道这是否是最优雅的方式，但我得到了依赖同余的想法，将正常和异质平等混合在一起：

Rec-cong : {x y : Rec}
    -> (val x ≡ val y)
    -> ((λ {n} -> inc x {n}) ≡ (λ{n} -> inc y {n}))
    -> (succ x ≅ succ y)
    -> x ≡ y
Rec-cong {x} {y}  prf1 prf2 prf3 with prf1 | prf2 | prf3
Rec-cong {x} {.x} prf1 prf2 prf3      refl | refl | refl = refl

incR0 : forall {x : Rec} -> incR x 0 ≡ x
incR0 {x} = Rec-cong {incR x 0} {x} (incRVal {x}) (incRinc {x}) (incRsucc {x})

我欢迎更好的解决方案！

Answer 2

一般来说，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}))
  ?

剩下的洞有一个相当讨厌的类型，但我们基本上可以忽略它，因为ℕ的等式证明是命题，i。 e.相同值之间的所有相等性证明都是相等的。也就是说，ℕ是一个集合：

ℕ-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；事实上，多查德的解决方案仅适用于启用公理 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 _ _)

依赖记录类型的平等

Equality on dependent record types

agda

dependent-type