## Stream: Coq users

### Topic: Wallis' integrals and inelegance

#### Julien Puydt (Aug 10 2021 at 14:19):

Here is what I have come up with to go from the recurrence relation to closed formulas:

``````Section Wallis.
Variable wallis: nat -> nat.
Variable Wrec: forall n, (n.+2)*(wallis n.+2) = (n.+1)*(wallis n).
Lemma Wexplicit: forall n, (\prod_(1 <= j < n.+1) (j.*2))*(wallis (n.*2))
= (\prod_(1 <= j < n.+1) (j.*2-1))*(wallis 0)
/\ (\prod_(1 <= j < n.+1) (j.*2.+1))*(wallis (n.*2.+1))
=(\prod_(1 <= j < n.+1) (j.*2))*(wallis 1).
Proof.
induction n.
(* germ *)
by rewrite unlock /=. (* unlock unrolls \prod, then we simplify - done! *)
(* induction *)
split. (* FIXME: how to avoid doing essentially twice the same thing? *)
rewrite big_nat_recr //= doubleS.
rewrite -mulnA. (* group factors to recognize the recurrence relation *)
rewrite Wrec.
rewrite mulnCA. (* mix the factors some in order to recognize the induction hypothesis *)
rewrite IHn.1.
rewrite mulnCA mulnA. (* again mixing factors *)
rewrite -big_nat_recr //=. (* we recognize a product with one more factor and it's done for the even's *)
(* FIXME: we do the same things for the odd's *)
rewrite big_nat_recr //= doubleS.
rewrite -mulnA.
rewrite Wrec.
rewrite mulnCA.
rewrite IHn.2.
rewrite mulnCA mulnA.
rewrite -big_nat_recr //=.
Qed.
End Wallis.
``````

It does work, but as you can see from the comments, I'm not satisfied with repeating essentially the same argument again.

Is there some elegant way to improve the proof?

#### Paolo Giarrusso (Aug 13 2021 at 23:24):

what if you remove `split` and let `rewrite` act on both halves of the goal? You might need to turn `rewrite foo` into `rewrite !foo`

#### Julien Puydt (Aug 14 2021 at 13:36):

Paolo Giarrusso said:

what if you remove `split` and let `rewrite` act on both halves of the goal? You might need to turn `rewrite foo` into `rewrite !foo`

Nope. I managed to make things better using:

``````Section Wallis.
Variable wallis: nat -> nat.
Variable Wrec: forall n, (n.+2)*(wallis n.+2) = (n.+1)*(wallis n).
Lemma Wexplicit: forall n, (\prod_(1 <= j < n.+1) (j.*2))*(wallis (n.*2))
= (\prod_(1 <= j < n.+1) (j.*2-1))*(wallis 0)
/\ (\prod_(1 <= j < n.+1) (j.*2.+1))*(wallis (n.*2.+1))
=(\prod_(1 <= j < n.+1) (j.*2))*(wallis 1).
Proof.
induction n.
(* germe *)
by rewrite unlock /=. (* le unlock déroule \prod, puis on simplifie *)
(* induction *)
by [split ; rewrite big_nat_recr //= doubleS ;
rewrite -mulnA ; (* regrouper les facteurs pour reconnaître la relation de récurrence *)
rewrite Wrec ; (* l'appliquer *)
rewrite mulnCA ; (* brasser un peu les facteurs pour reconnaître l'hypothèse de récurrence *)
rewrite ?IHn.1 ?IHn.2 ; (* l'appliquer *)
rewrite mulnCA mulnA ; (* encore un brassage de facteurs *)
rewrite -big_nat_recr]. (* on reconnaît un produit avec un facteur supplémentaire
du coup c'est terminé *)
Qed.
End Wallis.
``````

but it's still a bit... unreadable.

#### YAMAMOTO Mitsuharu (Aug 16 2021 at 08:34):

Maybe something like this?

``````Section Wallis.
Variable wallis: nat -> nat.
Variable Wrec: forall n, (n.+2)*(wallis n.+2) = (n.+1)*(wallis n).
Lemma Waux m n:
\prod_(0 <= j < n) (m + j.+1.*2) * wallis (m + n.*2)
= \prod_(0 <= j < n) (m + j.*2.+1) * wallis m.
Proof.
elim: n => [|n IHn]; first by rewrite !big_nil addn0.
rewrite !big_nat_recr //= doubleS.
by rewrite -mulnA !addnS Wrec mulnCA IHn mulnCA mulnA.
Qed.
Lemma Wexplicit: forall n, (\prod_(1 <= j < n.+1) (j.*2))*(wallis (n.*2))
= (\prod_(1 <= j < n.+1) (j.*2-1))*(wallis 0)
/\ (\prod_(1 <= j < n.+1) (j.*2.+1))*(wallis (n.*2.+1))
=(\prod_(1 <= j < n.+1) (j.*2))*(wallis 1).
Proof.
by move=> n; rewrite !big_add1 (Waux 0) (Waux 1).
Qed.
End Wallis.
``````

#### Michael Soegtrop (Aug 16 2021 at 08:57):

Although it looks also a bit verbose, I like the auxiliary lemma approach suggested by @YAMAMOTO Mitsuharu because it makes the proof much more understandable to the reader. I don't think it is required to comment on all the fine details of the proof - the statement of the aux lemma is a much better guide for the reader. In a way it is a comment written in Coq :-)

#### Julien Puydt (Aug 19 2021 at 21:54):

YAMAMOTO Mitsuharu proposed:

Maybe something like this?

`````` (* snip *)
``````

Finding a common expression to apply twice afterwards is a splendid idea! Since I didn't like having it as an additional result, I tried to fold it inside the main proof , noticed that indeed products 1..n.+1 could become 0..n in the process and here is the result:

``````Section Wallis.
Variable wallis: nat -> nat.
Variable Wrec: forall n, (n.+2)*(wallis n.+2) = (n.+1)*(wallis n).
Lemma Wexplicit: forall n, (\prod_(0 <= j < n) (j.*2.+2))*(wallis (n.*2))
= (\prod_(0 <= j < n) (j.*2.+1))*(wallis 0)
/\ (\prod_(0 <= j < n) (j.*2.+3))*(wallis (n.*2.+1))
=(\prod_(0 <= j < n) (j.*2.+2))*(wallis 1).
Proof.
(* common lemma for even and odd cases depending on m *)
have aux: forall m n, \prod_(0 <= j < n) (m + j.*2.+2) * wallis (m + n.*2)
= \prod_(0 <= j < n) (m + j.*2.+1) * wallis m.
move=> m n.
elim: n => [|n Hn].
(* germ *)
by rewrite !big_nil /= double0 addn0.
(* induction *)
rewrite !big_nat_recr //= doubleS.
rewrite -mulnA !addnS. (* group factors to recognize the recurrence relation *)
rewrite !Wrec. (* apply it *)
rewrite mulnCA. (* mix factors some more to use the recurrence hypothesis *)
rewrite Hn. (* apply it *)
by rewrite mulnCA mulnA. (* again some factor mixing to conclude *)

(* now just apply the common lemma twice *)
by [move => n ; rewrite (aux 0) (aux 1)].
Qed.
End Wallis.
``````

which is definitely a big improvement. Thanks!

Last updated: Feb 04 2023 at 21:02 UTC