namespace http://mathhub.info/MitM/core/geometry ❚

import base http://mathhub.info/MitM/Foundation ❚
import arith http://mathhub.info/MitM/core/arithmetics ❚
// TODO: ❚
import rules scala://rules.frameit.mmt.kwarc.info ❚

fixmeta base:?Logic ❚

theory 3DGeometry =
  include ☞base:?ProductTypes ❙
  include ?Geometry ❙

    // ℝ³ ❙

  point = ℝ × ℝ × ℝ ❙
  xofpoint : point ⟶ ℝ ❘ = [p] πl p ❘ # 1 _x prec 50 ❙
  yofpoint : point ⟶ ℝ ❘ = [p] πl (πr p) ❘ # 1 _y prec 50 ❙
  zofpoint : point ⟶ ℝ ❘ = [p] πr (πr p) ❘ # 1 _z prec 50 ❙

  point_addI = [p1,p2] ⟨ (p1 _x + p2 _x), (p1 _y + p2 _y), (p1 _z + p2 _z) ⟩ ❙
  point_subtractI = [p1,p2] ⟨ (p1 _x - p2 _x), (p1 _y - p2 _y), (p1 _z - p2 _z) ⟩ ❙
  vec_multI = [r,p] ⟨ r ⋅ p _x, r ⋅ p _y, r ⋅ p _z ⟩ ❙
  scalar_productI = [p1,p2] (p1 _x ⋅ p2 _x) + (p1 _y ⋅ p2 _y) + (p1 _z ⋅ p2 _z) ❙

  include (?Geometry/Common point point_addI point_subtractI vec_multI scalar_productI) ❙


  vec_cross : point ⟶ point ⟶ point ❘ = [v, w ] ⟨ ( v _y  ⋅ w _z  - v _z ⋅ w _y ) , ( v _z  ⋅ w _x  - v _x ⋅ w _z ) , ( v _x  ⋅ w _y  - v _y ⋅ w _x ) ⟩ ❘ # 1 Vcross  2  ❙

❚

theory InterceptTheorem =
    include ☞?3DGeometry ❙
    // naming like the images on
    https://en.wikipedia.org/wiki/Intercept_theorem ❙

    S : point ❙
    A : point ❙
    B : point ❙
    C : point ❙
    D : point ❙

    line1 : ⊦ S on (from A to B) ❙
    line2 : ⊦ S on (from C  to D) ❙
    twolines: ⊦  ¬ (A -- B) ∥ (C -- D) ❙
    par : ⊦ (A -- C) ∥ (B -- D) ❙

    ratio1: ⊦ (d- S A ) / (d- A B) ≐ (d- S C) / (d- C D) ❙
    ratio2: ⊦ (d- S A ) / (d- S B) ≐ (d- S C) / (d- S D) ❙
    ratio3: ⊦ (d- S A ) / (d- S B) ≐ (d- A C) / (d- B D) ❙
    ratio4: ⊦ (d- S C ) / (d- S D) ≐ (d- A C) / (d- B D) ❙
❚

theory 3DTriangles =
    include ☞?3DGeometry ❙

    include (?Geometry/Triangles point point_addI point_subtractI vec_multI scalar_productI) ❙

    area: triangle ⟶ ℝ ❘ = [T]  ( | ( _A T  --  _B T ) Vcross ( _A T -- _C T ) | )  ⋅ ( 1 / 2 )❘ # AΔ 1 ❙
    // area definition that does not use height; can be computed without needing ι ❙
❚

theory Planes =
    include ☞?3DTriangles ❙

    plane : type ❙
    triangleToPlane: triangle ⟶ plane ❘ # PofΔ 1 ❙
    ParametrizedPlane: point ⟶ point ⟶ point ⟶ plane ❘ # Ppara 1 2 3 ❙
    pointNormalPlane: point ⟶ point ⟶ plane ❘ # Ppn 1 2 ❙

    planeNormal : plane ⟶ point ❘ # Pnormal 1 prec 50❙
    planeBase : plane ⟶ point ❘ # Pbase 1  prec 50❙

    PlaneBaseAxiom1 : {v, w, b } ⊦ Pbase (Ppara b v w ) ≐ b ❘ role ForwardRule❙

    normalAxiom1 : { v, w, b } ⊦ ( Pnormal ( Ppara b v w ) ) ≐ ( normalize ( v Vcross w ) ) ❘ role ForwardRule ❙
    normalAxiom2 : { v, b } ⊦ ( Pnormal ( Ppn b v ) ) ≐ ( norm ( v ) ) ❘ role ForwardRule❙
    triangleAxiom :  { T } ⊦ ( PofΔ T ) ≐ Ppara ( _A T ) ( _A  T -- _B T  ) ( _A  T -- _B T)  ❘ role ForwardRule ❙

    pointOnPlane : point ⟶ plane ⟶ bool ❘= [v , p] < Pnormal p , v -- Pbase p > ≐  0  ❘ #  1 VonP 2 ❙
    lineOnPlane : line ⟶ plane ⟶ bool ❘= [l,p ] ( ( from l ) VonP p ) ∧  ( ( from l ) ++( dir l ) ) VonP p ❘#  1 LonP 2 ❙

    LinePlaneCollisionPoint : { A, B } ( ⊦ dir A ⊥⊥ Pnormal B ) ⟶ point  ❘ # colPLV 1 2 3 ❙
    LinePlaneCollisionPointAxiom : {A , B, p1 } ⊦  ( colPLV  A B p1 ) VonP B   ∧  ( colPLV  A B p1 ) on A ❙

    parallelPlanes : plane ⟶ plane ⟶ bool ❘= [ p1 ,p2] ( Pnormal p1 ) ∥ ( Pnormal p2 ) ❘# 1 Ppar 2 prec 50 ❙
    samePlane: plane ⟶ plane ⟶ bool ❘ = [ p1 , p2] ( Pbase p1 VonP  p2 ) ∧ ( p1 Ppar p2 )❘# Psame 1 2❙
    collidePlane : plane ⟶ plane ⟶ bool ❘ = [ A ,B ] ( ¬ A Ppar  B ) ∨ Psame A B ❘ #  colP 1 2 ❙

    collisionLine: {A, B } ⊦ colP A B ⟶ ⊦ ¬ Psame A B ⟶ line ❘ # colPPL 1 2 3 4❙
    collisionLineAxiom: {A, B, p1 ,p2} ⊦ ( ( colPPL A B p1 p2 ) LonP A ) ∧( ( colPPL A B p1 p2 ) LonP B )❙
❚

// TODO Generalize to n-Spheres? ❚
// theory Sphere : http://mathhub.info/MitM/Foundation?Math =
    include ?Vector ❙
    include ?Lines ❙

    sphere: type ❘ # S ❙
    sphereAround: V ⟶ ℝ ⟶ S ❘# So 1 2 ❙
    center: S ⟶ V ❘ # Sm 1 ❙
    centerAxiom: {m,r}  ⊦ Sm ( So m r) ≐ m ❙
    radius: S ⟶ ℝ ❘ # Sr 1 ❙
    radiusAxiom : {m,r} ⊦ Sr (So m r) ≐ r ❙

    onSphere: S ⟶ V ⟶ bool ❘ =  [s, v] ( d ( Sm s ) ( v ) ) ≐ ( Sr s ) ❘ # 2 VonS  1 ❙
    inSphere: S ⟶ V ⟶ bool ❘ =  [s, v] ( d ( Sm s ) ( v ) ) < ( Sr s ) ❘ # 2 VinS  1 ❙

    collidesSphereLine: S ⟶ L ⟶ bool ❘ = [s,l] ∃ [v] ( v VonL  l ) ∨  (v VinS s ) ❘ # 1 ScolL  2 ❙

    circumfenceSphere: S ⟶ ℝ ❘ = [s] ( Sr s ) ⋅ ( Sr s) ⋅ 4 ⋅ π  ❘ # CS 1 ❙
    areaSphere :  S ⟶ ℝ ❘ = [s] ( Sr s ) ⋅ ( Sr s ) ⋅ (Sr s) ⋅ ( 4 / 3 ) ⋅ π  ❘ # AS 1 ❙
❚

// theory Pyramid :  http://mathhub.info/MitM/Foundation?Math =
    include ☞http://BenniDoes.Stuff/?Vector ❙
    include ☞http://BenniDoes.Stuff/?Triangle ❙

    Pyramid : type ❘ # Pyr ❙
    pyramidOf : V ⟶ V ⟶ V ⟶ V ⟶ Pyr ❘ # Pyrof 1 2 3 4 ❙
    P_A : Pyr ⟶ V ❘ # P_A 1❙
    P_A_axiom : {a :V, b :V, c :V, dd :V } ⊦ ( P_A ( Pyrof a b c dd) ) ≐  a  ❘ role ForwardRule❙
    P_B : Pyr ⟶ V ❘ # P_B 1❙
    P_B_axiom : {a :V, b :V, c :V, dd :V } ⊦ ( P_B ( Pyrof a b c dd) ) ≐  b  ❘ role ForwardRule❙
    P_C : Pyr ⟶ V ❘ # P_C 1❙
    P_C_axiom : {a :V, b :V, c :V, dd :V } ⊦ ( P_C ( Pyrof a b c dd) ) ≐  c  ❘ role ForwardRule❙
    P_D : Pyr ⟶ V ❘ # P_D 1❙
    P_D_axiom : {a :V, b :V, c :V, dd :V } ⊦ ( P_D ( Pyrof a b c dd) ) ≐  dd  ❘ role ForwardRule❙

    Volume_Pyramid: Pyr ⟶ ℝ ❘ = [p ] ( 1 / 6) ⋅ ( < ( ( ( P_B p ) ⁻ ( P_A p ) ) Vcross ( ( P_C  p ) ⁻ ( P_A p ) ) ), (( P_D  p ) ⁻ ( P_A p )  ) > ) ❘# VolofP 1 ❙
❚