Stream: Coq users

Topic: Wallis' integrals and inelegance

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :-)

view this post on Zulip 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: Oct 04 2023 at 22:01 UTC