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應該以某種方式提供給我的，我不需要寫自己--or是我錯了。

此外，我不能證明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₃ _#_#_ 

然而，像你的情況命題和異構平等的混合複雜的一切。