1 files changed, 96 insertions, 0 deletions
diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v
new file mode 100644
index 00000000..8633986b
--- /dev/null
+++ b/theories/ZArith/Zwf.v
@@ -0,0 +1,96 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: Zwf.v,v 1.7.2.1 2004/07/16 19:31:22 herbelin Exp $ *)
+
+Require Import ZArith_base.
+Require Export Wf_nat.
+Require Import Omega.
+Open Local Scope Z_scope.
+
+(** Well-founded relations on Z. *)
+
+(** We define the following family of relations on [Z x Z]: 
+
+    [x (Zwf c) y]   iff   [x < y & c <= y]
+ *)
+
+Definition Zwf (c x y:Z) := 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|] *)
+
+Let f (z:Z) := Zabs_nat (z - c).
+
+Lemma Zwf_well_founded : well_founded (Zwf c).
+red in |- *; intros.
+assert (forall (n:nat) (a:Z), (f a < n)%nat \/ a < c -> Acc (Zwf c) a).
+clear a; simple induction n; intros.
+(** n= 0 *)
+case H; intros.
+case (lt_n_O (f a)); auto.
+apply Acc_intro; unfold Zwf in |- *; intros.
+assert False; omega || contradiction.
+(** inductive case *)
+case H0; clear H0; intro; auto.
+apply Acc_intro; intros.
+apply H.
+unfold Zwf in H1.
+case (Zle_or_lt c y); intro; auto with zarith.
+left.
+red in H0.
+apply lt_le_trans with (f a); auto with arith.
+unfold f in |- *.
+apply Zabs.Zabs_nat_lt; omega.
+apply (H (S (f a))); auto.
+Qed.
+
+End wf_proof.
+
+Hint 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 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|] *)
+
+Let f (z:Z) := Zabs_nat (c - z).
+
+Lemma Zwf_up_well_founded : well_founded (Zwf_up c).
+Proof.
+apply well_founded_lt_compat with (f := f).
+unfold Zwf_up, f in |- *.
+intros.
+apply Zabs.Zabs_nat_lt.
+unfold Zminus in |- *. split.
+apply Zle_left; intuition.
+apply Zplus_lt_compat_l; unfold Zlt in |- *; rewrite <- Zcompare_opp;
+ intuition.
+Qed.
+
+End wf_proof_up.
+
+Hint Resolve Zwf_up_well_founded: datatypes v62.
+\ No newline at end of file