Assuming that A, B, and C
are propositions, how does one write that all of them are
satisfied?
answer 1:
forall x : A B C, True(x)
answer 2:
forall A B C: Prop, True
answer 3:
A /\ B /\ C
answer 4:
forall x : A \/ B \/ C, x = True
Assuming that A, B, and C
are propositions, which of the following formulas expresses that
one of them is not satisfied?
answer 1:
count (A :: B :: C :: nil) = 1
answer 2:
exists A B C: Prop, False
answer 3:
~(A \/ B \/ C)
answer 4:
~A \/ ~B \/ ~C
Assuming that x, y, z are
integers, and even has type Z -> Prop,
How do you write "if x is even, then y
is the same as z?"
answer 1:
even x /\ y = z
answer 2:
~ even x /\ y = x
answer 3:
even x = (y = z)
answer 4:
even x -> y = z
assuming x and y are integers, how do you express that
x is a multiple of y?
answer 1: y - x * (y / x)
answer 2:
Fixpoint div (x y : Z) := match y with | 0 => true | p => div x (y - x) end.
answer 3: forall z :Z, x = z * y
answer 4: exists z : Z, x = z * y
How do you define the prime predicate on integers? (a
number is prime if it is larger than 1 and it has no divisor strictly between
1 and itself).
answer 1:
Definition prime (x : Z) := forall y z, x = y * z -> x = y.
answer 2:
Definition prime (x : Z) := (1 < x) /\ forall y z, 1 < y < x -> x <> y * z.
answer 3:
Definition prime : Z -> Prop := fun x => (1 < x) -> forall y z, 1 < y < z /\ x <> y * z.
answer 4:
Definition prime : Z -> Prop.
Which of the following expresses that the square root of 2 is not rational
answer 1:
forall p q, p * p <> q * q * 2
answer 2:
forall p q, p * p = q * q -> p = 2
answer 3:
~ exists p, p = 2 * q * q
answer 4:
forall p q : Z, p <> 0 -> p * p <> q * q * 2
With a goal of the following shape:
A, B : Prop Ha : A ============ A /\ B
What should be the effect of the following tactic?
split; assumption.
answer 1: None of the other answers is correct
answer 2: There will be one goal
answer 3: No more subgoals
answer 4: An error message
With a goal of the following shape:
A, B : Prop Ha : A ============ A \/ B
What should be the effect of the following tactic?
destruct Ha as [h1 | h2]; assumption.
answer 1: None of the other answers is correct
answer 2: Two goals will be generated
answer 3:
There will be one goal, whose statement is B
answer 4: No more subgoals
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
What should be the effect of the following tactic?
apply f.
answer 1: No more subgoals
answer 2:
A new goal, whose conclusion is Q x
answer 3:
A new goal, whose conclusion is P x
answer 4:
A new goal, whose conclusion is P y