GentzenWithProofTerms.agda

module BasicIPC.Syntax.GentzenWithProofTerms where

open import BasicIPC.Syntax.Common public


data Tm : Set where
  VAR  : Atom → Tm
  LAM  : Atom → Tm → Tm
  APP  : Tm → Tm → Tm
  PAIR : Tm → Tm → Tm
  FST  : Tm → Tm
  SND  : Tm → Tm
  UNIT : Tm


infix 6 _⦂_
record Hyp : Set where
  constructor _⦂_
  field
    name : Atom
    type : Ty

record Obj : Set where
  constructor _⦂_
  field
    proof : Tm
    type  : Ty


infix 3 _⊢_
data _⊢_ (Γ : Cx Hyp) : Obj → Set where
  var  : ∀ {x A}     → x ⦂ A ∈ Γ → Γ ⊢ VAR x ⦂ A
  lam  : ∀ {M A B}   → (x : Atom) → Γ , x ⦂ A ⊢ M ⦂ B → Γ ⊢ LAM x M ⦂ A ▻ B
  app  : ∀ {M N A B} → Γ ⊢ M ⦂ A ▻ B → Γ ⊢ N ⦂ A → Γ ⊢ APP M N ⦂ A ▻ B
  pair : ∀ {M N A B} → Γ ⊢ M ⦂ A → Γ ⊢ N ⦂ B → Γ ⊢ PAIR M N ⦂ A ∧ B
  fst  : ∀ {M A B}   → Γ ⊢ M ⦂ A ∧ B → Γ ⊢ FST M ⦂ A
  snd  : ∀ {M A B}   → Γ ⊢ M ⦂ A ∧ B → Γ ⊢ SND M ⦂ B
  unit : Γ ⊢ UNIT ⦂ ⊤

infix 3 _⊢⋆_
_⊢⋆_ : Cx Hyp → Cx Obj → Set
Γ ⊢⋆ ∅         = 𝟙
Γ ⊢⋆ Ξ , M ⦂ A = Γ ⊢⋆ Ξ × Γ ⊢ M ⦂ A


mono⊢ : ∀ {Γ Γ′ M A} → Γ ⊆ Γ′ → Γ ⊢ M ⦂ A → Γ′ ⊢ M ⦂ A
mono⊢ η (var i)    = var (mono∈ η i)
mono⊢ η (lam x t)  = lam x (mono⊢ (keep η) t)
mono⊢ η (app t u)  = app (mono⊢ η t) (mono⊢ η u)
mono⊢ η (pair t u) = pair (mono⊢ η t) (mono⊢ η u)
mono⊢ η (fst t)    = fst (mono⊢ η t)
mono⊢ η (snd t)    = snd (mono⊢ η t)
mono⊢ η unit       = unit

mono⊢⋆ : ∀ {Ξ Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢⋆ Ξ → Γ′ ⊢⋆ Ξ
mono⊢⋆ {∅}         η ∙        = ∙
mono⊢⋆ {Ξ , M ⦂ A} η (ts , t) = mono⊢⋆ η ts , mono⊢ η t


T[_≔_]_ : Atom → Tm → Tm → Tm
T[ x ≔ L ] VAR y    with x ≟ᵅ y
T[ x ≔ L ] VAR .x   | yes refl = L
T[ x ≔ L ] VAR y    | no  x≢y  = VAR y
T[ x ≔ L ] LAM y M  with x ≟ᵅ y
T[ x ≔ L ] LAM .x M | yes refl = LAM x M
T[ x ≔ L ] LAM y  M | no  x≢y  = LAM y (T[ x ≔ L ] M)
T[ x ≔ L ] APP M N  = APP (T[ x ≔ L ] M) (T[ x ≔ L ] N)
T[ x ≔ L ] PAIR M N = PAIR (T[ x ≔ L ] M) (T[ x ≔ L ] N)
T[ x ≔ L ] FST M    = FST (T[ x ≔ L ] M)
T[ x ≔ L ] SND M    = SND (T[ x ≔ L ] M)
T[ x ≔ L ] UNIT     = UNIT

[_≔_]_ : ∀ {Γ x M N A B} → (i : x ⦂ A ∈ Γ) → Γ ∖ i ⊢ M ⦂ A → Γ ⊢ N ⦂ B → Γ ∖ i ⊢ (T[ x ≔ M ] N) ⦂ B
[ i ≔ s ] var j    with i ≟∈ j
[ i ≔ s ] var .i   | same   = {!s!}
[ i ≔ s ] var ._   | diff j = {!var j!}
[ i ≔ s ] lam x t  = {!lam x ([ pop i ≔ mono⊢ weak⊆ s ] t)!}
[ i ≔ s ] app t u  = app ([ i ≔ s ] t) ([ i ≔ s ] u)
[ i ≔ s ] pair t u = pair ([ i ≔ s ] t) ([ i ≔ s ] u)
[ i ≔ s ] fst t    = fst ([ i ≔ s ] t)
[ i ≔ s ] snd t    = snd ([ i ≔ s ] t)
[ i ≔ s ] unit     = unit