diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /theories/ZArith/Zwf.v |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'theories/ZArith/Zwf.v')
-rw-r--r-- | theories/ZArith/Zwf.v | 96 |
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 |