TriangleScrolls.mmt

/T Modular scrolls having to do with triangles ❚

namespace http://mathhub.info/FrameIT/frameworld ❚
fixmeta ?FrameworldMeta ❚

/T A blueprint problem theory for triangle scrolls
       B
      /|
     / |
    /  |
   /___|
  A    C

  (nicer image: https://en.wikipedia.org/wiki/Right_triangle#/media/File:Rtriangle.svg)
❚
theory TriangleScroll_GeneralProblem =
    A: point ❘ meta ?MetaAnnotations?label "A" ❙
    B: point ❘ meta ?MetaAnnotations?label "B"❙
    C: point ❘ meta ?MetaAnnotations?label "C"❙
❚

/T A blueprint problem theory for triangle scrolls that require a right angle

   We use ?TriangleScroll_GeneralProblem and demand the angle at C to be 90° ❚
theory TriangleScroll_RightAngledProblem =
    include ?TriangleScroll_GeneralProblem ❙
    rightAngleBCA
        : ⊦ ( ∠ B,C,A ) ≐ 90.0 ❘
        meta ?MetaAnnotations?label s"∟${lverb C}" ❘
        meta ?MetaAnnotations?description s"Right angle at ${lverb C}"
    ❙
❚

theory AngleSum =
    meta ?MetaAnnotations?problemTheory ?AngleSum/Problem ❙
    meta ?MetaAnnotations?solutionTheory ?AngleSum/Solution ❙

    theory Problem =
        include ?TriangleScroll_GeneralProblem ❙

        angleBAC
            : Σ α: ℝ. ⊦ ( ∠ B,A,C ) ≐ α ❘
            meta ?MetaAnnotations?label s"∠${lverb B A C}" ❘
            meta ?MetaAnnotations?description s"Angle at ${lverb A}"
        ❙

        angleABC
            : Σ β: ℝ. ⊦ ( ∠ A,B,C ) ≐ β ❘
            meta ?MetaAnnotations?label s"∠${lverb A B C}" ❘
            meta ?MetaAnnotations?description s"Angle at ${lverb B}"
        ❙
    ❚

    theory Solution =
        include ?AngleSum/Problem ❙

        meta ?MetaAnnotations?label "AngleSum" ❙
        meta ?MetaAnnotations?description s"Given a triangle ${lverb A B C} and two known angles, we can deduce the missing angle by the sum of interior angles in triangles always being 180°" ❙

        angleBCA
            : Σ γ: ℝ. ⊦ ( ∠ B,C,A ) ≐ γ ❘
            = ⟨180.0 - (πl angleBAC) - (πl angleABC), sketch "By sum of interior angles = 180° in triangles"⟩ ❘
            meta ?MetaAnnotations?label s"∠${lverb B C A}" ❘
            meta ?MetaAnnotations?description s"The deduced angle by calculating 180° - ${lverb angleBAC} - ${lverb angleABC}"
        ❙
    ❚
❚

theory OppositeLen =
    meta ?MetaAnnotations?problemTheory ?OppositeLen/Problem ❙
    meta ?MetaAnnotations?solutionTheory ?OppositeLen/Solution ❙

    theory Problem =
        include ?TriangleScroll_RightAngledProblem ❙
    
        distanceBC
            : Σ x:ℝ . ⊦ ( d- B C ) ≐ x ❘
            meta ?MetaAnnotations?label s"${lverb B C}" ❘
            meta ?MetaAnnotations?description s"Length of leg ${lverb B C}"
        ❙
    
        angleABC
            : Σ a:ℝ . ⊦ ( ∠ A,B,C ) ≐ a ❘
            meta ?MetaAnnotations?label s"∠${lverb A B C}" ❘
            meta ?MetaAnnotations?description s"Angle at ${lverb B}"
        ❙
    ❚
    
    theory Solution =
        include ?OppositeLen/Problem ❙

        meta ?MetaAnnotations?label "OppositeLen" ❙
        meta ?MetaAnnotations?description s"Given a triangle ${lverb A B C} right angled at ${lverb C}, the distance ${lverb A B} can be computed from the angle at ${lverb B} and the distance ${lverb B C}" ❙
    
        deducedLineCA
            : Σ x:ℝ . ⊦ (d- C A) ≐ x ❘
            = ⟨(tan (πl angleABC)) ⋅ (πl distanceBC), sketch "OppositeLen Scroll"⟩ ❘
            meta ?MetaAnnotations?label s"${lverb C A}" ❘
            meta ?MetaAnnotations?description s"The deduced length of the line ${lverb C A}"
        ❙
    ❚
❚

// Doesn't typecheck, not sure why ❚
// theory Pythagoras =
    meta ?MetaAnnotations?problemTheory ?Pythagoras/Problem ❙
    meta ?MetaAnnotations?solutionTheory ?Pythagoras/Solution ❙

    theory Problem =
        include ?TriangleScroll_RightAngledProblem ❙
    
        distanceAC
             : Σ x:ℝ. ⊦ (d- A C) ≐ x ❘
             meta ?MetaAnnotations?description "Length of leg AC"
        ❙

        distanceBC
             : Σ x:ℝ. ⊦ (d- B C) ≐ x ❘
             meta ?MetaAnnotations?description "Length of leg BC"
        ❙
    ❚
    
    // theory Solution =
        include ?Pythagoras/Problem ❙

        meta ?MetaAnnotations?label "Pythagoras" ❙
        meta ?MetaAnnotations?description "Given a ABC right-angled at C and lengths of both legs, we can compute the length of the hypotenuse via Pythagora's theorem" ❙

        deducedHypotenuse
            : Σ x:ℝ. ⊦ (d- A B) ≐ x ❘
            = ⟨√ ((πl distanceAC) ⋅ (πl distanceAC) + (πl distanceBC) ⋅ (πl distanceBC)),
               sketch "By Pythagora's theorem"⟩ ❘
            meta ?MetaAnnotations?description "Deduced length of hypotenuse AB"
        ❙
    ❚
// ❚