Skip to content

Instantly share code, notes, and snippets.

@banacorn

banacorn/logic.agda

Created Sep 6, 2012
Embed
What would you like to do?
some higher order dependently typed polymorphic awesome shit
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'))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment