From 477574b664f32e0f508a8657c0143c2e17e78547 Mon Sep 17 00:00:00 2001 From: mohring Date: Thu, 19 Apr 2001 12:18:42 +0000 Subject: Remplacement Euclid_def Euclid_proof par Euclid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1617 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile | 4 +-- theories/Arith/Arith.v | 2 +- theories/Arith/Between.v | 2 +- theories/Arith/Compare.v | 4 +-- theories/Arith/Compare_dec.v | 2 +- theories/Arith/Div.v | 2 +- theories/Arith/Div2.v | 2 +- theories/Arith/EqNat.v | 2 +- theories/Arith/Euclid.v | 61 +++++++++++++++++++++++++++++++++++++++++++ theories/Arith/Euclid_def.v | 14 ---------- theories/Arith/Euclid_proof.v | 57 ---------------------------------------- theories/Arith/intro.tex | 2 +- 12 files changed, 72 insertions(+), 82 deletions(-) create mode 100644 theories/Arith/Euclid.v delete mode 100755 theories/Arith/Euclid_def.v delete mode 100755 theories/Arith/Euclid_proof.v diff --git a/Makefile b/Makefile index 9b22c333d6..6e0d1dd2bc 100644 --- a/Makefile +++ b/Makefile @@ -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 7917f15828..80c29c3951 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 8513e6b52b..ab22eca22c 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 a439417558..172ccf568a 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 72baafe3ac..1397326b24 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 24f4ba36c7..959f501b94 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 25b5d21da4..60fdc68ff6 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 cd3e404cd8..8392f17cec 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.v b/theories/Arith/Euclid.v new file mode 100644 index 0000000000..c6db2917bd --- /dev/null +++ b/theories/Arith/Euclid.v @@ -0,0 +1,61 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (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). +Intro lebn. +Elim (H0 (minus n b)); Auto with arith. +Intros q r g e. +Apply divex with (S q) r; Simpl; Auto with arith. +Elim plus_assoc_l. +Elim e; Auto with arith. +Intros gtbn. +Apply divex with O n; Simpl; Auto with arith. +Save. + +Lemma quotient : (b:nat)(gt b O)-> + (a:nat){q:nat|(EX r:nat | (a=(plus (mult q b) r))/\(gt b r))}. +Intros b H a; Pattern a; Apply gt_wf_rec; Intros n H0. +Elim (le_gt_dec b n). +Intro lebn. +Elim (H0 (minus n b)); Auto with arith. +Intros q Hq; Exists (S q). +Elim Hq; Intros r Hr. +Exists r; Simpl; Elim Hr; Intros. +Elim plus_assoc_l. +Elim H1; Auto with arith. +Intros gtbn. +Exists O; Exists n; Simpl; Auto with arith. +Save. + +Lemma modulo : (b:nat)(gt b O)-> + (a:nat){r:nat|(EX q:nat | (a=(plus (mult q b) r))/\(gt b r))}. +Intros b H a; Pattern a; Apply gt_wf_rec; Intros n H0. +Elim (le_gt_dec b n). +Intro lebn. +Elim (H0 (minus n b)); Auto with arith. +Intros r Hr; Exists r. +Elim Hr; Intros q Hq. +Elim Hq; Intros; Exists (S q); Simpl. +Elim plus_assoc_l. +Elim H1; Auto with arith. +Intros gtbn. +Exists n; Exists O; Simpl; Auto with arith. +Save. diff --git a/theories/Arith/Euclid_def.v b/theories/Arith/Euclid_def.v deleted file mode 100755 index a30b93cafc..0000000000 --- a/theories/Arith/Euclid_def.v +++ /dev/null @@ -1,14 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (a=(plus (mult q b) r))->(diveucl a b). diff --git a/theories/Arith/Euclid_proof.v b/theories/Arith/Euclid_proof.v deleted file mode 100755 index e4034b0a5d..0000000000 --- a/theories/Arith/Euclid_proof.v +++ /dev/null @@ -1,57 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (a:nat)(diveucl a b). -Intros b H a; Pattern a; Apply gt_wf_rec; Intros n H0. -Elim (le_gt_dec b n). -Intro lebn. -Elim (H0 (minus n b)); Auto with arith. -Intros q r g e. -Apply divex with (S q) r; Simpl; Auto with arith. -Elim plus_assoc_l. -Elim e; Auto with arith. -Intros gtbn. -Apply divex with O n; Simpl; Auto with arith. -Save. - -Lemma quotient : (b:nat)(gt b O)-> - (a:nat){q:nat|(EX r:nat | (a=(plus (mult q b) r))/\(gt b r))}. -Intros b H a; Pattern a; Apply gt_wf_rec; Intros n H0. -Elim (le_gt_dec b n). -Intro lebn. -Elim (H0 (minus n b)); Auto with arith. -Intros q Hq; Exists (S q). -Elim Hq; Intros r Hr. -Exists r; Simpl; Elim Hr; Intros. -Elim plus_assoc_l. -Elim H1; Auto with arith. -Intros gtbn. -Exists O; Exists n; Simpl; Auto with arith. -Save. - -Lemma modulo : (b:nat)(gt b O)-> - (a:nat){r:nat|(EX q:nat | (a=(plus (mult q b) r))/\(gt b r))}. -Intros b H a; Pattern a; Apply gt_wf_rec; Intros n H0. -Elim (le_gt_dec b n). -Intro lebn. -Elim (H0 (minus n b)); Auto with arith. -Intros r Hr; Exists r. -Elim Hr; Intros q Hq. -Elim Hq; Intros; Exists (S q); Simpl. -Elim plus_assoc_l. -Elim H1; Auto with arith. -Intros gtbn. -Exists n; Exists O; Simpl; Auto with arith. -Save. diff --git a/theories/Arith/intro.tex b/theories/Arith/intro.tex index 7d922c5b6e..655de34ca8 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 -- cgit v1.2.3