HilbertGentzenIPC.agda

{-

Inspired by Jan Malakhovski (2012) “Reinventing formal logic”
http://oxij.org/note/ReinventingFormalLogic

-}

module HilbertGentzenIPC where

open import Data.Product using (Σ) renaming (_,_ to _∙_)
open import Function using (_∘_ ; _$_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)


-- Names, for propositional variables.

postulate
  Nm : Set


-- Contexts.

infixl 2 _,_
data Cx (U : Set) : Set where
  ∅   : Cx U
  _,_ : Cx U → U → Cx U


-- Variables, as nameless typed de Bruijn indices.

module _ {U : Set} where
  infix 1 _∈_
  data _∈_ (A : U) : Cx U → Set where
    top : ∀ {Γ} → A ∈ Γ , A
    pop : ∀ {B Γ} → A ∈ Γ → A ∈ Γ , B

  i₀ : ∀ {A Γ} → A ∈ Γ , A
  i₀ = top

  i₁ : ∀ {A B Γ} → A ∈ Γ , A , B
  i₁ = pop i₀

  i₂ : ∀ {A B C Γ} → A ∈ Γ , A , B , C
  i₂ = pop i₁

  i₃ : ∀ {A B C D Γ} → A ∈ Γ , A , B , C , D
  i₃ = pop i₂

  i₄ : ∀ {A B C D E Γ} → A ∈ Γ , A , B , C , D , E
  i₄ = pop i₃

  i₅ : ∀ {A B C D E F Γ} → A ∈ Γ , A , B , C , D , E , F
  i₅ = pop i₄


-- Concatenation of contexts.

module _ {U : Set} where
  _++_ : Cx U → Cx U → Cx U
  Γ ++ ∅        = Γ
  Γ ++ (Γ′ , A) = (Γ ++ Γ′) , A

  mono⁺⁺∈ : ∀ {A Γ} Γ′ → A ∈ Γ → A ∈ Γ ++ Γ′
  mono⁺⁺∈ ∅        i = i
  mono⁺⁺∈ (Γ′ , B) i = pop (mono⁺⁺∈ Γ′ i)

  mono∈⁺⁺ : ∀ {A Γ Γ′} → A ∈ Γ′ → A ∈ Γ ++ Γ′
  mono∈⁺⁺ top     = top
  mono∈⁺⁺ (pop i) = pop (mono∈⁺⁺ i)


-- Order-preserving embeddings.

module _ {U : Set} where
  infix 1 _⊆_
  data _⊆_ : Cx U → Cx U → Set where
    done : ∅ ⊆ ∅
    skip : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊆ Γ′ , A
    keep : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ , A ⊆ Γ′ , A

  refl⊆ : ∀ {Γ} → Γ ⊆ Γ
  refl⊆ {∅}     = done
  refl⊆ {Γ , A} = keep refl⊆

  trans⊆ : ∀ {Γ Γ′ Γ″} → Γ ⊆ Γ′ → Γ′ ⊆ Γ″ → Γ ⊆ Γ″
  trans⊆ η        done      = η
  trans⊆ η        (skip η′) = skip (trans⊆ η η′)
  trans⊆ (skip η) (keep η′) = skip (trans⊆ η η′)
  trans⊆ (keep η) (keep η′) = keep (trans⊆ η η′)

  unskip⊆ : ∀ {A Γ Γ′} → Γ , A ⊆ Γ′ → Γ ⊆ Γ′
  unskip⊆ (skip η) = skip (unskip⊆ η)
  unskip⊆ (keep η) = skip η

  unkeep⊆ : ∀ {A Γ Γ′} → Γ , A ⊆ Γ′ , A → Γ ⊆ Γ′
  unkeep⊆ (skip η) = unskip⊆ η
  unkeep⊆ (keep η) = η

  weak⊆ : ∀ {A Γ} → Γ ⊆ Γ , A
  weak⊆ = skip refl⊆

  zero⊆ : ∀ {Γ} → ∅ ⊆ Γ
  zero⊆ {∅}     = done
  zero⊆ {Γ , A} = skip zero⊆

  mono∈ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → A ∈ Γ → A ∈ Γ′
  mono∈ done     ()
  mono∈ (skip η) i       = pop (mono∈ η i)
  mono∈ (keep η) top     = top
  mono∈ (keep η) (pop i) = pop (mono∈ η i)


-- Types of intuitionistic propositional calculus (IPC).

infixl 5 _∧_
infixl 4 _∨_
infixr 3 _⇒_
data Ty : Set where
  ι    : Nm → Ty
  _⇒_ : Ty → Ty → Ty
  _∧_  : Ty → Ty → Ty
  _∨_  : Ty → Ty → Ty
  ⊥   : Ty

¬_ : Ty → Ty
¬ A = A ⇒ ⊥

infix 3 _⇔_
_⇔_ : Ty → Ty → Ty
A ⇔ B = (A ⇒ B) ∧ (B ⇒ A)


-- Terms of IPC, as Hilbert-style combinator sequences.

module HS where
  infix 1 _⊢⁺_
  data _⊢⁺_ (Γ : Cx Ty) : Cx Ty → Set where
    nil  : Γ ⊢⁺ ∅
    var  : ∀ {Π A}     → A ∈ Γ → Γ ⊢⁺ Π → Γ ⊢⁺ Π , A
    app  : ∀ {Π A B}   → A ⇒ B ∈ Π → A ∈ Π → Γ ⊢⁺ Π → Γ ⊢⁺ Π , B
    icom : ∀ {Π A}     → Γ ⊢⁺ Π → Γ ⊢⁺ Π , A ⇒ A
    kcom : ∀ {Π A B}   → Γ ⊢⁺ Π → Γ ⊢⁺ Π , A ⇒ B ⇒ A
    scom : ∀ {Π A B C} → Γ ⊢⁺ Π → Γ ⊢⁺ Π , (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C
    pair : ∀ {Π A B}   → Γ ⊢⁺ Π → Γ ⊢⁺ Π , A ⇒ B ⇒ A ∧ B
    fst  : ∀ {Π A B}   → Γ ⊢⁺ Π → Γ ⊢⁺ Π , A ∧ B ⇒ A
    snd  : ∀ {Π A B}   → Γ ⊢⁺ Π → Γ ⊢⁺ Π , A ∧ B ⇒ B
    inl  : ∀ {Π A B}   → Γ ⊢⁺ Π → Γ ⊢⁺ Π , A ⇒ A ∨ B
    inr  : ∀ {Π A B}   → Γ ⊢⁺ Π → Γ ⊢⁺ Π , B ⇒ A ∨ B
    case : ∀ {Π A B C} → Γ ⊢⁺ Π → Γ ⊢⁺ Π , A ∨ B ⇒ (A ⇒ C) ⇒ (B ⇒ C) ⇒ C
    boom : ∀ {Π C}     → Γ ⊢⁺ Π → Γ ⊢⁺ Π , ⊥ ⇒ C

  mono⊢⁺ : ∀ {Π Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢⁺ Π → Γ′ ⊢⁺ Π
  mono⊢⁺ η nil          = nil
  mono⊢⁺ η (var i ts)   = var (mono∈ η i) (mono⊢⁺ η ts)
  mono⊢⁺ η (app i j ts) = app i j (mono⊢⁺ η ts)
  mono⊢⁺ η (icom ts)    = icom (mono⊢⁺ η ts)
  mono⊢⁺ η (kcom ts)    = kcom (mono⊢⁺ η ts)
  mono⊢⁺ η (scom ts)    = scom (mono⊢⁺ η ts)
  mono⊢⁺ η (pair ts)    = pair (mono⊢⁺ η ts)
  mono⊢⁺ η (fst ts)     = fst (mono⊢⁺ η ts)
  mono⊢⁺ η (snd ts)     = snd (mono⊢⁺ η ts)
  mono⊢⁺ η (inl ts)     = inl (mono⊢⁺ η ts)
  mono⊢⁺ η (inr ts)     = inr (mono⊢⁺ η ts)
  mono⊢⁺ η (case ts)    = case (mono⊢⁺ η ts)
  mono⊢⁺ η (boom ts)    = boom (mono⊢⁺ η ts)

  infix 1 _⊢_
  _⊢_ : Cx Ty → Ty → Set
  Γ ⊢ A = Σ (Cx Ty) (λ Π → Γ ⊢⁺ Π , A)

  mono⊢ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢ A → Γ′ ⊢ A
  mono⊢ η (Π ∙ ts) = Π ∙ mono⊢⁺ η ts


  -- Concatenation of combinator sequences.

  _++ᵀ_ : ∀ {Γ Π Π′} → Γ ⊢⁺ Π → Γ ⊢⁺ Π′ → Γ ⊢⁺ Π ++ Π′
  ss ++ᵀ nil          = ss
  ss ++ᵀ (var i ts)   = var i (ss ++ᵀ ts)
  ss ++ᵀ (app i j ts) = app (mono∈⁺⁺ i) (mono∈⁺⁺ j) (ss ++ᵀ ts)
  ss ++ᵀ (icom ts)    = icom (ss ++ᵀ ts)
  ss ++ᵀ (kcom ts)    = kcom (ss ++ᵀ ts)
  ss ++ᵀ (scom ts)    = scom (ss ++ᵀ ts)
  ss ++ᵀ (pair ts)    = pair (ss ++ᵀ ts)
  ss ++ᵀ (fst ts)     = fst (ss ++ᵀ ts)
  ss ++ᵀ (snd ts)     = snd (ss ++ᵀ ts)
  ss ++ᵀ (inl ts)     = inl (ss ++ᵀ ts)
  ss ++ᵀ (inr ts)     = inr (ss ++ᵀ ts)
  ss ++ᵀ (case ts)    = case (ss ++ᵀ ts)
  ss ++ᵀ (boom ts)    = boom (ss ++ᵀ ts)

open HS using (_++ᵀ_) renaming (_⊢⁺_ to HS[_⊢⁺_] ; _⊢_ to HS[_⊢_])


-- Terms of IPC, as Hilbert-style combinator trees.

module HT where
  infix 1 _⊢_
  data _⊢_ (Γ : Cx Ty) : Ty → Set where
    var  : ∀ {A}     → A ∈ Γ → Γ ⊢ A
    app  : ∀ {A B}   → Γ ⊢ A ⇒ B → Γ ⊢ A → Γ ⊢ B
    icom : ∀ {A}     → Γ ⊢ A ⇒ A
    kcom : ∀ {A B}   → Γ ⊢ A ⇒ B ⇒ A
    scom : ∀ {A B C} → Γ ⊢ (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C
    pair : ∀ {A B}   → Γ ⊢ A ⇒ B ⇒ A ∧ B
    fst  : ∀ {A B}   → Γ ⊢ A ∧ B ⇒ A
    snd  : ∀ {A B}   → Γ ⊢ A ∧ B ⇒ B
    inl  : ∀ {A B}   → Γ ⊢ A ⇒ A ∨ B
    inr  : ∀ {A B}   → Γ ⊢ B ⇒ A ∨ B
    case : ∀ {A B C} → Γ ⊢ A ∨ B ⇒ (A ⇒ C) ⇒ (B ⇒ C) ⇒ C
    boom : ∀ {C}     → Γ ⊢ ⊥ ⇒ C

  mono⊢ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢ A → Γ′ ⊢ A
  mono⊢ η (var i)   = var (mono∈ η i)
  mono⊢ η (app t u) = app (mono⊢ η t) (mono⊢ η u)
  mono⊢ η icom      = icom
  mono⊢ η kcom      = kcom
  mono⊢ η scom      = scom
  mono⊢ η pair      = pair
  mono⊢ η fst       = fst
  mono⊢ η snd       = snd
  mono⊢ η inl       = inl
  mono⊢ η inr       = inr
  mono⊢ η case      = case
  mono⊢ η boom      = boom


  -- The deduction theorem for combinator trees.

  ded : ∀ {A B Γ} → Γ , A ⊢ B → Γ ⊢ A ⇒ B
  ded (var top)     = icom
  ded (var (pop i)) = app kcom (var i)
  ded (app t u)     = app (app scom (ded t)) (ded u)
  ded icom          = app kcom icom
  ded kcom          = app kcom kcom
  ded scom          = app kcom scom
  ded pair          = app kcom pair
  ded fst           = app kcom fst
  ded snd           = app kcom snd
  ded inl           = app kcom inl
  ded inr           = app kcom inr
  ded case          = app kcom case
  ded boom          = app kcom boom

open HT using () renaming (_⊢_ to HT[_⊢_])


-- Conversion from combinator sequences to trees.

module HS→HT where
  conn : ∀ {A Γ Π} → HS[ Γ ⊢⁺ Π ] → A ∈ Π → HT[ Γ ⊢ A ]
  conn (HS.var i ts)   top     = HT.var i
  conn (HS.app i j ts) top     = HT.app (conn ts i) (conn ts j)
  conn (HS.icom ts)    top     = HT.icom
  conn (HS.kcom ts)    top     = HT.kcom
  conn (HS.scom ts)    top     = HT.scom
  conn (HS.pair ts)    top     = HT.pair
  conn (HS.fst ts)     top     = HT.fst
  conn (HS.snd ts)     top     = HT.snd
  conn (HS.inl ts)     top     = HT.inl
  conn (HS.inr ts)     top     = HT.inr
  conn (HS.case ts)    top     = HT.case
  conn (HS.boom ts)    top     = HT.boom
  conn (HS.var i ts)   (pop k) = conn ts k
  conn (HS.app i j ts) (pop k) = conn ts k
  conn (HS.icom ts)    (pop k) = conn ts k
  conn (HS.kcom ts)    (pop k) = conn ts k
  conn (HS.scom ts)    (pop k) = conn ts k
  conn (HS.pair ts)    (pop k) = conn ts k
  conn (HS.fst ts)     (pop k) = conn ts k
  conn (HS.snd ts)     (pop k) = conn ts k
  conn (HS.inl ts)     (pop k) = conn ts k
  conn (HS.inr ts)     (pop k) = conn ts k
  conn (HS.case ts)    (pop k) = conn ts k
  conn (HS.boom ts)    (pop k) = conn ts k

hs→ht : ∀ {A Γ} → HS[ Γ ⊢ A ] → HT[ Γ ⊢ A ]
hs→ht (Π ∙ ts) = HS→HT.conn ts i₀


-- Conversion from combinator trees to sequences.

module HT→HS where
  app : ∀ {A B Γ} → HS[ Γ ⊢ A ⇒ B ] → HS[ Γ ⊢ A ] → HS[ Γ ⊢ B ]
  app {A} {B} (Π ∙ ts) (Π′ ∙ ss) =
      (Π′ , A) ++ (Π , A ⇒ B) ∙
      HS.app i₀ (mono⁺⁺∈ (Π , A ⇒ B) i₀) (ss ++ᵀ ts)

ht→hs : ∀ {A Γ} → HT[ Γ ⊢ A ] → HS[ Γ ⊢ A ]
ht→hs (HT.var i)   = ∅ ∙ HS.var i HS.nil
ht→hs (HT.app t u) = HT→HS.app (ht→hs t) (ht→hs u)
ht→hs HT.icom      = ∅ ∙ HS.icom HS.nil
ht→hs HT.kcom      = ∅ ∙ HS.kcom HS.nil
ht→hs HT.scom      = ∅ ∙ HS.scom HS.nil
ht→hs HT.pair      = ∅ ∙ HS.pair HS.nil
ht→hs HT.fst       = ∅ ∙ HS.fst HS.nil
ht→hs HT.snd       = ∅ ∙ HS.snd HS.nil
ht→hs HT.inl       = ∅ ∙ HS.inl HS.nil
ht→hs HT.inr       = ∅ ∙ HS.inr HS.nil
ht→hs HT.case      = ∅ ∙ HS.case HS.nil
ht→hs HT.boom      = ∅ ∙ HS.boom HS.nil


-- The deduction theorem for combinator sequences.

hs-ded : ∀ {A B Γ} → HS[ Γ , A ⊢ B ] → HS[ Γ ⊢ A ⇒ B ]
hs-ded = ht→hs ∘ HT.ded ∘ hs→ht


-- Terms of IPC, as Gentzen-style natural deduction trees.

module ND where
  infix 1 _⊢_
  data _⊢_ (Γ : Cx Ty) : Ty → Set where
    var  : ∀ {A}     → A ∈ Γ → Γ ⊢ A
    lam  : ∀ {A B}   → Γ , A ⊢ B → Γ ⊢ A ⇒ B
    app  : ∀ {A B}   → Γ ⊢ A ⇒ B → Γ ⊢ A → Γ ⊢ B
    pair : ∀ {A B}   → Γ ⊢ A → Γ ⊢ B → Γ ⊢ A ∧ B
    fst  : ∀ {A B}   → Γ ⊢ A ∧ B → Γ ⊢ A
    snd  : ∀ {A B}   → Γ ⊢ A ∧ B → Γ ⊢ B
    inl  : ∀ {A B}   → Γ ⊢ A → Γ ⊢ A ∨ B
    inr  : ∀ {A B}   → Γ ⊢ B → Γ ⊢ A ∨ B
    case : ∀ {A B C} → Γ ⊢ A ∨ B → Γ , A ⊢ C → Γ , B ⊢ C → Γ ⊢ C
    boom : ∀ {C}     → Γ ⊢ ⊥ → Γ ⊢ C

  mono⊢ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢ A → Γ′ ⊢ A
  mono⊢ η (var i)      = var (mono∈ η i)
  mono⊢ η (lam t)      = lam (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⊢ η (inl t)      = inl (mono⊢ η t)
  mono⊢ η (inr t)      = inr (mono⊢ η t)
  mono⊢ η (case t u v) = case (mono⊢ η t) (mono⊢ (keep η) u) (mono⊢ (keep η) v)
  mono⊢ η (boom t)     = boom (mono⊢ η t)

  v₀ : ∀ {A Γ} → Γ , A ⊢ A
  v₀ = var i₀

  v₁ : ∀ {A B Γ} → Γ , A , B ⊢ A
  v₁ = var i₁

  v₂ : ∀ {A B C Γ} → Γ , A , B , C ⊢ A
  v₂ = var i₂


  -- Useful theorems.

  icom : ∀ {A Γ} → Γ ⊢ A ⇒ A
  icom = lam v₀

  kcom : ∀ {A B Γ} → Γ ⊢ A ⇒ B ⇒ A
  kcom = lam (lam v₁)

  scom : ∀ {A B C Γ} → Γ ⊢ (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C
  scom = lam (lam (lam (app (app v₂ v₀) (app v₁ v₀))))

  ded : ∀ {A B Γ} → Γ , A ⊢ B → Γ ⊢ A ⇒ B
  ded t = lam t

  fst′ : ∀ {A B Γ} → Γ ⊢ (A ∧ B) ⇒ A
  fst′ = lam (fst v₀)

open ND


-- Conversion from Hilbert-style to Gentzen-style terms.

ht→nd : ∀ {A Γ} → HT[ Γ ⊢ A ] → Γ ⊢ A
ht→nd (HT.var i)   = var i
ht→nd (HT.app t u) = app (ht→nd t) (ht→nd u)
ht→nd HT.icom      = ND.icom
ht→nd HT.kcom      = ND.kcom
ht→nd HT.scom      = ND.scom
ht→nd HT.pair      = lam (lam (pair v₁ v₀))
ht→nd HT.fst       = lam (fst v₀)
ht→nd HT.snd       = lam (snd v₀)
ht→nd HT.inl       = lam (inl v₀)
ht→nd HT.inr       = lam (inr v₀)
ht→nd HT.case      = lam (lam (lam (case v₂ (app v₂ v₀) (app v₁ v₀))))
ht→nd HT.boom      = lam (boom v₀)

hs→nd : ∀ {A Γ} → HS[ Γ ⊢ A ] → Γ ⊢ A
hs→nd = ht→nd ∘ hs→ht


-- Conversion from Gentzen-style to Hilbert-style terms.

nd→ht : ∀ {A Γ} → Γ ⊢ A → HT[ Γ ⊢ A ]
nd→ht (var i)      = HT.var i
nd→ht (lam t)      = HT.ded (nd→ht t)
nd→ht (app t u)    = HT.app (nd→ht t) (nd→ht u)
nd→ht (pair t u)   = HT.app (HT.app HT.pair (nd→ht t)) (nd→ht u)
nd→ht (fst t)      = HT.app HT.fst (nd→ht t)
nd→ht (snd t)      = HT.app HT.snd (nd→ht t)
nd→ht (inl t)      = HT.app HT.inl (nd→ht t)
nd→ht (inr t)      = HT.app HT.inr (nd→ht t)
nd→ht (case t u v) = HT.app (HT.app (HT.app HT.case (nd→ht t)) (HT.ded (nd→ht u))) (HT.ded (nd→ht v))
nd→ht (boom t)     = HT.app HT.boom (nd→ht t)

nd→hs : ∀ {A Γ} → Γ ⊢ A → HS[ Γ ⊢ A ]
nd→hs = ht→hs ∘ nd→ht