CODEWITHSUNDEEP
recordequalityagda
Musa Al-hassy
Musa Al-hassy

Reputation: 982

Equality of records in Agda

It seems that to prove that two items of a record type are equivalent, I need to write a helper that takes component wise proofs and applies them. An example:

postulate P : ℕ → Set

record Silly : Set (ℓsuc ℓ₀) where
 constructor _#_#_
 field
  n : ℕ
  pn : P n
  f : Set → ℕ

open Silly

SillyEq : ∀ s t → n s ≡ n t → pn s ≅ pn t → f s ≡ f t → s ≡ t
SillyEq (n # pn # f) (.n # .pn # .f) ≡-refl ≅-refl ≡-refl = ≡-refl

I feel like SillyEq should somehow be available to me, that I do not need to write it myself --or am I mistaken.

Also, I could not prove SillyEq without declaring a constructor and then pattern matching on it.

Thanks for your assistance!

Upvotes: 4

Views: 506

Answers (1)

effectfully
effectfully

Reputation: 12715

Having

SillyEq' : ∀ {n₁ n₂ pn₁ pn₂ f₁ f₂}
         → n₁ ≡ n₂ → pn₁ ≅ pn₂ → f₁ ≡ f₂ → (n₁ # pn₁ # f₁) ≡ (n₂ # pn₂ # f₂)

you can prove SillyEq as

SillyEq : ∀ s t → n s ≡ n t → pn s ≅ pn t → f s ≡ f t → s ≡ t
SillyEq _ _ = SillyEq'

due to the η-rule for Silly. So if you have an arity-generic version of cong, then you can prove SillyEq as (note the heterogeneous equality everywhere)

SillyEq : ∀ s t → n s ≅ n t → pn s ≅ pn t → f s ≅ f t → s ≅ t
SillyEq _ _ = gcong 3 _#_#_

I don't know whether gcong can be easily expressed via reflection, but I guess it can be written using the usual arity-generic programming stuff (like here), but the solution won't be short.

Here is an ad hoc proof:

cong₃ : ∀ {α β γ δ} {A : Set α} {B : A -> Set β} {C : ∀ {x} -> B x -> Set γ}
          {D : ∀ {x} {y : B x} -> C y -> Set δ} {x y v w s t}
      -> (f : ∀ x -> (y : B x) -> (z : C y) -> D z)
      -> x ≅ y -> v ≅ w -> s ≅ t -> f x v s ≅ f y w t
cong₃ f refl refl refl = refl

SillyEq : ∀ s t → n s ≅ n t → pn s ≅ pn t → f s ≅ f t → s ≅ t
SillyEq _ _ = cong₃ _#_#_

However, a mix of propositional and heterogeneous equalities like in your case complicates everything.

Upvotes: 5

Related Questions