Update TriangleScrolls.mmt

fb1565ff · Navid Roux · 7c414563 · fb1565ff
Commit fb1565ff authored 3 years ago by Navid Roux
--- a/source/Scrolls/TriangleScrolls.mmt
+++ b/source/Scrolls/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 opposide 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"
-        ❙
-    ❚
-// ❚
\ No newline at end of file
+/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"
+        ❙
+    ❚
+// ❚