Why in silly_ex (the software foundation)the first hypothesis is useless

Using Coq
1

Here is the code:

Theorem silly_ex :
     (forall n, evenb n = true -> oddb (S n) = true) ->
     oddb 3 = true ->
     evenb 4 = true.
Proof.
    intros cond eq. apply eq.  Qed.

Why I can’t apply cond and the Theorem doesn’t need cond to prove?

2 
(* Example implementations of [evenb] and [oddb] *)
Fixpoint evenb (n : nat) { struct n } : bool :=
  match n with
  | 0 => true
  | 1 => false
  | S (S n) => evenb n
  end.

Fixpoint oddb (n : nat) { struct n } : bool :=
  match n with
  | 0 => false
  | 1 => true
  | S (S n) => oddb n
  end.

Theorem silly_ex :
     (forall n, evenb n = true -> oddb (S n) = true) ->
     oddb 3 = true ->
     evenb 4 = true.
Proof.
  intros cond eq.
  (* Q: Why I can’t apply [cond]? *)
  (* A: Look at the statement of [cond] -- you can use it to prove [oddb (S n)] if you assume [evenb n]. *)
  (* However, in this case, you need to show [evenb 4], which doesn't match with the goal *)

  (* Q: Why can we do [apply eq]? *)
  (* Now, note that [eq] can be simplified to [true = true]: *) simpl in eq.
  (* This simply does some simplification given the fixpoint definition above *)
  (* We can also simplify the goal to [evenb 4 = evenb 2 = evenb 0 = true]: *) simpl.
  (* Now, we can prove the goal with [reflexivity], or we can apply [eq], since this assumption is exactly the goal *)
  exact eq.
Qed.
1 Like
3

In order to apply cond you need the implication the other way around

Theorem silly_ex' :
     (forall n, oddb n = true -> evenb (S n) = true) ->
     oddb 3 = true ->
     evenb 4 = true.
Proof.
  intros cond eq.
  apply cond.
  exact eq.
Qed.
1 Like