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
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
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
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
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.
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
With a goal of the following shape:
A, B : Prop Ha : A ============ A /\ BWhat should be the effect of the following tactic?
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
With a goal of the following shape:
A, B : Prop Ha : A ============ A \/ BWhat should be the effect of the following tactic?
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
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 xWhat should be the effect of the following tactic?
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