Skip to content

Instantly share code, notes, and snippets.

@mietek
Last active July 11, 2016 22:09
Show Gist options
  • Save mietek/17619be0386946c266c11fadd8cfc89f to your computer and use it in GitHub Desktop.
Save mietek/17619be0386946c266c11fadd8cfc89f to your computer and use it in GitHub Desktop.
{-
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment