barcher

Decidable.agda

open import Agda.Builtin.Equality public

data ⊥ : Set where

¬_ : (A : Set) → Set
¬ A = A → ⊥

infix 4 _≢_
_≢_ : {A : Set} → A → A → Set
x ≢ y = ¬(x ≡ y)

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

data Dec (A : Set) : Set where
  yes :   A → Dec A
  no  : ¬ A → Dec A

Pred : Set → Set₁
Pred A = A → Set

Decidable : {A : Set} → Pred A → Set
Decidable P = ∀ x → Dec (P x)

record Discrete (A : Set) : Set where
  constructor discrete
  field
    _⟨_≟_⟩ : (x y : A) → Dec (x ≡ y)
open Discrete public

_≟_ : {A : Set} ⦃ _ : Discrete A ⦄ → (x y : A) → Dec (x ≡ y)
_≟_ ⦃ d ⦄ x y = d ⟨ x ≟ y ⟩

data _⊎_ (A B : Set) : Set where
  inl : A → A ⊎ B
  inr : B → A ⊎ B

Formula.agda

open import Decidable

module Formula (X : Set) ⦃ _ : Discrete X ⦄ where

open import Agda.Builtin.Nat renaming (Nat to ℕ)

infixr 105 _⇒_
data Formula : Set where
  atom : X → Formula
  _⇒_  : Formula → Formula → Formula

instance formulaD : Discrete Formula
formulaD ⟨ atom x ≟ atom y ⟩ with x ≟ y
...                          | yes refl = yes refl
...                          | no  x≢y  = no λ { refl → x≢y refl }
formulaD ⟨ α ⇒ β  ≟ γ ⇒ δ  ⟩ with α ≟ γ | β ≟ δ
...                          | yes refl | yes refl = yes refl
...                          | _        | no γ≢δ   = no λ { refl → γ≢δ refl }
...                          | no α≢β   | _        = no λ { refl → α≢β refl }
formulaD ⟨ atom _ ≟ _ ⇒ _  ⟩ = no λ ()
formulaD ⟨ _ ⇒ _  ≟ atom _ ⟩ = no λ ()

List.agda

module List where

open import Agda.Builtin.Equality
open import Agda.Builtin.List public

open import Decidable

infixr 5 _++_
_++_ : {A : Set} → List A → List A → List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ xs ++ ys

++assoc : {A : Set} → (xs ys zs : List A) → xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
++assoc []       ys zs = refl
++assoc (x ∷ xs) ys zs rewrite ++assoc xs ys zs = refl


infix 4 _∈_ _∉_

data _∈_ {A : Set} (x : A) : List A → Set where
  [] : ∀{xs} → x ∈ (x ∷ xs)
  _∷_ : ∀{xs} → (y : A) → x ∈ xs → x ∈ (y ∷ xs)

_∉_ : {A : Set} → (x : A) → List A → Set
x ∉ xs = ¬(x ∈ xs)


after : {A : Set} {ys : List A} → ∀ x xs → x ∈ (xs ++ x ∷ ys)
after x []       = []
after x (y ∷ xs) = y ∷ after x xs

later : {A : Set} {x : A} {xs : List A} → ∀ ys → x ∈ xs → x ∈ ys ++ xs
later [] x∈xs = x∈xs
later (y ∷ ys) x∈xs = y ∷ later ys x∈xs

is_∈_ : {A : Set} ⦃ _ : Discrete A ⦄ → (x : A) → (xs : List A) → Dec (x ∈ xs)
is x ∈ []       = no λ ()
is x ∈ (y ∷ xs) with x ≟ y
...             | yes refl = yes []
...             | no  x≢y  with is x ∈ xs
...                        | yes x∈xs = yes (y ∷ x∈xs)
...                        | no  x∉xs = no  λ { []         → x≢y refl
                                              ; (_ ∷ x∈xs) → x∉xs x∈xs }


data All {A : Set} (P : Pred A) : List A → Set
syntax All P xs = ∀[ xs ] P
data All {A} P where
  []  : ∀[ [] ] P
  _∷_ : ∀{x xs} → P x → ∀[ xs ] P → ∀[ x ∷ xs ] P

is∀[_] : {A : Set} {P : Pred A} → (xs : List A) → Decidable P → Dec (∀[ xs ] P)
is∀[ [] ]     p = yes []
is∀[ x ∷ xs ] p with p x
...             | no ¬Px = no λ { (Px ∷ _) → ¬Px Px }
...             | yes Px with is∀[ xs ] p
...                      | yes ∀xsP = yes (Px ∷ ∀xsP)
...                      | no ¬∀xsP = no  λ { (_ ∷ ∀xsP) → ¬∀xsP ∀xsP }

Model.agda

open import Decidable

module Model (X : Set) ⦃ _ : Discrete X ⦄ where

open import Agda.Builtin.Sigma

open import Formula X
open import List
open import Tree

infix 1 _⊨_ _⊨̷_

data _⊨_ (l : List X) : Formula → Set
data _⊨̷_ (l : List X) : Formula → Set

data _⊨_ l where
  atom  : ∀{x} → x ∈ l         → l ⊨ atom x
  _∣⇒_  : ∀{β} → ∀ α   → l ⊨ β → l ⊨ α ⇒ β
  _⇒∣_  : ∀{α} → l ⊨̷ α → ∀ β   → l ⊨ α ⇒ β

data _⊨̷_ l where
  atom : ∀{x}   → x ∉ l         → l ⊨̷ atom x
  _⇒_  : ∀{α β} → l ⊨ α → l ⊨̷ β → l ⊨̷ α ⇒ β


Closed⊨atom : (x : X) → Closed λ {l} t → l ⊨ atom x
Closed⊨atom x t (atom x∈l) t≼t′ with Labelext t≼t′
...                             | s , refl = atom (later s x∈l)


does_⊨_ : (l : List X) → (α : Formula) → (l ⊨ α) ⊎ (l ⊨̷ α)
does l ⊨ atom x  with is x ∈ l
...              | yes x∈l = inl (atom x∈l)
...              | no  x∉l = inr (atom x∉l)
does l ⊨ (α ⇒ β) with does l ⊨ α | does l ⊨ β
...              | inr ⊨̷α | _      = inl (⊨̷α ⇒∣ β)
...              | _      | inl ⊨β = inl (α ∣⇒ ⊨β)
...              | inl ⊨α | inr ⊨̷β = inr (⊨α ⇒ ⊨̷β)


⊨̷elim : {l : List X} {α : Formula} → l ⊨̷ α → l ⊨ α → ⊥
⊨̷elim (atom x∉l) (atom x∈l) = x∉l x∈l
⊨̷elim (l⊨α ⇒ l⊨̷β) (α ∣⇒ l⊨β) = ⊨̷elim l⊨̷β l⊨β
⊨̷elim (l⊨α ⇒ l⊨̷β) (l⊨̷α ⇒∣ β) = ⊨̷elim l⊨̷α l⊨α


fromMeta : {l : List X} {α β : Formula} → (l ⊨ α → l ⊨ β) → l ⊨ α ⇒ β
fromMeta {l} {α} {β} ⊨α→⊨β with does l ⊨ α | does l ⊨ β
...                        | inr ⊨̷α | _      = ⊨̷α ⇒∣ β
...                        | _      | inl ⊨β = α ∣⇒ ⊨β
...                        | inl ⊨α | inr ⊨̷β = α ∣⇒ (⊨α→⊨β ⊨α)

toMeta : {l : List X} {α β : Formula} → l ⊨ α ⇒ β → l ⊨ α → l ⊨ β
toMeta (α ∣⇒ ⊨β) ⊨α = ⊨β
toMeta (⊨̷α ⇒∣ β) ⊨α = ⊥-elim (⊨̷elim ⊨̷α ⊨α)

-- WRONG DEFN
--_⊩_ : {l : List X} → (t : Tree l) → Formula → Set
--t ⊩ α = ∀[≽ t ] λ {m} t′ → m ⊨ α
--
--⊩closed : (α : Formula) → Closed (_⊩ α)
--⊩closed α = ClosedClosed λ {l} _ → l ⊨ α
--
--does_⊩_ : {l : List X} → (t : Tree l) → (α : Formula) → Dec (t ⊩ α)
--does_⊩_ {l} t (atom x) with does l ⊨ (atom x)
--...                    | inl l⊨x = yes λ t≼t′ → Closed⊨atom x t l⊨x t≼t′
--...                    | inr l⊨̷x = no λ { ≽t→⊩x → ⊨̷elim l⊨̷x (≽t→⊩x []) }
--does t ⊩ (α ⇒ β) with does t ⊩ α | does t ⊩ β
--...              | _      | yes ⊩β = yes λ t≼t′ → α ∣⇒ (⊩β t≼t′)
--...              | no ¬⊩α | _      = yes {!   !}
--...              | yes ⊩α | no ¬⊩β = no {!   !}
--
--
--_⊩atom_ : {l : List X} {x : X} → (t : Tree l) → x ∈ l → t ⊩ atom x
--(t       ⊩atom x∈l) []           = atom x∈l
--(stem ts ⊩atom x∈l) (t∈s ∷ t≼t′) = (_ ⊩atom later _ x∈l) t≼t′
--
--_⊩arrow_ : {l : List X} {x : X} {α β : Formula} → (t : Tree l) → ∀[≽ t ] (λ t′ → t ⊩ α → t ⊩ β) → t ⊩ α ⇒ β
--(t ⊩arrow k) [] = {!   !}
--  where
--    b : ?
--    b = k [] {!   !} {!   !}
--(.(stem _) ⊩arrow k) (x ∷ x₁) = {!   !}

test.agda

open import Agda.Builtin.Nat renaming (Nat to ℕ)

open import Decidable

instance ℕD : Discrete ℕ
ℕD ⟨ zero  ≟ zero  ⟩ = yes refl
ℕD ⟨ suc x ≟ suc y ⟩ with x ≟ y
...                  | yes refl = yes refl
...                  | no  x≢y  = no  λ { refl → x≢y refl }
ℕD ⟨ zero  ≟ suc _ ⟩ = no λ ()
ℕD ⟨ suc _ ≟ zero  ⟩ = no λ ()

open import Formula ℕ
open import List

fis_∈_ : (x : Formula) → (xs : List Formula) → Dec (x ∈ xs)
fis x ∈ xs = is x ∈ xs

Tree.agda

module Tree where

open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

open import List hiding (All)

data Tree {A : Set} (l : List A) : Set

record Subtree {A : Set} (l : List A) : Set where
  constructor subtree
  inductive
  field
    ext  : List A
    tree : Tree (ext ++ l)

data Tree {A} l where
  leaf : Tree l
  stem : List (Subtree l) → Tree l

Labels : {A : Set} {l : List A} → Tree l → List A
Labels {A} {l} t = l

TreePred : Set → Set₁
TreePred A = {l : List A} → Tree l → Set

-- A proof of ≼ is a path within the tree
data _≼_ {A : Set} {l : List A} : Tree l → {m : List A} → Tree m → Set where
  [] : ∀{t} → t ≼ t
  _∷_ : ∀{ts s t m} {t′ : Tree m} → (subtree s t) ∈ ts → t ≼ t′ → (stem ts) ≼ t′

≼trans : {A : Set} {l m n : List A} {t : Tree l} {t′ : Tree m} {t″ : Tree n}
         → t ≼ t′ → t′ ≼ t″ → t ≼ t″
≼trans []            t′≼t″ = t′≼t″
≼trans (t∈ts ∷ t≼t′) t′≼t″ = t∈ts ∷ ≼trans t≼t′ t′≼t″

Labelext : {A : Set} {l m : List A} {t : Tree l} {t′ : Tree m}
           → t ≼ t′ → Σ _ λ s → m ≡ s ++ l
Labelext [] = [] , refl
Labelext (t∈ts ∷ t≼t′) with Labelext t≼t′
Labelext (_∷_ {s = s} _ _) | s′ , refl = s′ ++ s , ++assoc s′ s _


∀[≽_]_ : {A : Set} {l : List A} → Tree l → TreePred A → Set
∀[≽ t ] P = ∀{m} {t′ : Tree m} → t ≼ t′ → P t′

Closed : {A : Set} → TreePred A → Set
Closed P = ∀{l} → (t : Tree l) → P t → ∀[≽ t ] P

-- A tree predicate defined by generalising another tree predicate over the
-- entire tree is closed
ClosedClosed : {A : Set} → (P : TreePred A) → Closed (∀[≽_] P)
ClosedClosed P t ∀[≽t]P t≼t′ t′≼t″ = ∀[≽t]P (≼trans t≼t′ t′≼t″)