Automated Reasoning Tools in GeoGebra
Computing numerical checks of certain relations between geometric objects in a planar construction is a well known feature of dynamic geometry systems. GeoGebra's newest improvements offer symbolic checks of equality, parallelism, perpendicularity, collinearity, concurrency or concyclicity. Also dragging of locus curves, defined explicitly or implicitly (or as an envelope curve) is a new feature in GeoGebra to visually check conjectures in planar geometry. By combining plotting and proving we can focus on some new possibilities to teach Euclidean geometry in the classrooms. This GeoGebraBook was presented at the University of South Bohemia in České Budějovice at [url=http://home.pf.jcu.cz/~upvm/2017/index.php/english-info/]the 8th conference "The Use of Computers in Mathematics Education"[/url] on 10 November 2017. A [url=http://test.geogebra.org/~kovzol/talks/upvm2017/]plenary talk[/url] was also given before it in the same topic.
Table of Contents
- New tools
- Existing and new tools
- Relation tool and command demo (Euler line)
- LocusEquation (explicit)
- LocusEquation (implicit)
- Envelope
- Example of explicit locus derivation VIII
- A possible workflow
- A possible classroom scenario
- Converse of Thales' circle theorem and the theorem of the inscribed angle in a triangle
- Converse of the intercept theorem
- A generalization of Simson-Wallace
- Pech-Blažek theorem
- Further examples (workshop)
- Golden ratio
- The right triangle altitude theorem
- 4-bar linkages: drag and play
- The lambda version of Chebyshev's linkage
- This is not a circle
Existing and new tools
Automated reasoning tools are a collection of GeoGebra tools and commands ready to conjecture, discover, adjust and prove geometric statements in a dynamic geometric construction. First the user needs to draw a geometric figure by using certain tools. After constructing the figure, GeoGebra has many ways to promote investigating geometrical properties of a figure by various tools and settings:[br][list=1][*]By [b]dragging the free objects[/b] their dependent objects can be visually investigated.[br][/*][*]The [b]Relation[/b] tool helps comparing objects and obtaining relations.[/*][*]By setting the [b]trace[/b] of a constructed object on/off the movement of an object will be visualized when its parent objects are changing.[br][/*][*]The [b]Locus[/b] tool shows the trace of an object for all possible positions of a parent object (while it moves on a path).[/*][*]By typing the [b]Relation[/b] or [b]Locus[/b] [b]command[/b] in GeoGebra's Input Bar more refined information can be[br]obtained.[/*]These methods are usually well known by the GeoGebra community, and therefore they are well documented. On the other hand, currently GeoGebra also offers symbolic automated reasoning tools for generalizing the observed/conjectured geometric properties:[br][*]The [b]Relation tool[/b] and [b]command[/b] can be used to recompute the results [b]symbolically[/b].[/*][*]The [b]LocusEquation command[/b] refines the result of the Locus command by displaying the algebraic equation of the graphical output.[/*][*]The LocusEquation command can investigate [b]implicit loci[/b].[/*][*]The [b]Envelope[/b] command computes the equation of a curve which is tangent to a family of objects while a certain parent of the object moves on a path.[/*]Also some low level methods exists (only for experts or for debugging purposes):[br][*]The [b]Prove[/b] command to get yes/no answer on a truth a statement.[/*][*]The [b]ProveDetails[/b] command to get yes/no answer on a truth a statement with more information (including non-degeneracy or essential conditions).[/*][/list]
A possible classroom scenario
Technically the Relation tool and command are the easiest symbolic means. On the other hand, some teaching scenarios may require different tools to consider, or more than one tool, but in a different order than listed previously.
The workflow
[list=1][*]An [b]implicit locus[/b] is computed with GeoGebra,[br][/*][*]a [b]conjecture[/b] for the output curve is made by the pupil,[br][/*][*]the conjecture is checked by the [b]Relation tool[/b] or [b]command[/b] in GeoGebra,[br][/*][*]the proof can be optionally worked out by [b]paper and pencil[/b] by the pupil,[br][/*][*]the theorem can be generalized by plotting further implicit loci with GeoGebra—as further experiments for the pupil. Actually the pupils should be allowed to "just [b]play[/b]" with the applet, to modify it: to just try to find new, interesting relations.[/*][/list]
Golden ratio
Definition
Two quantities are in the golden ratio if their ratio is the same as the ratio of their sum to the larger of the two quantities.
By using the [code]LocusEquation[g/h==f/g,C][/code] command one can find the approximate place of the golden cut of segment [i]AB[/i]. (For technical reasons, if the locus is a zero dimensional object, then its algebraic equation contains some numerical approximations. If you zoom in the figure, you may find that the equation is changing on deeper zooming: its coefficients are usually bigger.)[br]By zooming out, surprisingly you will find another point at about -1.618 which also fulfills the criterion. Actually, GeoGebra's Automated Reasoning Tools, due to the mathematical background being used, always handles both irrational roots of a quadratic equation indistinguishly, so it is impossible to designate only one root of them.
Constructing the golden ratio
The classic method to construct the golden ratio for a given segment [i]AB[/i] is as shown below. Here we explicitly construct the length [math]\frac{\sqrt{5}-1}{2}[/math], assuming that [i]AB[/i]=1. Now by typing [code]Relation[f/p,p/(f-p)][/code] we can conclude that [i]f[/i]/[i]p[/i] is indeed the golden ratio of [i]f[/i].
It makes sense to compare other expressions of [i]f[/i] and [i]p[/i]. For example, [i]G[/i] must be the golden cut for the segment [i]AH[/i]. Can you check this property by using the Relation command again?
Diagonals of a regular pentagon
It is well known that the proportion of a diagonal and a side of a regular pentagon is in the golden ratio. To check this, draw a regular pentagon with GeoGebra, create one of its diagonals, and check the proportion by using the Relation command. (Make sure you show the labels of the created objects by using the right click of the mouse. Then you can refer to the labels easily in the typed command.)
Pentagon in the pentagon, and so on
In the following figure (taken from a [url=http://italianroots.blogspot.co.at/2012/05/]blog[/url], but it can also be found in Jonathan Quintin's video [url=https://www.youtube.com/watch?v=VkHiV2SvATk]The Golden Key[/url] from 1:40) you can find an idea to embed arbitrary many pentagons in a regular way.
Construct this figure with GeoGebra and find equal long segments among the appearing ones. So you can directly derive further proportions which are again the golden ratio.
Finallly... the regular decagon
The golden ratio also appears in a combination of a regular pentagon and a regular decagon, having the same side lengths, as shown below.
Challenges
[list=1][*]Find golden cuts in the figure and confirm your conjectures by using GeoGebra Automated Reasoning Tools. You can create additional segments by using the appropriate tool if needed.[/*][*]Which property does the point [i]L[/i] have? Confirm your conjecture.[/*][/list]