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?

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?

```
(* 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

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