(* Coq is a formal proof management system. It provides a formal
 * language to write mathematical definitions, executable algorithms 
 * and theorems together with an environment for semi-interactive 
 * development of machine-checked proofs.
 *
 * This code, when compiled with Coq, produce a formal proof of the 
 * fact that 99 + 98 is an odd number. This proof is built 
 * successively in 100 steps thanks to the fact that if a + b is an 
 * odd number, then (1 + a) + (1 + b) is, too. These steps call an 
 * informative routine which sings the 99 bottles of beer song all 
 * along the construction of the proof.
 *
 * to compile: "coqc ninetynine.v"
 *
 * You can't execute the proof compiled (in fact you could, thanks 
 * to the Curry-Howard correspondence, but executing proofs 
 * unfortunately does not sing anything.)
 *)

Require Import Arith.

(* Informative singing routine *)
Ltac sing := match goal with
  | |- _ (2 + _) =>
      idtac "2 bottles of beer on the wall, 2 bottles of beer.";
      idtac "Take one down and pass it around, 1 bottle of beer on the wall."
  | |- _ (1 + _) =>
      idtac "1 bottle of beer on the wall, 1 bottle of beer.";
      idtac "Take one down and pass it around, no more bottles of beer on the wall."
  | |- _ (O + _) =>
      idtac "No more bottles of beer on the wall, no more bottles of beer.";
      idtac "Go to the store and buy some more, 99 bottles of beer on the wall."
  | |- _ (?n + ?n') =>
     idtac n "bottles of beer on the wall," n "bottles of beer.";
     idtac "Take one down and pass it around," n' "bottles of beer on the wall."
end.

(* What does it mean a number is odd? *)
Definition odd n := exists p, n = 2 * p + 1.

(* Proof that is a+b is odd then (1+a)+(1+b) is odd. *)
Lemma odd_plus_s_s : forall a b, odd (a + b) -> odd (S a + S b).
Proof.
 intros a b odd_a_b.
 destruct odd_a_b as (p, Hp).
 rewrite <- plus_n_Sm.
 simpl.
 rewrite Hp.
 exists (1 + p).
 simpl.
 repeat rewrite <- plus_n_Sm.
 reflexivity.
Qed.

(* Routine which apply the previous lemma and call "sing" then call itself *)
Ltac bottle := match goal with
  | |- _ => sing; apply odd_plus_s_s; idtac ""; bottle
  | |- _ =>
    idtac "";
    idtac "No more bottles of beer on the wall, no more bottles of beer.";
    idtac "Go to the store and buy some more, 99 bottles of beer on the wall."
end.

(* The theorem this file eventually proves *)
Theorem odd_99_plus_98 : odd (99 + 98).
Proof.
 bottle.
 exists O.
 simpl.
 reflexivity.
Qed.

(* Of course, you can prove that faster, for instance "exists 98; 
 * auto." is enough to complete the proof, but can't sing the song, 
 * how sad it is?
 *)