diff options
| -rw-r--r-- | Makefile | 4 | ||||
| -rwxr-xr-x | theories/Arith/Arith.v | 2 | ||||
| -rwxr-xr-x | theories/Arith/Between.v | 2 | ||||
| -rwxr-xr-x | theories/Arith/Compare.v | 4 | ||||
| -rwxr-xr-x | theories/Arith/Compare_dec.v | 2 | ||||
| -rwxr-xr-x | theories/Arith/Div.v | 2 | ||||
| -rw-r--r-- | theories/Arith/Div2.v | 2 | ||||
| -rwxr-xr-x | theories/Arith/EqNat.v | 2 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Arith/Euclid.v (renamed from theories/Arith/Euclid_proof.v) | 10 | ||||
| -rwxr-xr-x | theories/Arith/Euclid_def.v | 14 | ||||
| -rwxr-xr-x | theories/Arith/intro.tex | 2 |
11 files changed, 18 insertions, 28 deletions
@@ -347,8 +347,8 @@ ARITHVO=theories/Arith/Arith.vo theories/Arith/Gt.vo \ theories/Arith/Div2.vo theories/Arith/Minus.vo \ theories/Arith/Mult.vo theories/Arith/Even.vo \ theories/Arith/EqNat.vo theories/Arith/Peano_dec.vo \ - theories/Arith/Euclid_def.vo theories/Arith/Plus.vo \ - theories/Arith/Euclid_proof.vo theories/Arith/Wf_nat.vo \ + theories/Arith/Euclid.vo theories/Arith/Plus.vo \ + theories/Arith/Wf_nat.vo \ # theories/Arith/Div.vo BOOLVO=theories/Bool/Bool.vo theories/Bool/IfProp.vo \ diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v index 7917f1582..80c29c395 100755 --- a/theories/Arith/Arith.v +++ b/theories/Arith/Arith.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Export Le. Require Export Lt. diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 8513e6b52..ab22eca22 100755 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Le. Require Lt. diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index a43941755..172ccf568 100755 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v @@ -6,10 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (********************************************) -(* equality is decidable on nat *) +(* Equality is decidable on [nat] *) (********************************************) diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 72baafe3a..1397326b2 100755 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Le. Require Lt. diff --git a/theories/Arith/Div.v b/theories/Arith/Div.v index 24f4ba36c..959f501b9 100755 --- a/theories/Arith/Div.v +++ b/theories/Arith/Div.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (* Euclidean division *) diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index 25b5d21da..60fdc68ff 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Lt. Require Plus. diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index cd3e404cd..8392f17ce 100755 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (**************************************************************************) (* Equality on natural numbers *) diff --git a/theories/Arith/Euclid_proof.v b/theories/Arith/Euclid.v index e4034b0a5..c6db2917b 100755..100644 --- a/theories/Arith/Euclid_proof.v +++ b/theories/Arith/Euclid.v @@ -6,13 +6,17 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) -Require Minus. -Require Euclid_def. +Require Mult. Require Compare_dec. Require Wf_nat. + +Inductive diveucl [a,b:nat] : Set + := divex : (q,r:nat)(gt b r)->(a=(plus (mult q b) r))->(diveucl a b). + + Lemma eucl_dev : (b:nat)(gt b O)->(a:nat)(diveucl a b). Intros b H a; Pattern a; Apply gt_wf_rec; Intros n H0. Elim (le_gt_dec b n). diff --git a/theories/Arith/Euclid_def.v b/theories/Arith/Euclid_def.v deleted file mode 100755 index a30b93caf..000000000 --- a/theories/Arith/Euclid_def.v +++ /dev/null @@ -1,14 +0,0 @@ -(***********************************************************************) -(* 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 *) -(***********************************************************************) - -(* $Id$ *) - -Require Export Mult. - -Inductive diveucl [a,b:nat] : Set - := divex : (q,r:nat)(gt b r)->(a=(plus (mult q b) r))->(diveucl a b). diff --git a/theories/Arith/intro.tex b/theories/Arith/intro.tex index 7d922c5b6..655de34ca 100755 --- a/theories/Arith/intro.tex +++ b/theories/Arith/intro.tex @@ -46,7 +46,7 @@ properties of it. \item {\tt Eqnat.v} defines a specific equality on {\tt nat} and shows the equivalence with Leibniz' equality. -\item {\tt Euclid\_def.v} and {\tt Euclid\_prog.v} prove that the euclidean +\item {\tt Euclid.v} proves that the euclidean division specification is realisable. Conversely, {\tt Div.v} exhibits two different algorithms and semi-automatically reconstruct the proof of their correctness. These files emphasize the extraction of program vs |