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?

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`

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.

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.
```

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 :-)

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: Jun 20 2024 at 11:02 UTC