From 365d52586fdbe05c2eee6caf49ddce1327ef9665 Mon Sep 17 00:00:00 2001
From: ComFreek <comfreek@outlook.com>
Date: Wed, 26 Jul 2023 01:39:23 +0200
Subject: [PATCH] clean up scrolls mmt code
---
source/Scrolls/CircleScroll.mmt | 173 ++++++++--------------------
source/Scrolls/ConeVolumeScroll.mmt | 4 -
source/Scrolls/CylinderScroll.mmt | 8 --
source/Scrolls/InterceptTheorem.mmt | 4 +-
source/Scrolls/MiscScrolls.mmt | 27 ++---
source/Scrolls/ParallelLines.mmt | 6 +-
source/Scrolls/TriangleScrolls.mmt | 10 +-
7 files changed, 65 insertions(+), 167 deletions(-)
delete mode 100644 source/Scrolls/CylinderScroll.mmt
diff --git a/source/Scrolls/CircleScroll.mmt b/source/Scrolls/CircleScroll.mmt
index 7404717..811c564 100644
--- a/source/Scrolls/CircleScroll.mmt
+++ b/source/Scrolls/CircleScroll.mmt
@@ -1,166 +1,87 @@
namespace http://mathhub.info/FrameIT/frameworld âš
-
fixmeta ?FrameworldMeta âš
-
-/T
-This scrolls calculates a circle based on three points special pooints.
-
-The arguments required:
-
-M - The center of the circle
-A - A point on the edge of the circle
-B - A point on the plane that the circle is supposed to lie in.
-
-This Scrolls returns:
-
-deduceC - The actual cirlce as a fact
-deduceR - The radius of the circle as RadiusFact
-deduceR2 - The radius of the circle as DistanceFact
-midOnCircle - a proof that M is on the circle
-edgeOnCircle - a proof that A is on the circle
-
-
-
+/T This scrolls infers a 2D circle from three dedicated 3D points (the circle's supposed center,
+ one of the supposed circle itself, one in the plane the circle should lie in).
âš
-
-
-
theory CircleScroll =
meta ?MetaAnnotations?problemTheory ?CircleScroll/Problem â™
meta ?MetaAnnotations?solutionTheory ?CircleScroll/Solution â™
// the three special points M, A and B â™
theory Problem =
- M : point ☠meta ?MetaAnnotations?label "M" â™
- A : point ☠meta ?MetaAnnotations?label "A" â™
- B : point ☠meta ?MetaAnnotations?label "B" â™
-
-
-
-
+ M : point ☠meta ?MetaAnnotations?label "M"
+ ☠meta ?MetaAnnotations?description "The circle's center" â™
+ A : point ☠meta ?MetaAnnotations?label "A"
+ ☠meta ?MetaAnnotations?description "A point on the circle" â™
+ B : point ☠meta ?MetaAnnotations?label "B"
+ ☠meta ?MetaAnnotations?description "A point within the plane the circle should lie in." â™
âš
- // the output of the scroll â™
-
theory Solution =
include ?CircleScroll/Problem â™
-
- deduceC
- : circle â˜
- = ( pointsToC M A B ) â˜
- meta ?MetaAnnotations?label s"â—‹${lverb M}" â˜
- meta ?MetaAnnotations?description "Circle"
+ deduceC: circle
+ ☠= ( pointsToC M A B )
+ ☠meta ?MetaAnnotations?label s"○${lverb M}"
+ ☠meta ?MetaAnnotations?description "Circle"
â™
- deduceR : Σ x:â„ . ⊦ ( circleRadius deduceC) ≠x â˜
- = ⟨ d- M A , sketch "deduce Radius"⟩ â˜
- meta ?MetaAnnotations?label s"r${lverb deduceC}" â˜
- meta ?MetaAnnotations?description "radius of C"
+ deduceR: Σ x:℠. ⊦ ( circleRadius deduceC) ≠x
+ ☠= ⟨ d- M A , sketch "deduce Radius"⟩
+ ☠meta ?MetaAnnotations?label s"r${lverb deduceC}"
+ ☠meta ?MetaAnnotations?description s"radius of ${lverb deduceC} (radius fact)"
â™
- deduceR2 : Σ x:â„ . ⊦ ( d- A M ) ≠x â˜
- = ⟨ d- A M , sketch "deduce Radius2"⟩ â˜
- meta ?MetaAnnotations?label s"${lverb A M}" â˜
- meta ?MetaAnnotations?description "radius of C"
+ deduceR2: Σ x:℠. ⊦ ( d- A M ) ≠x
+ ☠= ⟨ d- A M , sketch "deduce Radius2"⟩
+ ☠meta ?MetaAnnotations?label s"${lverb A M}"
+ ☠meta ?MetaAnnotations?description s"radius of ${lverb deduceC} (distance fact)"
â™
-
- midOnCircle : ⊦ M VonC deduceC â˜
- = midOnC deduceC M â˜
- meta ?MetaAnnotations?label s"${lverb M}∈${lverb deduceC}" â˜
- meta ?MetaAnnotations?description "proof of M being on the circle"
+ midOnCircle: ⊦ M VonC deduceC
+ ☠= midOnC deduceC M
+ ☠meta ?MetaAnnotations?label s"${lverb M}∈${lverb deduceC}"
+ ☠meta ?MetaAnnotations?description s"proof of M being on the circle ${lverb deduceC}"
â™
-
- edgeOnCircle : ⊦ A VonC deduceC â˜
- meta ?MetaAnnotations?label s"${lverb A}∈${lverb deduceC}" â˜
- meta ?MetaAnnotations?description "proof of A being on the circle"
- â™
-
-
-
-
-
-
+ edgeOnCircle: ⊦ A VonC deduceC
+ ☠meta ?MetaAnnotations?label s"${lverb A}∈${lverb deduceC}"
+ ☠meta ?MetaAnnotations?description s"proof of A being on the circle ${lverb deduceC}"
+ â™
// the description verbalizes CircleCircumference, hence must come after its declaration â™
- meta ?MetaAnnotations?label "CircleScroll" â™
- meta ?MetaAnnotations?description s"Calculating a circle defined by the middle ${lverb M}, an edge point ${lverb A} and a point on the circle plane ${lverb B}. " â™
+ meta ?MetaAnnotations?label "CircleScroll" â™
+ meta ?MetaAnnotations?description s"Calculating a circle defined by the middle ${lverb M}, an edge point ${lverb A} and a point on the circle plane ${lverb B}. " â™
âš
âš
-
-
-
-/T
-This scrolls calculates the area of a given circle based on the circle and its radius circle:
-
-The arguments required:
-
-C - The circle
-radiusC - The actual radius of the circle
-
-This Scrolls returns:
-
-deduceArea - The area of the circle
-
-
-âš
-
-
-
theory CircleAreaScroll =
- meta ?MetaAnnotations?problemTheory ?CircleAreaScroll/Problem â™
+ meta ?MetaAnnotations?problemTheory ?CircleAreaScroll/Problem â™
meta ?MetaAnnotations?solutionTheory ?CircleAreaScroll/Solution â™
theory Problem =
- cir : circle ☠meta ?MetaAnnotations?label "â—‹C" â™
-
- radiusC : Σ x:â„ . ⊦ radius cir ≠x â˜
- meta ?MetaAnnotations?label "r" â˜
- meta ?MetaAnnotations?description s"Radius of the circle ${lverb cir}"
+ cir: circle
+ ☠meta ?MetaAnnotations?label "○C"
+ ☠meta ?MetaAnnotations?description s"the circle"
â™
+ /T todo: why can't we compute the radius directly from cir? â™
+ radiusC: Σ x:℠. ⊦ radius cir ≠x
+ ☠meta ?MetaAnnotations?label "r"
+ ☠meta ?MetaAnnotations?description s"radius of the circle ${lverb cir}"
+ â™
âš
theory Solution =
- include ?CircleAreaScroll/Problem â™
- deduceArea
- : Σ x:â„ . ⊦ areaCirc cir ≠x â˜
- = ⟨ ( (Ï€l radiusC) â‹… ( Ï€l radiusC) ) â‹… pi_num , sketch "CircleArea Scroll"⟩ â˜
- meta ?MetaAnnotations?label s"A(${lverb cir})" â˜
- meta ?MetaAnnotations?description s"The area of the circle ${lverb cir}"
- â™
+ include ?CircleAreaScroll/Problem â™
+ deduceArea: Σ x:℠. ⊦ areaCirc cir ≠x
+ ☠= ⟨ ( (πl radiusC) ⋅ ( πl radiusC) ) ⋅ pi_num , sketch "CircleArea Scroll"⟩
+ ☠meta ?MetaAnnotations?label s"A(${lverb cir})"
+ ☠meta ?MetaAnnotations?description s"The area of the circle ${lverb cir}"
+ â™
- meta ?MetaAnnotations?label "CircleAreaScroll" â™
- meta ?MetaAnnotations?description s" This scroll is calculating the area of the circle ${lverb cir} via the formula A = ${lverb radiusC}â‹… ${lverb radiusC}â‹… pi" â™
+ meta ?MetaAnnotations?label "CircleAreaScroll" â™
+ meta ?MetaAnnotations?description s" This scroll is calculating the area of the circle ${lverb cir} via the formula A = ${lverb radiusC}â‹… ${lverb radiusC}â‹… pi" â™
âš
âš
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
diff --git a/source/Scrolls/ConeVolumeScroll.mmt b/source/Scrolls/ConeVolumeScroll.mmt
index fcbe21b..2c9db00 100644
--- a/source/Scrolls/ConeVolumeScroll.mmt
+++ b/source/Scrolls/ConeVolumeScroll.mmt
@@ -2,10 +2,6 @@ namespace http://mathhub.info/FrameIT/frameworld âš
fixmeta ?FrameworldMeta âš
-
-
-
-
/T
This scrolls calculates the volume of a cone with a circle as base.
diff --git a/source/Scrolls/CylinderScroll.mmt b/source/Scrolls/CylinderScroll.mmt
deleted file mode 100644
index 5e214e9..0000000
--- a/source/Scrolls/CylinderScroll.mmt
+++ /dev/null
@@ -1,8 +0,0 @@
-namespace http://mathhub.info/FrameIT/frameworld âš
-fixmeta ?FrameworldMeta âš
-
-
-
-
-
-
diff --git a/source/Scrolls/InterceptTheorem.mmt b/source/Scrolls/InterceptTheorem.mmt
index f7daa9c..1a1183a 100644
--- a/source/Scrolls/InterceptTheorem.mmt
+++ b/source/Scrolls/InterceptTheorem.mmt
@@ -16,10 +16,8 @@ fixmeta ?FrameworldMeta âš
The scroll encodes the InterceptTheorem
âš
-
-
theory InterceptTheorem =
- meta ?MetaAnnotations?problemTheory ?InterceptTheorem/Problem â™
+ meta ?MetaAnnotations?problemTheory ?InterceptTheorem/Problem â™
meta ?MetaAnnotations?solutionTheory ?InterceptTheorem/Solution â™
theory Problem =
diff --git a/source/Scrolls/MiscScrolls.mmt b/source/Scrolls/MiscScrolls.mmt
index 3e52ad0..cf16d25 100644
--- a/source/Scrolls/MiscScrolls.mmt
+++ b/source/Scrolls/MiscScrolls.mmt
@@ -4,20 +4,18 @@ namespace http://mathhub.info/FrameIT/frameworld âš
fixmeta ?FrameworldMeta âš
theory Midpoint =
- meta ?MetaAnnotations?problemTheory ?Midpoint/Problem â™
+ meta ?MetaAnnotations?problemTheory ?Midpoint/Problem â™
meta ?MetaAnnotations?solutionTheory ?Midpoint/Solution â™
theory Problem =
- P
- : point â˜
- meta ?MetaAnnotations?label "P" â˜
- meta ?MetaAnnotations?description "Some arbitrary input point"
+ P: point
+ ☠meta ?MetaAnnotations?label "P"
+ ☠meta ?MetaAnnotations?description "Some arbitrary input point"
â™
- Q
- : point â˜
- meta ?MetaAnnotations?label "Q" â˜
- meta ?MetaAnnotations?description "Some other arbitrary input point"
+ Q: point
+ ☠meta ?MetaAnnotations?label "Q"
+ ☠meta ?MetaAnnotations?description "Some other arbitrary input point"
â™
âš
@@ -27,11 +25,10 @@ theory Midpoint =
meta ?MetaAnnotations?label "MidPoint" â™
meta ?MetaAnnotations?description s"Our MidPoint scroll that given two points ${lverb P} and ${lverb Q} computes the midpoint of the line ${lverb P Q}." â™
- midpoint
- : point â˜
- = ⟨0.5 â‹… (P _x + Q _x), 0.5 â‹… (P _y + Q _y), 0.5 â‹… (P _z + Q _z)⟩ â˜
- meta ?MetaAnnotations?label s"Mid[${lverb P Q}]" â˜
- meta ?MetaAnnotations?description s"The midpoint between points ${lverb P} and ${lverb Q}."
+ midpoint: point
+ ☠= ⟨0.5 ⋅ (P _x + Q _x), 0.5 ⋅ (P _y + Q _y), 0.5 ⋅ (P _z + Q _z)⟩
+ ☠meta ?MetaAnnotations?label s"Mid[${lverb P Q}]"
+ ☠meta ?MetaAnnotations?description s"The midpoint between points ${lverb P} and ${lverb Q}."
â™
âš
-âš
\ No newline at end of file
+âš
diff --git a/source/Scrolls/ParallelLines.mmt b/source/Scrolls/ParallelLines.mmt
index e52d466..cbffc5d 100644
--- a/source/Scrolls/ParallelLines.mmt
+++ b/source/Scrolls/ParallelLines.mmt
@@ -23,14 +23,10 @@ A ------B
The scroll encodes the InterceptTheorem .
âš
-
-
theory ParallelLines =
- meta ?MetaAnnotations?problemTheory ?ParallelLines/Problem â™
+ meta ?MetaAnnotations?problemTheory ?ParallelLines/Problem â™
meta ?MetaAnnotations?solutionTheory ?ParallelLines/Solution â™
-
-
theory Problem =
A: point ☠meta ?MetaAnnotations?label "A" â™
B: point ☠meta ?MetaAnnotations?label "B" â™
diff --git a/source/Scrolls/TriangleScrolls.mmt b/source/Scrolls/TriangleScrolls.mmt
index c66d508..ada4d82 100644
--- a/source/Scrolls/TriangleScrolls.mmt
+++ b/source/Scrolls/TriangleScrolls.mmt
@@ -25,8 +25,7 @@ theory TriangleProblem =
theory TriangleProblem_RightAngleAtC =
include ?TriangleProblem â™
rightAngleC
- // : ⊦ ( ∠B,C,A ) ≠90.0 â˜
- : ⊦ ( ∠r B C A ) â˜
+ : ⊦ ( ∠r 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}."
â™
@@ -51,7 +50,7 @@ theory TriangleProblem_AngleAtB =
âš
theory AngleSum =
- meta ?MetaAnnotations?problemTheory ?AngleSum/Problem â™
+ meta ?MetaAnnotations?problemTheory ?AngleSum/Problem â™
meta ?MetaAnnotations?solutionTheory ?AngleSum/Solution â™
theory Problem =
@@ -77,7 +76,7 @@ theory AngleSum =
âš
theory OppositeLen =
- meta ?MetaAnnotations?problemTheory ?OppositeLen/Problem â™
+ meta ?MetaAnnotations?problemTheory ?OppositeLen/Problem â™
meta ?MetaAnnotations?solutionTheory ?OppositeLen/Solution â™
theory Problem =
@@ -109,11 +108,10 @@ theory OppositeLen =
âš
theory Pythagoras =
- meta ?MetaAnnotations?problemTheory ?Pythagoras/Problem â™
+ meta ?MetaAnnotations?problemTheory ?Pythagoras/Problem â™
meta ?MetaAnnotations?solutionTheory ?Pythagoras/Solution â™
theory Problem =
- // include ?TriangleScroll_RightAngledProblem â™
include ?TriangleProblem_RightAngleAtC â™
distanceAC
: Σ x:â„. ⊦ (d- A C) ≠x â˜
--
GitLab