Mus*_*ssy 4 equality record agda
似乎为了证明记录类型的两个项目是等效的，我需要编写一个助手来获取组件明智的证明并应用它们。\n示例：
\n\npostulate P : \xe2\x84\x95 \xe2\x86\x92 Set\n\nrecord Silly : Set (\xe2\x84\x93suc \xe2\x84\x93\xe2\x82\x80) where\n constructor _#_#_\n field\n n : \xe2\x84\x95\n pn : P n\n f : Set \xe2\x86\x92 \xe2\x84\x95\n\nopen Silly\n\nSillyEq : \xe2\x88\x80 s t \xe2\x86\x92 n s \xe2\x89\xa1 n t \xe2\x86\x92 pn s \xe2\x89\x85 pn t \xe2\x86\x92 f s \xe2\x89\xa1 f t \xe2\x86\x92 s \xe2\x89\xa1 t\nSillyEq (n # pn # f) (.n # .pn # .f) \xe2\x89\xa1-refl \xe2\x89\x85-refl \xe2\x89\xa1-refl = \xe2\x89\xa1-refl\n我感到SillyEq应该以某种方式提供给我，我不需要自己写它——或者我错了。
另外，我无法证明SillyEq另外，如果不声明构造函数然后对其进行模式匹配，
感谢你的协助！
\n拥有
\n\nSillyEq\' : \xe2\x88\x80 {n\xe2\x82\x81 n\xe2\x82\x82 pn\xe2\x82\x81 pn\xe2\x82\x82 f\xe2\x82\x81 f\xe2\x82\x82}\n \xe2\x86\x92 n\xe2\x82\x81 \xe2\x89\xa1 n\xe2\x82\x82 \xe2\x86\x92 pn\xe2\x82\x81 \xe2\x89\x85 pn\xe2\x82\x82 \xe2\x86\x92 f\xe2\x82\x81 \xe2\x89\xa1 f\xe2\x82\x82 \xe2\x86\x92 (n\xe2\x82\x81 # pn\xe2\x82\x81 # f\xe2\x82\x81) \xe2\x89\xa1 (n\xe2\x82\x82 # pn\xe2\x82\x82 # f\xe2\x82\x82)\n你可以证明SillyEq证明
SillyEq : \xe2\x88\x80 s t \xe2\x86\x92 n s \xe2\x89\xa1 n t \xe2\x86\x92 pn s \xe2\x89\x85 pn t \xe2\x86\x92 f s \xe2\x89\xa1 f t \xe2\x86\x92 s \xe2\x89\xa1 t\nSillyEq _ _ = SillyEq\'\n由于 的 \xce\xb7 规则Silly。因此，如果您有 的 arity-generic 版本cong，那么您可以证明SillyEq为（请注意各处的异构相等性）
SillyEq : \xe2\x88\x80 s t \xe2\x86\x92 n s \xe2\x89\x85 n t \xe2\x86\x92 pn s \xe2\x89\x85 pn t \xe2\x86\x92 f s \xe2\x89\x85 f t \xe2\x86\x92 s \xe2\x89\x85 t\nSillyEq _ _ = gcong 3 _#_#_\n我不知道是否gcong可以通过反射轻松表达，但我想它可以使用通常的数量通用编程东西来编写（就像这里），但解决方案不会很短。
这是一个临时证明：
\n\ncong\xe2\x82\x83 : \xe2\x88\x80 {\xce\xb1 \xce\xb2 \xce\xb3 \xce\xb4} {A : Set \xce\xb1} {B : A -> Set \xce\xb2} {C : \xe2\x88\x80 {x} -> B x -> Set \xce\xb3}\n {D : \xe2\x88\x80 {x} {y : B x} -> C y -> Set \xce\xb4} {x y v w s t}\n -> (f : \xe2\x88\x80 x -> (y : B x) -> (z : C y) -> D z)\n -> x \xe2\x89\x85 y -> v \xe2\x89\x85 w -> s \xe2\x89\x85 t -> f x v s \xe2\x89\x85 f y w t\ncong\xe2\x82\x83 f refl refl refl = refl\n\nSillyEq : \xe2\x88\x80 s t \xe2\x86\x92 n s \xe2\x89\x85 n t \xe2\x86\x92 pn s \xe2\x89\x85 pn t \xe2\x86\x92 f s \xe2\x89\x85 f t \xe2\x86\x92 s \xe2\x89\x85 t\nSillyEq _ _ = cong\xe2\x82\x83 _#_#_\n然而，像你的例子一样，命题和异构等式的混合使一切变得复杂。
\n