Gleichheit auf abhängigen Datensatztypen

Question

Ich habe meinen Kopf für eine Weile gegen dieses Problem gestoßen: Ich habe Datensatztypen, mit abhängigen Feldern, und ich möchte Gleichheiten bei Datensatztransformationen beweisen. Ich habe versucht, den Kern meines Problems in ein kleines Beispiel zu zerlegen. Betrachten Sie den folgenden Satztyp Rec, die Abhängigkeit zwischen den Feldern hat:

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 

Die succ Eigenschaft Staaten eine Beziehung zwischen den beiden anderen Bereichen: dass inc {0} kehrt val. Die folgende Funktion definiert einen incRRec Transformator, der den Wert und die Inkrementierer um einen festen Wert erhöht m, die ihre Wechselwirkung bewahrt:

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 Hier gibt den Beweis, daß die inc/val Beziehung hält.

Nun möchte ich folgendes beweisen:

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

Das macht ziemlich schwierig, aber sein, weil der Abhängigkeit innerhalb der Datensätze.

versuchte ich es in einzelne Gleichheiten auf den Feldern zu brechen, mit dem Ziel, eine Kongruenz mit ihm zusammen zu setzen: und es scheint, kann ich ziemlich weit kommen:

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 

Und auf der succ Feld wir müssen zu heterogener Gleichheit greifen

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 

Aber ich bemühe mich, diese zusammen angemessen zu kombinieren. Ich brauche wirklich eine Art von Kongruenz für Pi-Typen, so dass ich incRinc und incRsucc zusammen auf einmal verbinden kann, aber ich habe es versäumt, dies zu bauen. Ich bin an dem Punkt, wo ich den Wald für die Bäume nicht sehen kann, obwohl ich sehen würde, was SO dachte. Fehle mir hier eine leichte Technik?

Answer 1

allgemeine Gleichheit von Sigmas zu einem Sigma von Gleichheiten entsprechen:

Σ-≡-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 

Wir können die Einführung der Regel auf Rec spezialisieren und anzupassen, und es auch Curry und nur mit den tatsächlichen Abhängigkeiten ersetzen (ich habe die Definitionen etwas deutlicher und komprimiert, weil mein Loch Typen auf diese Weise sauberer waren):

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 

Wir Rec-≡-intro verwenden können, um Gleichheiten auf Rec zu beweisen:

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

Das verbleibende Loch hat einen ziemlich fiesen Typ, aber wir können es im Grunde ignorieren, weil Gleichheitsbeweise von ℕ propositional sind, ich. e.Alle Gleichheitsbeweise zwischen den gleichen Werten sind gleich. Mit anderen Worten, ist ℕ ein Satz:

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

Ich glaube, dass alle hier Beweise schließlich Verwendung einiger Aussage entspricht ℕ-set machen müssen (oder Axiom K, ja Lösung nur mit Axiom K aktiviert arbeitet, dorchard Jahre), weil wenn wir versuchen, im allgemeinen das Loch Verpflichtung zu beweisen, ohne Bezug auf ℕ, dann werden wir ein Lemma benötigen, die in intensionalen Martin-Löf Typentheorie nicht beweisbar ist:

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₂ = {!!} 

Es scheint mir nicht beweisbar in MLTT weil wir es können finde Gegenbeispiele in HoTT.

Wenn wir Axiom K annehmen, haben wir den Beweis Irrelevanz, die hier verwendet werden können:

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

Aber das ist ein bisschen dumm, denn jetzt können wir auch nur in unserem ursprünglichen Loch füllen:

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

Answer 2

Entschuldigung für eine selbst Antwort, aber ich habe es geknackt. Ich weiß nicht, ob dies die eleganteste Art und Weise ist, aber ich habe meine Vorstellung von einer abhängigen Kongruenz zu arbeiten, zusammen, um die normale und heterogene Gleichheit Mischen:

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

Ich würde eine bessere Lösung begrüßen zu können!