Prove a constant is even
Question
Given the inductive definition of evenness, how is it best proved that, say, 1024 is an even number? Repeating apply even_S down to zero is certainly not the right approach.
Answer (Arthur Azevedo De Amorim)
As HTNW pointed out, you can use Ltac automation to produce such a proof. This has the disadvantage of producing a large proof term even_S (even_S ... even_O), thus slowing down proofs. In this case, it is better to reformulate the goal using a boolean decision procedure:
Fixpoint evenb (n : nat) : bool := match n with | 0 => true | 1 => false | S (S m) => evenb m end.(* Fun exercise! *)forall n : nat, evenb n = true <-> even n
Coq can prove that evenb 1024 = true simply by evaluating the left-hand side:
even 1024reflexivity. Qed.evenb 1024 = true
Answer (HTNW)
Repeating apply even_S is not the way. repeat apply even_S is. If even_S is a constructor, there's also repeat constructor.
Inductive even : nat -> Prop := | even_O : even O | even_S : forall n, even n -> even (S (S n)).even 1024exact even_O. Qed.even 0repeat constructor. Qed. (* also finds even_O, would leave as goal otherwise *)even 1024