Search code examples
coqtheorem-proving

Adding infiinity to set of even numbers?

I've defined even numbers via the following format:

Inductive even : nat -> Prop :=
| ev0: even 0
| evSS: forall n, even n -> even S (S n) .

I want to add infinity to the list, so something like (even inf) as a Proposition. How can I do this?

Solution

  • The definition of nat in Coq does not have an infinite value. Thus, the first step is to add such an element. Here is one possible definition:

    Inductive nat_inf :=
| Fin : nat -> nat_inf
| Inf.

    You can now define evenness as follows:

    Inductive even : nat_inf -> Prop :=
| ev0   : even (Fin 0)
| evSS  : forall n, even (Fin n) -> even (Fin (S (S n)))
| evInf : even Inf.