module Logic where

-- The universe of propositions is denoted by Prp. By the Curry-Howard
-- isomorphism, it is the universe of types, sometimes called sets in
-- Agda. I like to keep a mental distinction between a proposition and
-- a set though. Sometimes a type is to be thought of as a set, and
-- sometimes as a proposition, at least if one wants the development to
-- be somewhat intellegible to non-type-theorists.

Prp = Set

-- False:

data ⊥ : Prp where
-- nothing defined here: there are no constructors of this type.

⊥-elim : {A : Prp} → ⊥ → A
⊥-elim = λ ()

¬_ : Prp → Prp
¬ A = (A → ⊥)

infix   ¬_

data _∧_ (A₀ A₁ : Prp) : Prp where
  ∧-intro : A₀ → A₁ → A₀ ∧ A₁

infixr  _∧_


∧-elim₀ : {A₀ A₁ : Prp} →
---------------
 A₀ ∧ A₁ → A₀
---------------
∧-elim₀ (∧-intro a₀ a₁) = a₀


∧-elim₁ : {A₀ A₁ : Prp} →
---------------
 A₀ ∧ A₁ → A₁
---------------
∧-elim₁ (∧-intro a₀ a₁) = a₁


data _∨_ (A₀ A₁ : Prp) : Prp where
  ∨-intro₀ : A₀ → A₀ ∨ A₁
  ∨-intro₁ : A₁ → A₀ ∨ A₁

infixr  _∨_


∨-elim : {A₀ A₁ B : Prp} →
----------------------------------
 (A₀ → B) → (A₁ → B) → A₀ ∨ A₁ → B
----------------------------------
∨-elim f₀ f₁ (∨-intro₀ a₀) = f₀ a₀
∨-elim f₀ f₁ (∨-intro₁ a₁) = f₁ a₁


record ∃ {X : Set} (A : X → Prp) : Prp where
 constructor ∃-intro
 field
  ∃-witness : X
  ∃-elim : A ∃-witness


∃-witness : {X : Set} {A : X → Prp} →
----------------------------
 (∃ \(x : X) → A x) → X
----------------------------
∃-witness (∃-intro x a) = x


∃-elim : {X : Set} {A : X → Prp} →
------------------------------------------------------
 (proof : ∃ \(x : X) → A x) → A (∃-witness proof)
------------------------------------------------------
∃-elim(∃-intro x a) = a


-- Some basic logical facts:

_∘_ : {A B : Prp} {C : B → Prp} →
----------------------------------------------------
 (∀(b : B) → C b) → ∀(f : A → B) → ∀(a : A) → C(f a)
----------------------------------------------------
g ∘ f = λ x → g(f x)

infixl  _∘_

-- The following is usually used with R=⊥:

contra-positive : {R A B : Prp} →
----------------------------
 (A → B) → (B → R) → (A → R)
----------------------------
contra-positive f p = p ∘ f