types - 如何在 Agda 中定义归纳定义类型的子公式？

Question

我试图定义一个简单的谓词来确定一个公式是否是一个给定形式的子公式，而不是一个简单的归纳定义的语法。我遇到了一些可能很简单的问题。

(i) 我宁愿使用具有给定类型 A 的参数化模块。在 A 具有可判定相等性的意义上，如何导入 A 是一个集合的信息？如果无法做到这一点，有什么解决方法？这就是我使用 Nat 的原因。

(ii)t1 ≡ (t2 // t3)谓词（并且定义类似）isSubFormula是处理相等子公式的正确方法吗？如果没有，还有什么方法可以轻松做到这一点？我也考虑过编写一个谓词equalFmla，然后用它制作一个全局子公式谓词，isSubFormula ⊎ equalFmla但我不确定这是否如此干净。

(iii) 当我在第一行内部进行模式匹配时，为什么最后三行会突出显示蓝色？我怎样才能解决这个问题

(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

标签： typesagdatype-theorydecidable

Answer 1