(** * binomial coefficients, polynomials, continuity, Weierstrass' theorem through Bernstein's polynomials *)
(*
FIRST MINI-PROJECT
During the next three sessions, we will prove Weierstrass' theorem, using this template file.
As usual, I'll ask you to send me this file back every week.
You don't have to do everything for the first week: I'll tell you where to stop during the session.
I indicate the number of lines I used in my answer file, as before, this is just an indication, so that you can estimate whether you are proceeding efficiently, or through a long detour.
The shorter your proofs the better, but don't overdo it either: if you are able to get all proofs done, that's already good!
*)
(* REMINDER:
Basic tactics:
intro, intros, destruct, intros [[H1 H2]| ->], ...
apply, assumption,
induction, induction n as [|n IHn]
rewrite H, rewrite (H 5), rewrite <-H, rewrite H by ...
reflexivity
simpl (to simplify computations)
unfold D, fold D (to unfold a defnition)
replace a with b, replace a with b by ... (a maybe a pattern)
set(n:=e) (giving a name to a sub-expression - e may be a pattern)
assert(H: T), assert(H: T) by ... (intermediate lemma)
pose M, pose M as H (add a result to the context - sometimes useful to help lia/lra)
Tactic combinators:
tac1; tac2 (apply tac2 to all subgoals generated by tac1)
now tac (apply tac and conclude with easy steps)
High-level tactics:
tauto propositional tautologies
ring, ring_simplify rings - polynomials (processes only the conclusion of the current goal)
field, field_simplify fields (idem)
lia, lra linear integer/real arithmetic (exploit the hypotheses of the goal but doesn't deal with multiplication)
Useful commands (in CoqIDE, you often have to use the corresponding menu)
About D. [C-c C-a C-b .. RET] informations about definition D
Print D. [C-c C-a C-p .. RET] body (and type) of definition D
Check t. [C-c C-a C-b .. RET] prints the type of expression t (if typeable)
Locate "_ - _". [C-c C-a C-l .. RET] find the content of a notation in the various scopes
Search t1 t2 -t3 [C-c C-a C-a .. RET] print all lemmas whose statement contains terms/patterns t1 t2 but not t3
*)
(* GOOD CODING PRACTICES:
- only one induction per lemma
- ident the code using bullets
- name explicitly all hypotheses you plan to mention later in the proof
(e.g., [intros. apply H42] is forbidden )
- stay as high-level as possible: use forward-reasonning and exploit the power of lia/lra/ring/field
*)
(** first loading a few libraries *)
Require Import Setoid Morphisms.
Require Import List.
Import ListNotations Nat.
Arguments sub !n !m /.
Require Import Psatz Rbase Rfunctions Ranalysis.
Local Open Scope R_scope.
(** and defining a few helpers which are missing from the standard library *)
Lemma INR0: INR O = 0. Proof. reflexivity. Qed.
Definition INRS := S_INR.
Lemma INRpred n: (0 INR (pred n) = INR n - 1.
Proof. destruct n. lia. rewrite INRS. simpl. lra. Qed.
Opaque INR.
Lemma Rdiv1 x: x/1 = x.
Proof. field. Qed.
Ltac field_simpl := field_simplify; rewrite ?Rdiv1.
Instance Rle_PreOrder: PreOrder Rle.
Proof. constructor; cbv; intros; lra. Qed.
Instance Rlt_PreOrder: Transitive Rlt.
Proof. cbv; intros; lra. Qed.
Instance Rlt_Rle: subrelation Rlt Rle.
Proof. cbv. tauto. Qed.
Instance Rplus_Rle: Proper (Rle ==> Rle ==> Rle) Rplus.
Proof. repeat intro. lra. Qed.
(** ** FIRST SESSION: binomials coefficients *)
(** *** factorial *)
(* factorial function, from nat to R *)
Fixpoint fact (n: nat) :=
match n with
| 0 => 1
| S n' => INR n * fact n'
end.
(* [fact] always returns a positive number *)
Lemma fact_gt_0 n: fact n > 0.
Proof.
induction n; simpl.
- lra.
- apply Rmult_gt_0_compat; trivial. apply lt_0_INR. lia.
Qed.
(* and thus a non-zero value *)
Lemma fact_neq_0 n: fact n <> 0.
Proof. pose (fact_gt_0 n). lra. Qed.
(* a simple tactic to discharge goals generated by [field]
(i.e, facts that some values are non-zero)
you can use it below
*)
Ltac neq_0 := repeat split; solve [ apply not_O_INR; lia | apply fact_neq_0 ].
(** *** binomial coefficients *)
Definition C n p := fact n / (fact p * fact (n - p)).
Lemma Cnn: forall n, C n n = 1.
Admitted. (* TODO, feasible 2 lines *)
Lemma Cn0: forall n, C n 0 = 1.
Admitted. (* TODO, feasible in 2 lines *)
Lemma pascal1: forall n i, (i <= n)%nat -> C n i = C n (n - i).
Admitted. (* TODO, feasible in 3 lines *)
Lemma pascal2: forall n i,
(i <= n)%nat -> C (S n) i = INR (S n) / INR (S n - i) * C n i.
Admitted. (* TODO, feasible in 3 lines *)
Lemma pascal3: forall n i,
(i < n)%nat -> C n (S i) = INR (n - i) / INR (S i) * C n i.
Admitted. (* TODO, feasible in 3 lines *)
Lemma pascal4: forall n i, C (S n) (S i) = INR (S n) / INR (S i) * C n i.
Admitted. (* TODO, feasible in 1 lines *)
Lemma pascal: forall n i,
(i < n)%nat -> C (S n) (S i) = C n i + C n (S i).
Admitted. (* TODO, feasible in 4 lines *)
(* a variant of [pascal4] which may be useful later *)
Lemma pascal4': forall n i, (0 INR i / INR n * C n i = C (pred n) (pred i).
Proof.
intros.
replace n with (S (pred n)) by lia.
replace i with (S (pred i)) by lia.
rewrite pascal4 at 1 by assumption.
simpl. field; neq_0.
Qed.
(** *** finite sums *)
(* [sum f n] computes f 0 + ... + f n, for a natural number n and a function f: nat -> R *)
Fixpoint sum n f :=
match n with
| O => 0
| S n => sum n f + f n
end.
Lemma sum0 f: sum 0 f = 0.
Admitted. (* TODO, 1 line *)
Lemma sum1 f: sum 1 f = f O.
Admitted. (* TODO, 1 line *)
Lemma sumS_last n f: sum (S n) f = sum n f + f n.
Admitted. (* TODO, 1 line *)
Lemma sumS_first n f: sum (S n) f = f 0%nat + sum n (fun i => f (S i)).
Admitted. (* TODO, 2 lines *)
(* the above lemmas are nice to use when we have an explicit successor (S);
the ones below are equivalent, and easier to use when the successor is not explicit *)
Lemma sum_last n f: (0 sum n f = sum (pred n) f + f (pred n).
Proof. destruct n. lia. reflexivity. Qed.
Lemma sum_first n f: (0 sum n f = f 0%nat + sum (pred n) (fun i => f (S i)).
Proof. destruct n. lia. intros _. apply sumS_first. Qed.
Lemma sum_rev n f: sum n f = sum n (fun i => f (n-S i)%nat).
Admitted. (* TODO, 3 lines *)
Lemma xsum n x f: x * sum n f = sum n (fun i => x * f i).
Admitted. (* TODO, 3 lines *)
(* the two lemmas below can be useful because [rewrite] cannot rewrite
inside the body of sums (under lambdas in general) *)
Lemma sum_eq n f g: (forall i, (i f i = g i) -> sum n f = sum n g.
Proof.
intros H; induction n; simpl.
- reflexivity.
- rewrite H by lia. rewrite IHn. reflexivity. intros. apply H. lia.
Qed.
Lemma sum_le n f g: (forall i, (i f i <= g i) -> sum n f <= sum n g.
Proof.
intros H; induction n; simpl.
- reflexivity.
- rewrite H by lia. rewrite IHn. reflexivity. intros. apply H. lia.
Qed.
(* using the following lines, we tell Coq rewriting tools that rewriting under sums is ok (not however that we cannot exploit the bound on indices by doing so: the above lemmas are stronger) *)
Instance sum_pwr_eq n: Proper (pointwise_relation nat eq ==> eq) (sum n).
Proof. intros ???. apply sum_eq. intros ? _. apply H. Qed.
Instance sum_pwr_le n: Proper (pointwise_relation nat Rle ==> Rle) (sum n).
Proof. intros ???. apply sum_le. intros ? _. apply H. Qed.
Lemma split_sum (p: nat -> bool) n f:
sum n f =
sum n (fun i => if p i then f i else 0) +
sum n (fun i => if p i then 0 else f i).
Admitted. (* TODO, 3 lines *)
Lemma Rabs_sum n f: Rabs (sum n f) <= sum n (fun i => Rabs (f i)).
Admitted. (* TODO, 3 lines *)
Opaque sum.
(** ** binomial equation *)
Lemma cancel_r x y z: y-x=z-x -> y=z.
Admitted. (* TODO, feasible in 3 letters and a dot;
this lemma can be used as follows:
[apply cancel_r with (2*x^3)] *)
Proposition binomial: forall x y n,
(x + y) ^ n = sum (S n) (fun i => C n i * x ^ i * y ^ (n - i)).
Proof.
intros; induction n as [|n IH].
(* TODO, harder, feasible in 12 lines + a lemma feasible in 2 lines *)
Admitted.
Corollary binomial' x n: sum (S n) (fun k => C n k * x^k * (1-x)^(n-k)) = 1.
Admitted. (* TODO, 2 lines *)
(* like before with [sum_first/last], the variant below is sometimes more convenient *)
Corollary binomial'' x n: (0 sum n (fun k => C (pred n) k * x^k * (1-x)^(pred n-k)) = 1.
Proof.
intro. replace n with (S (pred n)) by lia. apply binomial'.
Qed.
Corollary pow2n: forall n, sum (S n) (fun i => C n i) = 2^n.
Admitted. (* TODO, 3 lines *)
Corollary powk2n: forall n, sum (S n) (fun i => INR i * C n i) = INR n * 2^(n-1).
Admitted. (* TODO, 6 lines *)
(** ** SECOND SESSION: polynomials, continuity *)
(** *** polynomials *)
(** we represent polynomials by their list of coefficients
[a;b;c] represents a+bX+cX^2
note that we do *not* impose that the last coefficient must be non-zero.
*)
Definition poly := list R.
Fixpoint eval (P: poly) (x: R): R :=
match P with
| [] => 0
| a::Q => a + x * eval Q x
end.
Definition pcst a: poly := ...
Lemma eval_cst a x: eval (pcst a) x = a.
Admitted. (* TODO, 1 line *)
Definition pid: poly := ...
Lemma eval_id x: eval pid x = x.
Admitted. (* TODO, 1 line *)
Fixpoint pxk (k: nat): poly :=
match k with
| O => ...
| S k => ...
end.
Lemma eval_xk k x: eval (pxk k) x = x^k.
Admitted. (* TODO, 1 line *)
Fixpoint pplus (P Q: poly): poly :=
match P,Q with
...
end.
Arguments pplus !P !Q /.
Lemma eval_plus: forall P Q x, eval (pplus P Q) x = eval P x + eval Q x.
Admitted. (* TODO, 1 long line *)
Definition pscal a (P: poly): poly := ... (* use List.map *)
Lemma eval_scal a P x: eval (pscal a P) x = a * eval P x.
Admitted. (* TODO, 1 long line *)
Fixpoint pmult (P Q: poly): poly := ...
Lemma eval_mult: forall P Q x, eval (pmult P Q) x = eval P x * eval Q x.
Admitted. (* TODO, 2 lines *)
Fixpoint pcomp (P Q: poly): poly := ...
Lemma eval_comp: forall P Q x, eval (pcomp P Q) x = eval P (eval Q x).
Admitted. (* TODO, 2 lines *)
(** *** isolating polynomials amongst arbitrary functions
(this is some boilerplate you can safely skip) *)
Definition is_poly (f: R -> R) := exists P: poly, forall x, eval P x = f x.
Lemma is_poly_cst a: is_poly (fun _ => a).
Proof. exists (pcst a). apply eval_cst. Qed.
Lemma is_poly_id: is_poly (fun x => x).
Proof. exists pid. apply eval_id. Qed.
Lemma is_poly_xk k: is_poly (fun x => x^k).
Proof. exists (pxk k). apply eval_xk. Qed.
Lemma is_poly_plus f g: is_poly f -> is_poly g -> is_poly (fun x => f x + g x).
Proof.
intros (P&Pf) (Q&Qg). exists (pplus P Q).
intro. now rewrite eval_plus, Pf, Qg.
Qed.
Lemma is_poly_scal f a: is_poly f -> is_poly (fun x => a * f x).
Proof.
intros (P&Pf). exists (pscal a P).
intro. now rewrite eval_scal, Pf.
Qed.
Lemma is_poly_opp: is_poly Ropp.
Proof.
exists (pscal (-1) pid).
intro. simpl. ring.
Qed.
Lemma is_poly_mult f g: is_poly f -> is_poly g -> is_poly (fun x => f x * g x).
Proof.
intros (P&Pf) (Q&Qg). exists (pmult P Q).
intro. now rewrite eval_mult, Pf, Qg.
Qed.
Lemma is_poly_comp f g: is_poly f -> is_poly g -> is_poly (fun x => f (g x)).
Proof.
intros (P&Pf) (Q&Qg). exists (pcomp P Q).
intro. now rewrite eval_comp, Pf, Qg.
Qed.
Instance is_poly_Proper: Proper (pointwise_relation R eq ==> Basics.impl) is_poly.
Proof. intros f g H. unfold is_poly. now setoid_rewrite H. Qed.
Lemma is_poly_sum n f:
(forall i, i is_poly (f i))%nat -> is_poly (fun x => sum n (fun i => f i x)).
Proof.
induction n; intro H.
- setoid_rewrite sum0. apply is_poly_cst.
- setoid_rewrite sumS_last. apply is_poly_plus.
apply IHn. intros. apply H. lia.
apply H. lia.
Qed.
(** *** continuity *)
Definition continuous_at f x :=
forall e, 0 exists d, 0 Rabs(f y-f x)<=e.
(** we prove that this definition is equivalent to the one in the
standard library (the one above is slightly easier to work with) *)
Lemma continuous_at_standard f x:
continuous_at f x <-> continuity_pt f x.
Admitted. (* TODO, 10l, hint: Check Req_dec *)
Lemma continuous_id x: continuous_at id x.
Admitted. (* TODO, 2l *)
Lemma continuous_cst a x: continuous_at (fun _ => a) x.
Admitted. (* TODO, 2l *)
Lemma continuous_plus f g x:
continuous_at f x -> continuous_at g x -> continuous_at (fun y => f y + g y) x.
Admitted. (* TODO, 8l *)
Lemma continuous_Rabs x: continuous_at Rabs x.
Admitted. (* TODO, 2l *)
Lemma continuous_comp f g x:
continuous_at f x -> continuous_at g (f x) -> continuous_at (fun y => g (f y)) x.
Admitted. (* TODO, 5l *)
(* digression: a technique to rewrite inequalities inside products
rewriting with <= works reasonably well in Coq, except for products, since we must guarantee that the resulting context is monotone.
(i.e. in a goal
H: a<=b
=========
a*c <= b*c
one can intuitively rewrite using H only if c is not negative)
since Coq has no way to prove automatically that c is not negative, such rewriting steps are just forbidden
*)
Goal forall a b c, a<=b -> 0<=c -> a*c <= b*c.
Proof.
intros a b c H C.
(* the following line implements a [rewrite H thanks to C] *)
erewrite Rmult_le_compat_r. 2: apply C. 2: apply H.
(* in more complex scenarios, you might want to replace [apply C] with [lra],
or whatever tactic proving that c is indeed non-negative *)
(* if you need to rewrite on the right of a product, use
[erewrite Rmult_le_compat_l]
*)
reflexivity.
Qed.
Lemma continuous_mult f g x:
continuous_at f x -> continuous_at g x -> continuous_at (fun y => f y * g y) x.
Admitted. (* BONUS, hard, 26l + a 2l lemma, recall the paper proof first! *)
Lemma poly_continuous P x: continuous_at (eval P) x.
Admitted. (* TODO, 4l *)
(** ** THIRD SESSION: Weierstrass' theorem, via Bernstein's polynomials *)
(** *** Bernstein's polynomials *)
Definition b n k x := C n k * x^k * (1-x)^(n-k).
Lemma is_poly_b k n: is_poly (b n k).
Admitted. (* TODO, 3l *)
Definition B n g x := sum (S n) (fun k => g(INR k / INR n) * b n k x).
Lemma is_poly_B n g: is_poly (B n g).
Admitted. (* TODO, 2l *)
Lemma B1 n x: B n (fun _ => 1) x = 1.
Admitted. (* TODO, 1l *)
(* small tactics to rewrite under a sum, with the required assumptions on the indices *)
Ltac open_sum i Hi := erewrite sum_eq; swap 1 2; [intros i Hi|].
Ltac close_sum := reflexivity.
Lemma Bx n x: (0 B n (fun x => x) x = x.
intros N. unfold B, b.
rewrite sumS_first, INR0. unfold Rdiv at 1. ring_simplify.
simpl.
(* the [open_sum] tactic makes it possible to work inside the
first encountered sum *)
open_sum k Hk.
rewrite <-2Rmult_assoc, pascal4' by lia.
transitivity (x*(C (pred n) k * x^k * (1-x)^(pred n-k))).
replace (n - S k)%nat with (pred n - k)%nat by lia.
simpl. ring.
(* we call [close_sum] when we are done *)
close_sum.
Admitted. (* TOFINISH: 1l *)
Lemma Bx2 n x: (0 B n (fun x => x^2) x = x/INR n + x^2 * (INR n-1)/INR n.
Proof.
intro N'. assert (C: (n=1 \/ 1|N]; clear N'; unfold B, b.
(* HINT: follow the proof in Nicolas' lecture notes:
Bn(x^2,x)
= Sum k=0..n (n k)(k/n)^2 x^k (1-x)^(n-k)
= x Sum k=1..n (k/n) (n-1 k-1) x^(k-1) (1-x)^(n-k)
= x Sum k=1..n ((k-1)/n)(n-1 k-1) x^(k-1) (1-x)^(n-k) + x/n
= (n-1)/n x^2 Sum k=2..n (n-2 k-2) x^(k-2) (1-x)^(n-k) + x/n
= (n-1)/n x^2 + x/n
*)
Admitted. (* TOFINISH, hard, 30l *)
(** *** Weierstrass' theorem: polynomials are dense in C(a,b) *)
(* the following 'least natural upper bound' will be more convenient to use than the native 'least relative upper bound *)
Definition nup (x: R) := Z.to_nat (up x).
Lemma IPR_pos p: 0 0 <= b n k x.
Proof.
intro H. unfold b. apply Rmult_le_pos. apply Rmult_le_pos.
apply Rlt_le, C_pos.
apply pow_le, H.
apply pow_le. lra.
Qed.
Lemma Ikn k n: (k<=n)%nat -> (0 0<=INR k/INR n<=1.
Proof.
intros. pose proof (pos_INR k).
assert(INR k <= INR n) by now apply le_INR.
assert(0 < INR n) by now apply lt_0_INR.
split; apply Rmult_le_reg_l with (INR n). assumption.
ring_simplify. replace (_ * _) with (INR k). assumption. field. neq_0. assumption.
ring_simplify. replace (_ * _) with (INR k). assumption. field. neq_0.
Qed.
Lemma Rdiv_ge0 a b: 0 <= a -> 0 < b -> 0 <= a / b.
Proof.
intros. assert (0 < /b) by now apply Rinv_0_lt_compat. nra.
Qed.
(* this function will be useful in combination with lemma [split_sum] *)
Definition Rlt_bool x y := if Rlt_dec x y then true else false.
(* two auxiliary lemmas, ignore them if they don't look useful to you *)
Lemma Weierstrass_aux1 d x y: 0 < d <= Rabs (x-y) -> 1 <= ((x-y)/d)^2.
Proof.
intro H. rewrite <-Ratan.pow2_abs. apply pow_R1_Rle.
unfold Rdiv. rewrite Rabs_mult. apply Rmult_le_reg_l with d. tauto.
replace (Rabs (/d)) with (/d).
field_simpl. split_Rabs; lra. lra.
symmetry; apply Rabs_pos_eq.
apply proj1, Rinv_0_lt_compat in H. lra.
Qed.
Lemma Weierstrass_aux2 x: 0 <= x <= 1 -> x*(1-x) <= 1.
Proof.
intro H. replace 1 with (1*1) at 2 by ring.
apply Rmult_le_compat; lra.
Qed.
(** we first prove the theorem on the interval [0;1], and we rely for
that on Heine's theorem, which is in the standard library.
we state it here with a form which is more convenient in the sequel. *)
(* Heine's theorem *)
Theorem Heine01 f:
(forall x, 0<=x<=1 -> continuous_at f x) ->
forall e, 0 exists d, 0 0<=y<=1 -> Rabs (x-y) <= d -> Rabs (f x - f y) <= e.
Proof.
intros F e E.
assert(UC: uniform_continuity f (fun x => 0<=x<=1)).
apply Heine. apply compact_P3. intros. apply continuous_at_standard. now apply F.
specialize (UC (mkposreal _ E)) as ((d&D)&Hd). simpl in Hd.
exists (d/2). split. lra.
intros x y. specialize (Hd x y). lra.
Qed.
Definition norm_inf a b f g e := forall x, a<=x<=b -> Rabs (f x - g x) <= e.
Theorem Weierstrass01 f:
(forall x, 0<=x<=1 -> continuous_at f x) ->
forall e, 0 exists p, is_poly p /\ norm_inf 0 1 f p e.
(* hints: look at the proof in the courses notes ; [Check continuity_ab_maj] *)
(* 1. f is uniformly continuous on [0;1] => pick corresponding d (delta) *)
(* 2. then call M an upper-bound of the absolute value of f on [0;1], reached at m *)
(* 2'. M is non negative *)
(* 3. guess a large enough value for n (implicit in the lecture notes, leave it undefined until it becomes clear which value to take) *)
eset (n: nat).
(* this value is certainly positive (in R and in nat) *)
assert(N: 0 continuous_at f x) ->
forall e, 0 exists p, is_poly p /\ norm_inf a b f p e.
Admitted. (* BONUS, 14l + 13l of auxiliary defs/lems *)