module logic where

-- conjunction

data _∧_ (A B : Set) : Set where
  ∧-intro : A → B → A ∧ B

infixr 2 _∧_

∧-elim₀ : ∀ {A B : Set} → A ∧ B → A
∧-elim₀ (∧-intro a b) = a

∧-elim₀′ : ∀ {A B : Set} → A ∧ B → A
∧-elim₀′ = λ { (∧-intro a b) → a}

∧-elim₁ : ∀ {A B : Set} → A ∧ B → B
∧-elim₁ (∧-intro a b) = b

record _∧′_ (A B : Set) : Set where
 constructor ∧′-intro
 field
  ∧′-elim₀ : A
  ∧′-elim₁ : B

and-example : ∀ {A B : Set} → A ∧ B → B ∧ A
and-example (∧-intro a b) = ∧-intro b a

-- exercises

ex2-1 : ∀ {A B C : Set} → (A ∧ B → C) → (A → B → C)
ex2-1 = {!!}

ex2-2 : ∀ {A B C : Set} → (A → B → C) → (A ∧ B → C) 
ex2-2 = {!!}

ex2-3 : ∀ {A B C : Set} → (A → B) → (A ∧ C) → (B ∧ C)
ex2-3 = {!!}

ex2-4 : ∀ {A B C D : Set} → (A → B) ∧ (C → D) → (A ∧ C) → (B ∧ D)
ex2-4 = {!!}

-- disjunction

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

infixr 1 _∨_

or-example1 : ∀ {A : Set} → A ∨ A → A
or-example1 (∨-intro₀ a) = a
or-example1 (∨-intro₁ a) = a

or-example1′ : ∀ {A : Set} → A ∨ A → A
or-example1′ = λ { (∨-intro₀ a) → a ; (∨-intro₁ a) → a}

or-example2 : ∀ {A B : Set} → A ∨ B → B ∨ A
or-example2 (∨-intro₀ a) = ∨-intro₁ a
or-example2 (∨-intro₁ b) = ∨-intro₀ b

or-example3 : ∀ {A B C D : Set} → (A → B ∨ C) → (B → D) → (C → D) → (A → D)
or-example3 {A} {B} {C} {D} f g h a = helper (f a)
 where
  helper : B ∨ C → D
  helper (∨-intro₀ b) = g b
  helper (∨-intro₁ c) = h c
  
or-example3′ : ∀ {A B C D : Set} → (A → B ∨ C) → (B → D) → (C → D) → (A → D)
or-example3′ f g h a with f a
... | ∨-intro₀ b = g b
... | ∨-intro₁ c = h c

-- exercises

ex4-1 : ∀ {A B C : Set} → (A → B) → (A ∨ C) → (B ∨ C)
ex4-1 = {!!}

ex4-2 : ∀ {A B C : Set} → (A ∨ B) ∨ C → A ∨ (B ∨ C)
ex4-2 = {!!}

ex4-3 : ∀ {A B C : Set} → A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C)
ex4-3 = {!!}

-- top, the unit type

data ⊤ : Set where
  tt : ⊤

-- bottom, the empty type

data ⊥ : Set where

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

-- negation

¬ : Set → Set
¬ A = A → ⊥

bot-example : ∀ {A : Set} → ⊥ ∨ A → A
bot-example (∨-intro₁ x) = x

neg-example : ∀ {A B : Set} → A ∧ ¬ A → B
neg-example (∧-intro a na) = ⊥-elim (na a)

-- exercises

ex6-1 : ∀ {A B : Set} → (A → B) → (¬ B → ¬ A)
ex6-1 = {!!}

ex6-2 : ∀ {A B : Set} → ¬ (A ∨ B) → (A → B)
ex6-2 = {!!}

ex6-3 : ∀ {A B C : Set} → (A → (B ∨ C)) → ¬ B → ¬ C → ¬ A
ex6-3 = {!!}

ex6-4 : ∀ {A B : Set} → ¬ (A ∨ B) → ¬ A ∧ ¬ B
ex6-4 = {!!}

-- universal quantification

∀-dist-∧ : ∀ (A : Set) (B C : A → Set)
            → (∀ (a : A) → B a ∧ C a)
            → (∀ (a : A) → B a) ∧ (∀ (a : A) → C a)
∀-dist-∧ A B C f = {!!}

-- existential quantification

data Σ (A : Set) (B : A → Set) : Set where
  _,_ : (x : A) → B x → Σ A B

Σ-syntax = Σ
infix 2 Σ-syntax
syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B

∃ : ∀ {A : Set} (B : A → Set) → Set
∃ {A} B = Σ A B

∃-syntax = ∃
syntax ∃-syntax (λ x → B) = ∃[ x ] B

-- exercises

∃¬∀¬ : ∀ {A : Set} {B : A → Set} → ∃[ x ] B x → ¬ ∀ x → ¬ (B x)
∃¬∀¬ = {!!}

¬∃∀¬ : ∀ {A : Set} {B : A → Set} → ¬ (∃[ x ] B x) → ∀ x → ¬ (B x)
¬∃∀¬ = {!!}

∃¬¬∀ : ∀ {A : Set} {B : A → Set} → ∃[ x ] ¬ (B x) → ¬ ∀ x → B x
∃¬¬∀ = {!!}

∃-distr-∨ : ∀ {A : Set} {B C : A → Set}
             → ∃[ x ] (B x ∨ C x) → (∃[ x ] B x) ∨ (∃[ x ] C x)
∃-distr-∨ = {!!}

-- Excluded middle cannot be proved in intuitionistic logic, but
-- adding it is consistent, and gives classical logic.  Here are four
-- other classical theorems with the same property.  The task is to
-- show that each of them is logically equivalent to all the others.
-- You do not need to prove twenty implications, since implication is
-- transitive.  But there is a lot of choice as to how to proceed!

-- Excluded Middle
em = ∀ {A : Set} → A ∨ ¬ A

-- Double Negation Elimination
dne = ∀ {A : Set} → ¬ (¬ A) → A

-- Peirce’s Law
peirce = ∀ {A B : Set} → ((A → B) → A) → A

-- Implication as disjunction
iad = ∀ {A B : Set} → (A → B) → ¬ A ∨ B

-- De Morgan:
dem = ∀ {A B : Set} → ¬ (¬ A ∧ ¬ B) → A ∨ B