Mechanized Mathematics and Its Applications, Works in Progress

Highschool Trigonometry with Mizar (Coghetto R.)

LetterHighschool (Secondary School) Trigonometry:
Some Exercices with Mizar
Roland Coghetto“cafr MAS2P” asbl (non proﬁt organization)
Rue de la Brasserie 5,7100 La Louvière, Belgium
roland.coghetto@cafr-msa2p.be
Proof checked by Mizar Version: 8.1.10 and MML Version: 5.63.1382
Received: October 13, 2021. Accepted: December 13, 2021.

Abstract
In this article, we have chosen 4 trigonometry exercises of high school level, 2 of whichhave been proposed to an entrance exam for engineering schools in Belgium. We showthat it is possible to formalize these exercises by taking into account the same instructions given to the students.
Our main motivation is to allow motivated students or those who do not have apedagogical support network to use the proof assistant to prepare their exam. For thisreason, we are exploring the possibility of simplifying as much as possible the obstacles
that would be speciﬁcally linked to Mizar and MML.
More precisely, we propose a methodology to avoid a long search for useful theorems
in the MML: Mizar allows to gather in a single ﬁle these results, the use of the Mizar
mode for emacs, the pursuit of proofs of useful trigonometry theorems, as well as theevaluation of the impact of some deﬁnitions and the use of division in the solution of
exercises.

1

Introduction

Historically, Mizar and the MML were not designed speciﬁcally for trigonometry [1]:“From its beginnings, Mizar was used as a tool for teaching mathematics:
initially, for teaching propositional logic, then, with the help of especially useful for educational purposes Mizar-MSE, introduction to logic for secondary
school students (this was also an example of a distant learning interactive
course as it was published in Polish popular science monthly Delta)” [2]
From 1998, some theorems related to trigonometry appear mainly in the series ofarticles SIN_COS ( [3–12] ) as well as in the series of articles DIFF ( [13–15] ) andFDIFF for the diﬀerentiation of trigonometric functions ( [16–21] ).
These articles have allowed the formalization of other theorems: Trigonometric Formof Complex Numbers [22], Borsuk-Ulam theorem [23], Basel problem [24, 25], Law of
cosines, Heron’s Formula and Ptolemy’s Theorem,... [26], Morley’s trisector theorem

MMA-WiP (2022), vol.4, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2022.4.1 - ISSN 2434-5458 (Online)

1/17

Mechanized Mathematics and Its Applications, Works in Progress

Highschool Trigonometry with Mizar (Coghetto R.)[27], Extended Law of sines [28], Model of euclidean plane (in Tarski plane geometry)[29], Leibniz’s Series for Pi [30], Routh’s, Menelaus’ and Generalized Ceva’s Theorems[31], Niven’s theorem [32], Primitive Roots of Unity and Cyclotomic Polynomials [33],. . .
Trigonometry has several entries in the MSC20201 (Mathematics Subject Classiﬁcation). For example, Trigonometric and exponential sums, general (11L03), Exponential
and trigonometric functions(33B10) and Plane and spherical trigonometry (educational
aspects)(97G60).
In this article we focus on trigonometry studied in high school and mainly the lastyears as well as exercises for the engineering entrance exam.
We hope to show that some exercises could be accessible to students using Mizar on
a PC, in combination with the Emacs extension for Mizar [34].
However, there are some limitations to letting students be autonomous with Mizar.
Indeed, it seems necessary to select some exercises that will be presented to the students.
This limitation is mainly due to some obstacles that may appear for the student:
lack of MML theorems ready for direct use, lack of knowledge of some subtleties of theMizar language, lack of understanding of algebraic reductions that Mizar performs ornot.
Moreover, the current feature, present in some proof assistants, of obtaining a result
when dividing by 0 can destabilize and lead to mathematically false results, as it will be
discussed in a later section. Nevertheless, this diﬀerence with respect to mathematics
can be contextualized in order not to lose the potential beneﬁts of using a proof assistant.
In spite of this, this article hopes to show that it is possible to formalize a certain
category of trigonometry exercises but also to parameterize the presentation of thetheorems.
For example, one diﬃculty is the complexity of exploring MML. It is possible toreduce this search complexity manually.
Indeed, the student is not obliged to navigate through the whole MML to ﬁnd thetheorems needed to justify the proofs. It is possible to group them in a ﬁle prepared by
the teacher.
Moreover this ﬁle can also contain justiﬁcations which are necessarily trivial but
which are distributed in other articles of the MML but which do not concern directly
the trigonometric functions: for example algebraic simpliﬁcations. Thus, the student
can ﬁnd the justiﬁcation more easily, because he does not know whether Mizar willautomatically perform a purely algebraic justiﬁcation or not.
For autonomous students, particularly motivated and aware of the current limitationsof the system, it is also possible to do without the teacher who would have prepare thesynthesis of the formulas to be used: he could theoretically solve the exercises by directly
using the MML. In the examples we present, the steps follow essentially the same steps
as those in the solutions proposed by high school teachers or exam testers.

2

Motivations

In Belgium, trigonometry is a subject taught in secondary school. The exercises proposed in this article will be at the level of the last years or at the level of an entrance
exam for civil engineering studies.
In the case of these entrance exams, all students are tested in writing on the various subjects mathematical subjects that make up the entrance examination. Theseevaluations take the form of four tests of two to three hours in length (trigonometry
and numerical calculation, analytical and synthetic geometry algebra, mathematicalanalysis) organized in two consecutive days.
1 https://zbmath.org/classiﬁcation/

MMA-WiP (2022), vol.4, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2022.4.1 - ISSN 2434-5458 (Online)

2/17

Mechanized Mathematics and Its Applications, Works in Progress

Highschool Trigonometry with Mizar (Coghetto R.)

The ﬁve disciplines that make up the subject matter of the exam include essentially the mathematics program of the three higher classes (strong mathematics) of the(strong mathematics) of secondary education: Algebra, Analysis, Geometry, Analytical
Geometry, and Trigonometry.
The exam questions of the previous years are made public as well as some solutions[35, 36].
The purpose of this article is not to check whether the statements are correct or not.
Our main goal is to evaluate the possibility to formalize, thanks to Mizar and MML,
some exercises or exam questions in trigonometry. This formalization must be of a level,
not of a mathematical researcher but of a level accessible to a secondary school teacher
and/or a student.
We hope to increase the interest of high school teachers on the usefulness of using a
proof assistant in this subject and to allow students, who would not have easy access toa pedagogical support network, to be autonomous in the understanding of some schoolor exam exercises.
To try to achieve this goal, we started with the following questions: Is it possible
to formalise certain exercises or exam questions using Mizar and MML ? what are thelimitations and obstacles of Mizar and MML ? can solutions be found to these limitations
and obstacles ? and why use Mizar ?
For this last question, our answer is that it is also possible to explore trigonometry exercises with other proof assistants. But after some personnal experimentation,
Mizar [37] seems to be suitable for the achievement of our main goal with three usefuladvantages:• Mizar is a ‘declarative’ proof assistants (as opposed to the ‘procedural’ proof
assistants) [38].
• Mizar allow Structured proofs [39]:”Structured Proofs.. Structured proofs allow a high degree of generality
and control without sacriﬁcing readability. Mizar is the canonical structured proof language and Isar is another prominent example. Structured
features can include fact naming, function deﬁnitions, declarative block
structure, and explicit syntax for low-level proof steps.” [40]• Emacs extension for Mizar [34].

3

Trigonometric questions

The particular choice of the following questions was inﬂuenced as much by the clear
and explicit instructions as by the statements already introduced and formalised in thecurrent MML.
The main instructions are [41, 42]:
• Knowledge of the classical special values of trigonometric and cyclometric functions• Knowledge and application of the formulae giving:– sin(−a), cos(−a), tan(−a);– sin(π ± a), cos(π ± a), tan(π ± a);– sin( π2 ± a), cos( π2 ± a), tan( π2 ± a);– sin(a ± b), cos(a ± b), tan(a ± b), sin(2a), cos(2a), tan(2a);MMA-WiP (2022), vol.4, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2022.4.1 - ISSN 2434-5458 (Online)

3/17

Mechanized Mathematics and Its Applications, Works in Progress

Highschool Trigonometry with Mizar (Coghetto R.)– sin p ± sinq, cos p ± cosq;– 1 ± cos(2a);– sin a, cos a, tan a as a function of tan a2 .
• The solution of the questions requires only the use of the above trigonometricformulae.
• Any other trigonometric formula used must be demonstrated.
The statements are
Q1 If C = (cos(x))2 − 2 ∗ cos(a) ∗ cos(x) ∗ cos(a + x) + (cos(a + x))2 et D = (cos(x))2 −2 ∗ sin(a) ∗ cos(x) ∗ sin(a + x) + (sin(a + x))2
Q1A Show that C and D are independent of the value of x.
Q1B Show that C + D = 1
Q2 Show that sin(78◦ ) − sin(18◦ ) + cos(132◦ ) = 0
Q3 (Question 2. Exam - Septembrer 1999 [41])Show that, if a + b + c = π then sin a − sin b + sin c = 4 sin a2 cos 2b sin 2c
Q4 (Question 2. Exam - July 2018 [42]) Prove that if A, B and C are three strictly
positive angles such that A + B + C = π2 thentan A tan B + tan B tan C + tan A tan C = 1

4

Exploring

In this exploration phase, we use the ’mmlreference’ tool to locate and identify thedeﬁnitions present in the MML and interesting in this stage, namely: sin, cos and tan2 .
It appears that the MML contains 2 deﬁnitions of sin, cos and tan:
Listing 1. SIN_COS:def 16
reserve d for Real;deﬁnition
func sin −> Function of REAL, REAL means:: SIN_COS:def 16
for d holds it.d = Im(Sum(d∗<i> ExpSeq));
end;which is the imaginary part of the Taylor series expansion of the well-known Euler
formula:+∞∑(ix)n(= =e(ix) )sin : R → R : x 7→ =n!
n=0
The following function is used to obtain the value at a point of R of the function sin,deﬁned previously.

2 MIZAR Forum:
Kazuhisa NAKASHO, 2 apr 2020, ’New URL of Mizar Reference Tool’.
(https://mimosa-project.github.io/mmlreference/current/)

MMA-WiP (2022), vol.4, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2022.4.1 - ISSN 2434-5458 (Online)

4/17

Mechanized Mathematics and Its Applications, Works in Progress

Highschool Trigonometry with Mizar (Coghetto R.)

Listing 2. SIN_COS:def 17
deﬁnition
let th be Real;func sin th −> number equals:: SIN_COS:def 17
sin.th;end;

Listing 3. SIN_COS:def 18
reserve d for Real;deﬁnition
func cos −> Function of REAL, REAL means:: SIN_COS:def 18
for d holds it.d = Re(Sum(d∗<i> ExpSeq));
end;which is the real part of the Taylor series expansion of the well-known Euler formula:( +∞)∑ (ix)n(= <e(ix) )cos : R → R : x 7→ <n!
n=0
The following function is used to obtain the value at a point of R of the function cos,deﬁned previously.
Listing 4. SIN_COS:def 19
deﬁnition
let th be Real;func cos th −> number equals:: SIN_COS:def 19
cos.th;end;

The function tan is deﬁned by
Listing 5. SIN_COS:def 26
deﬁnition
func tan −> PartFunc of REAL, REAL equals:: SIN_COS:def 26
sin/cos;end;

the domain of deﬁnition is given by the following theorem:
Listing 6. BASEL_1:16
theorem :: BASEL_1:16
dom tan = union the set of all ]. −PI/2+PI∗i,PI/2+PI∗i .[ where i is Integer;

Another deﬁnition of tan is given:
Listing 7. SIN_COS4:def 1
deﬁnition
let th be Real;func tan(th) −> Real equals:: SIN_COS4:def 1
sin(th)/cos(th);end;

MMA-WiP (2022), vol.4, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2022.4.1 - ISSN 2434-5458 (Online)

5/17

Mechanized Mathematics and Its Applications, Works in Progress

Highschool Trigonometry with Mizar (Coghetto R.)

these two deﬁnitions coincide on the domain of deﬁnition of the function tan deﬁned
in [SIN_COS:def 26] (see [BASEL_1:16]).
Listing 8. SIN_COS9:15
theorem :: SIN_COS9:15
for x be Real st cos.x <> 0 holds tan.x = tan x;but, [SIN_COS4:def 1] is also deﬁned for th = π2 + kπ, k ∈ Z.
In this case, in this MML version, see [TANERROR - abstract]tan(π+ kπ) =M izar 0
2

We discuss this result in a later section.
This version of the MML contains most of the results contained in the resolution
instructions.
For clarity, we have added 4 results that were not in the MML. (see ADDENDUM.MIZ).
We chose theorems with deﬁnitions of “sin”, “cos” and “tan” ([SIN_COS:def 17],
[SIN_COS:def 19], [SIN_COS4:def 1]), which seemed more numerous than those with
deﬁnitions [SIN_COS:def 16][SIN_COS:def 18][SIN_COS:def 26]. This choice is arbitrary.
Here are the diﬀerent results already contained in the MML. Some results have been
added (ADDENDUM ﬁle).
• Speciﬁc value of trigonometric functions:sin(0),cos(0), sin( π2 ), cos( π2 ), sin(π), cos(π) , sin(2π), cos(2π) (in SIN_COS [3]),3πsin( π4 ), cos( π4 ), sin(π), cos(π) (in SINCOS10 [12]), sin( π4 ), cos( π4 ), sin( 3π4 ), cos( 4 )
4π
4π
5π
5π
(in INTEGRA8 [43]), sin( 3 ), cos( 3 ), sin( 3 ), cos( 3 ) (in NIVEN [32]), sin( π3 ),
2πππcos( π3 ), sin( π6 ), cos( π6 ), sin( 2π3 ), cos( 3 ) (in EUCLID10 [44]), tan( 3 ), tan( 6 ) (inEUCLID10 [44]);• sin(-a), cos(-a), tg(-a):
sin(−a), cos(−a) (in SIN_COS [3]), tan(−a) (in SIN_COS4, [6]);• sin(pi ± a), cos(pi ± a), tg(pi ± a):sin(π−a), cos(π−a) (in EUCLID10, [44]), sin(π+a), cos(π+a) (in SIN_COS, [3]),tan(π −a) ([ADDENDUM:1]), tan(π +a) ([ADDENDUM:2]) sin(a−π), cos(a−π)(in COMPLEX2, [45]);• sin(pi/2 ± a), cos(pi/2 ± a), tg(pi/2 ± a):sin( π2 − a), cos( π2 − a), sin( π2 + a), cos( π2 + a) (in SIN_COS [3]) tan( π2 + a)([ADDENDUM:4]), tan( π2 − a) ([ADDENDUM:3])• sin (a ± b), cos(a ± b), tg(a ± b), sin 2a, cos 2a, tg 2a:sin(a + b), cos(a + b) (in SIN_COS [3]) sin(a − b), cos(a − b) (in COMPLEX2 [45]),tan(a + b),tan(a − b) (in SIN_COS4 [6]), sin(2a), cos(2a), tan(2a) (in SIN_COS5[7]);• sin p ± sin q, cos p ± cos q:
sin p + sin q, sin p − sin q, cos p + cos q, cos p − cos q (in SIN_COS4 [6])• 1 ± cos 2a:
1+cos(2a) 1−cos(2a),(in SIN_COS5 [7])22MMA-WiP (2022), vol.4, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2022.4.1 - ISSN 2434-5458 (Online)

6/17

Mechanized Mathematics and Its Applications, Works in Progress

Highschool Trigonometry with Mizar (Coghetto R.)• sin a, cos a, tg a depending on tg a/2:
2 tan(x)1−tan(x)2∗tan(x)sin(2a) = 1+(tan(x)2 ) , cos(2a) = 1+(tan(x)2 ) , tan(2a) = 1−(tan(x)2 ) (in SIN_COS5[7])

Listing 9. ADDENDUM:1
reserve a for Real;
theorem :: ADDENDUM:1
tan(PI − a) = − tan(a);Listing 10. ADDENDUM:2
reserve a for Real;
theorem :: ADDENDUM:2
tan(PI + a) = tan(a);Listing 11. ADDENDUM:3
reserve a for Real;
theorem :: ADDENDUM:3tan(PI/2 − a) = cot(a);Listing 12. ADDENDUM:4
reserve a for Real;
theorem :: ADDENDUM:4tan(PI/2 + a) = − cot(a);

5

Proof

The ﬁle “rep01.miz” ([REP01 - abstract]) contains the resolution of the 4 questions. We
try to follow the solutions that have been proposed and made public. It is obvious that
there are other proofs, both mathematically and by using other results of MML.
It has been reduced only with “relprem.”
Note that:• The Question Q2 has been solved using the unit "radian" and not "degree."• We introduced algebraic results, known to high school students but not yet formalised in the MML.
To translate question Q2 in terms of "degree" and not "radian," we used a feature ofMizar. This solution has been implemented in a ﬁle “deg.miz” ([DEG - abstract]) In thenext version of proofs, we have grouped in a ﬁle "formul1.miz" ([FORMUL1 - abstract])
only the useful results and previously at the "ﬁrst proof" stage.
The ﬁle "rep02.miz" was produced using only "formul1.miz." The demonstrations
have not been changed. The names of the theorems used have been updated.

MMA-WiP (2022), vol.4, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2022.4.1 - ISSN 2434-5458 (Online)

7/17

Mechanized Mathematics and Its Applications, Works in Progress

6

Discussion

6.1

Unicity of proof

Highschool Trigonometry with Mizar (Coghetto R.)

Each of the exercises studied in this article can be solved in diﬀerent ways. We havetested one method. We cannot guarantee that another method can be proven with thecurrent state of MML. This may limit mathematical creativity. It is possible to increase
the number of trigonometry theorems to increase the possible solution. It is not always
possible to predict methods for potential solutions.
It is well known that trigonometric statements, whose solution is accessible to highschool students, can admit an original proof. For example, with Hol/Light, the formalization of John Harrisson’s Morley’s theorem follows the proof of Alain Connes’s paper"A new proof of Morley’s theorem" [46]’3 . In this case, we cannot guarantee that there
is a simple and accessible proof for a student using the current MML.
The objective of this work is to guarantee at least one solution close to the solution
recommended by the examiners, taking into account their instructions.

6.2

Extending the domain of division

Trigonometry uses the division of real numbers.
It is well known that the division in expert assistants is a problem. Mizar is no
exception to this rule. ([DIVZERO.miz])
Listing 13. DIVZERO.miz
environvocabularies CARD_1, ARYTM_3;
notations NUMBERS, XCMPLX_0;
constructors EUCLID_3;
registrations ORDINAL1, XXREAL_0, XREAL_0;
requirements NUMERALS, SUBSET, ARITHM;
equalities XCMPLX_0;
begin
theorem
1 / 0 = 0;

“Extending the domain of division with x/0 = 0 (and also for integers) is acommon choice in a great many systems, not just Isabelle/HOL but HOL
Light, HOL4, MetiTarski and doubtless many other systems. They do it
simply for convenience and not for any deep reason. The point is that manylaws involving division will then hold unconditionally, an example being(a*b)/(c*d) = (a/c)*(b/d).” (Larry Paulson, June 2018)4
What solution to implement for the "division by 0" result problem. Several solutions
are to be explored:• not change anything because, historically, experiments have found it more interesting to keep the deﬁnition of the division and report diﬀerent eﬀects.
• not change anything because of this current diﬀerence between some proof assistants and mathematics, a proof assistant is not always appropriate, especially forhigh school math. It is better to wait for the next generation of proof assistant.
3 https://github.com/ jrh13/hol-light/blob/master/100/morley.ml
4 https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-June/msg00108.html

MMA-WiP (2022), vol.4, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2022.4.1 - ISSN 2434-5458 (Online)

8/17

Mechanized Mathematics and Its Applications, Works in Progress

Highschool Trigonometry with Mizar (Coghetto R.)• change nothing in the MML, but clone the theorems and allow only the algebraic
operations possible in mathematics?
• deﬁne a new operation "division"?
• modify the division operation by adding a condition "assume b <> 0", for thecase ’a/b’ ?
The tangent being deﬁned as a quotient, the same problem can also reappear.
It is easy to prove with Mizar [TANERROR - abstract] thatπtan( ) =Mizar 0
2and also more generally that, if k is an integer, then wetan(π+ k × π) =Mizar 0
2What solutions for the π2 tangent problem?
• always use the ﬁrst deﬁnition of tan([SIN_COS:def 26]), which admits a mathematically correct domain. This would also require to consider only the formulas
containing the ﬁrst deﬁnitions of sin ([SIN_COS:def 16]) and cos ([SIN_COS:def
18]).
• use the second deﬁnition of tan ([SIN_COS4:def 1]) but adding "assume cos x<> 0 ", for example.

7

Work in progress

We have seen above that some useful theorems are not yet formalized. The current work
consists in completing this list. Moreover, given the proximity of the demonstrations
with some statements with spherical or hyperbolic trigonometry, the list would also becompleted with other statements with reference to these two types of trigonometries.
Listing 14. SIN_COS4:15
theorem :: SIN_COS4:15
sin(th1)+sin(th2)= 2∗(cos((th1−th2)/2)∗sin((th1+th2)/2));

During the formalization, some errors could be confusing. For example the use of the[SIN_COS4:15] theorem can lead to a benign error. Indeed, the parentheses indicate aright associativity while without parentheses, it is a left associativity. It is important tonote that sometimes Mizar oﬀers useful calculation automatisms, sometimes a simple
parenthesis in a multiplication can lead to the addition of an extra line. The work
continues to discover some algebraic diﬃculties.
About Emacs, it is not necessary in practice to know all the keyboard shortcuts.
Apart from a few keys for classic text changes, saving and exiting Emacs, the "CTRL x+RET" key is useful. Unfortunately, Emacs is not easily installed on some well-known
operating systems. We are looking for a solution to make the manipulations accessible
for a large part of users.
A web service might be useful, if it integrates the possibility to use the featuresof "miz2abs" and "miz2prel" in order to allow the use of formularies ﬁles. To ourknowledge, there is the web service Automated Reasoning for Mizar 5 , which one of thegoals is the automatic search for proof in an article, which also allows to check if an
5 http://grid01.ciirc.cvut.cz/ mptp/MizAR.html

MMA-WiP (2022), vol.4, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2022.4.1 - ISSN 2434-5458 (Online)

9/17

Mechanized Mathematics and Its Applications, Works in Progress

Highschool Trigonometry with Mizar (Coghetto R.)

article is correct or not. Unfortunately, at the moment it is not possible to combine thisservice with a tool like "miz2prel" to use another article. However, the possibility ofusing a remote service can be useful in certain situations. We explore the trigonometricstatements that would be compatible with the use of this system at this time.
It would be useful to test some proof automatisms for faster proof search of trigonometric statements. To the author’s knowledge, there are still few automatic proofs inthe ﬁeld of trigonometry. Indeed, in the list "Interesting ATP Proofs"6 by Josef Urban,
only one trigonometry theorem is listed:
Listing 15. SIN_COS6:28
theorem :: SIN_COS6:28
0 <= r & r <= 2∗PI & sin r = 1 implies r = PI/2;

We are also exploring the possibility of using the remote tool mentioned in the previous
paragraph to ﬁnd some proof more quickly. This work is limited to the preparation ofa method that could allow an easier use of Mizar in the presented context. If groups ofstudents test the method, modiﬁcations will be made according to the results. At thisstage, no experimentation is planned.

8Conclusion

In this letter, we use statements, most of which have already been demonstrated in the
MML, to solve trigonometry questions proposed in secondary school.
We have encountered some diﬃculties with the deﬁnitions of trigonometric functions,mainly those associated with division by zero and also, but more anecdotally, withalgebraic simpliﬁcations.
Although the licence of the MML allows for a fork, we ask the Mizar community
whether it would be useful to make changes to some of the deﬁnitions presented here inorder to integrate them into the main branch of the MML or not.
In order to prepare a more student-friendly protocol, we aim to complete, with
automatic or non-automatic demonstration tools, the missing trigonometric statements,
to evaluate the relevance of the deﬁnitions in this context, and to use a user-friendly
text editor.

References[1] Borak E, Zalewska A. Mizar course in logic and set theory. In: Towards Mechanized
Mathematical Assistants. Springer; 2007. p. 191–204.
[2] Grabowski A, Korniłowicz A, Naumowicz A. Four decades of Mizar. Journal ofAutomated Reasoning. 2015;55(3):191–198.
[3] Yang Y, Shidama Y. Trigonometric Functions and Existence of Circle Ratio. Formalized Mathematics. 1998;7(2):255–263. Available from: http://fm.mizar.org/
1998-7/pdf7-2/sin_cos.pdf.
[4] Mitsuishi T, Yang Y. Properties of the Trigonometric Function. Formalized
Mathematics. 1999;8(1):103–106. Available from: http://fm.mizar.org/1999-8/
pdf8-1/sin_cos2.pdf.

6 https://github.com/JUrban/ATP_Proofs#enigma-learns-to-count

MMA-WiP (2022), vol.4, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2022.4.1 - ISSN 2434-5458 (Online)

10/17

Mechanized Mathematics and Its Applications, Works in Progress

Highschool Trigonometry with Mizar (Coghetto R.)[5] Mitsuishi T, Endou N, Ohkubo K. Trigonometric Functions on Complex Space.
Formalized Mathematics. 2003;11(1):29–32. Available from: http://fm.mizar.
org/2003-11/pdf11-1/sin_cos3.pdf.
[6] Pacharapokin C, Kanchun, Yamazaki H. Formulas and Identities of Trigonometric
Functions. Formalized Mathematics. 2004;12(2):139–141. Available from: http://fm.mizar.org/2004-12/pdf12-2/sin_cos4.pdf.
[7] Ding Y, Liang X. Formulas and Identities of Trigonometric Functions. Formalized Mathematics. 2004;12(3):243–246. Available from: http://fm.mizar.org/
2004-12/pdf12-3/sin_cos5.pdf.
[8] Korniłowicz A, Shidama Y. Inverse Trigonometric Functions Arcsin and Arccos.
Formalized Mathematics. 2005;13(1):73–79. Available from: http://fm.mizar.
org/2005-13/pdf13-1/sin_cos6.pdf.
[9] Ge F, Liang X, Ding Y. Formulas and Identities of Inverse Hyperbolic Functions.
Formalized Mathematics. 2005;13(3):383–387. Available from: http://fm.mizar.
org/2005-13/pdf13-3/sin_cos7.pdf.
[10] Pacharapokin C, Yamazaki H. Formulas and Identities of Hyperbolic Functions.
Formalized Mathematics. 2005;13(4):511–513. Available from: http://fm.mizar.
org/2005-13/pdf13-4/sin_cos8.pdf.
[11] Liang X, Xie B. Inverse Trigonometric Functions Arctan and Arccot. Formalized
Mathematics. 2008;16(2):147–158.
[12] Xie B, Liang X, Ge F. Inverse Trigonometric Functions Arcsec and Arccosec.
Formalized Mathematics. 2008;16(2):159–165.
[13] Li B, Zhuang Y, Liang X. Diﬀerence and Diﬀerence Quotient. Part II. Formalized
Mathematics. 2008;16(1):45–49.
[14] Liang X, Tang L. Diﬀerence and Diﬀerence Quotient. Part III. Formalized Mathematics. 2010;18(1):57–64.
[15] Liang X, Tang L, Jiang X. Diﬀerence and Diﬀerence Quotient. Part IV. Formalized
Mathematics. 2011;19(1):35–39.
[16] Zhang Y, Liang X. Several Diﬀerentiable Formulas of Special Functions. Formalized Mathematics. 2005;13(3):427–434. Available from: http://fm.mizar.org/
2005-13/pdf13-3/fdiff_4.pdf.
[17] Cao J, Zhai F, Liang X. Some Diﬀerentiable Formulas of Special Functions. Formalized Mathematics. 2005;13(4):505–509. Available from: http://fm.mizar.org/
2005-13/pdf13-4/fdiff_5.pdf.
[18] Zhang Y, Li B, Liang X. Several Diﬀerentiable Formulas of Special Functions.
Part II. Formalized Mathematics. 2005;13(4):529–535. Available from: http://fm.mizar.org/2005-13/pdf13-4/fdiff_6.pdf.
[19] Li B, Zhang Y, Liang X. Several Diﬀerentiation Formulas of Special Functions.
Part III. Formalized Mathematics. 2006;14(1):37–45.
[20] Li B, Wang P. Several Diﬀerentiation Formulas of Special Functions. Part VI.
Formalized Mathematics. 2007;15(4):243–250.
[21] Ge F, Xie B. Several Diﬀerentiation Formulas of Special Functions. Part VII.
Formalized Mathematics. 2008;16(4):389–399.

MMA-WiP (2022), vol.4, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2022.4.1 - ISSN 2434-5458 (Online)

11/17

Mechanized Mathematics and Its Applications, Works in Progress

Highschool Trigonometry with Mizar (Coghetto R.)[22] Milewski R. Trigonometric Form of Complex Numbers. Formalized Mathematics. 2001;9(3):455–460. Available from: http://fm.mizar.org/2001-9/pdf9-3/
comptrig.pdf.
[23] Korniłowicz A, Riccardi M. The Borsuk-Ulam Theorem. Formalized Mathematics.
2012;20(2):105–112.
[24] Korniłowicz A, Pąk K. Basel Problem – Preliminaries. Formalized Mathematics.
2017;25(2):141–147.
[25] Pąk K, Korniłowicz A. Basel Problem. Formalized Mathematics. 2017;25(2):149–
155.
[26] Riccardi M. Heron’s Formula and Ptolemy’s Theorem. Formalized Mathematics.
2008;16(2):97–101.
[27] Coghetto R. Morley’s Trisector Theorem. Formalized Mathematics. 2015;23(2):75–
79.
[28] Coghetto R. Circumcenter, Circumcircle and Centroid of a Triangle. Formalized
Mathematics. 2016;24(1):17–26.
[29] Coghetto R, Grabowski A. Tarski Geometry Axioms – Part II. Formalized Mathematics. 2016;24(2):157–166.
[30] Pąk K. Leibniz Series for π. Formalized Mathematics. 2016;24(4):275–280.
[31] Shminke BA. Routh’s, Menelaus’ and Generalized Ceva’s Theorems. Formalized
Mathematics. 2012;20(2):157–159.
[32] Korniłowicz A, Naumowicz A.
2016;24(4):301–308.

Niven’s Theorem.

Formalized Mathematics.

[33] Arneson B, Rudnicki P. Primitive Roots of Unity and Cyclotomic Polynomials.
Formalized Mathematics. 2004;12(1):59–67. Available from: http://fm.mizar.
org/2004-12/pdf12-1/uniroots.pdf.
[34] Urban J. MizarMode―an integrated proof assistance tool for the Mizar way offormalizing mathematics. Journal of Applied Logic. 2006;4(4):414–427.
[35] FACSA Examen d’entrée;. Accessed: 2021-09-03. https://www.facsa.uliege.
be/cms/c_3231988/fr/facsa-examen-d-entree.
[36] Examen d’admission : Trigonométrie et calcul numérique;. Accessed: 2021-09-03.
http://www.ingveh.ulg.ac.be/index.php?page=examen-d-admission.
[37] Bancerek G, Byliński C, Grabowski A, Korniłowicz A, Matuszewski R, Naumowicz
A, et al. Mizar: State-of-the-art and beyond. In: International Conference onIntelligent Computer Mathematics. Springer; 2015. p. 261–279.
[38] Wenzel M, Wiedijk F. A comparison of Mizar and Isar. Journal of AutomatedReasoning. 2002;29(3):389–411.
[39] Naumowicz A. Teaching how to write a proof. Formal Methods in Computer
Science Education. 2008;p. 91.
[40] Bohrer B, Platzer A. Structured Proofs for Adversarial Cyber-Physical Systems.
ACM Transactions on Embedded Computing Systems (TECS). 2021;20(5s):1–26.

MMA-WiP (2022), vol.4, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2022.4.1 - ISSN 2434-5458 (Online)

12/17

Mechanized Mathematics and Its Applications, Works in Progress

Highschool Trigonometry with Mizar (Coghetto R.)[41] Dewallef P, Duysinx P. Examen d admission aux études de bachelier ingénieur
civil et architecte Trigonométrie et calcul numérique; 1999. Accessed: 202109-03. Available from: http://www.ingveh.ulg.ac.be/uploads/admin_exam/
QSept1999_trigono_solution.pdf.
[42] Dewallef P, Louveaux Q. Examen d admission aux études de bachelier ingénieur civil et architecte Trigonométrie et calcul numérique; 2018. Available from:https://www.facsa.uliege.be/upload/docs/application/pdf/
2018-09/q2018_trigono_solution.pdf.
[43] Peng C, Ge F, Liang X. Several Integrability Formulas of Special Functions. Formalized Mathematics. 2007;15(4):189–198.
[44] Coghetto R. Some Facts about Trigonometry and Euclidean Geometry. Formalized
Mathematics. 2014;22(4):313–319.
[45] Chang W, Nakamura Y, Rudnicki P. Inner Products and Angles of Complex
Numbers. Formalized Mathematics. 2003;11(3):275–280. Available from: http://fm.mizar.org/2003-11/pdf11-3/complex2.pdf.
[46] Connes A. A new proof of Morley’s theorem. Publications Mathématiques del’IHÉS. 1998;88:43–46.

Mizar article information
Works in Progress
FORMUGEN FORMUGEN.miz is a ﬁle containing some deﬁnitions and results
concerning trigonometry and already proved in the MML. We try to increase the corpusof theorems directly related to this subject. It is possible, if the results are interesting
and useful to propose them in a new article for the MML.
Listing 16. TANERROR - abstract
environvocabularies CARD_1, RELAT_1, ARYTM_3, SIN_COS, INT_1;
notations NUMBERS, XCMPLX_0, SIN_COS, SIN_COS4, INT_1;
constructors SIN_COS, SIN_COS4, EUCLID_3;
registrations ORDINAL1, XXREAL_0, XREAL_0, INT_1, SIN_COS;
requirements NUMERALS, SUBSET, ARITHM;
equalities XCMPLX_0, SIN_COS4;
theorems SIN_COS, BASEL_1;
begintan(PI/2) = 0 by SIN_COS:77;
for i being Integer holds tan(PI/2 + i ∗ PI) = 0
proof
let i be Integer;tan(PI/2 + i ∗ PI) = sin(PI/2 + i ∗ PI) / cos(PI/2 + i ∗ PI).= sin(PI/2 + i ∗ PI) / 0 by BASEL_1:14.= 0;
hence thesis;
end;

MMA-WiP (2022), vol.4, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2022.4.1 - ISSN 2434-5458 (Online)

13/17

Mechanized Mathematics and Its Applications, Works in Progress

Highschool Trigonometry with Mizar (Coghetto R.)

Listing 17. REP01 - abstract
environvocabularies NUMBERS, REAL_1, RELAT_1, ARYTM_3, ARYTM_1, SQUARE_1, SIN_COS,
CARD_1, XXREAL_0, INT_1;
notations XREAL_0, XCMPLX_0, SQUARE_1, SIN_COS, XXREAL_0, SIN_COS4, NUMBERS,
INT_1;
constructors SQUARE_1, SIN_COS, SIN_COS4, TOPALG_6;
registrations XREAL_0, SQUARE_1, SIN_COS, XCMPLX_0, ORDINAL1, XXREAL_0, INT_1,
SIN_COS6;
requirements REAL, NUMERALS, SUBSET, ARITHM;
equalities SQUARE_1, SIN_COS4, XCMPLX_0;
theorems SIN_COS, SIN_COS4, EUCLID10, XCMPLX_1,
XREAL_1, XXREAL_0, BORSUK_7, INT_1,SIN_COS5;
begin
theorem :: REP01:1
for a,x being Real holds(cos(x))^2 − 2 ∗ cos(a)∗cos(x)∗cos(a+x)+(cos(a+x))^2 = (sin(a))^2;
theorem :: REP01:2
for a,x being Real holds(cos(x))^2 − 2 ∗ sin(a)∗cos(x)∗sin(a+x)+(sin(a+x))^2 = (cos(a))^2;
theorem :: REP01:3
for a,x being Real holds(cos(x))^2 − 2 ∗ cos(a)∗cos(x)∗cos(a+x)+(cos(a+x))^2 +(cos(x))^2 − 2 ∗ sin(a)∗cos(x)∗sin(a+x)+(sin(a+x))^2 = 1;
theorem :: REP01:4
for a,b,c being Real st a + b + c = PI holdssin(a) − sin(b) + sin(c) = 4 ∗ sin(a/2) ∗ cos(b/2) ∗ sin(c/2);
theorem :: REP01:5
for a being Real holds cos(2∗a) = 1 − 2 ∗ (sin(a))^2;
theorem :: REP01:6
for a being Real holds (sin(a))^2 = (1 − cos(2 ∗ a))/2;
theorem :: REP01:7
for a,b,c being Real st a + b + c = PI holds(sin(a))^2 + (sin(b))^2 + (cos(c))^2 = 1 + 2 ∗ sin(a) ∗ sin(b) ∗ cos(c);theorem :: REP01:8
for a,b,c being Real st 0 < a & 0 < b & 0 < c & a + b + c = PI/2 holds
a < PI/2;
theorem :: REP01:9
for a,b,c being Real st 0 < a & 0 < b & 0 < c & a + b + c = PI/2 holds
a < PI/2 & b < PI/2 & c < PI/2;
theorem :: REP01:10
for a being Real st 0 < a < PI/2 holds cos(a) <> 0;
theorem :: REP01:11
for a,b,c,d,e,f being Real holds(a / b) ∗ (c / d) ∗ (e / f) = (a ∗ c ∗ e) / (b ∗ d ∗ f);theorem :: REP01:12
for a,b,c being Real st a > 0 & b > 0 & c > 0 & a + b + c = PI/2 holds
tan(a) ∗ tan(b) + tan(b) ∗ tan(c) + tan(a) ∗ tan(c) = 1;:: sin(78)−sin(18)+cos(132)=0
theorem :: REP01:13
for x being Real holds
sin(x)−sin(x−(PI/3))+cos(PI + PI/6 − x) = 0;

MMA-WiP (2022), vol.4, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2022.4.1 - ISSN 2434-5458 (Online)

14/17

Mechanized Mathematics and Its Applications, Works in Progress

Highschool Trigonometry with Mizar (Coghetto R.)

Listing 18. DEG - abstract
environvocabularies REAL_1, CARD_1, RELAT_1, ARYTM_3, ARYTM_1, SIN_COS, DEG;
notations NUMBERS, XREAL_0, XCMPLX_0, SIN_COS;
constructors XXREAL_2, SIN_COS;
registrations ORDINAL1, XCMPLX_0, XREAL_0;
requirements NUMERALS, SUBSET, ARITHM;
theorems XCMPLX_1, COMPTRIG;
begin
deﬁnition
let a be Real;func a deg −> Real equals:: DEG:def 1
PI ∗ (a / 180);end;
deﬁnition
let a be Real;func a rad −> Real equals:: DEG:def 2a;end;
theorem :: DEG:1
for a being Real holds a deg = (PI / 180) ∗ a rad;theorem :: DEG:2
for a being Real holds a rad = (180 / PI) ∗ a deg;
deﬁnition
let a be Real;func a^o −> Real equals:: DEG:def 3
PI ∗ (a / 180);
end;
theorem :: DEG:30 ^o = 0 & 30^o = PI/6 & 45^o = PI/4& 60^o = PI/3&90 ^o = PI/2 &120^o = 4∗ PI/6 & 135^o = 3∗PI/4& 150^o=5∗PI/6& 180^o = PI;theorem :: DEG:40 deg = 0 & 30 deg = PI/6 & 45 deg = PI/4 & 60 deg = PI/3 rad &90 deg = PI/2 rad &120 deg = 4∗ PI/6 & 135 deg = 3∗PI/4& 150 deg =5∗PI/6& 180 deg = PI;theorem :: DEG:5
18 deg = 78 deg − PI/3 &132 deg = PI + PI/6 − 78 deg;

Listing 19. FORMUL1 - abstract
environvocabularies NUMBERS, REAL_1, XXREAL_0, CARD_1, RELAT_1, XCMPLX_0, ARYTM_3,
ARYTM_1, SQUARE_1, SIN_COS, INT_1;
notations NUMBERS, XXREAL_0, XREAL_0, XCMPLX_0, SQUARE_1, SIN_COS, INT_1;
constructors SQUARE_1, SIN_COS, TOPREALC;
registrations ORDINAL1, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, INT_1, SIN_COS,
SIN_COS6;
requirements REAL, NUMERALS, SUBSET, ARITHM;
theorems INT_1, SIN_COS, SIN_COS4, SIN_COS5, EUCLID10, XXREAL_0, XREAL_1,
BORSUK_7, XCMPLX_1;
begin

MMA-WiP (2022), vol.4, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2022.4.1 - ISSN 2434-5458 (Online)

15/17

Mechanized Mathematics and Its Applications, Works in Progress

Highschool Trigonometry with Mizar (Coghetto R.)

reserve a,x,th,th1,th2 for Real;
theorem :: FORMUL1:1(cos(th))^2+(sin(th))^2=1 &(cos(th))∗(cos(th))+(sin(th))∗(sin(th))=1;
theorem :: FORMUL1:2
sin(th1+th2)=(sin(th1)) ∗(cos(th2))+(cos(th1)) ∗ (sin(th2)) &cos(th1+th2)=(cos(th1)) ∗(cos(th2))−(sin(th1)) ∗ (sin(th2));
theorem :: FORMUL1:3
sin(2∗x) = 2∗sin(x)∗cos(x);theorem :: FORMUL1:4
sin(th1)−sin(th2)= 2∗(cos((th1+th2)/2)∗sin((th1−th2)/2));
theorem :: FORMUL1:5
sin(th1)+sin(th2)= 2∗(cos((th1−th2)/2)∗sin((th1+th2)/2));
theorem :: FORMUL1:6
cos(0)=1 & sin(0)=0 & cos(−th)=cos(th) & sin(−th)=−sin(th);theorem :: FORMUL1:7
cos(2∗x)=(cos(x))^2−(sin(x))^2 & cos(2∗x)=2∗(cos(x))^2−1 & cos(2∗x)=1−2∗(sin(x))^2;
theorem :: FORMUL1:8
cos (PI−a) = − cos a;theorem :: FORMUL1:9
cos(th1)+cos(th2)= 2∗(cos((th1+th2)/2)∗cos((th1−th2)/2));
theorem :: FORMUL1:10
cos(th1)−cos(th2)= −2∗(sin((th1+th2)/2)∗sin((th1−th2)/2));
theorem :: FORMUL1:11
cos(0)=1 & sin(0)=0 & cos(−th)=cos(th) & sin(−th)=−sin(th);theorem :: FORMUL1:12
sin(th+2 ∗ PI) = sin(th) & cos(th+2 ∗ PI) = cos(th) &sin(PI/2−th) = cos(th) & cos(PI/2−th) = sin(th) & sin(PI/2+th) = cos(th) &cos(PI/2+th) = −sin(th) & sin(PI+th) = −sin(th) &cos(PI+th) = −cos(th);theorem :: FORMUL1:13
sin(PI/6) = 1/2;
begin
theorem :: FORMUL1:14
for a,b,c being Real st 0 < a & 0 < b & 0 < c & a + b + c = PI/2 holds
a < PI/2;
theorem :: FORMUL1:15
for a,b,c being Real st 0 < a & 0 < b & 0 < c & a + b + c = PI/2 holds
a < PI/2 & b < PI/2 & c < PI/2;
theorem :: FORMUL1:16
for a being Real st 0 < a < PI/2 holds cos(a) <> 0;
begin
theorem :: FORMUL1:17
for a,b,c,d,e,f being Real holds(a / b) ∗ (c / d) ∗ (e / f) = (a ∗ c ∗ e) / (b ∗ d ∗ f);theorem :: FORMUL1:18
for a being Complex st a <> 0 holds a / a = 1;

MMA-WiP (2022), vol.4, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2022.4.1 - ISSN 2434-5458 (Online)

16/17

Mechanized Mathematics and Its Applications, Works in Progress

Highschool Trigonometry with Mizar (Coghetto R.)

Listing 20. REP02 - abstract
environvocabularies NUMBERS, REAL_1, RELAT_1, ARYTM_3, ARYTM_1, SQUARE_1, SIN_COS,
CARD_1, XXREAL_0, INT_1,DEG;
notations XREAL_0, XCMPLX_0, SQUARE_1, SIN_COS, XXREAL_0, SIN_COS4, NUMBERS,
INT_1,DEG;
constructors SQUARE_1, SIN_COS, SIN_COS4, TOPALG_6,DEG;
registrations XREAL_0, SQUARE_1, SIN_COS, XCMPLX_0, ORDINAL1, XXREAL_0, INT_1,
SIN_COS6;
requirements REAL, NUMERALS, SUBSET, ARITHM;
equalities SQUARE_1, SIN_COS4, XCMPLX_0;
theorems SIN_COS, SIN_COS4, EUCLID10, XCMPLX_1,
XREAL_1, XXREAL_0, BORSUK_7, INT_1,SIN_COS5;
theorems FORMUL1,DEG;
begintheorem :: REP02:1
for a,x being Real holds(cos(x))^2 − 2 ∗ cos(a)∗cos(x)∗cos(a+x)+(cos(a+x))^2 = (sin(a))^2;
theorem :: REP02:2
for a,x being Real holds(cos(x))^2 − 2 ∗ sin(a)∗cos(x)∗sin(a+x)+(sin(a+x))^2 = (cos(a))^2;
theorem :: REP02:3
for a,x being Real holds(cos(x))^2 − 2 ∗ cos(a)∗cos(x)∗cos(a+x)+(cos(a+x))^2 +(cos(x))^2 − 2 ∗ sin(a)∗cos(x)∗sin(a+x)+(sin(a+x))^2 = 1;
theorem :: REP02:4
for a,b,c being Real st a + b + c = PI holdssin(a) − sin(b) + sin(c) = 4 ∗ sin(a/2) ∗ cos(b/2) ∗ sin(c/2);
theorem :: REP02:5
for a being Real holds cos(2∗a) = 1 − 2 ∗ (sin(a))^2;
theorem :: REP02:6
for a being Real holds (sin(a))^2 = (1 − cos(2 ∗ a))/2;
theorem :: REP02:7
for a,b,c being Real st a + b + c = PI holds(sin(a))^2 + (sin(b))^2 + (cos(c))^2 = 1 + 2 ∗ sin(a) ∗ sin(b) ∗ cos(c);theorem :: REP02:8
for a,b,c being Real st a > 0 & b > 0 & c > 0 & a + b + c = PI/2 holds
tan(a) ∗ tan(b) + tan(b) ∗ tan(c) + tan(a) ∗ tan(c) = 1;:: sin(78)−sin(18)+cos(132)=0
theorem :: REP02:9
for x being Real holds
sin(x)−sin(x−(PI/3))+cos(PI + PI/6 − x) = 0;
theorem :: REP02:10
sin(78 deg) − sin(18 deg) + cos(132 deg) = 0;

MMA-WiP (2022), vol.4, no.1 - http://mizar-jp.org/journal/MMA-WiP/j2022.4.1 - ISSN 2434-5458 (Online)

17/17