在AGDA中为泛型归纳类型定义可确定的相等性

如何解决在AGDA中为泛型归纳类型定义可确定的相等性

下面，我有一些公式的普通归纳数据类型，并且想知道是否有任何方法可以简化此过程，以便在Agda内部对任何归纳定义的类型定义可确定的相等性（即，不使用某些编译指示或其他元编程功能）。 / p>

具体地说，有什么方法可以定义任何Arity的任何类型构造函数的*ConstrInherets*。然后在可确定的相等性定义中将其用于任何情况下的参数化（因为我们必须相对于构造函数的稀疏性在with上进行线性模式匹配），并消除所有no (λ ())不同类型的构造函数会产生噪音吗？

还有，当人们使用更有趣的归纳类型（参数化，索引，归纳递归等）时，这种情况是否会分解？

这似乎是一个定义的实例，在Ltac的帮助下可以很自然地在coq中进行定义，但是在Agda中却非常痛苦和丑陋，但是如果不是这种情况，我将不胜感激可以在其中阅读的参考文献对此有更多了解。

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)

open import Data.Nat using (ℕ ; zero; suc ; _+_; _≟_)
open import Data.Empty

-- type symbols
data tSymb : Set where
  base : ℕ → tSymb
  ~ : tSymb → tSymb
  _\\_ : tSymb → tSymb → tSymb
  _//_ : tSymb → tSymb → tSymb

baseConstrInherets¬ : {x y : ℕ} → ¬ x ≡ y → ¬ base x ≡ base y
baseConstrInherets¬ ¬xy refl = ¬xy refl

~ConstrInherets¬ : {x y : tSymb} → ¬ x ≡ y → ¬ ~ x ≡ ~ y
~ConstrInherets¬ ¬xy refl = ¬xy refl

\\ConstrInherets¬L : {x y z1 z2 : tSymb} → ¬ x ≡ y → ¬ x \\ z1 ≡ y \\ z2
\\ConstrInherets¬L ¬xy refl = ¬xy refl

//ConstrInherets¬L : {x y z1 z2 : tSymb} → ¬ x ≡ y → ¬ x // z1 ≡ y // z2
//ConstrInherets¬L ¬xy refl = ¬xy refl

\\ConstrInherets¬R : {x y z : tSymb} → ¬ x ≡ y → ¬ z \\ x ≡ z \\ y
\\ConstrInherets¬R ¬xy refl = ¬xy refl

//ConstrInherets¬R : {x y z : tSymb} → ¬ x ≡ y → ¬ z // x ≡ z // y
//ConstrInherets¬R ¬xy refl = ¬xy refl

eql-tSymb : Decidable {A = tSymb} _≡_
eql-tSymb (base x) (base y) with Data.Nat._≟_ x y
... | no ¬p = false because (ofⁿ (baseConstrInherets¬ ¬p))
... | yes refl = true because ofʸ refl
eql-tSymb (base x) (~ y) = no (λ ())
eql-tSymb (base x) (y \\ y₁) = no (λ ())
eql-tSymb (base x) (y // y₁) = no (λ ())
eql-tSymb (~ x) (base x₁) = no (λ ())
eql-tSymb (~ x) (~ y) with eql-tSymb x y
... | no ¬p = false because (ofⁿ (~ConstrInherets¬ ¬p))
... | yes refl = true because (ofʸ refl)
eql-tSymb (~ x) (y \\ y₁) = no (λ ())
eql-tSymb (~ x) (y // y₁) = no (λ ())
eql-tSymb (x \\ x₁) (base x₂) = no (λ ())
eql-tSymb (x \\ x₁) (~ y) = no (λ ())
eql-tSymb (x \\ x₁) (y \\ y₁) with eql-tSymb x y
... | no ¬p          = false because (ofⁿ (\\ConstrInherets¬L ¬p))
... | yes refl with eql-tSymb x₁ y₁
... | no ¬p = false because (ofⁿ (\\ConstrInherets¬R ¬p))
... | yes refl = true because ofʸ refl
eql-tSymb (x \\ x₁) (y // y₁) = no (λ ())
eql-tSymb (x // x₁) (base x₂) = no (λ ())
eql-tSymb (x // x₁) (~ y) = no (λ ())
eql-tSymb (x // x₁) (y \\ y₁) = no (λ ())
eql-tSymb (x // x₁) (y // y₁) with eql-tSymb x y
... | no ¬p          = false because (ofⁿ (//ConstrInherets¬L ¬p))
... | yes refl with eql-tSymb x₁ y₁
... | no ¬p = false because (ofⁿ (//ConstrInherets¬R ¬p))
... | yes refl = true because ofʸ refl

注意：这是How to define a subformula of an inductively defined type in Agda?

的后续问题