0
$\begingroup$

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 ?

$\endgroup$
1
  • $\begingroup$ Perhaps you can prove something like Goal forall n, even_one n <-> even_two n. $\endgroup$
    – djao
    Commented Dec 6, 2023 at 5:06

1 Answer 1

3
$\begingroup$

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.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.