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.