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

2 files changed, 1 insertions, 86 deletions

diff --git a/contrib/correctness/Correctness.v b/contrib/correctness/Correctness.v
index 5cc7b6aa7..8f3f90b95 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 f51506d21..000000000
--- 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.