You can ask Coq to show you its proof object. Before
(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
It comes from the definition of
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
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
oddb 3 = negb false which is in turn equal to
true by the definition of
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
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
oddb, but do nothing else.
cbv delta in H2.
4 are syntactic sugar, not named constants.
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.
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
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.