证明一个常数是偶数

Question

鉴于偶数的归纳定义，如何最好地证明1024是偶数？将apply even_S重复降低到零肯定不是正确的方法。

Answer 1

不是重复apply even_S。 repeat apply even_S是。如果even_S是构造函数，则还有repeat constructor。

Inductive even : nat -> Prop :=
| even_O : even O
| even_S : forall n, even n -> even (S (S n)).

Goal (even 1024). repeat apply even_S. exact even_O. Qed.
Goal (even 1024). repeat constructor. Qed. (* also finds even_O, would leave as goal otherwise *)