Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- 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 ()
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement