types - Agdaで帰納的に定義された型の部分式を定義する方法は?

Question

式が単純な帰納的に定義された構文上の特定の形式の部分式であるかどうかを判断する単純な述語を定義しようとしています。おそらく単純な問題がいくつか発生しています。

(i) 与えられた型 A を持つパラメータ化されたモジュールを使用したい. A が決定可能な等値を持つという意味で、A がセットであるという情報をどのようにインポートできますか? これができない場合、いくつかの回避策はありますか? これが私が代わりにナットを持っている理由です。

(ii) t1 ≡ (t2 // t3)(および同様に定義された) 述語isSubFormulaは、等しい部分式を処理する適切な方法ですか? そうでない場合、他にどのように簡単にこれを行うことができますか? equalFmlaまた、 for の述語を作成してから、 with でグローバルな部分式の述語を作成することも検討しましisSubFormula ⊎ equalFmlaたが、これがそれほどきれいかどうかはわかりません。

(iii) 最初の行の内部でパターン マッチを行うと、最後の 3 行が青色で強調表示されるのはなぜですか? どうすればこれを修正できますか

(iv){!Data.Nat._≟_ n1 n2 !}以下の絞り込みを行わないのはなぜですか?

module categorial1 (A : Set) where

open import Data.Nat using (ℕ)
open import Data.Empty
open import Data.Sum
open import Relation.Binary.PropositionalEquality

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

-- A needs a decideable notion of equality
isSubFormula : tSymb → tSymb → Set
-- isSubFormula y (base x) = {!!}
isSubFormula (base n1) (base n2) = {!Data.Nat._≟_ n1 n2 !}
isSubFormula (~ t1) (base x) = ⊥
isSubFormula (t1 \\ t2) (base x) = ⊥
isSubFormula (t1 // t2) (base x) = ⊥
isSubFormula t1 (~ t2) = t1 ≡ (~ t2) ⊎ isSubFormula t1 t2
isSubFormula t1 (t2 \\ t3) = t1 ≡ (t2 \\ t3) ⊎ isSubFormula t1 t2 ⊎ isSubFormula t1 t3
isSubFormula t1 (t2 // t3) = t1 ≡ (t2 // t3) ⊎ isSubFormula t1 t2 ⊎ isSubFormula t1 t3