(* Assignment 2 - 2018/19
Solve the exercises below. You can choose between the following options.
1) Install Coq on your own machine, run "coqide" and fill in the
blanks below with appropriate lambda terms.
You can also check your answers directly in coqide.
Send your answers by email to me within the deadline.
2) Use pen & paper. For each type shown below, define a lambda term
having such type. Submit your answers during class (or scan and
email your submission) on the deadline day.
*)
Definition ex1: forall p q r : Prop,
((p /\ (q /\ (p -> q -> r))) \/ r) -> (r \/ p) :=
(** answer here **)
.
Definition ex2: forall p q : Prop,
((p -> p /\ p) -> q) -> q :=
(** answer here **)
.
Definition ex3: forall (A : Type) (p : A -> Prop),
(forall a b : A, p a \/ p b) -> (forall a : A, p a) :=
(** answer here **)
.
Definition ex4: forall p : Prop,
(forall q: Prop, (p -> q) -> q) -> p :=
(** answer here **)
.
(* Exercise 5.
Without using Coq, also solve this exercise on temporal logic.
Define (using words, symbols or drawings) a transition system
among at least 5 states satisfying the following CTL formula,
assuming that "red" is an atomic formula. Clearly show which
states are the "red" ones.
(AF red) /\ (EF ~ red) /\ AG(red -> AX red)
(Above, the symbol ~ denotes negation, while -> denotes
implication.)
Then, answer:
- Is it possible to satisfy the above formula using only one state?
- What about using two states?
*)