module Martes where

{- Propositional logic in Agda -}

prop : Set₁
prop = Set

{- Proving some basic combinators. -}

K : {P Q : prop} → P → Q → P
K x y = x

S : {P Q R : prop} → (P → Q → R) → (P → Q) → P → R
S pqr pq p = pqr p (pq p) 

{- S, K are sufficent to prove all other tautologies involving only →. -}

I : {P : prop} → P → P
I x = x

B : {P Q R : prop} → (P → Q) → (Q → R) → P → R
B = λ pq qr p → qr (pq p)

C : {P Q R : prop} → (P → Q → R) → Q → P → R
C = λ x x' x0 → x x0 x'

{- S, K are sufficent to prove all other tautologies involving only →. -}

I' : {P : prop} → P → P
I' {P} = S K (K {Q = P})


--Too hard for me.
CB' : {P Q R : prop} → (Q → R) → (P → Q)  → P → R
CB' = S (K S) K

C' : {P Q R : prop} → (P → Q → R) → Q → P → R
C' = S (S (K S) (S (K K) S)) (K K)

B' : {P Q R : prop} → (P → Q) → (Q → R) → P → R
B' = C' CB'

{- draw the truth table and then try to prove it -}

{-
P : {P Q : prop} → ((P → Q) → P) → P
P = {!!}

Pierces' formula is uprovable.
-}

{- Defining other connectives -}

data _∧_ (P Q : prop) : prop where
  _,_ : P → Q → P ∧ Q

infixr  _∧_
{- C-c C-, gives you the current "proof state" -}
∧-comm : {P Q : prop} → P ∧ Q → Q ∧ P
∧-comm (p , q) = q , p

data _∨_ (P Q : prop) : prop where
    left : P → P ∨ Q
    right : Q → P ∨ Q

distrib→ : {P Q R : prop} → P ∧ (Q ∨ R) → (P ∧ Q) ∨ (P ∧ R)
distrib→ (p , left q) = left (p , q)
distrib→ (p , right r) = right (p , r)

distrib← : {P Q R : prop} → (P ∧ Q) ∨ (P ∧ R) → P ∧ (Q ∨ R)
distrib← (left (p , q)) = p , left q
distrib← (right (p , r)) = p , right r

{- how do the two programs relate?
   there is more than just if and only iff.
 -}

_⇔_ : prop → prop → prop
P ⇔ Q = (P → Q) ∧ (Q → P)

infixr  _⇔_

distrib⇔ : {P Q R : prop} → P ∧ (Q ∨ R) ⇔ (P ∧ Q) ∨ (P ∧ R)
distrib⇔ = distrib→ , distrib←

curry→ : {P Q R : prop} → (P ∧ Q → R) → (P → Q → R)
curry→ pqr p q = pqr (p , q)

curry← : {P Q R : prop} → (P → Q → R) → (P ∧ Q → R)
curry← pqr (p , q) = pqr p q

curry⇔ : {P Q R : prop} → (P ∧ Q → R) ⇔ (P → Q → R)
curry⇔ = curry→ , curry←

∨∧→ : {P Q R : prop} → (P ∨ Q → R) → ((P → R) ∧ (Q → R))
∨∧→ pqr = (λ p → pqr (left p)) , λ q → pqr (right q)

∨∧← : {P Q R : prop} → ((P → R) ∧ (Q → R)) → (P ∨ Q → R) 
∨∧← (pr , qr) (left p) = pr p
∨∧← (pr , qr) (right q) = qr q  

∨∧ : {P Q R : prop} → (P ∨ Q → R) ⇔ ((P → R) ∧ (Q → R))
∨∧ = ∨∧→ , ∨∧←

{- some combinators -}

fst : {A B : prop} → A ∧ B → A
fst (a , b) = a

snd : {A B : prop} → A ∧ B → B
snd (a , b) = b

case : {A B C : prop} → (A → C) → (B → C) → A ∨ B → C
case ac bc (left a) = ac a
case ac bc (right b) = bc b

or-com : {P Q : prop} → P ∨ Q → Q ∨ P
or-com = case right left

{- a different equivalence -}

copy : {A : prop} → A ⇔ A ∧ A
copy = (λ x → (x , x)) , (λ x → fst x)


{- challenge: reprove distrib only with combinators. -}

{-
distribC : {P Q R : prop} → P ∧ (Q ∨ R) → (P ∧ Q) ∨ (P ∧ R)
distribC = {!!}

--to hard for me.
-}

{- introduce true (⊤) and false (⊥) -}

{- \top = ⊤ -}
data ⊤ : prop where
  tt : ⊤

{- \bot = ⊥ -}
data ⊥ : prop where
{- this space is intentionally left blank. -}

efq : {P : prop} → ⊥ → P
efq ()

¬ : prop → prop
¬ P = P → ⊥

contradict : {P : prop} → ¬ (P ∧ ¬ P)
contradict (p , np) = np p

contrapos : {P Q : prop} → (P → Q) → ¬ Q → ¬ P
contrapos pq nq p = nq (pq p)

paradox : {P : prop} → ¬ (P ⇔ ¬ P) 
paradox (pnp , npp) = pnp (npp (λ x → pnp x x)) (npp (λ x → pnp x x))

{- Let's prove the de Morgan laws -}

deMorgan¬∨ : {P Q : prop} → ¬ (P ∨ Q) → ¬ P ∧ ¬ Q 
deMorgan¬∨ npq = (λ p → npq (left p)) , λ q → npq (right q)
  
deMorgan¬∧¬ : {P Q : prop} → (¬ P) ∧ (¬ Q) → ¬ (P ∨ Q)
deMorgan¬∧¬ (np , nq) (left p) = np p
deMorgan¬∧¬ (np , nq) (right q) = nq q
  
deMorgan¬∨¬ : {P Q : prop} → (¬ P) ∨ (¬ Q) → ¬ (P ∧ Q)
deMorgan¬∨¬ (left np) (p , q) = np p
deMorgan¬∨¬ (right nq) (p , q) = nq q

{-
deMorgan¬∧ : {P Q : prop} → ¬ (P ∧ Q) → (¬ P) ∨ (¬ Q)
deMorgan¬∧ npq = {!!}

the last de Morgan formula is unprovable!
-}

{- on classical vs intuitionistic reasoning. -}

{-
tnd : {P : prop} → P ∨ ¬ P
tnd = {!!}
Tertium non datur (excluded middle) is unprovable.
-}

¬¬ : prop → prop
¬¬ P = ¬ (¬ P)

pnnp : {P : prop} → P → ¬¬ P 
pnnp p np = np p
{-
raa : {P : prop} → ¬¬ P → P
raa nnp = {!!}
reductio ad absurdo (indirect proof)
is unprovable.
-}

¬¬tnd : {P : prop} → ¬¬ (P ∨ ¬ P)
¬¬tnd npnp = npnp (right (λ p → npnp (left p)))

TND : Set₁
TND = {P : prop} → P ∨ ¬ P

RAA : Set₁
RAA = {P : prop} → ¬¬ P → P

RAA→TND : RAA → TND
RAA→TND raa = raa ¬¬tnd

TND→RND : TND → RAA
TND→RND tnd {P} nnp with tnd {P}
TND→RND tnd nnp | left p = p
TND→RND tnd nnp | right np = efq (nnp np)

ret¬¬ : {P : prop} → P → ¬¬ P
ret¬¬ p np = np p 

bind¬¬ : {P Q : prop} → ¬¬ P → (P → ¬¬ Q) → ¬¬ Q 
bind¬¬ nnp pnnq nq = nnp (λ p → pnnq p nq)

map¬¬ : {P Q : prop} → ¬¬ P → (P → Q) → ¬¬ Q
map¬¬ np pq = bind¬¬ np (λ p → ret¬¬ (pq p))

app¬¬ : {P Q : prop} → ¬¬ (P → Q) → ¬¬ P → ¬¬ Q
app¬¬ nnpq nnp = bind¬¬ nnpq (λ pq → bind¬¬ nnp (λ p → ret¬¬ (pq p)))

∧¬¬-1 : {P Q : prop} → ¬¬ (P ∧ Q) → ¬¬ P ∧ ¬¬ Q
∧¬¬-1 nnpq = map¬¬ nnpq fst , map¬¬ nnpq snd

∧¬¬-2 : {P Q : prop} → ¬¬ P ∧ ¬¬ Q → ¬¬ (P ∧ Q) 
∧¬¬-2 (nnp , nnq) = bind¬¬ nnp (λ p → map¬¬ nnq  (λ q → p , q))

∧¬¬ : {P Q : prop} → ¬¬ (P ∧ Q) ⇔ ¬¬ P ∧ ¬¬ Q
∧¬¬ = ∧¬¬-1 , ∧¬¬-2

{-
∨¬¬-1 : {P Q : prop} → ¬¬ (P ∨ Q) → ¬¬ P ∨ ¬¬ Q
∨¬¬-1 nnpq = {!!} 
is unprovable.
-}

∨¬¬-2 : {P Q : prop} → ¬¬ P ∨ ¬¬ Q → ¬¬ (P ∨ Q) 
∨¬¬-2 (left np) = map¬¬ np left
∨¬¬-2 (right nq) = map¬¬ nq right

{-
∨¬¬ : {P Q : prop} → ¬¬ (P ∨ Q) ⇔ ¬¬ P ∨ ¬¬ Q
∨¬¬ = {!!} 
is unprovable.
-}

¬¬deMorgan¬∧ : {P Q : prop} → ¬ (P ∧ Q) → ¬¬ ((¬ P) ∨ (¬ Q))
¬¬deMorgan¬∧ npq = λ x → x (left (λ x' → x (right (λ x0 → npq (x' , x0)))))

{- Predicate logic -}

{- If A : Set,
      P : A → prop
   then ∀ a : A, P a
   is   (a : A) → P a
-}

∀∧ : {A : Set}{P Q : A → prop} → 
  ((a : A) → P a ∧ Q a) → ((a : A) → P a) ∧ ((a : A) → Q a)
∀∧ pq = (λ a → fst (pq a)) , (λ a → snd (pq a))

∧∀ : {A : Set}{P Q : A → prop} → 
  ((a : A) → P a) ∧ ((a : A) → Q a) → ((a : A) → P a ∧ Q a)
∧∀ (ap , aq) = λ a → (ap a , aq a)

{-
∀∨ : {A : Set}{P Q : A → prop} → 
  ((a : A) → P a ∨ Q a) → ((a : A) → P a) ∨ ((a : A) → Q a)
∀∨ pq = {!!}
is even classically not true. -}

∨∀ : {A : Set}{P Q : A → prop} → 
  ((a : A) → P a) ∨ ((a : A) → Q a) → ((a : A) → P a ∨ Q a)
∨∀ (left ap) = λ a → left (ap a)
∨∀ (right aq) = λ a → right (aq a)

{- Existential quantification: given a set A, and a predicate P : A → Prp
   ∀' A P : Prop means that P a is true (inhabited) for some a:A.
   A proof of this is a (depndent) pair (a , p) where a : A and 
   p : P a is a proof that P a is true (inhabited).
-}
data ∃ (A : Set)(P : A → prop) : prop where
  _,_ : (a : A) → P a → ∃ A P

∃∧ : {A : Set}{P Q : A → prop} → 
  (∃ A (λ a → P a ∧ Q a)) → (∃ A P) ∧ (∃ A Q)
∃∧ (a , (p , q)) = (a , p) , (a , q)

{-
∧∃ : {A : Set}{P Q : A → prop} →
  (∃ A P) ∧ (∃ A Q) → (∃ A (λ a → P a ∧ Q a))
∧∃ x = {!!}
is even classically not true.
-}

∃∨ : {A : Set}{P Q : A → prop} → 
  (∃ A (λ a → P a ∨ Q a)) → (∃ A P) ∨ (∃ A Q)
∃∨ (a , left p) = left (a , p)
∃∨ (a , right q) = right (a , q)

∨∃ : {A : Set}{P Q : A → prop} → 
  (∃ A P) ∨ (∃ A Q) → (∃ A (λ a → P a ∨ Q a))
∨∃ (left (a , p)) = a , left p
∨∃ (right (a , q)) = a , right q

{- the infinite deMorgan rules - which ones are provable? -}

{- ¬ (∃ x:A. P x) ⇔ ∀ x:A. ¬ P x -}

deMorgan¬∃ : {A : Set}{P : A → prop} →
           ¬ (∃ A (λ x → P x)) → ((x : A) → ¬ (P x))
deMorgan¬∃ = λ x x' x0 → x (x' , x0)

deMorgan∀¬ : {A : Set}{P : A → prop} →
           ((x : A) → ¬ (P x)) → ¬ (∃ A (λ x → P x))
deMorgan∀¬ x (a , y) = x a y

{- ¬ (∀ x:A. P x) ⇔ ∃ x:A . ¬ P x -}

{-
deMorgan¬∀ : {A : Set}{P : A → prop} →
             ¬ ((x : A) → P x) → ∃ A (λ x → ¬ (P x))
deMorgan¬∀ = {!!}
-- unprovable.
-}

deMorgan∃¬ : {A : Set}{P : A → prop} →
           ∃ A (λ x → ¬ (P x)) → ¬ ((x : A) → P x)
deMorgan∃¬ (a , y) = λ x → y (x a)

{- relating ∀ and ∃ -}

curry∀→ : {A : Set}{P : A → Set}{Q : prop}
         → ((∃ A P) → Q) → (a : A) → P a → Q
curry∀→ x = λ a x' → x (a , x')

curry∀← : {A : Set}{P : A → Set}{Q : prop}
         → ((a : A) → P a → Q) → ((∃ A P) → Q)
curry∀← x (a , y) = x a y

{- the axiom of choice -}

fst' : {A : Set}{P : A → prop} → ∃ A P → A
fst' (a , p) = a
{- Note that fst' really exploits the identification of prop and Set. -}

{- And show that the fst' satisfies the predicate: -}
snd' : {A : Set}{P : A → prop} → (p : ∃ A P) → P (fst' p)
snd' (a , p) = p

ac : {A B : Set}{R : A → B → prop} → 
     ((a : A) → ∃ B λ b → R a b)
     → ∃ (A → B) λ f → (a : A) → R a (f a)
ac f = (λ a → fst' (f a)) , λ a → snd' (f a)

{- unprovable.
cac : {A B : Set}{R : A → B → prop} → 
     ((a : A) → ¬¬ (∃ B λ b → R a b))
     → ¬¬ (∃ (A → B) λ f → (a : A) → R a (f a))
cac h = {!!}

Counterexample:
 A = Turingmachines, B = Bool, R m b = b <-> m holds -}

dac : {A : Set}{B : A → Set}{R : (a : A) → B a → Set} 
      → ((a : A) → ∃ (B a) (λ b → R a b))
      → ∃ ((a : A) → B a) (λ f → (a : A) → R a (f a))
dac f = (λ a → fst' (f a)) , λ a → snd' (f a)