-- 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))