When addition between natural numbers is defined as follows
Fixpoint add (n m : nat) : nat := match n with | O => m | S p => S (add p m) end.
and the goal has the following shape
x, y, z : nat ========================= add x (add y z) = add (add x y) zWhat is the most efficient way to perform the proof by induction? the correct answer is answer no. 3:
induction x as [ | x' IH].
With the following function
Fixpoint f (n m : nat) : nat := match n with | O => m | S p => f p (S m) end.and the following goal
x, y : nat ============================ f (S x) y = S (f y)How should one start the proof by induction? the correct answer is answer no. 1: assert (main : forall m n, f (S m) n = S (f m n)). intros m; induction m as [|m' IH].
With function add
defined as follows:
Fixpoint add (n m : nat) : nat := match n with | O => m | S p => S (add p m) end.and the following goal:
x, y : nat ============== add (S (S x)) y = S (S (add x y))How does one perform the proof? the correct answer is answer no. 3:
reflexivity
With the function g
defined as follows
Fixpoint g n := match n with | S (S p) => S (g p) | _ => 0 end.and the goal
x : nat ================== g x <= xHow does one start the proof? the correct answer is answer no. 4: assert (main : g x <= x /\ g (S x) <= S x). induction x as [| x' IH].