aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories7/ZArith/Zwf.v
blob: 5468f82cc8cda683592e9b68074f1272c9213e89 (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___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(* $Id$ *)

Require ZArith_base.
Require Export Wf_nat.
Require Omega.
V7only [Import Z_scope.].
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:Z][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|] *)

Local f := [z:Z](absolu (Zminus z c)).

Lemma Zwf_well_founded : (well_founded Z (Zwf c)).
Red; Intros.
Assert (n:nat)(a:Z)(lt (f a) n)\/(`a<c`) -> (Acc Z (Zwf c) a).
Clear a; Induction n; Intros.
(** n= 0 *)
Case H; Intros.
Case (lt_n_O (f a)); Auto.
Apply Acc_intro; Unfold Zwf; Intros.
Assert False;Omega Orelse 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.
Apply absolu_lt; Omega.
Apply (H (S (f a))); Auto.
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.