← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Reals/Rsigma.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/Reals/Rsigma.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
(*i $Id: Rsigma.v 9454 2006-12-15 15:30:59Z bgregoir $ i*)
 
10
 
 
11
Require Import Rbase.
 
12
Require Import Rfunctions.
 
13
Require Import Rseries.
 
14
Require Import PartSum.
 
15
Open Local Scope R_scope.
 
16
 
 
17
Set Implicit Arguments.
 
18
 
 
19
Section Sigma.
 
20
 
 
21
  Variable f : nat -> R.
 
22
 
 
23
  Definition sigma (low high:nat) : R :=
 
24
    sum_f_R0 (fun k:nat => f (low + k)) (high - low).
 
25
 
 
26
  Theorem sigma_split :
 
27
    forall low high k:nat,
 
28
      (low <= k)%nat ->
 
29
      (k < high)%nat -> sigma low high = sigma low k + sigma (S k) high.
 
30
  Proof.
 
31
    intros; induction  k as [| k Hreck].
 
32
    cut (low = 0%nat).
 
33
    intro; rewrite H1; unfold sigma in |- *; rewrite <- minus_n_n;
 
34
      rewrite <- minus_n_O; simpl in |- *; replace (high - 1)%nat with (pred high).
 
35
    apply (decomp_sum (fun k:nat => f k)).
 
36
    assumption.
 
37
    apply pred_of_minus.
 
38
    inversion H; reflexivity.
 
39
    cut ((low <= k)%nat \/ low = S k).
 
40
    intro; elim H1; intro.
 
41
    replace (sigma low (S k)) with (sigma low k + f (S k)).
 
42
    rewrite Rplus_assoc;
 
43
      replace (f (S k) + sigma (S (S k)) high) with (sigma (S k) high).
 
44
    apply Hreck.
 
45
    assumption.
 
46
    apply lt_trans with (S k); [ apply lt_n_Sn | assumption ].
 
47
    unfold sigma in |- *; replace (high - S (S k))%nat with (pred (high - S k)).
 
48
    pattern (S k) at 3 in |- *; replace (S k) with (S k + 0)%nat;
 
49
      [ idtac | ring ].
 
50
    replace (sum_f_R0 (fun k0:nat => f (S (S k) + k0)) (pred (high - S k))) with
 
51
    (sum_f_R0 (fun k0:nat => f (S k + S k0)) (pred (high - S k))).
 
52
    apply (decomp_sum (fun i:nat => f (S k + i))).
 
53
    apply lt_minus_O_lt; assumption.
 
54
    apply sum_eq; intros; replace (S k + S i)%nat with (S (S k) + i)%nat.
 
55
    reflexivity.
 
56
    ring.
 
57
    replace (high - S (S k))%nat with (high - S k - 1)%nat.
 
58
    apply pred_of_minus.
 
59
    omega.
 
60
    unfold sigma in |- *; replace (S k - low)%nat with (S (k - low)).
 
61
    pattern (S k) at 1 in |- *; replace (S k) with (low + S (k - low))%nat.
 
62
    symmetry  in |- *; apply (tech5 (fun i:nat => f (low + i))).
 
63
    omega.
 
64
    omega.
 
65
    rewrite <- H2; unfold sigma in |- *; rewrite <- minus_n_n; simpl in |- *;
 
66
      replace (high - S low)%nat with (pred (high - low)).
 
67
    replace (sum_f_R0 (fun k0:nat => f (S (low + k0))) (pred (high - low))) with
 
68
    (sum_f_R0 (fun k0:nat => f (low + S k0)) (pred (high - low))).
 
69
    apply (decomp_sum (fun k0:nat => f (low + k0))).
 
70
    apply lt_minus_O_lt.
 
71
    apply le_lt_trans with (S k); [ rewrite H2; apply le_n | assumption ].
 
72
    apply sum_eq; intros; replace (S (low + i)) with (low + S i)%nat.
 
73
    reflexivity.
 
74
    ring.
 
75
    omega.
 
76
    inversion H; [ right; reflexivity | left; assumption ].
 
77
  Qed.
 
78
 
 
79
  Theorem sigma_diff :
 
80
    forall low high k:nat,
 
81
      (low <= k)%nat ->
 
82
      (k < high)%nat -> sigma low high - sigma low k = sigma (S k) high.
 
83
  Proof.
 
84
    intros low high k H1 H2; symmetry  in |- *; rewrite (sigma_split H1 H2); ring.
 
85
  Qed.
 
86
 
 
87
  Theorem sigma_diff_neg :
 
88
    forall low high k:nat,
 
89
      (low <= k)%nat ->
 
90
      (k < high)%nat -> sigma low k - sigma low high = - sigma (S k) high.
 
91
  Proof.
 
92
    intros low high k H1 H2; rewrite (sigma_split H1 H2); ring.
 
93
  Qed.
 
94
 
 
95
  Theorem sigma_first :
 
96
    forall low high:nat,
 
97
      (low < high)%nat -> sigma low high = f low + sigma (S low) high.
 
98
  Proof.
 
99
    intros low high H1; generalize (lt_le_S low high H1); intro H2;
 
100
      generalize (lt_le_weak low high H1); intro H3;
 
101
        replace (f low) with (sigma low low).
 
102
    apply sigma_split.
 
103
    apply le_n.
 
104
    assumption.
 
105
    unfold sigma in |- *; rewrite <- minus_n_n.
 
106
    simpl in |- *.
 
107
    replace (low + 0)%nat with low; [ reflexivity | ring ].
 
108
  Qed.
 
109
 
 
110
  Theorem sigma_last :
 
111
    forall low high:nat,
 
112
      (low < high)%nat -> sigma low high = f high + sigma low (pred high).
 
113
  Proof.
 
114
    intros low high H1; generalize (lt_le_S low high H1); intro H2;
 
115
      generalize (lt_le_weak low high H1); intro H3;
 
116
        replace (f high) with (sigma high high).
 
117
    rewrite Rplus_comm; cut (high = S (pred high)).
 
118
    intro; pattern high at 3 in |- *; rewrite H.
 
119
    apply sigma_split.
 
120
    apply le_S_n; rewrite <- H; apply lt_le_S; assumption.
 
121
    apply lt_pred_n_n; apply le_lt_trans with low; [ apply le_O_n | assumption ].
 
122
    apply S_pred with 0%nat; apply le_lt_trans with low;
 
123
      [ apply le_O_n | assumption ].
 
124
    unfold sigma in |- *; rewrite <- minus_n_n; simpl in |- *;
 
125
      replace (high + 0)%nat with high; [ reflexivity | ring ].
 
126
  Qed.
 
127
 
 
128
  Theorem sigma_eq_arg : forall low:nat, sigma low low = f low.
 
129
  Proof.
 
130
    intro; unfold sigma in |- *; rewrite <- minus_n_n.
 
131
    simpl in |- *; replace (low + 0)%nat with low; [ reflexivity | ring ].
 
132
  Qed.
 
133
 
 
134
End Sigma.