-- Advanced Functional Programming course 2016 Chalmers/GU
--
-- 2016-02-25 Guest lecture by Andreas Abel
--
-- Introduction to Agda
--
-- File 4: Logic via the Curry-Howard isomorphism

module Logic where

-- Agda is based on constructive type theory à la Martin-Löf.
-- It relies on the Curry-Howard corresponence between programming and proving.

-- A proposition is a set (or type).
-- A proof of a proposition is an element of that set (type).

prop = Set

-- The proposition that is unconditionally true is a non-empty set
-- whose in habitant can be constructed effortlessly.

data ⊤ : prop where
  trivial : ⊤

-- The proposition that is unconditionally false is the empty set.
-- The data type has no constructors.

data ⊥ : prop where

-- "Ex falsum quod libet":
-- Assuming the absurd statement everything is provable.
-- We have reached an impossible situation, so we do need to continue our proof.

⊥-elim : ∀{A : prop} → ⊥ → A
⊥-elim ()

-- Implication is just the function space.
-- A proof of A → B turns a proof of A into a proof of B.

-- Implication is transitive.

comp : ∀{A B C : prop} → (A → B) → (B → C) → (A → C)
comp f g = λ a → g (f a)

-- Negation is implication of absurdity.

¬ : prop → prop
¬ A = A → ⊥

-- The contraposition law becomes a special case of transitivity.

contraposition : ∀{A B : prop} → (A → B) → ¬ B → ¬ A
contraposition = comp

-- To prove a conjunction, we need to provide proofs of both conjuncts.
-- Thus, conjunction is pairing.

data _∧_ (A B : prop) : prop where
  pair : (p : A) (q : B) → A ∧ B

-- Conjunction is commutative (of course).

commute : ∀{A B : prop} → A ∧ B → B ∧ A
commute (pair p q) = pair q p

-- A and ¬ A cannot hold at the same time

contradiction : ∀{A : prop} → ¬(A ∧ ¬ A)
contradiction (pair a ¬a) = ¬a a

-- To prove a disjunction A ∨ B,
-- we need to provide either a proof of A or a proof of B.

data _∨_ (A B : prop) : prop where
  inl : (q : A) → A ∨ B
  inr : (q : B) → A ∨ B

-- If either ¬A or B, then the implication A → B must hold

impl : ∀{A B} → ¬ A ∨ B → (A → B)
impl (inl q) a = ⊥-elim (q a)
impl (inr q) a = q

-- The converse is not provable constructively, as A → B neither implies ¬ A nor B.

-- The excluded middle ¬ A ∨ A is also not provable in general.

-- Propositions that fulfill the excluded middle are called "decidable".

-- Exercise: prove the double negation of the excluded middle:
-- ¬ (¬ (¬ A ∨ A))