Simple diagnostic tests

Question 1:

What is the value of the following expression:

match 4 with
| S (S x) => x
| _ => 0
end.

answer 1: 0

answer 2: 6

answer 3: 2

answer 4: Error: Non exhaustive pattern matching

Question 2:

What is the value of the following expression:

match 5 with
| S (S x) => x
| _ => 0
end.

answer 1: 0

answer 2: Error: Non exhaustive pattern matching

answer 3: 3

answer 4: 7

Question 3:

What is the value of the following expression:

match 5 with
| S (S x) => x
| 0 => 0
end.

answer 1: Error: Non exhaustive pattern matching

answer 2: 7

answer 3: 0

answer 4: 3

Question 4:

In a context where lists have been defined, what is the value of the following expression:

match (1 :: 2 :: 3 :: 4 :: nil) with
| _ :: _ :: n :: _ =>  n
| _ => 0
end

answer 1: 3

answer 2: Error: Non exhaustive pattern matching

answer 3: 2

answer 4: Error: In environment ... the term ... has type ... while it expected to have type ...

Question 5:

What is the value of the following expression:

(fun (f : nat -> nat) => f 3) (Nat.add 2)

answer 1: 5

answer 2: Error: in environment ... the term (Nat.add 2) has type (nat -> nat) while it is expected to have type nat

answer 3: 3

answer 4: Error: Function Nat.add is expecting two arguments

Question 6:

What is the value of the following expression:

match (4 + 2) with
| x + 2 => x
| _ => 0
end

answer 1: 4

answer 2: 8

answer 3: Error: Invalid notation for pattern

answer 4: 0

Question 7:

What is the value of the following expression:

match 3, 4 with x, x => x | x, y => x + y end.

answer 1: 3

answer 2: 7

answer 3: 4

answer 4: Error: the variable x is bound several times in pattern

Question 8:

What is the value of the following expression:

(fun x y => match y with 0 => true | x => false end) 3 5

answer 1: 5

answer 2: false

answer 3: Error: Non exhaustive pattern matching

answer 4: true

Question 9:

Here is the definition of a recursive function:

Fixpoint f (x : nat) : nat :=
  match x with 0 => 0 | 1 => 0 | S p => S (f p) end.

answer 1: 3

answer 2: 2

answer 3: Error: Pattern "S p" is redundant ...

answer 4: 0

Question 10:

Here is the definition of a recursive function:

Fixpoint f (x : nat) : nat :=
  match x with 0 => 1 | S p => p * f p end.

answer 1: 2

answer 2: 1

answer 3: 0

answer 4: 6

Hard advanced question (recursion, arithmetic)

Question 11:

Here is the definition of a recursive function:

Fixpoint f (x : nat) : nat :=
  match x with S (S p) => S (f p) | _ => 0 end.

answer 1: 1

answer 2: 5

answer 3: 4

answer 4: 6

Question 12:

What is the value of the following expression:

fun x => match 2 + x with
| S (S x) => x
| _ => 0
end

answer 1: Error : Invalid notation for pattern

answer 2: fun x : nat => x

answer 3: S (S (2 + x))

answer 4: 0