Simple diagnostic tests on formulas

Question 1:

Assuming that A, B, and C are propositions, how does one write that all of them are satisfied?

answer 1: A /\ B /\ C

answer 2: forall x : A B C, True(x)

answer 3: forall A B C: Prop, True

answer 4: forall x : A \/ B \/ C, x = True

Question 2:

Assuming that A, B, and C are propositions, which of the following formulas expresses that one of them is not satisfied?

answer 1: ~(A \/ B \/ C)

answer 2: exists A B C: Prop, False

answer 3: ~A \/ ~B \/ ~C

answer 4: count (A :: B :: C :: nil) = 1

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?"

answer 1: ~ even x /\ y = x

answer 2: even x /\ y = z

answer 3: even x = (y = z)

answer 4: even x -> y = z

Question 4:

assuming x and y, how do you express that x is a multiple of y?

answer 1:

Fixpoint div (x y : nat) :=
  match y with
  | 0 => true
  | p => div x (y - x)
  end.

answer 2: exists z : nat, x = z * y

answer 3: y - x * (y / x)

answer 4: forall z : nat, x = z * y

Question 5:

How do you define the prime predicate on natural numbers?

answer 1:

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

answer 2:

Definition prime : nat -> Prop.

answer 3:

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

answer 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

answer 1:

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

answer 2:

~ exists p, p = 2 * q * q

answer 3:

forall p q, p * p = q * q -> p = 2

answer 4:

forall p q, p * p <> q * q * 2

Question 7:

With a goal of the following shape:

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

split; assumption.

answer 1: The behavior is not covered by the other answers

answer 2: No more subgoals

answer 3: There will be one goal

answer 4: An error message

Question 8:

With a goal of the following shape:

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

destruct Ha as [h1 | h2]; assumption.

answer 1: Two goals will be generated

answer 2: There will be one goal, whose statement is B

answer 3: The behavior is not covered by the other answers

answer 4: No more subgoals

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.

answer 1: A new goal, whose conclusion is P x

answer 2: A new goal, whose conclusion is Q x

answer 3: No more subgoals

answer 4: A new goal, whose conclusion is P y