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
---
 contrib/correctness/Correctness.v |  2 +-
 contrib/correctness/ProgWf.v      | 85 ---------------------------------------
 2 files changed, 1 insertion(+), 86 deletions(-)
 delete mode 100644 contrib/correctness/ProgWf.v

(limited to 'contrib')

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.
-- 
cgit v1.2.3