diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-11 07:56:19 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-11 07:56:19 +0000 |
| commit | 8a7452976731275212f0c464385b380e2d590f5e (patch) | |
| tree | 966ccb9cc83c2c38dcec9b7456b6adde3f8da7a4 /contrib/correctness/examples/fact_int.v | |
| parent | f88abe3e8012ab271ef09de5761d70fcad103d56 (diff) | |
réparation d'un bug de Correctness: whd_programs ne doit pas réduire les terms contenant des Evar pas des Metas; mise à jour des exemples
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1577 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/correctness/examples/fact_int.v')
| -rw-r--r-- | contrib/correctness/examples/fact_int.v | 32 |
1 files changed, 12 insertions, 20 deletions
diff --git a/contrib/correctness/examples/fact_int.v b/contrib/correctness/examples/fact_int.v index f510fe32b..c234c5ca3 100644 --- a/contrib/correctness/examples/fact_int.v +++ b/contrib/correctness/examples/fact_int.v @@ -1,20 +1,14 @@ -(****************************************************************************) -(* The Calculus of Inductive Constructions *) -(* *) -(* Projet Coq *) -(* *) -(* INRIA LRI-CNRS ENS-CNRS *) -(* Rocquencourt Orsay Lyon *) -(* *) -(* Coq V6.3 *) -(* July 1st 1999 *) -(* *) -(****************************************************************************) -(* Certification of Imperative Programs *) -(* Jean-Christophe Filliâtre *) -(****************************************************************************) -(* fact_int.v *) -(****************************************************************************) +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliâtre *) + +(* $Id$ *) (* Proof of an imperative program computing the factorial (over type Z) *) @@ -179,6 +173,7 @@ Correctness factorielle end { (fact x@0 y) }. Proof. +Split. (* decreasing *) Unfold Zwf. Unfold Zpred. Omega. (* preservation of the invariant *) @@ -198,6 +193,3 @@ Decompose [and] Inv. Rewrite H0 in H2. Exact (invariant_0 x y1 H2). Save. - - -(* $Id$ *) |