← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Reals/Binomial.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/Binomial.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: Binomial.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
10
 
 
11
Require Import Rbase.
 
12
Require Import Rfunctions.
 
13
Require Import PartSum.
 
14
Open Local Scope R_scope.
 
15
 
 
16
Definition C (n p:nat) : R :=
 
17
  INR (fact n) / (INR (fact p) * INR (fact (n - p))).
 
18
 
 
19
Lemma pascal_step1 : forall n i:nat, (i <= n)%nat -> C n i = C n (n - i).
 
20
Proof.
 
21
  intros; unfold C in |- *; replace (n - (n - i))%nat with i.
 
22
  rewrite Rmult_comm.
 
23
  reflexivity.
 
24
  apply plus_minus; rewrite plus_comm; apply le_plus_minus; assumption.
 
25
Qed.
 
26
 
 
27
Lemma pascal_step2 :
 
28
  forall n i:nat,
 
29
    (i <= n)%nat -> C (S n) i = INR (S n) / INR (S n - i) * C n i.
 
30
Proof.
 
31
  intros; unfold C in |- *; replace (S n - i)%nat with (S (n - i)).
 
32
  cut (forall n:nat, fact (S n) = (S n * fact n)%nat).
 
33
  intro; repeat rewrite H0.
 
34
  unfold Rdiv in |- *; repeat rewrite mult_INR; repeat rewrite Rinv_mult_distr.
 
35
  ring.
 
36
  apply INR_fact_neq_0.
 
37
  apply INR_fact_neq_0.
 
38
  apply not_O_INR; discriminate.
 
39
  apply INR_fact_neq_0.
 
40
  apply INR_fact_neq_0.
 
41
  apply prod_neq_R0.
 
42
  apply not_O_INR; discriminate.
 
43
  apply INR_fact_neq_0.
 
44
  intro; reflexivity.
 
45
  apply minus_Sn_m; assumption.
 
46
Qed.
 
47
 
 
48
Lemma pascal_step3 :
 
49
  forall n i:nat, (i < n)%nat -> C n (S i) = INR (n - i) / INR (S i) * C n i.
 
50
Proof.
 
51
  intros; unfold C in |- *.
 
52
  cut (forall n:nat, fact (S n) = (S n * fact n)%nat).
 
53
  intro.
 
54
  cut ((n - i)%nat = S (n - S i)).
 
55
  intro.
 
56
  pattern (n - i)%nat at 2 in |- *; rewrite H1.
 
57
  repeat rewrite H0; unfold Rdiv in |- *; repeat rewrite mult_INR;
 
58
    repeat rewrite Rinv_mult_distr.
 
59
  rewrite <- H1; rewrite (Rmult_comm (/ INR (n - i)));
 
60
    repeat rewrite Rmult_assoc; rewrite (Rmult_comm (INR (n - i)));
 
61
      repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
 
62
  ring.
 
63
  apply not_O_INR; apply minus_neq_O; assumption.
 
64
  apply not_O_INR; discriminate.
 
65
  apply INR_fact_neq_0.
 
66
  apply INR_fact_neq_0.
 
67
  apply prod_neq_R0; [ apply not_O_INR; discriminate | apply INR_fact_neq_0 ].
 
68
  apply not_O_INR; discriminate.
 
69
  apply INR_fact_neq_0.
 
70
  apply prod_neq_R0; [ apply not_O_INR; discriminate | apply INR_fact_neq_0 ].
 
71
  apply INR_fact_neq_0.
 
72
  rewrite minus_Sn_m.
 
73
  simpl in |- *; reflexivity.
 
74
  apply lt_le_S; assumption.
 
75
  intro; reflexivity.
 
76
Qed.
 
77
 
 
78
  (**********)
 
79
Lemma pascal :
 
80
  forall n i:nat, (i < n)%nat -> C n i + C n (S i) = C (S n) (S i).
 
81
Proof.
 
82
  intros.
 
83
  rewrite pascal_step3; [ idtac | assumption ].
 
84
  replace (C n i + INR (n - i) / INR (S i) * C n i) with
 
85
    (C n i * (1 + INR (n - i) / INR (S i))); [ idtac | ring ].
 
86
  replace (1 + INR (n - i) / INR (S i)) with (INR (S n) / INR (S i)).
 
87
  rewrite pascal_step1.
 
88
  rewrite Rmult_comm; replace (S i) with (S n - (n - i))%nat.
 
89
  rewrite <- pascal_step2.
 
90
  apply pascal_step1.
 
91
  apply le_trans with n.
 
92
  apply le_minusni_n.
 
93
  apply lt_le_weak; assumption.
 
94
  apply le_n_Sn.
 
95
  apply le_minusni_n.
 
96
  apply lt_le_weak; assumption.
 
97
  rewrite <- minus_Sn_m.
 
98
  cut ((n - (n - i))%nat = i).
 
99
  intro; rewrite H0; reflexivity.
 
100
  symmetry  in |- *; apply plus_minus.
 
101
  rewrite plus_comm; rewrite le_plus_minus_r.
 
102
  reflexivity.
 
103
  apply lt_le_weak; assumption.
 
104
  apply le_minusni_n; apply lt_le_weak; assumption.
 
105
  apply lt_le_weak; assumption.
 
106
  unfold Rdiv in |- *.
 
107
  repeat rewrite S_INR.
 
108
  rewrite minus_INR.
 
109
  cut (INR i + 1 <> 0).
 
110
  intro.
 
111
  apply Rmult_eq_reg_l with (INR i + 1); [ idtac | assumption ].
 
112
  rewrite Rmult_plus_distr_l.
 
113
  rewrite Rmult_1_r.
 
114
  do 2 rewrite (Rmult_comm (INR i + 1)).
 
115
  repeat rewrite Rmult_assoc.
 
116
  rewrite <- Rinv_l_sym; [ idtac | assumption ].
 
117
  ring.
 
118
  rewrite <- S_INR.
 
119
  apply not_O_INR; discriminate.
 
120
  apply lt_le_weak; assumption.
 
121
Qed.
 
122
 
 
123
  (*********************)
 
124
  (*********************)
 
125
Lemma binomial :
 
126
  forall (x y:R) (n:nat),
 
127
    (x + y) ^ n = sum_f_R0 (fun i:nat => C n i * x ^ i * y ^ (n - i)) n.
 
128
Proof.
 
129
  intros; induction  n as [| n Hrecn].
 
130
  unfold C in |- *; simpl in |- *; unfold Rdiv in |- *;
 
131
    repeat rewrite Rmult_1_r; rewrite Rinv_1; ring.
 
132
  pattern (S n) at 1 in |- *; replace (S n) with (n + 1)%nat; [ idtac | ring ].
 
133
  rewrite pow_add; rewrite Hrecn.
 
134
  replace ((x + y) ^ 1) with (x + y); [ idtac | simpl in |- *; ring ].
 
135
  rewrite tech5.
 
136
  cut (forall p:nat, C p p = 1).
 
137
  cut (forall p:nat, C p 0 = 1).
 
138
  intros; rewrite H0; rewrite <- minus_n_n; rewrite Rmult_1_l.
 
139
  replace (y ^ 0) with 1; [ rewrite Rmult_1_r | simpl in |- *; reflexivity ].
 
140
  induction  n as [| n Hrecn0].
 
141
  simpl in |- *; do 2 rewrite H; ring.
 
142
  (* N >= 1 *)
 
143
  set (N := S n).
 
144
  rewrite Rmult_plus_distr_l.
 
145
  replace (sum_f_R0 (fun i:nat => C N i * x ^ i * y ^ (N - i)) N * x) with
 
146
    (sum_f_R0 (fun i:nat => C N i * x ^ S i * y ^ (N - i)) N).
 
147
  replace (sum_f_R0 (fun i:nat => C N i * x ^ i * y ^ (N - i)) N * y) with
 
148
    (sum_f_R0 (fun i:nat => C N i * x ^ i * y ^ (S N - i)) N).
 
149
  rewrite (decomp_sum (fun i:nat => C (S N) i * x ^ i * y ^ (S N - i)) N).
 
150
  rewrite H; replace (x ^ 0) with 1; [ idtac | reflexivity ].
 
151
  do 2 rewrite Rmult_1_l.
 
152
  replace (S N - 0)%nat with (S N); [ idtac | reflexivity ].
 
153
  set (An := fun i:nat => C N i * x ^ S i * y ^ (N - i)).
 
154
  set (Bn := fun i:nat => C N (S i) * x ^ S i * y ^ (N - i)).
 
155
  replace (pred N) with n.
 
156
  replace (sum_f_R0 (fun i:nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) n)
 
157
    with (sum_f_R0 (fun i:nat => An i + Bn i) n).
 
158
  rewrite plus_sum.
 
159
  replace (x ^ S N) with (An (S n)).
 
160
  rewrite (Rplus_comm (sum_f_R0 An n)).
 
161
  repeat rewrite Rplus_assoc.
 
162
  rewrite <- tech5.
 
163
  fold N in |- *.
 
164
  set (Cn := fun i:nat => C N i * x ^ i * y ^ (S N - i)).
 
165
  cut (forall i:nat, (i < N)%nat -> Cn (S i) = Bn i).
 
166
  intro; replace (sum_f_R0 Bn n) with (sum_f_R0 (fun i:nat => Cn (S i)) n).
 
167
  replace (y ^ S N) with (Cn 0%nat).
 
168
  rewrite <- Rplus_assoc; rewrite (decomp_sum Cn N).
 
169
  replace (pred N) with n.
 
170
  ring.
 
171
  unfold N in |- *; simpl in |- *; reflexivity.
 
172
  unfold N in |- *; apply lt_O_Sn.
 
173
  unfold Cn in |- *; rewrite H; simpl in |- *; ring.
 
174
  apply sum_eq.
 
175
  intros; apply H1.
 
176
  unfold N in |- *; apply le_lt_trans with n; [ assumption | apply lt_n_Sn ].
 
177
  intros; unfold Bn, Cn in |- *.
 
178
  replace (S N - S i)%nat with (N - i)%nat; reflexivity.
 
179
  unfold An in |- *; fold N in |- *; rewrite <- minus_n_n; rewrite H0;
 
180
    simpl in |- *; ring.
 
181
  apply sum_eq.
 
182
  intros; unfold An, Bn in |- *; replace (S N - S i)%nat with (N - i)%nat;
 
183
    [ idtac | reflexivity ].
 
184
  rewrite <- pascal;
 
185
    [ ring
 
186
      | apply le_lt_trans with n; [ assumption | unfold N in |- *; apply lt_n_Sn ] ].
 
187
  unfold N in |- *; reflexivity.
 
188
  unfold N in |- *; apply lt_O_Sn.
 
189
  rewrite <- (Rmult_comm y); rewrite scal_sum; apply sum_eq.
 
190
  intros; replace (S N - i)%nat with (S (N - i)).
 
191
  replace (S (N - i)) with (N - i + 1)%nat; [ idtac | ring ].
 
192
  rewrite pow_add; replace (y ^ 1) with y; [ idtac | simpl in |- *; ring ];
 
193
    ring.
 
194
  apply minus_Sn_m; assumption.
 
195
  rewrite <- (Rmult_comm x); rewrite scal_sum; apply sum_eq.
 
196
  intros; replace (S i) with (i + 1)%nat; [ idtac | ring ]; rewrite pow_add;
 
197
    replace (x ^ 1) with x; [ idtac | simpl in |- *; ring ]; 
 
198
      ring.
 
199
  intro; unfold C in |- *.
 
200
  replace (INR (fact 0)) with 1; [ idtac | reflexivity ].
 
201
  replace (p - 0)%nat with p; [ idtac | apply minus_n_O ].
 
202
  rewrite Rmult_1_l; unfold Rdiv in |- *; rewrite <- Rinv_r_sym;
 
203
    [ reflexivity | apply INR_fact_neq_0 ].
 
204
  intro; unfold C in |- *.
 
205
  replace (p - p)%nat with 0%nat; [ idtac | apply minus_n_n ].
 
206
  replace (INR (fact 0)) with 1; [ idtac | reflexivity ].
 
207
  rewrite Rmult_1_r; unfold Rdiv in |- *; rewrite <- Rinv_r_sym;
 
208
    [ reflexivity | apply INR_fact_neq_0 ].
 
209
Qed.