Question 1:

Assuming that A, B, and C are propositions, how does one write that all of them are satisfied? the correct answer is answer no. 1: A /\ B /\ C

Question 2:

Assuming that A, B, and C are propositions, which of the following formulas expresses that one of them is not satisfied? the correct answer is answer no. 3: ~A \/ ~B \/ ~C

Question 3:

Assuming that x, y, z are natural numbers, and even has type nat -> Prop, How do you write "if x is even, then y is the same as z?" the correct answer is answer no. 4: even x -> y = z

Question 4:

assuming x and y, how do you express that x is a multiple of y? the correct answer is answer no. 2: exists z : nat, x = z * y

Question 5:

How do you define the prime predicate on natural numbers? the correct answer is answer no. 4:

Definition prime (x : nat) :=
  (1 < x) /\ forall y z, 1 < y < x -> x <> y * z.
  

Question 6:

Which of the following expresses that the square root of 2 is not rational the correct answer is answer no. 1:

forall p q : nat, p <> 0 -> p * p <> q * q * 2

Question 7:

With a goal of the following shape:

 A, B : Prop
 Ha : A
 ============
  A /\ B

split; assumption.

Question 8:

With a goal of the following shape:

 A, B : Prop
 Ha : A
 ============
  A \/ B

destruct Ha as [h1 | h2]; assumption.

Question 9:

With a goal of the following shape:

 P, Q : nat -> Prop
 f : forall y : nat, P y -> Q y
 x : nat
 r : P x
 ===========
   Q x

apply f.