Coq script for the collatz conjecture.

collatz.v

Require Export Coq.PArith.BinPos.

Inductive odd : positive -> Prop :=
  | odd_one : odd xH
  | odd_xI : forall n : positive, odd (xI (n)).
Inductive even : positive -> Prop :=
  | even_xO : forall n : positive, even (xO (n)).

Lemma even_or_odd n : even n \/ odd n.
Proof.
  induction n. Focus 3.
    right. apply odd_one.
    right. apply odd_xI.
    left. apply even_xO.

Inductive collatz : positive -> Prop :=
  | collatz_one : collatz xH
  | collatz_double : forall n : positive, collatz n -> collatz (n + n)
| collatz_divide_three : forall n : positive, ((odd n) /\ (collatz (n + n + n + 1))) -> collatz n.