some higher order dependently typed polymorphic awesome shit

logic.agda

module Logic where

open import Function using (const; _∘_)
open import Data.Unit using (⊤; tt)
open import Data.Bool using (Bool; false; true; not; _∨_; if_then_else_)
open import Data.Nat using (ℕ; zero; suc; _≟_; _+_)
open import Data.List using (List; []; _∷_; map; _++_)
open import Data.Product using (Σ; _,_; _×_)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; inspect; [_])

Tuple : Set → ℕ → Set
Tuple A zero = ⊤
Tuple A (suc n) = A × Tuple A n

tuple : Tuple ℕ 5
tuple = 1 , 2 , 3 , 4 , 5 , tt

sum : (n : ℕ) → Tuple ℕ n → ℕ
sum zero t = 0
sum (suc n) (m , t) = m + sum n t

data Prop⁻ : Set where
  ⊥   : Prop⁻
  v   : ℕ → Prop⁻
  _⇒_ : Prop⁻ → Prop⁻ → Prop⁻

¬_ : Prop⁻ → Prop⁻
¬ φ = φ ⇒ ⊥

infix 2 _∈_

data _∈_ {A : Set} : A → List A → Set where
  here  : ∀ {x xs} → x ∈ (x ∷ xs)
  there : ∀ {x y xs} → x ∈ xs → x ∈ (y ∷ xs)

data NJ⁻ : List Prop⁻ → Prop⁻ → Set where
  assum : ∀ {Γ φ} → φ ∈ Γ → NJ⁻ Γ φ
  ⊥E    : ∀ {Γ φ} → NJ⁻ Γ ⊥ → NJ⁻ Γ φ
  ⇒I    : ∀ {Γ φ ψ} → NJ⁻ (φ ∷ Γ) ψ → NJ⁻ Γ (φ ⇒ ψ)
  ⇒E    : ∀ {Γ φ ψ} → NJ⁻ Γ (φ ⇒ ψ) → NJ⁻ Γ φ → NJ⁻ Γ ψ

⟦_⟧_ : Prop⁻ → (ℕ → Bool) → Bool
⟦ ⊥     ⟧ σ = false
⟦ v x   ⟧ σ = σ x
⟦ φ ⇒ ψ ⟧ σ = (not (⟦ φ ⟧ σ)) ∨ (⟦ ψ ⟧ σ)

_satisfies_ : (ℕ → Bool) → Prop⁻ → Set
σ satisfies φ = ⟦ φ ⟧ σ ≡ true

_satisfies'_ : (ℕ → Bool) → List Prop⁻ → Set
σ satisfies' []      = ⊤
σ satisfies' (φ ∷ Γ) = σ satisfies φ × σ satisfies' Γ

_⊧_ : List Prop⁻ → Prop⁻ → Set
Γ ⊧ φ = (σ : ℕ → Bool) → σ satisfies' Γ → σ satisfies φ

soundness : ∀ {Γ φ} → NJ⁻ Γ φ → Γ ⊧ φ
soundness (assum here)      σ (s , s') = s
soundness (assum (there i)) σ (s , s') = soundness (assum i) σ s'
soundness (⊥E d)            σ s with soundness d σ s
soundness (⊥E d)            σ s | ()
soundness (⇒I {φ = φ} d)    σ s with ⟦ φ ⟧ σ | inspect (⟦_⟧_ φ) σ
soundness (⇒I {φ = φ} d)    σ s | false | _      = refl
soundness (⇒I {φ = φ} d)    σ s | true  | [ eq ] = soundness d σ (eq , s)
soundness (⇒E d e)          σ s with soundness d σ s | soundness e σ s
soundness (⇒E {φ = ψ} d e)  σ s | eq | _   with ⟦ ψ ⟧ σ
soundness (⇒E {φ = ψ} d e)  σ s | eq | ()  | false
soundness (⇒E {φ = ψ} d e)  σ s | eq | _   | true = eq

data NK⁻ : List Prop⁻ → Prop⁻ → Set where
  assum : ∀ {Γ φ} → φ ∈ Γ → NK⁻ Γ φ
  ⊥E    : ∀ {Γ φ} → NK⁻ Γ ⊥ → NK⁻ Γ φ
  ⇒I    : ∀ {Γ φ ψ} → NK⁻ (φ ∷ Γ) ψ → NK⁻ Γ (φ ⇒ ψ)
  ⇒E    : ∀ {Γ φ ψ} → NK⁻ Γ (φ ⇒ ψ) → NK⁻ Γ φ → NK⁻ Γ ψ
  ¬¬E   : ∀ {Γ φ} → NK⁻ Γ (¬ ¬ φ) → NK⁻ Γ φ

_⊆_ : {A : Set} → List A → List A → Set
xs ⊆ ys = ∀ {x} → x ∈ xs → x ∈ ys

weaken : ∀ {Γ φ} → NK⁻ Γ φ → ∀ {Γ'} → Γ ⊆ Γ' → NK⁻ Γ' φ
weaken (assum x) Γ⊆Γ' = assum (Γ⊆Γ' x)
weaken (⊥E d)    Γ⊆Γ' = ⊥E (weaken d Γ⊆Γ')
weaken (⇒I d)    Γ⊆Γ' = ⇒I (weaken d (λ { {._} here → here; {_} (there i) → there (Γ⊆Γ' i) }))
weaken (⇒E d e)  Γ⊆Γ' = ⇒E (weaken d Γ⊆Γ') (weaken e Γ⊆Γ')
weaken (¬¬E d)   Γ⊆Γ' = ¬¬E (weaken d Γ⊆Γ')

T : (ℕ → Bool) → Prop⁻ → Prop⁻
T σ φ = if ⟦ φ ⟧ σ then φ else ¬ φ

vars : Prop⁻ → List ℕ
vars ⊥       = []
vars (v x)   = x ∷ []
vars (φ ⇒ ψ) = vars φ ++ vars ψ

++-⊆-l : {A : Set} {xs ys : List A} → xs ⊆ (xs ++ ys)
++-⊆-l here = here
++-⊆-l (there i) = there (++-⊆-l i)

++-⊆-r : {A : Set} {xs ys : List A} → ys ⊆ (xs ++ ys)
++-⊆-r {xs = []}     i = i
++-⊆-r {xs = x ∷ xs} i = there (++-⊆-r {xs = xs} i)

map-∈ : {A B : Set} {f : A → B} → ∀ {x xs} → x ∈ xs → f x ∈ map f xs
map-∈ here = here
map-∈ (there i) = there (map-∈ i)

map-⊆ : {A B : Set} {f : A → B} → ∀ {xs ys} → xs ⊆ ys → map f xs ⊆ map f ys
map-⊆ {xs = []}     Γ⊆Γ' ()
map-⊆ {xs = x ∷ xs} Γ⊆Γ' here      = map-∈ (Γ⊆Γ' here)
map-⊆ {xs = x ∷ xs} Γ⊆Γ' (there i) = map-⊆ (Γ⊆Γ' ∘ there) i

reconstruct : (φ : Prop⁻) (σ : ℕ → Bool) → NK⁻ (map (T σ ∘ v) (vars φ)) (T σ φ)
reconstruct ⊥ σ = ⇒I (assum here)
reconstruct (v x) σ with σ x
reconstruct (v x) σ | false = assum here
reconstruct (v x) σ | true  = assum here
reconstruct (φ ⇒ ψ) σ with ⟦ φ ⇒ ψ ⟧ σ | inspect (⟦_⟧_ (φ ⇒ ψ)) σ
reconstruct (φ ⇒ ψ) σ | false | [ eq ] with reconstruct φ σ
reconstruct (φ ⇒ ψ) σ | false | [ eq ] | d with ⟦ φ ⟧ σ
reconstruct (φ ⇒ ψ) σ | false | [ () ] | d | false
reconstruct (φ ⇒ ψ) σ | false | [ eq ] | d | true with reconstruct ψ σ
reconstruct (φ ⇒ ψ) σ | false | [ eq ] | d | true | e with ⟦ ψ ⟧ σ
reconstruct (φ ⇒ ψ) σ | false | [ eq ] | d | true | e | false =
  ⇒I (⇒E (weaken e (there ∘ map-⊆ (++-⊆-r {xs = vars φ} {vars ψ}))) (⇒E (assum here) (weaken d (there ∘ map-⊆ (++-⊆-l {xs = vars φ} {vars ψ})))))
reconstruct (φ ⇒ ψ) σ | false | [ () ] | d | true | e | true
reconstruct (φ ⇒ ψ) σ | true  | [ eq ] with reconstruct ψ σ
reconstruct (φ ⇒ ψ) σ | true  | [ eq ] | d with ⟦ ψ ⟧ σ
reconstruct (φ ⇒ ψ) σ | true  | [ eq ] | d | false with reconstruct φ σ
reconstruct (φ ⇒ ψ) σ | true  | [ eq ] | d | false | e with ⟦ φ ⟧ σ
reconstruct (φ ⇒ ψ) σ | true  | [ eq ] | d | false | e | false =
  ⇒I (⊥E (⇒E (weaken e (there ∘ map-⊆ (++-⊆-l {xs = vars φ} {vars ψ}))) (assum here)))
reconstruct (φ ⇒ ψ) σ | true  | [ () ] | d | false | e | true
reconstruct (φ ⇒ ψ) σ | true  | [ eq ] | d | true = ⇒I (weaken d (there ∘ map-⊆ (++-⊆-r {xs = vars φ} {vars ψ})))

_[_/_] : (ℕ → Bool) → Bool → ℕ → ℕ → Bool
(σ [ b / x ]) y with x ≟ y
(σ [ b / x ]) y | yes x≡y = b
(σ [ b / x ]) y | no  x≢y = σ y

completeness' : (Γ : List ℕ) (φ : Prop⁻) → (∀ σ → NK⁻ (map (T σ ∘ v) Γ) φ) → NK⁻ [] φ
completeness' [] φ ds = ds (const false)
completeness' (x ∷ Γ) φ ds = completeness' Γ φ (λ σ → ¬¬E (⇒I (⇒E {φ = ¬ (v x)} (⇒I (⇒E (assum (there here)) {!ds (σ [ false / x ])!})) (⇒I (⇒E (assum (there here)) {!!})))))

-- DEM λ ¬(A⇒A) → (λ ¬A → ¬(A⇒A) (λ A → abort (¬A A))) (λ A → ¬(A⇒A) (λ A' → A'))