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 TriangleProblem =
    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 TriangleProblem_RightAngleAtC =
    include ?TriangleProblem ❙
    rightAngleC
        : ⊦ ( ∠ B,C,A ) ≐ 90.0 ❘
        meta ?MetaAnnotations?label s"⊾${lverb C}" ❘
        meta ?MetaAnnotations?description s"${lverb A C} ⟂ ${lverb B C}: right angle at ${lverb C} as enclosed by legs ${lverb A C} and ${lverb B C}."
    ❙
❚

theory TriangleProblem_AngleAtA =
   include ?TriangleProblem ❙
   angleA
       : Σ α: ℝ. ⊦ ( ∠ B,A,C ) ≐ α ❘
       meta ?MetaAnnotations?label s"∠${lverb B A C}" ❘
       meta ?MetaAnnotations?description s"Angle at ${lverb A} as enclosed by legs ${lverb A B} and ${lverb A C}"
   ❙
❚

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

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

    theory Problem =
        include ?TriangleProblem ❙
        include ?TriangleProblem_AngleAtA ❙
        include ?TriangleProblem_AngleAtB ❙
    ❚

    theory Solution =
        include ?AngleSum/Problem ❙

        angleC
            : Σ γ: ℝ. ⊦ ( ∠ B,C,A ) ≐ γ ❘
            = ⟨180.0 - (πl angleA) - (πl angleB), 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 angleA} - ${lverb angleB}"
        ❙

        // the description verbalizes angleC, hence must come after its declaration ❙
        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: ${lverb angleC} = 180° - ${lverb angleA} - ${lverb angleB}." ❙
    ❚
❚

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

    theory Problem =
        include ?TriangleProblem_RightAngleAtC ❙
    
        distanceBC
            : Σ x:ℝ . ⊦ ( d- B C ) ≐ x ❘
            meta ?MetaAnnotations?label s"${lverb B C}" ❘
            meta ?MetaAnnotations?description s"Length of leg ${lverb B C}"
        ❙

        include ?TriangleProblem_AngleAtB ❙
    ❚
    
    theory Solution =
        include ?OppositeLen/Problem ❙
    
        deducedLineCA
            : Σ x:ℝ . ⊦ (d- C A) ≐ x ❘
            = ⟨(tan (πl angleB)) ⋅ (π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}"
        ❙

        // the description verbalizes deducedLineCA, hence must come after its declaration ❙
        meta ?MetaAnnotations?label "OppositeLen" ❙
        meta ?MetaAnnotations?description s"Given a triangle △${lverb A B C} right-angled at ⊾${lverb C}, the opposite side has length ${lverb deducedLineCA} = tan(${lverb angleB}) ⋅ ${lverb B C}." ❙
    ❚
❚

// 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"
        ❙
    ❚
// ❚