agda – 依赖记录类型的平等

我一直在抨击这个问题一段时间：我有记录类型,有依赖字段,我想证明记录转换的平等性.我试图将我的问题的症结提炼成一个小例子.考虑以下记录类型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变换器,它将值和增量器递增一个固定值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的想法.我在这里错过了一些简单的技巧吗？

一般来说,西格玛的平等等同于平等的西格玛：

Σ-≡-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}))
  ?

剩下的洞有一个非常讨厌的类型,但我们基本上可以忽略它,因为equality的平等证明是命题,i.即相同值之间的所有相等证明都是相等的.换句话说,ℕ是一组：

ℕ-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的语句;实际上,dorchard的解决方案仅适用于启用公理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 _ _)