I'm trying to define a simple predicate to determine if a formula is a subformula of a given formal over a simple inductively defined syntax. I'm running into a few, presumably simple, problems.
(i) I'd rather use a parameterized module with a given type A. How can one import the information that A is a set, in the sense that A has decideable equality? If this can't be done, what are some workarounds? This is why I have Nat instead.
(ii) Is the t1 ≡ (t2 // t3) (and similairly defined) predicates isSubFormula the proper way to deal with equal subformulas? If not, how else does one easily do this? I've also considered writing a predicate for equalFmla and then making a global subformula predicate with isSubFormula ⊎ equalFmla but am not sure if this is so clean.
(iii) Why do the last three lines highlight blue when I pattern match internal to the first one? How can I fix this
(iv) Why won't the {!Data.Nat._≟_ n1 n2 !} refine below?
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
That's quite a lot of different questions; Stack Overflow works better if you post each question separately.
Nevertheless, here are some answers:
(i) I'd rather use a parameterized module with a given type A. How can one import the information that A is a set, in the sense that A has decideable equality?
You can parametrize your module by the decision procedure, i.e. something like this:
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
module categorical1 {A : Set} (_≟_ : Decidable (_≡_ {A = A})) where
Note that we import Relation.Binary (for Decidable) and R.B.PropositionalEquality (for _≡_) before the module header, since the parameter types of our module depend on these definitions.
(iii) Why do the last three lines highlight blue when I pattern match internal to the first one? How can I fix this
This is Agda warning you that those clauses won't hold definitionally, because they depend on the previous clauses not matching on t1.
(iv) Why won't the {!Data.Nat.≟ n1 n2 !} refine below?
Because isSubFormula returns a Set, but n1 ≟ n2 returns a Dec _≡_.
I think there is confusion in your code about whether isSubFormula is supposed to be a proposition or a decision procedure. If it returns a Set, it means it is a proposition. You can write that without decidable equality since there is nothing to decide -- isSubFormula-ness of two base values means they are equal:
isSubFormula : tSymb → tSymb → Set
isSubFormula (base n1) (base n2) = n1 ≡ n2
If you want a decision procedure, you could do it "boolean-blindly" by instead writing isSubFormula : tSymb → tSymb → Bool, or by keeping isSubFormula as a proposition and writing decSubFormula : Decidable isSubFormula.
Note also that you only need decidable equality on A if you are trying to decide isSubFormula, so you can do
module categorical1 (A : Set) where
...
isSubFormula : tSymb → tSymb → Set
decSubFormula : Decidable (_≡_ {A = A}) → Decidable isSubFormula
decSubFormula _≟A_ = ? -- You can use _≟A_ here to decide equality of A values