Assignment 2
- Write Agda functions that convert between
Prod Boolean Boolean
andSum Boolean Boolean
. [2.5 pts] - Supposed that we have conversion functions
f : A1 -> A2
andf' : A2 -> A1
and, respectively,g : B1 -> B2
andg' : B2 -> B1
. Construct conversion functions- between
Sum A1 B1
andSum A2 B2
[2.5 pts] - between
Prod A1 B1
andProd A2 B2
. [2.5 pts] - define functions of type
(A1 -> A2) -> (B1 -> B2) -> (Sum A1 B1) -> (Sum A2 B2)
and(A2 -> A1) -> (B2 -> B1) -> (Sum A2 B2) -> (Sum A1 B1)
and , respectively,(A1 -> A2) -> (B1 -> B2) -> (Prod A1 B1) -> (Prod A2 B2)
and(A2 -> A1) -> (B2 -> B1) -> (Prod A2 B2) -> (Prod A1 B1)
which produce the functions above. [2.5 pts]
- between
- Write Agda proof (terms) for [2.5 pts]
(A1 -> A2) -> (B1 -> B2) -> (A1 or B1) -> (A2 or B2)
(A1 -> A2) -> (B1 -> B2) -> (A1 and B1) -> (A2 and B2)
Write the proofs for the following propositions in Agda:
R -> (not Q -> S) -> (Q and R -> not R) -> S
(not P or Q) -> not (P and not Q)