Collatz Conjecture in Coq

collatz.v

(* The Collatz conjecture, to illustrate reckless statements. *)
Section Collatz.

(* Collatz mapping. *)
Definition collatz_map n := if even n then div2 n else n*3+1.

(* Collatz sequence starting with n. *)
Fixpoint collatz_seq n i :=
  match i with
  | 0 => n
  | S j => collatz_map (collatz_seq n j)
  end.

(* Note that ⟨α;n⟩ reverses the sequence order. *)
Example collatz_seq_11 : rev ⟨collatz_seq 11; 15⟩
  = [11; 34; 17; 52; 26; 13; 40; 20; 10; 5; 16; 8; 4; 2; 1].
Proof. lazy; auto. Qed.

(* Every Collatz sequence reaches 1. *)
Definition collatz_conjecture := forall n, exists i, collatz_seq n i = 1.

(* This would be worth a Fields Medal ;) *)
Theorem collatz : collatz_conjecture.
Proof.
(* "notorious for absorbing massive amounts of time
    from both professional and amateur mathematicians" *)
Abort.

(*
If the Collatz Conjecture does not hold, then there exists a another cycle than
1, 4, 2, 1, ... in which the sequence can get stuck. We are interested in the
length of such a cycle. 
with the following property: all previous numbers do reach 1, and the Collatz
sequence of n does *not* reach 1. Again, the existence of this number cannot,
yet, be ruled out.
*)
Definition collatz_first_stuck n :=
  (forall m, m < n -> exists i, collatz_seq m i = 1) /\
  (forall i, collatz_seq n i <> 1).

(*
And indeed, if one day the Collatz conjecture is proven, we know for sure such
a number does not exist. If it does, then the Collatz conjecture is false.
*)
Theorem collatz_conjecture_iff_not_stuck :
  (collatz_conjecture -> ~exists n, collatz_first_stuck n) /\
  ((exists n, collatz_first_stuck n) -> ~collatz_conjecture).
Proof.
split; intros.
- intros [n [_ Hn]]. destruct (H n) as [i Hi]. apply (Hn i); auto.
- intros P; destruct H as [n [_ Hn]], (P n) as [i Hi]. apply (Hn i); auto.
Qed.

End Collatz.