Lambda terms for natural deduction, sequent calculus and cut elimination

sequent.lean

import tactic

-- https://wen.works/posts/2016-03-20-one-lambda-calculus-many-times.html

-- Lambda terms for natural deduction, sequent calculus and cut elimination
-- https://pdfs.semanticscholar.org/da8a/c9652cf1f6098125c28c8a94a3dafbc92317.pdf

section

parameters {atom : Type} [decidable_eq atom] {atom.eval : atom → Prop}

inductive formula
| atom : atom → formula
| impl : formula → formula → formula

-- `@[derive decidable_eq]` is broken.
instance formula.decidable_eq : decidable_eq formula :=
sorry

def formula.eval : formula → Prop
| (formula.atom a) := atom.eval a
| (formula.impl a b) := formula.eval a → formula.eval b

local infixr ` ⇒ `:80 := formula.impl

inductive N : list formula → formula → Prop
| ax {Γ a} : a ∈ Γ → N Γ a
| elim {Γ a b} : N Γ (a ⇒ b) → N Γ a → N Γ b
| intro {Γ a b} : N (a :: Γ) b → N Γ (a ⇒ b)

local infix ` ⊢ₙ `:25 := N

variables {Γ Γ' : list formula} {a b : formula}

lemma N.ax₁ : a :: Γ ⊢ₙ a := N.ax $ or.inl rfl
lemma N.ax₂ : a :: b :: Γ ⊢ₙ b := N.ax $ or.inr (or.inl rfl)

lemma N.rename (h : Γ ⊆ Γ') : Γ ⊢ₙ a → Γ' ⊢ₙ a :=
begin
  intro s,
  induction s with _ _ ha _ _ _ _ _ ih₁ ih₂ _ _ _ _ ih generalizing Γ',
  { exact N.ax (h ha) },
  { exact N.elim (ih₁ h) (ih₂ h) },
  { exact N.intro (ih (list.cons_subset_cons _ h)) }
end

lemma N.weaken : Γ ⊢ₙ a → b :: Γ ⊢ₙ a :=
N.rename (list.subset_cons _ _)

inductive L : list formula → formula → Prop
| ax {Γ a} : a ∈ Γ → L Γ a
| left {Γ a b c} : L Γ a → L (b :: Γ) c → L (a ⇒ b :: Γ) c
| right {Γ a b} : L (a :: Γ) b → L Γ (a ⇒ b)
| cut {Γ a b} : L Γ a → L (a :: Γ) b → L Γ b

local infix ` ⊢ₗ `:25 := L

lemma L.ax₁ : a :: Γ ⊢ₗ a := L.ax $ or.inl rfl

lemma N_iff_L : Γ ⊢ₙ a ↔ Γ ⊢ₗ a :=
begin
  split; intro s,
  { induction s with _ _ ha _ _ _ _ _ ih₁ ih₂ _ _ _ _ ih,
    { exact L.ax ha },
    { exact L.cut ih₁ (L.left ih₂ L.ax₁) },
    { exact L.right ih } },
  { induction s with _ _ ha _ _ _ _ _ _ ih₁ ih₂ _ _ _ _ ih _ _ _ _ _ ih₁ ih₂,
    { exact N.ax ha },
    { refine N.elim _ (N.weaken (N.intro ih₂)),
      refine N.elim (N.weaken (N.intro (N.intro _))) N.ax₁,
      exact N.elim N.ax₁ (N.elim N.ax₂ (N.weaken (N.weaken ih₁))) },
    { exact N.elim (N.intro N.ax₁) (N.intro ih) },
    { exact N.elim (N.intro (N.elim N.ax₁ (N.weaken ih₁))) (N.intro ih₂) } }
end

lemma L.rename (h : Γ ⊆ Γ') : Γ ⊢ₗ a → Γ' ⊢ₗ a :=
begin
  rw [←N_iff_L, ←N_iff_L],
  exact N.rename h
end

lemma L.weaken : Γ ⊢ₗ a → b :: Γ ⊢ₗ a :=
L.rename (list.subset_cons _ _)

def env (Γ : list formula) : Prop := ∀ ⦃a⦄, a ∈ Γ → formula.eval a

def env.ext (ε : env Γ) (x : formula.eval a) : env (a :: Γ) :=
λ b hb,
  if h : b = a
    then h.symm ▸ x
    else ε (list.mem_of_ne_of_mem h hb)

lemma N.eval_env : env Γ → Γ ⊢ₙ a → formula.eval a :=
begin
  intros ε s,
  induction s with _ _ ha Γ a b s₁ s₂ ih₁ ih₂ Γ a b s ih generalizing ε,
  { exact ε ha },
  { exact ih₁ ε (ih₂ ε) },
  { exact λ x, ih (ε.ext x) }
end

def N.eval : ∅ ⊢ₙ a → formula.eval a := N.eval_env (λ x, false.elim)

def L.eval : ∅ ⊢ₗ a → formula.eval a := N.eval ∘ N_iff_L.mpr

end