Hilbert.agda

open import Function                              using (_$_) renaming (_∘′_ to _∘_) public
open import Category.Monad public
open import Data.Empty                            using (⊥) public
open import Data.Unit                             using (⊤) renaming (tt to •) public
open import Data.Fin                              using (Fin) renaming (zero to zeroᶠ; suc to sucᶠ) public
open import Data.Product                          using (_×_) renaming (_,_ to ⟨_,_⟩; proj₁ to π₁; proj₂ to π₂) public
open import Data.Bool                             using (Bool; true; false; if_then_else_; not) renaming (_∧_ to _and_; _∨_ to _or_) public
open import Data.Maybe                            using (Maybe; just; nothing) renaming (monad to Mmonad) public
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst₂; cong₂) public
open import Relation.Nullary                      using (Dec; yes; no; ¬_) public


-- Atoms, used as variable identifiers.
open import Data.Nat using (ℕ) renaming (zero to zeroⁿ; suc to sucⁿ)

Atom : Set
Atom = ℕ

v₀ v₁ v₂ : Atom
v₀ = 0
v₁ = 1
v₂ = 2


-- Lists, used as contexts.
data List (A : Set) : Set where
  ∅   : List A
  _,_ : List A → A → List A
infixl 10 _,_

[_] : ∀ {A} → A → List A
[ x ] = ∅ , x


-- List inclusion, or de Bruijn indices.
data _∈_ {A} : A → List A → Set where
  zero : ∀ {x xs} → x ∈ xs , x
  suc  : ∀ {x y xs} → x ∈ xs → x ∈ xs , y
infix 8 _∈_


-- Context extension.
data _⊆_ {A} : List A → List A → Set where
  stop : ∀ {Γ} → Γ ⊆ Γ
  skip : ∀ {Γ Γ' A} → Γ ⊆ Γ' → Γ ⊆ Γ' , A
  keep : ∀ {Γ Γ' A} → Γ ⊆ Γ' → Γ , A ⊆ Γ' , A
infix 8 _⊆_



-- List concatenation.
_⧺_ : ∀ {A} → List A → List A → List A
Γ ⧺ ∅     = Γ
Γ ⧺ Δ , A = (Γ ⧺ Δ) , A
infixl 9 _⧺_ _⁏_

_⁏_ : ∀ {A} → List A → List A → List A
_⁏_ = _⧺_

assoc⧺ : ∀ {A} {L₁ L₂ L₃ : List A} → L₁ ⧺ (L₂ ⧺ L₃) ≡ (L₁ ⧺ L₂) ⧺ L₃
assoc⧺ {L₃ = ∅} = refl
assoc⧺ {L₃ = xs , x} = cong₂ _,_ (assoc⧺ {L₃ = xs}) refl

unit⧺₁ : ∀ {A} {L : List A} → ∅ ⧺ L ≡ L
unit⧺₁ {L = ∅} = refl
unit⧺₁ {L = xs , x} = cong₂ _,_ (unit⧺₁ {L = xs}) refl

unit⧺₂ : ∀ {A} {L₁ L₂ : List A} → ∅ ⧺ L₁ ⧺ L₂ ≡ L₁ ⧺ L₂
unit⧺₂ {L₁ = L₁} {L₂} = trans (sym (assoc⧺ {L₁ = ∅} {L₁} {L₂})) unit⧺₁


-- Types reused by multiple systems.
data ★ : Set where
  ι   : ★
  _⊳_ : ★ → ★ → ★
infixr 8 _⊳_


data Form : Set where
  var : Atom → Form
  _⇒_ : Form → Form → Form
infixr 10 _⇒_

Cx : Set
Cx = List Form

data _⊢_ : Cx → Form → Set where
  ID : ∀ {A}         → [ A ] ⊢ A
  MP : ∀ {Γ₁ Γ₂ A B} → Γ₁ ⊢ A ⇒ B  → Γ₂ ⊢ A → Γ₁ ⁏ Γ₂ ⊢ B
  EX : ∀ {Γ₁ Γ₂ A}   → Γ₁ ⁏ Γ₂ ⊢ A → Γ₂ ⁏ Γ₁ ⊢ A
  AB : ∀ {A B C}     → ∅ ⊢ (B ⇒ C) ⇒ (A ⇒ B) ⇒ (A ⇒ C)
  AC : ∀ {A B C}     → ∅ ⊢ (A ⇒ B ⇒ C) ⇒ B ⇒ A ⇒ C
  AI : ∀ {A}         → ∅ ⊢ A ⇒ A
infix 5 _⊢_


ded : ∀ {Γ Δ A B} → Γ ⊢ B → Γ ≡ Δ , A → Δ ⊢ A ⇒ B
ded ID refl                       = AI
ded (MP {Γ₂ = ∅} t₁ t₂) eq        = subst₂ _⊢_ unit⧺₁ refl (MP (MP AC (ded t₁ eq)) t₂)
ded (MP {Γ₁} {xs , A} t₁ t₂) refl = subst₂ _⊢_ (unit⧺₂ {L₁ = Γ₁} {xs}) refl (MP (MP AB t₁) (ded t₂ refl))
ded (EX {∅} t) refl               = subst₂ _⊢_ unit⧺₁ refl (ded t refl)
ded (EX {Γ₁ , A} {∅} t) refl      = subst₂ _⊢_ (sym unit⧺₁) refl (ded t refl)
ded (EX {Γ₁ , A} {Γ₂ , x} t) refl = {!ded t refl!}
ded AB ()
ded AC ()
ded AI ()