Simple diagnostic tests on program verification

Question 1:

With a goal of the following shape

  A : true = false
  ============
    V = W
what 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

Question 2:

With a goal of the following shape

  x : nat
  B : 4 = S x
  ===============
    x - 1 = 2
what is the best tactic to apply next?

answer 1: injection B

answer 2: rewrite <- B

answer 3: rewrite B

answer 4: discriminate

Question 3:

With a goal of the following shape

  x : nat
  ===============
  match x with
  | 0 => 42
  | S p => 17
  end = 42 -> x = 0
what 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]

Question 4:

With a goal of the following shape

  x : nat
  ===============
   x + 3 <= 2
What 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 <= 2
because the base case is obviously false

answer 2: it produces two goals

  x : nat
  ===============
   0 + 3 <= 2
and
  k : IHk
  ===============
   S k + 3 <= 2

answer 3: it produces two goals

  x : nat
  ===============
   0 + 3 <= 2
and
  k : IHk
  IHk : k + 3 <= 2
  ===============
   S k + 3 <= 2

answer 4: It produces an error message because the statement is obviously false.