Question 1:

With a goal of the following shape

  A : true = false
  ============
    V = W

what is the best tactic to apply? the correct answer is answer no. 2: discriminate

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? the correct answer is answer no. 1: injection B

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? the correct answer is answer no. 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]
the correct answer is answer no. 3:
it produces two goals
  x : nat
  ===============
   0 + 3 <= 2

and
  k : IHk
  IHk : k + 3 <= 2
  ===============
   S k + 3 <= 2