Voting
Category
real language
Bookmarking
Language Coq
(Coq with Ltac)
| Date: | 06/25/10 |
| Author: | Jean-Marie Madiot |
| URL: | http://perso.ens-lyon.fr/jeanmarie.madiot |
| Comments: | 0 |
| Info: | http://coq.inria.fr/ |
| Score: |  (2.92 in 12 votes) |
(* 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?
*)
Download Source | Write Comment
Download Source | Write Comment
Add Comment
Please provide a value for the fields Name,
Comment and Security Code.
This is a gravatar-friendly website.
E-mail addresses will never be shown.
Enter your e-mail address to use your gravatar.
Please don't post large portions of code here! Use the form to submit new examples or updates instead!
Comments