Equality on dependent record types

Question

I've been bashing my head against this problem for a while: I have record types, with dependent fields, and I want to prove equalities on record transformations. I've tried to distill the crux of my problem into a small example. Consider the following record type Rec, which has dependency between the fields:

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

The succ property states a relationship between the other two fields: that inc {0} returns val. The following function incR defines a Rec transformer that increments the value and the incrementor by a fixed value m, which preserves their interaction:

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

Here succPrf gives the proof that the inc/val relationship holds.

Now, I want to prove the following:

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

This turns out to be quite difficult however because of the dependency within the records.

I tried breaking it down into individual equalities on the fields, with the aim of using a congruence to put it back together: and it seems I can get fairly far:

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

And on the succ field, we have to resort to heterogenous equality

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

But I'm struggling to combine these together adequately. I really need some kind of congruence for Pi-types so that I can plug incRinc and incRsucc together in one go, but I've failed to build this. I'm at the point where I can't see the wood for the trees, so though I would see what SO thought. Am I missing some easy technique here?

Answer 1

Generally, equality of sigmas is equivalent to a sigma of equalities:

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

We can specialize and adapt the introduction rule to Rec, and also curry it and only substitute with the actual dependencies (I made the definitions a bit more explicit and compressed, because my hole types were cleaner this way):

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 

We can use Rec-≡-intro to prove equalities on Rec:

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

The remaining hole has a pretty nasty type, but we can basically ignore it, because equality proofs of ℕ are propositional, i. e. all equality proofs between the same values are equal. In other words, ℕ is a 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 _ _)

I believe that all proofs here must eventually make use of some statement equivalent to ℕ-set (or axiom K; indeed, dorchard's solution only works with axiom K enabled), because if we try to prove the hole obligation generally, without reference to ℕ, then we'll need a lemma that is unprovable in intensional Martin-Löf type theory:

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

It seems unprovable to me in MLTT because we can find counterexamples in HoTT.

If we assume axiom K, we have proof irrelevance, which can be used here:

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

But this is a bit silly, since now we might as well just fill in our original hole:

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