Agda 中的记录平等

Question

似乎为了证明一个记录类型的两个项目是等价的，我需要编写一个帮助程序来获取组件明智的证明并应用它们。 一个例子：

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

我觉得SillyEq 应该以某种方式提供给我，我不需要自己编写它——或者我弄错了。

此外，如果不声明构造函数并对其进行模式匹配，我无法证明 SillyEq。

感谢您的帮助！

Answer 1

拥有

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

你可以证明SillyEq为

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

由于Silly 的 η 规则。因此，如果你有一个cong 的通用版本，那么你可以证明SillyEq 为（注意到处都是异构相等）

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

我不知道gcong 是否可以通过反射轻松表达，但我想它可以使用通常的arity-generic 编程东西（如here）来编写，但解决方案不会很短。

这是一个临时证明：

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

但是，像您的情况一样，命题和异质等式的混合会使一切变得复杂。