module PropositionalLogic where

I : {A : Set} -> A -> A
I x = x

B : {A B C : Set} -> (B -> C) -> (A -> B) -> A -> C
B g f x = g (f x)

K : {A B : Set} -> A -> B -> A
K x y = x

S : {A B C : Set} -> (A -> B -> C) -> (A -> B) -> A -> C
S g f x = g x (f x)

-- This is what Haskell B Curry observed! 
-- Types of identity, composition, K and S correspond to axioms of implication

-- conjunction = product
-- constructor = "introduction rule"

data _&_ (A B : Set) : Set where
  <_,_> : A -> B -> A & B

-- projections = "elimination rules"

fst : {A B : Set} -> A & B -> A
fst < x , y > = x

snd : {A B : Set} -> A & B -> B
snd < x , y > = y

-- disjunction = disjoint union (sum)
-- constructors = introduction rules

data _∨_ (A B : Set) : Set where
  inl : A -> A ∨ B
  inr : B -> A ∨ B

-- definition by cases = proof by cases (elimination rule)

case : {A B C : Set} -> (A -> C) -> (B -> C) -> A ∨ B -> C
case f g (inl x) = f x
case f g (inr y) = g y

comm-∨ : (A B : Set) → A ∨ B → B ∨ A 
comm-∨ A B p = case inr inl p 

-- the true proposition = the unit type

data ⊤ : Set where
  <> : ⊤

-- the false proposition = the empty type

data ⊥ : Set where

-- definition by no case = proof by no case (falsity implies anything)

nocase : {C : Set} -> ⊥ -> C
nocase ()

-- note: nocase is defined by an empty case analysis (pattern matching)
-- but Agda requires a line "nocase ()"  to express this, 
-- rather than just an empty set of patterns

-- Negation

¬ : Set → Set
¬ A = A → ⊥

-- Excluded middle is not valid

-- em : (A : Set) → A ∨ ¬ A
-- em A = {!!}

-- Double negation is not valid either

-- dn :  (A : Set) → ¬ (¬ A) → A
-- dn A g = {!!}

-- BHK (Brouwer-Heyting-Kolmogorov) interpretation of logic