{-

Exercises for Type Theory at MGS 2023

Monday

Prove all the propositional tautologies below by completing the sheds.

C-c C-l load
\<=> ⇔
\and ∧
...
\neg ¬

In the shed.
C- C-, see goal and givens
C-c C-, like C-c C-. but also shows the type of your partial solution.
C-c C-SPC  check solution, and remove shed
C-c C-r    refine, use function or do lambdas
C-c C-c    pattern matching (if you give a parameter) or copatternmatching (no par).
-}
open import mon-lib

p1 : P ⇔ P ∧ P
p1 = {!!}

p2 : (P ∧ (Q ∨ R)) ⇔ P ∧ Q ∨ P ∧ R
p2 = {!!}

p3 : (P ⇒ Q) ⇒ ¬ Q ⇒ ¬ P
p3 = {!!}

p4 : ¬ (P ∧ ¬ P)
p4 = {!!}

p5 : ¬ (P ⇔ ¬ P)
p5 = {!!}

p6 : ¬ ¬ (P ∨ ¬ P)
p6 = {!!}

p7 : P ∨ ¬ P ⇒ (¬ (P ∧ Q) ⇔ ¬ P ∨ ¬ Q)
p7 = {!!}

p8 : ¬ P ⇔ ¬ ¬ ¬ P
p8 = {!!}