summaryrefslogtreecommitdiff
path: root/theories/ZArith/Zwf.v
blob: bd6172043e3b58e7af856b11240f2b97b811589c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
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 9245 2006-10-17 12:53:34Z notin $ *)

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.