\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Pointed
\import Algebra.Semiring
\import Arith.Rat
\import Arith.Real
\import Arith.Real.Field
\import Arith.Trig.ArcTan
\import Arith.Trig.Real
\import Function.Meta
\import Meta
\import Order.StrictOrder
\import Paths
\import Paths.Meta

\sfunc pi : Real
  =>  * arctan (ratio  ) (ratio-norm-<1 ) -  * arctan (ratio  ) (ratio-norm-<1 )
  \where {
    -- | $\left|\tfrac{1}{m+2}\right| < 1$ — domain witness for $\arctan\tfrac{1}{m+2}$.
    \lemma ratio-norm-<1 (m : Nat)
      : RealAbGroup.abs (ratio  (suc (suc m))) < 
      => transportInv (< )
          (RealAbGroup.abs-ofPos (rat_real_<=. (RatField.<=-char linarith)))
          (rat_real_<. (RatField.<-char linarith))
  }

-- | $\cos \pi_M = -1$.
\lemma cos_pi : cos pi = negative 
  => \have sin2=1 : sin ( * pi/4) * sin ( * pi/4) = 
              => rewrite (cos_pi/2, zro_*-left {RealField} {zro}, zro-left) in pythagoras { * pi/4}
     \in pmap cos pi=4*pi/4
         *> pmap cos linarith
         *> cos_+
         *> pmap (\lam c => c * c - sin ( * pi/4) * sin ( * pi/4)) cos_pi/2
         *> pmap (\lam s =>  RealField.*  - s) sin2=1
         *> simplify
  \where {
    \func pi/4 : Real
      =>  * arctan (ratio  ) (pi.ratio-norm-<1 ) - arctan (ratio  ) (pi.ratio-norm-<1 )

    \lemma tan_pi/4 : sin pi/4 = cos pi/4
      => \let | a => arctan (ratio  ) (pi.ratio-norm-<1 )
              | b => arctan (ratio  ) (pi.ratio-norm-<1 )
         \in \have
              | tan_a :  * sin a = cos a
                      => pmap ( *) (tan-arctan _) *> inv *-assoc *> pmap (* _) RealField.*-rat *> ide-left
              | tan_b :  * sin b = cos b
                      => pmap ( *) (tan-arctan _) *> inv *-assoc *> pmap (* _) RealField.*-rat *> ide-left
              | A :  * a - b = (a + a) + (a + a) - b
                  => linarith
            \in unfold pi/4 $ rewrite A $
                rewrite (sin_minus {(a + a) + (a + a)} {b},
                         cos_minus {(a + a) + (a + a)} {b},
                         sin_+ {a + a} {a + a}, cos_+ {a + a} {a + a},
                         sin_+ {a} {a},         cos_+ {a} {a},
                         inv tan_a, inv tan_b)
                        equation.cRing

    \lemma pi=4*pi/4 : pi =  * pi/4
      => (\peval pi) *> equation.cRing

    \lemma cos_pi/2 : cos ( * pi/4) = 
      => pmap cos linarith *> cos_+ *> pmap (\lam s => cos pi/4 * cos pi/4 - s * s) tan_pi/4 *> negative-right
  }



-- | $\sin \pi = 0$.
\lemma sin_pi : sin pi = {Real} 
  => pmap sin cos_pi.pi=4*pi/4
    *> pmap sin (linarith :  * cos_pi.pi/4 = {Real}  * cos_pi.pi/4 +  * cos_pi.pi/4)
         *> sin_+ { * cos_pi.pi/4} { * cos_pi.pi/4}
              *> rewrite cos_pi.cos_pi/2 equation.cRing

-- | $\cos(2\pi) = 1$.
\lemma cos_two_pi : cos ( * pi) = {Real} 
  => pmap cos linarith *> cos_+ *> rewrite (cos_pi, sin_pi) equation.cRing

-- | $\sin(2\pi) = 0$.
\lemma sin_two_pi : sin ( * pi) = {Real} 
  => pmap sin linarith *> sin_+ {pi} {pi} *> rewrite (cos_pi, sin_pi) equation.cRing

-- | $\cos$ is $2\pi$-periodic.
\lemma cos_period {x : Real} : cos (x +  * pi) = cos x
  => cos_+ *> rewrite (cos_two_pi, sin_two_pi) equation.cRing

-- | $\sin$ is $2\pi$-periodic.
\lemma sin_period {x : Real} : sin (x +  * pi) = sin x
  => sin_+ *> rewrite (cos_two_pi, sin_two_pi) equation.cRing