With a goal of the following shape
A : true = false ============ V = Wwhat is the best tactic to apply?
answer 1:
It depends on the value of V
and W
answer 2:
discriminate
answer 3:
true <> false
answer 4: destruct A
With a goal of the following shape
x : nat B : 4 = S x =============== x - 1 = 2what is the best tactic to apply next?
answer 1:
injection B
answer 2:
rewrite <- B
answer 3:
rewrite B
answer 4: discriminate
With a goal of the following shape
x : nat =============== match x with | 0 => 42 | S p => 17 end = 42 -> x = 0what is the best tactic to apply next?
answer 1:
assert (x = 0).
answer 2:
reflexivity
answer 3:
intros h; rewrite h.
answer 4:
destruct x as [ | p]
With a goal of the following shape
x : nat =============== x + 3 <= 2What is the effect of tactic
induction x as [ | k IH]answer 1: it produces one goal
k : IHk IHk : k + 3 <= 2 =============== S k + 3 <= 2because the base case is obviously falseanswer 2: it produces two goals
x : nat =============== 0 + 3 <= 2andk : IHk =============== S k + 3 <= 2answer 3: it produces two goals
x : nat =============== 0 + 3 <= 2andk : IHk IHk : k + 3 <= 2 =============== S k + 3 <= 2answer 4: It produces an error message because the statement is obviously false.