module Homework2 where

open import PropositionalLogic

{-
Problem 1:
----------

Implement, in Agda, the proofs of the propositions in problem 2 and 3 of
homework 1[1] in the course Logic for CS. Hint: Use the Curry-Howard
identification of propositions and sets. If you need classical logic, you may
assume the law of excluded middle `em` and the law of double negation `dn` as
Agda postulates.

postulate em : (A : Set) → A ∨ ¬ A
postulate dn : (A : Set) → ¬ ¬ A → A

-- Some propositional atoms.
postulate p q r s t : Set

assoc-∧     : p ∧ (q ∧ r) → (p ∧ q) ∧ r
P2          : p → q → p
tt          : (p → r) ∨ (q → r) → p ∧ q → r
tf          : (p → ¬ p) → (¬ p → p) → ⊥
demorgan-2  : ¬ (p ∧ q) → ¬ p ∨ ¬ q
PL          : ((p → q) → p) → p

Remark: In [1] it is stated that you should give "natural deduction proofs". You
don't need to worry about this requirement - any proof that you can write in
Agda is fine: All Agda proofs are lambda terms and thus correspond to natural
deduction proofs. You don't need to worry about the details of this connection
with the natural deduction proofs you are taught in the Logic for CS course,
either.

[1] http://www.cse.chalmers.se/edu/course/DAT060/ex1.pdf
-}

{-
Problem 2:
----------

Prove the following three laws.

(a) the law of triple negation:

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

(b) excluded middle implies double negation:

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

(c) 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
proposition `A` it does not suffice to know double negation for `A` only but you
assume you know it for any proposition `X`.
-}

open import Bool
open import BoolProofs
open import Identity

open import Division
open import Nat

{-
Problem 3:
----------

In Haskell there is a class `Ord` of total orderings, see for example [2].

a) Implement an Agda record where there is one field for each method in the
   Haskell class `Ord`.

record Ord (A : Set) : Set

b) Implement an Agda structure showing that the natural numbers type `Nat` (with
   suitable implementations of the methods) is an instance of the ordering
   class.

NatOrd : Ord Nat

c) In the natural language specification of `Ord` it is stated that "[t]he `Ord`
   class is used for totally ordered datatypes". What does "totally ordered"
   actually mean? Add a field to your `Ord` record which expresses this
   requirement.

d) Prove that the `Ord Nat` instance in b) indeed satisfies the totally ordered
   requirement.

[2] https://hackage.haskell.org/package/base/docs/Data-Ord.html
-}

{-
Problem 4:
----------

Subtraction on integers is defined as the inverse of addition, that is, the
following two equations should hold

(i)  (a + b) - b ≡ a
(ii) (a - b) + b ≡ a

In the case of cut-off subtraction of natural numbers, the first equation always
holds, but the second only holds when `a` is greater than or equal to `b`. Call
this conditional version (ii').

(ii') isTrue (b <= a) → (a - b) + b ≡ a

If `a` is less than `b` then we instead have that

(iii) isTrue (a <= b) → a - b ≡ 0

Prove equations (i), (ii') and (iii) for cut-off subtraction. Hint: Do proof by
case analysis on `a` and `b` and look at the definitions of `_+_` and `_-_` for
the different cases.
-}