From 1afa589b280c6366c46d4c51184ee1bf5ef89f40 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 19 Jun 2002 13:35:20 +0000
Subject: deplacement contrib/correctness/ProgWf -> theories/ZArith/Zwf

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2795 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 .depend.coq                       | 13 ++++--
 Makefile                          |  6 +--
 contrib/correctness/Correctness.v |  2 +-
 contrib/correctness/ProgWf.v      | 85 ---------------------------------------
 theories/ZArith/Zwf.v             | 83 ++++++++++++++++++++++++++++++++++++++
 5 files changed, 96 insertions(+), 93 deletions(-)
 delete mode 100644 contrib/correctness/ProgWf.v
 create mode 100644 theories/ZArith/Zwf.v

diff --git a/.depend.coq b/.depend.coq
index 53788ead05..32a312384c 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -3,12 +3,11 @@ contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/fourier/Fourier_ut
 contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/Rbase.vo
 contrib/correctness/Tuples.vo: contrib/correctness/Tuples.v
 contrib/correctness/Sorted.vo: contrib/correctness/Sorted.v contrib/correctness/Arrays.vo contrib/correctness/ArrayPermut.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
-contrib/correctness/ProgWf.vo: contrib/correctness/ProgWf.v theories/ZArith/ZArith.vo theories/Arith/Wf_nat.vo
 contrib/correctness/ProgInt.vo: contrib/correctness/ProgInt.v theories/ZArith/ZArith.vo theories/ZArith/ZArith_dec.vo
 contrib/correctness/ProgBool.vo: contrib/correctness/ProgBool.v theories/Arith/Compare_dec.vo theories/Arith/Peano_dec.vo theories/ZArith/ZArith.vo theories/Bool/Sumbool.vo
 contrib/correctness/ArrayPermut.vo: contrib/correctness/ArrayPermut.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo contrib/correctness/Exchange.vo contrib/omega/Omega.vo
 contrib/correctness/Exchange.vo: contrib/correctness/Exchange.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo
-contrib/correctness/Correctness.vo: contrib/correctness/Correctness.v contrib/correctness/Tuples.vo contrib/correctness/ProgInt.vo contrib/correctness/ProgBool.vo contrib/correctness/ProgWf.vo contrib/correctness/Arrays.vo
+contrib/correctness/Correctness.vo: contrib/correctness/Correctness.v contrib/correctness/Tuples.vo contrib/correctness/ProgInt.vo contrib/correctness/ProgBool.vo theories/ZArith/Zwf.vo contrib/correctness/Arrays.vo
 contrib/correctness/Arrays.vo: contrib/correctness/Arrays.v contrib/correctness/ProgInt.vo
 contrib/field/Field.vo: contrib/field/Field.v contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo contrib/field/Field_Tactic.vo
 contrib/field/Field_Tactic.vo: contrib/field/Field_Tactic.v contrib/ring/Ring.vo contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo
@@ -33,8 +32,13 @@ theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/PolyList.vo the
 theories/Setoids/Setoid.vo: theories/Setoids/Setoid.v
 theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rsigma.vo theories/Reals/Rlimit.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/Rgeom.vo theories/Reals/Rderiv.vo theories/Reals/Rseries.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Ranalysis.vo theories/Reals/DiscrR.vo theories/Reals/SplitRmult.vo theories/Reals/SplitAbsolu.vo
 theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/Rbase.vo theories/Reals/R_sqr.vo theories/Reals/Rtrigo.vo
-theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo
-theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/ZArith/ZArith.vo theories/Logic/Classical_Prop.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/R_sqr.vo theories/Reals/Rfunctions.vo theories/Reals/Rsigma.vo
+theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Ranalysis4.vo
+theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo
+theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo
+theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo contrib/omega/Omega.vo
+theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Init/Specif.vo
+theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/ZArith/ZArith.vo theories/Logic/Classical_Prop.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/R_sqr.vo theories/Reals/Rfunctions.vo theories/Reals/Rsigma.vo theories/Reals/Rtrigo_def.vo
+theories/Reals/Rtrigo_def.vo: theories/Reals/Rtrigo_def.v theories/Arith/Max.vo theories/Reals/Raxioms.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Rtrigo_fun.vo theories/Init/Specif.vo
 theories/Reals/Rsigma.vo: theories/Reals/Rsigma.v theories/Reals/Rbase.vo
 theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/Rseries.vo
 theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rderiv.vo theories/Logic/Classical.vo theories/Arith/Compare.vo
@@ -111,6 +115,7 @@ theories/Lists/Streams.vo: theories/Lists/Streams.v
 theories/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/PolyList.vo
 theories/Lists/PolyListSyntax.vo: theories/Lists/PolyListSyntax.v theories/Lists/PolyList.vo
 theories/Lists/List.vo: theories/Lists/List.v theories/Arith/Le.vo
+theories/ZArith/Zwf.vo: theories/ZArith/Zwf.v theories/ZArith/ZArith.vo theories/Arith/Wf_nat.vo
 theories/ZArith/Zsqrt.vo: theories/ZArith/Zsqrt.v theories/ZArith/ZArith.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
 theories/ZArith/Zdiv.vo: theories/ZArith/Zdiv.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo contrib/ring/ZArithRing.vo theories/ZArith/Zcomplements.vo
 theories/ZArith/Zcomplements.vo: theories/ZArith/Zcomplements.v theories/ZArith/ZArith.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
diff --git a/Makefile b/Makefile
index 15e2d236dc..84c8059581 100644
--- a/Makefile
+++ b/Makefile
@@ -455,7 +455,8 @@ ZARITHVO=theories/ZArith/Wf_Z.vo        theories/ZArith/Zsyntax.vo \
 	 theories/ZArith/Zmisc.vo       theories/ZArith/zarith_aux.vo \
 	 theories/ZArith/Zhints.vo	theories/ZArith/Zlogarithm.vo \
 	 theories/ZArith/Zpower.vo 	theories/ZArith/Zcomplements.vo \
-	 theories/ZArith/Zdiv.vo	theories/ZArith/Zsqrt.vo
+	 theories/ZArith/Zdiv.vo	theories/ZArith/Zsqrt.vo \
+	 theories/ZArith/Zwf.vo
 
 LISTSVO=theories/Lists/List.vo      theories/Lists/PolyListSyntax.vo \
         theories/Lists/ListSet.vo   theories/Lists/Streams.vo \
@@ -558,8 +559,7 @@ CORRECTNESSVO=contrib/correctness/Arrays.vo				\
 	contrib/correctness/Exchange.vo					\
 	contrib/correctness/ArrayPermut.vo				\
 	contrib/correctness/ProgBool.vo contrib/correctness/ProgInt.vo	\
-	contrib/correctness/ProgWf.vo contrib/correctness/Sorted.vo	\
-	contrib/correctness/Tuples.vo
+	contrib/correctness/Sorted.vo	contrib/correctness/Tuples.vo
 #	contrib/correctness/ProgramsExtraction.vo			
 
 OMEGAVO = contrib/omega/Omega.vo
diff --git a/contrib/correctness/Correctness.v b/contrib/correctness/Correctness.v
index 5cc7b6aa74..8f3f90b95e 100644
--- a/contrib/correctness/Correctness.v
+++ b/contrib/correctness/Correctness.v
@@ -16,7 +16,7 @@ Require Export Tuples.
 
 Require Export ProgInt.
 Require Export ProgBool.
-Require Export ProgWf.
+Require Export Zwf.
 
 Require Export Arrays.
 
diff --git a/contrib/correctness/ProgWf.v b/contrib/correctness/ProgWf.v
deleted file mode 100644
index f51506d21c..0000000000
--- a/contrib/correctness/ProgWf.v
+++ /dev/null
@@ -1,85 +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       *)
-(***********************************************************************)
-
-(* Certification of Imperative Programs / Jean-Christophe Filliātre *)
-
-(* $Id$ *)
-
-Require ZArith.
-Require Export Wf_nat.
-
-(* Well-founded relations on Z. *)
-
-(* We define the following family of relations on ZxZ : 
- * 
- *      x (Zwf c) y   iff   c <= x < y
- *)
-
-Definition Zwf := [c:Z][x,y:Z] `c <= x` /\ `c <= y` /\ `x < y`.
-
-
-(* and we prove that (Zwf c) is well founded *)
-
-Section wf_proof.
-
-Variable c : Z.
-
-(* The proof of well-foundness is classic : we do the proof by induction
- * on a measure in nat, which is here |x-c| *)
-
-Local f := [z:Z](absolu (Zminus z c)).
-
-Lemma Zwf_well_founded : (well_founded Z (Zwf c)).
-Proof.
-Apply well_founded_lt_compat with f:=f.
-Unfold Zwf f.
-Intros.
-Apply absolu_lt.
-Unfold Zminus. Split.
-Apply Zle_left; Intuition.
-Rewrite (Zplus_sym x `-c`). Rewrite (Zplus_sym y `-c`).
-Apply Zlt_reg_l; Intuition.
-Save.
-
-End wf_proof.
-
-Hints Resolve Zwf_well_founded : datatypes v62.
-
-
-(* We also define the other family of relations :
- *
- *      x (Zwf_up c) y   iff   y < x <= c
- *)
-
-Definition Zwf_up := [c:Z][x,y:Z] `y < x <= c`.
-
-(* and we prove that (Zwf_up c) is well founded *)
-
-Section wf_proof_up.
-
-Variable c : Z.
-
-(* The proof of well-foundness is classic : we do the proof by induction
- * on a measure in nat, which is here |c-x| *)
-
-Local f := [z:Z](absolu (Zminus c z)).
-
-Lemma Zwf_up_well_founded : (well_founded Z (Zwf_up c)).
-Proof.
-Apply well_founded_lt_compat with f:=f.
-Unfold Zwf_up f.
-Intros.
-Apply absolu_lt.
-Unfold Zminus. Split.
-Apply Zle_left; Intuition.
-Apply Zlt_reg_l; Unfold Zlt; Rewrite <- Zcompare_Zopp; Intuition.
-Save.
-
-End wf_proof_up.
-
-Hints Resolve Zwf_up_well_founded : datatypes v62.
diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v
new file mode 100644
index 0000000000..386317e831
--- /dev/null
+++ b/theories/ZArith/Zwf.v
@@ -0,0 +1,83 @@
+(***********************************************************************)
+(*  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 ZArith.
+Require Export Wf_nat.
+
+(** Well-founded relations on Z. *)
+
+(** We define the following family of relations on [Z x Z]: 
+
+    [x (Zwf c) y]   iff   [c <= x < y]
+ *)
+
+Definition Zwf := [c:Z][x,y:Z] `c <= x` /\ `c <= y` /\ `x < y`.
+
+
+(** and we prove that [(Zwf c)] is well founded *)
+
+Section wf_proof.
+
+Variable c : Z.
+
+(** The proof of well-foundness is classic: we do the proof by induction
+    on a measure in nat, which is here [|x-c|] *)
+
+Local f := [z:Z](absolu (Zminus z c)).
+
+Lemma Zwf_well_founded : (well_founded Z (Zwf c)).
+Proof.
+Apply well_founded_lt_compat with f:=f.
+Unfold Zwf f.
+Intros.
+Apply absolu_lt.
+Unfold Zminus. Split.
+Apply Zle_left; Intuition.
+Rewrite (Zplus_sym x `-c`). Rewrite (Zplus_sym y `-c`).
+Apply Zlt_reg_l; Intuition.
+Save.
+
+End wf_proof.
+
+Hints Resolve Zwf_well_founded : datatypes v62.
+
+
+(** We also define the other family of relations:
+
+    [x (Zwf_up c) y]   iff   [y < x <= c]
+ *)
+
+Definition Zwf_up := [c:Z][x,y:Z] `y < x <= c`.
+
+(** and we prove that [(Zwf_up c)] is well founded *)
+
+Section wf_proof_up.
+
+Variable c : Z.
+
+(** The proof of well-foundness is classic: we do the proof by induction
+    on a measure in nat, which is here [|c-x|] *)
+
+Local f := [z:Z](absolu (Zminus c z)).
+
+Lemma Zwf_up_well_founded : (well_founded Z (Zwf_up c)).
+Proof.
+Apply well_founded_lt_compat with f:=f.
+Unfold Zwf_up f.
+Intros.
+Apply absolu_lt.
+Unfold Zminus. Split.
+Apply Zle_left; Intuition.
+Apply Zlt_reg_l; Unfold Zlt; Rewrite <- Zcompare_Zopp; Intuition.
+Save.
+
+End wf_proof_up.
+
+Hints Resolve Zwf_up_well_founded : datatypes v62.
-- 
cgit v1.2.3