More practice with Intuitionistic Logic proofs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUATE TypeOperators #-}

-- Formulae
data Atom = P | Q | R
data Form = At Atom
          | Form :/\ Form -- Conjunctions
          | Form :\/ Form -- Disjunctions
          | Form :-> Form -- Implications
          | Taut          -- Tautology
          | Contr         -- Contradiction

-- Contexts
data Context = Empty | Cons Form Context

-- Ways of being in a context
data In (φ :: Form) (γ :: Context) where
  First :: In φ (Cons φ γ)
  Next :: In φ γ -> In φ (Cons ψ γ)

-- Proofs
data Proof (γ :: Context) (φ :: Form) where
  Ax :: In φ γ -> Proof γ φ                  -- Ax
  OrIntroL :: Proof γ φ -> Proof γ (φ :\/ ψ) -- ∨I_L
  OrIntroR :: Proof γ ψ -> Proof γ (φ :\/ ψ) -- ∨I_R
  OrElim :: Proof γ (φ :\/ ψ) -> Proof (Cons φ γ) χ -> Proof (Cons ψ γ) χ -> Proof γ χ -- ∨E
  AndIntro :: Proof γ φ -> Proof γ ψ -> Proof γ (φ :/\ ψ)  -- ∧I
  AndElimL :: Proof γ (φ :/\ ψ) -> Proof γ φ  -- ∧E_L
  AndElimR :: Proof γ (φ :/\ ψ) -> Proof γ ψ  -- ∧E_R
  ArrIntro :: Proof (Cons φ γ) ψ -> Proof γ (φ :-> ψ)  -- →I
  ArrElim :: Proof γ (φ :-> ψ) -> Proof γ φ -> Proof γ ψ   -- →E
  TautIntro :: Proof γ Taut -- ⊤I
  ContrElim :: Proof γ Contr -> Proof γ φ -- ⊥E