Proof.hs

{-# LANGUAGE UnicodeSyntax #-}
module Proof where
import System.Console.ANSI
import Prelude.Unicode
import Control.Monad.Unicode

{-
  Calculations and mathematical proofs of circular computations.
  @author Marcelo Camargo
-}
type 𝔹 = Bool
type Ω = Double
type Z = Int
data Shape = Circle Ω Ω Ω deriving (Show, Eq)

(∙) ∷ Ω → Ω → Ω → Shape
(∙) x y r = Circle x y r

(≈) ∷ Ω → Float → Bool
(≈) a b = (realToFrac a) ≡ b

(<~>) ∷ (RealFrac a) ⇒ a → a
(<~>) f = (fromInteger $ round $ f ⋅ (10 ^ 2)) ÷ (10.0 ^^ 2)

a <≈> b = ((<~>) a) ≈ ((<~>) b)

-- proofDiameterWithRadius
getDiameterByRadius ∷ Shape → Ω
getDiameterByRadius (Circle _ _ 0) = 0
getDiameterByRadius (Circle _ _ r) = r ⋅ 2

-- proofDiameterWithRadius
getRadiusByDiameter ∷ Ω → Ω
getRadiusByDiameter = (÷ 2)

-- proofRadiusWithArea
getRadiusByArea ∷ Ω → Ω
getRadiusByArea 0 = 0
getRadiusByArea a = sqrt $ a ÷ π

-- proofRadiusWithArea, proofAreaByRadiusWithNth, proofNthRadius
getAreaByRadius ∷ Shape → Ω
getAreaByRadius (Circle _ _ 0) = 0
getAreaByRadius (Circle _ _ r) = π ⋅ r ** 2

-- proofAreaByRadiusWithNth
getNthArea ∷ Shape → Ω → Ω
getNthArea c 0 = 0
getNthArea c n = (getAreaByRadius c) ÷ n

-- proofNthRadius
getNthRadius ∷ Shape → Ω → Ω
getNthRadius c 0 = 0
getNthRadius c n = (getNthArea c n) ÷ 2

-- proofSumArea
(∑) ∷ Shape → Shape → Ω
(∑) (Circle _ _ 0) (Circle _ _ 0)       = 0
(∑) a@(Circle _ _ xr) b@(Circle _ _ yr) =
  (getAreaByRadius a) + (getAreaByRadius b)

-- proofAngle
(<..>) ∷ Z → Ω
(<..>) 0 = error "Impossible"
(<..>) n = 360.0 ÷ (fromIntegral n)

-- proofHorDistArea
(<÷>) ∷ Shape → Z → Ω
(<÷>) _ 0              = 0
(<÷>) (Circle _ _ r) n =
  getAreaByRadius $ (∙) 0 0 radius
  where
    radius = r ÷ (fromIntegral n)

-- proofDensestPacking
densestPacking ∷ Ω
densestPacking = (1 ÷ 6) ⋅ π ⋅ (sqrt 3.0)

-- TODO: Apply proof (unproofed theory)
getPos ∷ Shape → ℤ → Ω
getPos c@(Circle x y r) n = let area = getNthRadius c (fromIntegral n)
  in getDiameterByRadius $ ((∙) 0 0 (getRadiusByArea area))

-- Math proofs
proofRadiusWithArea ∷ IO ()
proofRadiusWithArea =
  displayTruth fn ((getRadiusByArea $ getAreaByRadius ((∙) 0 0 10)) ≡ 10)
  where
    fn = "proofRadiusWithArea"

proofDiameterWithRadius ∷ IO ()
proofDiameterWithRadius =
  let diam = getDiameterByRadius ((∙) 0 0 10)
  in case diam of
    20        → displayTruth fn (getRadiusByDiameter diam ≡ 10)
    otherwise → displayTruth fn False
  where
    fn = "proofDiameterWithRadius"

proofAreaByRadiusWithNth ∷ IO ()
proofAreaByRadiusWithNth = let c = ((∙) 0 0 3) in
  displayTruth fn (getAreaByRadius c ≡ getNthArea c 1)
  where
    fn = "proofAreaByRadiusWithNth"

proofNthRadius ∷ IO ()
proofNthRadius = let c = ((∙) 0 0 3) in
  displayTruth fn (((getAreaByRadius c) ÷ 2) ≡ (getNthRadius c 1))
  where
    fn = "proofNthRadius"

proofSumArea ∷ IO ()
proofSumArea = displayTruth fn correctness
  where
    a = ((∙) 0 0 3)
    b = ((∙) 0 0 4)
    e = 5.0
    correctness = getRadiusByArea (a ∑ b) ≡ e
    fn = "proofSumArea"

proofAngle ∷ IO ()
proofAngle = displayTruth fn applyProof
  where
    applyProof = let
        integral   = ((<..>) 4) ≡ 90
        fractional = ((<..>) 18) ≡ (360 ÷ 18)
      in (integral ∧ fractional)
    fn = "proofAngle"

proofHorDistArea ∷ IO ()
proofHorDistArea = displayTruth fn ((((∙) 0 0 10) <÷> 3) ≡ 34.90658503988659)
  where
    fn = "proofHorDistArea"

displayTruth ∷ [Char] → 𝔹 → IO ()
displayTruth msg True  = (sayMsg msg)
  ≫ setSGR [ SetConsoleIntensity BoldIntensity
           , SetColor Foreground Vivid Green
           ] ≫ putStrLn "(T)"
displayTruth msg False = (sayMsg msg)
  ≫ setSGR [ SetConsoleIntensity BoldIntensity
           , SetColor Foreground Vivid Red
           ] ≫ putStrLn "(F)"

sayMsg ∷ [Char] → IO ()
sayMsg msg = setSGR [ SetConsoleIntensity NormalIntensity
                    , SetColor Foreground Dull Cyan
                    ] ≫ (putStr $ '+' : formating msg)
                    where
                      formating m
                        | length m < 30 = m ⧺ replicate (30 - length m) ' '
                        | otherwise     = take 27 m ⧺ "..."

resetColors ∷ IO ()
resetColors = setSGR [ SetConsoleIntensity NormalIntensity
                     , SetColor Foreground Dull White
                     ]

proofDensestPacking ∷ IO ()
proofDensestPacking = displayTruth fn (densestPacking ≈ 0.9068996821)
  where
    fn = "proofDensestPacking"

-- Try to proof the optimal arrangement of the circles in a 1-scale.
arrange ∷ Int → (Float, Float)
arrange n
  | n ≡ 1     = (1, 1)
  | n ≡ 2     = (2, 0.5)
  | n ≡ 3     = let opt = (1 + (2 ÷ 3) ⋅ (sqrt 3))
    in (opt, 0.6466)
  | n ≡ 4     = let opt = (1 + (sqrt 2))
    in (opt, 0.6864)
  | n ≡ 5     = let opt = (1 + (sqrt $ 2 ⋅ (1 + (1 ÷ (sqrt 5)))))
    in (opt, 0.6854)
  | n ≡ 6     = (3, 0.6667)
  | n ≡ 7     = (3, 0.7778)
  | n ≡ 8     = let opt = (1 + (1 ÷ sin (pi ÷ 7)))
    in (opt, 0.7328)
  | otherwise = error "Mathematically unkown and unproofed optimal result"

proofArrange ∷ [(Int, Bool)]
proofArrange =
  map eachProof arr
  where
    arr = [1 .. 8]
    eachProof = \i → let tuple = expect !! i
      in (i, ((snd tuple) <≈> (fst $ arrange i)))
    expect = [(0, 0), (1, 1), (2, 2), (3, 2.154), (4, 2.414), (5, 2.701),
      (6, 3), (7, 3), (8, 3.304)]

putEachArrangeResult ∷ IO ()
putEachArrangeResult = mapM_ display proofArrange
  where
    display = \tuple -> let
      index  = (show $ fst tuple)
      result = snd tuple
      in displayTruth (index ⧺ " element proof") result

-- TODO: Proof correct distribution of mass by radius
main ∷ IO ()
main = (setTitle "Math Proofs")
  ≫ displayLine
  ≫ displayTitle
  ≫ displayLine
  ≫ proofRadiusWithArea
  ≫ proofDiameterWithRadius
  ≫ proofAreaByRadiusWithNth
  ≫ proofNthRadius
  ≫ proofSumArea
  ≫ proofAngle
  ≫ proofHorDistArea
  ≫ proofDensestPacking
  ≫ putEachArrangeResult
  ≫ resetColors
  ≫ displayLine
  where
    displayTitle = let title = ("    Function", "(X)") in
      putStrLn $ ((fst title) ⧺ (replicate (31 - (length $ fst title)) ' ')) ⧺
        snd title
    displayLine  = putStrLn $ replicate 34 '-'