Section π.
Pi (alternate)
(Please import CRpi instead)This version is slower to compute than CRpi_fast; however it is faster to compile.
Pi is defined as
68*arctan(1/23) + 32*arctan(1/182) + 40*arctan(1/5118) + 20*arctan(1/6072).
Lemma small_per_23 : (0 <= (1#(23%positive)) <= 1)%Q.
Lemma small_per_182 : (0 <= (1#(182%positive)) <= 1)%Q.
Lemma small_per_5118 : (0 <= (1#(5118%positive)) <= 1)%Q.
Lemma small_per_6072 : (0 <= (1#(6072%positive)) <= 1)%Q.
Definition r_pi (r:Q) : CR :=
((scale (68%Z*r) (rational_arctan_small_pos small_per_23) +
scale (32%Z*r) (rational_arctan_small_pos small_per_182)) +
(scale (40%Z*r) (rational_arctan_small_pos small_per_5118) +
scale (20%Z*r) (rational_arctan_small_pos small_per_6072)))%CR.
To prove that pi is is correct we repeatedly use the arctan sum law.
The problem is that the arctan sum law only works for input between -1
and 1. We use reflect to show that our use of arctan sum law always
satifies this restriction.
Let f (a b:Q) : Q :=
let (x,y) := a in
let (z,w) := b in
Qred ((x*w + y*z)%Z/(y*w-x*z)%Z).
Lemma f_char : forall a b, f a b == (a+b)/(1-a*b).
Lemma ArcTan_plus_ArcTan_Q : forall x y, -(1) <= x <= 1 -> -(1) <= y <= 1 -> ~1-x*y==0 ->
(ArcTan (inj_Q _ x)[+]ArcTan (inj_Q _ y)[=]ArcTan (inj_Q _ (f x y))).
Definition ArcTan_multiple : forall x, -(1) <= x <= 1 -> forall n, {True} + {(nring n)[*]ArcTan (inj_Q _ x)[=]ArcTan (inj_Q _ (iter_nat n _ (f x) 0))}.
Defined.
Lemma reflect_right : forall A B (x:{A}+{B}), (if x then ⊥ else True) -> B.
Lemma Pi_Formula :
(((nring 17)[*]ArcTan (inj_Q IR (1 / 23%Z))[+]
(nring 8)[*]ArcTan (inj_Q IR (1 / 182%Z))[+]
(nring 10)[*]ArcTan (inj_Q IR (1 / 5118%Z))[+]
(nring 5)[*]ArcTan (inj_Q IR (1 / 6072%Z)))[=]
π[/]4).
Lemma r_pi_correct : forall r,
(r_pi r == IRasCR ((inj_Q IR r)[*]π))%CR.
Definition CRpi : CR := (r_pi 1).
Lemma CRpi_correct : (IRasCR π == CRpi)%CR.
End π.
let (x,y) := a in
let (z,w) := b in
Qred ((x*w + y*z)%Z/(y*w-x*z)%Z).
Lemma f_char : forall a b, f a b == (a+b)/(1-a*b).
Lemma ArcTan_plus_ArcTan_Q : forall x y, -(1) <= x <= 1 -> -(1) <= y <= 1 -> ~1-x*y==0 ->
(ArcTan (inj_Q _ x)[+]ArcTan (inj_Q _ y)[=]ArcTan (inj_Q _ (f x y))).
Definition ArcTan_multiple : forall x, -(1) <= x <= 1 -> forall n, {True} + {(nring n)[*]ArcTan (inj_Q _ x)[=]ArcTan (inj_Q _ (iter_nat n _ (f x) 0))}.
Defined.
Lemma reflect_right : forall A B (x:{A}+{B}), (if x then ⊥ else True) -> B.
Lemma Pi_Formula :
(((nring 17)[*]ArcTan (inj_Q IR (1 / 23%Z))[+]
(nring 8)[*]ArcTan (inj_Q IR (1 / 182%Z))[+]
(nring 10)[*]ArcTan (inj_Q IR (1 / 5118%Z))[+]
(nring 5)[*]ArcTan (inj_Q IR (1 / 6072%Z)))[=]
π[/]4).
Lemma r_pi_correct : forall r,
(r_pi r == IRasCR ((inj_Q IR r)[*]π))%CR.
Definition CRpi : CR := (r_pi 1).
Lemma CRpi_correct : (IRasCR π == CRpi)%CR.
End π.