← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/ZArith/Zwf.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/ZArith/Zwf.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(* $Id: Zwf.v 9245 2006-10-17 12:53:34Z notin $ *)
 
10
 
 
11
Require Import ZArith_base.
 
12
Require Export Wf_nat.
 
13
Require Import Omega.
 
14
Open Local Scope Z_scope.
 
15
 
 
16
(** Well-founded relations on Z. *)
 
17
 
 
18
(** We define the following family of relations on [Z x Z]: 
 
19
 
 
20
    [x (Zwf c) y]   iff   [x < y & c <= y]
 
21
 *)
 
22
 
 
23
Definition Zwf (c x y:Z) := c <= y /\ x < y.
 
24
 
 
25
(** and we prove that [(Zwf c)] is well founded *)
 
26
 
 
27
Section wf_proof.
 
28
 
 
29
  Variable c : Z.
 
30
 
 
31
  (** The proof of well-foundness is classic: we do the proof by induction
 
32
      on a measure in nat, which is here [|x-c|] *)
 
33
 
 
34
  Let f (z:Z) := Zabs_nat (z - c).
 
35
 
 
36
  Lemma Zwf_well_founded : well_founded (Zwf c).
 
37
    red in |- *; intros.
 
38
    assert (forall (n:nat) (a:Z), (f a < n)%nat \/ a < c -> Acc (Zwf c) a).
 
39
    clear a; simple induction n; intros.
 
40
  (** n= 0 *)
 
41
    case H; intros.
 
42
    case (lt_n_O (f a)); auto.
 
43
    apply Acc_intro; unfold Zwf in |- *; intros.
 
44
    assert False; omega || contradiction.
 
45
  (** inductive case *)
 
46
    case H0; clear H0; intro; auto.
 
47
    apply Acc_intro; intros.
 
48
    apply H.
 
49
    unfold Zwf in H1.
 
50
    case (Zle_or_lt c y); intro; auto with zarith.
 
51
    left.
 
52
    red in H0.
 
53
    apply lt_le_trans with (f a); auto with arith.
 
54
    unfold f in |- *.
 
55
    apply Zabs.Zabs_nat_lt; omega.
 
56
    apply (H (S (f a))); auto.
 
57
  Qed.
 
58
 
 
59
End wf_proof.
 
60
 
 
61
Hint Resolve Zwf_well_founded: datatypes v62.
 
62
 
 
63
 
 
64
(** We also define the other family of relations:
 
65
 
 
66
    [x (Zwf_up c) y]   iff   [y < x <= c]
 
67
 *)
 
68
 
 
69
Definition Zwf_up (c x y:Z) := y < x <= c.
 
70
 
 
71
(** and we prove that [(Zwf_up c)] is well founded *)
 
72
 
 
73
Section wf_proof_up.
 
74
 
 
75
  Variable c : Z.
 
76
 
 
77
  (** The proof of well-foundness is classic: we do the proof by induction
 
78
      on a measure in nat, which is here [|c-x|] *)
 
79
 
 
80
  Let f (z:Z) := Zabs_nat (c - z).
 
81
 
 
82
  Lemma Zwf_up_well_founded : well_founded (Zwf_up c).
 
83
  Proof.
 
84
    apply well_founded_lt_compat with (f := f).
 
85
    unfold Zwf_up, f in |- *.
 
86
    intros.
 
87
    apply Zabs.Zabs_nat_lt.
 
88
    unfold Zminus in |- *. split.
 
89
    apply Zle_left; intuition.
 
90
    apply Zplus_lt_compat_l; unfold Zlt in |- *; rewrite <- Zcompare_opp;
 
91
      intuition.
 
92
  Qed.
 
93
 
 
94
End wf_proof_up.
 
95
 
 
96
Hint Resolve Zwf_up_well_founded: datatypes v62.