Decidability for the implicational fragment in Agda

arrow.agda

module Logic (X : Set) where

open import Decidable
open import List

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

data Tree (l : List X) : Set where
  leaf   : Tree l
  lift   : ∀ s → Tree (s ++ l) → Tree l
  branch : List (Tree l) → Tree l

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

infix 1 _⊢_ _⊩_ _⊩̷_
data _⊢_ : List Formula → Formula → Set where
  assume : ∀ Δ α Γ → Δ ++ (α ∷ Γ) ⊢ α
  intro  : ∀{Γ α β} → α ∷ Γ ⊢ β → Γ ⊢ α ⇒ β
  elim  : ∀{Γ α β} → Γ ⊢ α ⇒ β → Γ ⊢ α → Γ ⊢ β

data [_]⊩_ (xs : List X) : Formula → Set
data [_]⊩̷_ (xs : List X) : Formula → Set

data [_]⊩_ xs where
  atom : ∀{x} → x ∈ xs → [ xs ]⊩ atom x
  _∣⇒_  : ∀{β} → ∀ α → [ xs ]⊩ β → [ xs ]⊩ (α ⇒ β)
  _⇒∣_  : ∀{α} → [ xs ]⊩̷ α → ∀ β → [ xs ]⊩ (α ⇒ β)

data [_]⊩̷_ xs where
  atom : ∀{x} → x ∉ xs → [ xs ]⊩̷ atom x
  _⇒_  : ∀{α β} → [ xs ]⊩ α → [ xs ]⊩̷ β → [ xs ]⊩̷ (α ⇒ β)


data _⊩_ {l} : Tree l → Formula → Set where
  leaf   : ∀{α} → [ l ]⊩ α → leaf ⊩ α
  lift   : ∀{s t α} → t ⊩ α → (lift s t) ⊩ α
  branch : ∀{ts α} → [ l ]⊩ α → All (_⊩ α) ts → branch ts ⊩ α

data _⊩̷_ {l} : Tree l → Formula → Set where
  here  : ∀{t α} → [ l ]⊩̷ α → t ⊩̷ α
  lift  : ∀{s t α} → t ⊩̷ α → (lift s t) ⊩̷ α
  later : ∀{ts α} → Any (_⊩̷ α) ts → branch ts ⊩̷ α