従属レコードタイプの等価性

Question

私はこの問題に対してしばらくの間頭を打っていました。従属フィールドを持つレコードタイプがあり、レコード変換の等価性を証明したいと思います。私は私の問題の要点を小さな例にしてみようとしました。

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財産状態、他の2つのフィールド間の関係：そのinc {0}戻りvalフィールド間の依存関係を持って、次のレコード型Recを、考えてみましょう。次の関数incRは、それらの相互作用を保持固定値mによって値とインクリメンタをインクリメントRecトランス定義：ここ

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} } 

をsuccPrfinc/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 

しかし、私はこれらを十分に組み合わせることに苦労しています。私は実際には、incRincとincRsuccを一度につなげることができるように、Piタイプのためにいくつかの合同が必要ですが、これを構築することに失敗しました。私は木の木が見えないほどのところにいるので、私はそれが何を考えているのか分かりました。私はここで簡単な技術が欠けていますか？

Answer 1

は一般的に、シグマの平等は、等式のシグマに相当します。

Σ-≡-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上の等式を証明するためにRec-≡-introを使用することができます。

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

残りの穴はかなり厄介なタイプがありますが、ℕの平等プルーフは、私命題であるため、我々は基本的には、それを無視することができます。 e。同じ値の間のすべての等価プルーフは等しい。 （;確かに、dorchardのソリューションは、唯一の公理Kを有効にして動作しますか公理K）ので、私はここにすべての証拠は、最終的にℕ-setに同等のいくつかのステートメントの使用をしなければならないと信じてい

ℕ-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 _ _) 

：他の言葉では、ℕはセットです我々はℕを参照することなく、一般的に穴の義務を証明しようとした場合、その後、我々は内包マーティン・LOFの型理論でunprovableある補題必要があります：

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に私にunprovable思えます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 _ _) 

Answer 2

自己回答の申し訳ありませんが、私はそれをクラックしました。これが最もエレガントな方法であれば、私は知らないが、私は仕事に依存合同の私の考えを持って、一緒に通常の異種平等を混合：

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

私はよりよい解決策を歓迎します！