module Homework2 where

{-
Note that you may import appropriate files from the course page. To get full credit you need to do four of the following six problems correctly.

Problem 5: First prove transitivity of identity by doing pattern matching in both arguments:

trans : {A : Set} → {a₁ a₂ a₃ : A} → a₁ ≡ a₂ → a₂ ≡ a₃ → a₁ ≡ a₃
trans p₁ p₂ = ?

Then prove the principle of substitution of equals for equals:

subst : {A : Set} -> {P : A → Set} → {a₁ a₂ : A} → a₁ ≡ a₂ -> P a₂ -> P a₁

Then prove trans as an instance of subst. Hint: how do you instantiate P?

Problem 6: Prove the following de Morgan law 

deMorgan-or-1 : (b b' : Bool) → not (b && b') ≡ not b || not b'

Prove it also with the alternative formulation using isTrue:

deMorgan-or-2 : (b b' : Bool) → isTrue (not (b && b') <==> not b || not b')

Problem 7: Prove commutativity of addition

commutativity-plus : (m n : Nat) → m + n ≡ n + m

Hint: First prove the lemmas

zero + n ≡ n
succ m + n ≡ succ (m + n)

by induction on n. Show both how you write the proof with pattern matching and with only using 

natind : {C : Nat -> Set} -> C zero -> ((n : Nat) -> C n -> C (succ n)) -> (n : Nat) -> C n

Cf how we proved associativity of + using pattern matching and natind.

Problem 8: Prove the law of distibutivity 

m * (n + p) ≡ m * n + m * p

Problem 8: Prove the following three laws. 
(a) the law of triple negation:

tn :  (A : Set) → ¬ (¬ (¬ A)) → ¬ A

(b) that excluded middle implies double negation:

em-dn : {A : Set} → (A ∨ ¬ A) →  ¬ (¬ A) → A

(c) that double negation implies excluded middle:

dn-em : ({X : Set} → ¬ (¬ X) → X) → (A : Set) →  (A ∨ ¬ A)

Note the strengthening of the assumption here: to prove excluded middle for A it does not suffice to know double negation for A only but you need to assume you know it for any proposition X.

Problem 9: The following laws are valid in classical predicate logic:

    ¬ ∀ x P ( x ) ⇔ ∃ x ¬ P ( x ) 
    ¬ ∃ x P ( x ) ⇔ ∀ x ¬ P ( x ) 
    ∀ x ∀ y P ( x , y ) ⇔ ∀ y ∀ x P ( x , y )
    ∃ x ∃ y P ( x , y ) ⇔ ∃ y ∃ x P ( x , y )

Which of them are valid in intuitionistic predicate logic, and hence provable in Agda (using the formalization of the file PredicateLogic.agda)? Implement the proofs in Agda, whenever possible! Note that P ⇔ Q means "equivalent" that is, that P implies Q and Q implies P. If only one of the implications is valid prove that one! Recall that intuitionistic predicate logic is like classical predicate logic without the law of excluded middle.
-}