useronym

-- BCI "linear" typed combinator calculus.

data ★ : Set where
  ι   : ★
  _⊳_ : ★ → ★ → ★
infixr 10 _⊳_

data List (A : Set) : Set where
  ∅   : List A
  _,_ : List A → A → List A

useronym

module STLC where

open import Data.Empty using (⊥) public
open import Data.Unit using (⊤) renaming (tt to •) public
open import Function using () renaming (_∘′_ to _∘_) public
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩; proj₁ to π₁; proj₂ to π₂) public
open import Data.Nat using (ℕ) renaming (_≟_ to _≟ₙ_)
open import Data.Bool using (Bool; true; false; if_then_else_; not) renaming (_∧_ to _and_; _∨_ to _or_) public
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong₂) public
open import Relation.Nullary using (Dec; yes; no; ¬_) public

useronym

data ★ : Set where
  ι : ★
  _⊳_ : ★ → ★ → ★
infixr 15 _⊳_

data Term : Set where
  var  : Atom → Term
  ƛ_↦_ : Atom → Term → Term
  _⋅_  : Term → Term → Term
infix 7 ƛ_↦_

useronym

data _⊢_ : Cx → Form → Set where
  ID : ∀ {Γ A}     → A ∈ Γ
                     → Γ ⊢ A
  MP : ∀ {Γ A B}   → Γ ⊢ A ⇒ B → Γ ⊢ A
                     → Γ ⊢ B
  DT : ∀ {Γ A B}   → Γ , A ⊢ B
                     → Γ ⊢ A ⇒ B
  AB : ∀ {Γ A B C} → Γ ⊢ (B ⇒ C) ⇒ (A ⇒ B) ⇒ (A ⇒ C)
  AC : ∀ {Γ A B C} → Γ ⊢ (A ⇒ (B ⇒ C)) ⇒ B ⇒ (A ⇒ C)
  AI : ∀ {Γ A}     → Γ ⊢ A ⇒ A

useronym

  record Valuation : Set₁ where
    field
      _⊩ᵃ_   : Cx → Atom → Set
      mono⊩ᵃ : ∀ {Γ Γ' a} → Γ ⊆ Γ' → Γ ⊩ᵃ a → Γ' ⊩ᵃ a
  open Valuation {{…}} public

  module _ {{V : Valuation}} where
    _⊩_ : Cx → Form → Set
    Γ ⊩ var x     = Γ ⊩ᵃ x
    Γ ⊩ (f₁ ⇒ f₂) = ∀ {Γ'} → Γ ⊆ Γ' → (Γ' ⊩ f₁) → (Γ' ⊩ f₂)

useronym

data _⊢_ : Cx → Form → Set where
  ID : ∀ {Γ A}     → A ∈ Γ
                     → Γ ⊢ A
  MP : ∀ {Γ A B}   → Γ ⊢ A ⇒ B → Γ ⊢ A
                     → Γ ⊢ B
  AB : ∀ {Γ A B C} → Γ ⊢ (B ⇒ C) ⇒ (A ⇒ B) ⇒ (A ⇒ C)
  AC : ∀ {Γ A B C} → Γ ⊢ (A ⇒ (B ⇒ C)) ⇒ B ⇒ (A ⇒ C)
  AI : ∀ {Γ A}     → Γ ⊢ A ⇒ A

useronym

open import Data.Nat using (ℕ; zero; suc)
open import Data.Bool using (Bool; true; false)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

_=ℕ_ : ℕ → ℕ → Bool
0 =ℕ 0 = true
suc x =ℕ suc y = x =ℕ y
_ =ℕ _ = false

=ℕ-to-≡ : ∀ {x y : ℕ} → x =ℕ y ≡ true → x ≡ y

useronym

module Int where

import Nat using (_+_; _≤_; ≤-antisym)
open import Nat using (ℕ; zero; suc)
open import Bool using (𝔹; ⊤; ⊥; ¬_; _⇒_; _⊕_; if_then_else)
open import Relation using (_≡_; refl; Unit; U; cong₂; 𝔹-contra; antisym)


ℤ-s : ℕ → Set
ℤ-s zero = Unit

useronym

module Fold where

open import Data.Nat.Base using (ℕ; suc)

data List {l} (A : Set l) : Set l where
  [] : List A
  _::_ : (x : A) → List A → List A
infixr 6 _::_

useronym

open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Bool
open import Data.Maybe
open import Data.Product


module Bst {l} (A : Set l) (_≤A_ : A → A → Bool) where


_isoBool_ : A → A → (_≤A_ : A → A → Bool) → Bool