blob: 90754af3b4665b8fecf0ec2312465e02b257f107 (
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Require Import ZArith_base.
Require Export Wf_nat.
Require Import Omega.
Local Open 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) := Z.abs_nat (z - c).
Lemma Zwf_well_founded : well_founded (Zwf c).
red; 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; intros.
assert False; omega || contradiction.
(** inductive case *)
case H0; clear H0; intro; auto.
apply Acc_intro; intros.
apply H.
unfold Zwf in H1.
case (Z.le_gt_cases c y); intro; auto with zarith.
left.
red in H0.
apply lt_le_trans with (f a); auto with arith.
unfold f.
apply Zabs2Nat.inj_lt; omega.
apply (H (S (f a))); auto.
Qed.
End wf_proof.
Hint Resolve Zwf_well_founded: datatypes.
(** 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) := Z.abs_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.
intros.
apply Zabs2Nat.inj_lt; try (apply Z.le_0_sub; intuition).
now apply Z.sub_lt_mono_l.
Qed.
End wf_proof_up.
Hint Resolve Zwf_up_well_founded: datatypes.
|
