meta-system.agda

module Scratch where


data Nat : Set where
  zero : Nat
  suc : Nat → Nat


data Fin : Nat → Set where
  fzero : ∀ {n} → Fin (suc n)
  fsuc : ∀ {n} → Fin n → Fin (suc n)


infix 60 <_,_>
infixl 50 _$_

data RawTerm (n : Nat) : Set where
  var : Fin n → RawTerm n
  unit : RawTerm n
  abort : RawTerm n → RawTerm n
  <_,_> : RawTerm n → RawTerm n → RawTerm n
  fst snd : RawTerm n → RawTerm n
  lam : RawTerm (suc n) → RawTerm n
  _$_ : RawTerm n → RawTerm n → RawTerm n


infixr 60 _*_
infixr 50 _=>_

data Ty : Set where
  Zero One : Ty
  _*_ _=>_ : Ty → Ty → Ty


-- indexing by length is nicer when dealing
-- with raw terms than computing length

infixl 50 _,_

data Ctx : Nat → Set where
  <> : Ctx zero
  _,_ : ∀ {n} → Ctx n → Ty → Ctx (suc n)


data Var : ∀ {n} → Ctx n → Ty → Set where
  here : ∀ {n} {G : Ctx n} {A} → Var (G , A) A
  there : ∀ {n} {G : Ctx n} {A B} → Var G A → Var (G , B) A


infix 40 _!-_::_

data _!-_::_ {n} (G : Ctx n) : Ty → RawTerm n → Set where
  meta-var   : ∀ {A x} → Var G A → G !- A :: var x
  meta-unit  : G !- One :: unit
  meta-abort : ∀ {C M} →       G !- Zero :: M   →   G !- C :: abort M
  meta-pair  : ∀ {A B M N} →   G !- A :: M   →   G !- B :: N   →   G !- A * B :: < M , N >
  meta-fst   : ∀ {A B M} →     G !- A * B :: M   →   G !- A :: fst M
  meta-snd   : ∀ {A B M} →     G !- A * B :: M   →   G !- B :: snd M
  meta-lam   : ∀ {A B M} →     G , A !- B :: M   →   G !- A => B :: lam M
  meta-app   : ∀ {A B M N} →   G !- A => B :: M   →   G !- A :: N   →   G !- B :: M $ N


data ⊥ : Set where


-- with this lemma, we prove that there's no G, A, B, and M such that
-- we can prove   G ⊢ λM : A*B

lemma : ∀ {n} {G : Ctx n} {A B M} →   G !- A * B :: lam M   →   ⊥
lemma ()