What is the difference between these inductive definitions in Coq?

Question

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 ?

Answer 1

You have an extra colon in the first definition such that your code does not in fact compile. Anyway, that fixed, the two definitions are exactly the same, as you can see if you do the following:

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)).

Print even_one.
Print even_two.