I came up with the following inductive definitions in Coq for an even number:
Inductive even_one : nat -> Prop :=
| even_one_nil : even_one O
| even_one_ss : (n : nat) (H : even_one n) : even_one (S (S n)).
Inductive even_two : nat -> Prop :=
| even_two_nil : even_two O
| even_two_ss : forall n, even_two n -> even_two (S (S n)).
I tested both definitions for the following theorems:
Theorem even_th_one : forall n, even_one (S (S n)) -> even_one (S (S (S (S n)))).
Theorem even_th_two : forall n, even_two (S (S n)) -> even_two (S (S (S (S n)))).
And from what I saw, both basically come up with the same hypothesis in the proofs upon an application of apply
. For instance,
Theorem even_th_one : forall n, even_one (S (S n)) -> even_one (S (S (S (S n)))).
Proof.
intros n. intros H.
apply even_one_ss with (n:=(S (S n))). apply even_one_ss. apply even_one_nil.
Qed.
So what's the difference between these two ways of writing ?
Goal forall n, even_one n <-> even_two n.
$\endgroup$