FAS Computer Services to Harvard University IT: (617) 495-7777.
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.
Download page:
An example from
the
documentation:
Fixpoint gcd a b :=
match a with
| O => b
| S a' => gcd (b mod (S a')) (S a')
end.
Definition divide x y := exists z, y=z*x.
Notation "( x | y )" := (divide x y) (at level 0) : nat_scope.
Lemma gcd_divide : forall a b, (gcd a b | a) / (gcd a b | b).
Lemma gcd_divide_l : forall a b, (gcd a b | a).
Lemma gcd_divide_r : forall a b, (gcd a b | b).
Lemma gcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|gcd a b).
