How does this use of "apply" in Coq work?

I'm working my way through software foundations. In the Chapter titled "Tactics", I'm able to prove this theorem in Coq:

Theorem silly_ex :
     (∀ n, evenb n = true → oddb (S n) = true) →
     oddb 3 = true →
     evenb 4 = true.
Proof.
  intros H1 H2. apply H2.
Qed.

Even though I was able to get through the example, I don't understand how that is a solution. After performing intros H1 H2 I'm left with proving that evenb 4 = true. The two hypotheses I have at this state are H1 : forall n : nat, evenb n = true -> oddb (S n) = true and H2 : oddb 3 = true.

How can apply H2 solve this? Even knowing that 3 is odd doesn't fulfill the antecedent of the conditional.

You can ask Coq to show you its proof object. Before Qed, type Show Proof.

(fun (_ : forall n : nat, evenb n = true -> oddb (S n) = true)
   (H2 : oddb 3 = true) => H2)

As you can see, H1 is not used at all, and the goal is H2.

It comes from the definition of oddb and evenb, the definition of negb and the definition of the natural numbers and the booleans.

Definition oddb (n:nat) : bool := negb (evenb n).

• oddb 3 is equal to negb (evenb 3) by the definition of oddb above.

• evenb 3 is equal to evenb (S (S (S O))) by the definition of 3. This is equal to evenb (S O) which is equal to false by the definition of evenb.

• Therefore oddb 3 = negb false which is in turn equal to true by the definition of negb.

• evenb 4 is equal to evenb (S (S (S (S O)))) by the definition of 4. Applying the definition of evenb three shows that this is equal to evenb (S (S O)), to evenb O, and to true.

All of these equalities come from computation: if $x$ reduces to $y$ then $x$ is equal to $y$ — this is the most basic form of equality¹. The reductions above use the $\beta$ rule (applying a lambda term to an argument), the $\delta$ rule (replacing a name by its definition) and the $\iota$ rule (applying a recursive function fix … and simplifying pattern matching).

Coq has a large set of tactics to perform computations, though they're only needed in advanced cases. For example, after intros H1 H2, you can ask it to expand evenb and oddb, but do nothing else.

cbv delta.
cbv delta in H2.

Integers like 3 and 4 are syntactic sugar, not named constants. 3 is S (S (S O)), not just some term that reduces to it. If you want to see everything that's going on, turn off pretty-printing of notations.

Unset Printing Notations.

(Use Set Printing Notations. to turn them back on.)

You can watch the goal being reduced to its value.

cbn iota. cbn beta. cbn iota. cbn beta. cbn iota. cbn beta. cbn iota. cbn beta. cbn iota.

Of course you don't need to guide Coq so much, this is just if you want to see all the steps. You can simply ask Coq to compute as much as possible. Just after intros H1 H2, run

compute. compute in H2.

and you'll see that both H2 and the goal simplify to true = true.

In this particular case there's no simpler way to go from H2 to the goal than to fully calculate both. If you continue the tutorial a bit, you'll get to recursive proofs, where it's very common to have similar hypotheses and a similar goal, but with a variable instead of constants like 3. There you would typically combine H1 and H2 together (but here H1 is not particularly interesting — since you're proving something about evenb, you'd want the an implication of the form oddb … -> evenb … rather than evenb … -> oddb …).

¹ In a certain sense, it's the only form of equality.

StackExchange Computer Science Q#101309, answer score: 8