Proof Checking Euclid

This repository is an attempt to understand

Beeson, Michael, et al. ‘Proof-Checking Euclid’. Annals of Mathematics and Artificial Intelligence, vol. 85, no. 2–4, Apr. 2019, pp. 213–57. DOI.org (Crossref), https://doi.org/10.1007/s10472-018-9606-x.

and https://github.com/GeoCoq/GeoCoq specifically.

Most of the code here is a direct translation but auto tactic and the like are not used. The goal is to be able to follow how the proof unfolds.

Reading order

Each lemma has a tree of dependencies, and so the dependencies need to be introduced in a particular order.

With all the above proved the following unrelated lemma can also be proved:

lemma_road_to_reality_2_7

Differences from GeoCoq

cn_equalityreverse is renamed to cn_congruencereverse. I think the original name is due to how this common notion was applied in the .prf files: EEABBA cn:equalityreverse . I found this hard to follow given that the rest of the congruence common notions start with congruence.
lemma_3_6a and the like are renamed to lemma_orderofpoints_ABC_ACD_BCD and the like. Section "8 Book Zero and filling in book I" mentions "several important and often-used lemmas [that] are about the order of four points on a line, when two betweenness relations are known between them", which seems to match lemma_3_6a and the like. I found orderofpoints to be a more appropriate name for those lemmas.
axiom_innertransitivity is renamed to axiom_orderofpoints_ABD_BCD_ABC to match the renaming of lemma_3_6a into lemma_orderofpoints_ABC_ACD_BCD.
Most primitives and definitions are renamed to be more spelled out.
- OS -> SameSide
  - OS presumably comes from "one side", but there are lemmas like lemma_samesidereflexive, whish suggest SameSide to be an appropriate name.
- TS -> OppositeSide
  - TS presumably comes from "two sides", but there are lemmas like lemma_oppositesideflip, whish suggest OppositeSide to be an appropriate name.
- Out -> OnRay
- Per -> RightTriangle
  - I found definition of Square to be more natural with 4 RightTriangles than with 4 Pers.
- RT -> SumTwoRT
- SumA -> AngleSum
- TG -> TogetherGreater
- TP -> TarskiPar
- CR -> Cross
- PG -> Parallelogram
- SQ -> Square
- Cong_3 -> CongTriangles
- ET -> EqAreaTri
  - Being explicit about the kind of equality used seems prudent, especially given how prominent congruence is.
- EF -> EqAreaQuad
- RE -> Rectangle
Lemmas that encode properties of objects that can be pithily expressed were renamed to start with by_prop_$OBJECT_ so that it is easier to find them and to ignore them in proof text. If there was no pithy way to express the property, or if the proof of the property turned out to be very complex, I've mostly left unchanged.
lemma_onray[12345] instead of having numeric suffixes have evocative if not descriptive suffixes, by_prop_OnRay_orderofpoints_any instead of lemma_ray1.
lemma_collinear[124] instead of having a numeric suffixes have evocative if not descriptive suffixes, by_prop_Col_ABC_BAC instead of lemma_collinear1.
You can find the full list of renames in sed_renames.txt.
Many lemmas are introduced to make it easier to use some of the definitions, these lemmas were named to start with by_def_$OBJECT_.
Many lemmas are introduced to make sense of what is going on. Newly introduced lemmas start with lemma_s , with s for supporting.
Long proofs by contradiction that assert the lemma's goal were re-structured as proofs "by cases", thus turning contrdict+exact into just exact.

Diagrams

lemma_localextension
proposition_01
proposition_02
by_prop_Lt_congruence
- The illustration includes triangles implied by axiom_5_line, where point D is "moving onto the line". See section "6.6 Degenerate cases".
proposition_09
proposition_10_pasch_F
proposition_10_pasch_M
proposition_12
proposition_16_LtA_BAC_ACD
proposition_16_LtA_CBA_ACD
proposition_18

How diagrams were generated

Diagrams were built by hand in GeoGebra .
Downloaded as SVG.
Clipped with Inkscape .
Cleaned up with format_geogebra_svg.sh .

GeoGebra is used as a way of enforcing straightedge-and-compass construction.

Name		Name	Last commit message	Last commit date
Latest commit History 189 Commits
.gitignore		.gitignore
LICENSE		LICENSE
README.md		README.md
_CoqProject.in		_CoqProject.in
build_order.sh		build_order.sh
by_def_AngleSum.v		by_def_AngleSum.v
by_def_Col_from_BetS_A_B_C.v		by_def_Col_from_BetS_A_B_C.v
by_def_Col_from_BetS_A_C_B.v		by_def_Col_from_BetS_A_C_B.v
by_def_Col_from_BetS_B_A_C.v		by_def_Col_from_BetS_B_A_C.v
by_def_Col_from_eq_A_B.v		by_def_Col_from_eq_A_B.v
by_def_Col_from_eq_A_C.v		by_def_Col_from_eq_A_C.v
by_def_Col_from_eq_B_C.v		by_def_Col_from_eq_B_C.v
by_def_Col_from_n_nCol.v		by_def_Col_from_n_nCol.v
by_def_CongA.v		by_def_CongA.v
by_def_CongTriangles.v		by_def_CongTriangles.v
by_def_Cross.v		by_def_Cross.v
by_def_Cut.v		by_def_Cut.v
by_def_InAngle.v		by_def_InAngle.v
by_def_InCirc_center.v		by_def_InCirc_center.v
by_def_InCirc_within_radius.v		by_def_InCirc_within_radius.v
by_def_Lt.v		by_def_Lt.v
by_def_LtA.v		by_def_LtA.v
by_def_LtA_from_InAngle.v		by_def_LtA_from_InAngle.v
by_def_Meet.v		by_def_Meet.v
by_def_Midpoint.v		by_def_Midpoint.v
by_def_OnCirc.v		by_def_OnCirc.v
by_def_OnRay.v		by_def_OnRay.v
by_def_OnRay_from_BetS_A_B_E.v		by_def_OnRay_from_BetS_A_B_E.v
by_def_OnRay_from_BetS_A_E_B.v		by_def_OnRay_from_BetS_A_E_B.v
by_def_OnRay_from_neq_A_B.v		by_def_OnRay_from_neq_A_B.v
by_def_OppositeSide.v		by_def_OppositeSide.v
by_def_OutCirc.v		by_def_OutCirc.v
by_def_Par.v		by_def_Par.v
by_def_Parallelogram.v		by_def_Parallelogram.v
by_def_Perp_at.v		by_def_Perp_at.v
by_def_Rectangle.v		by_def_Rectangle.v
by_def_RightTriangle.v		by_def_RightTriangle.v
by_def_SameSide.v		by_def_SameSide.v
by_def_Square.v		by_def_Square.v
by_def_SumTwoRT.v		by_def_SumTwoRT.v
by_def_Supp.v		by_def_Supp.v
by_def_TT.v		by_def_TT.v
by_def_TarskiPar.v		by_def_TarskiPar.v
by_def_TogetherGreater.v		by_def_TogetherGreater.v
by_def_Triangle.v		by_def_Triangle.v
by_def_isosceles.v		by_def_isosceles.v
by_def_nCol_from_Triangle.v		by_def_nCol_from_Triangle.v
by_def_nCol_from_n_Col.v		by_def_nCol_from_n_Col.v
by_def_n_Col_from_nCol.v		by_def_n_Col_from_nCol.v
by_prop_AngleSum_respects_congruence.v		by_prop_AngleSum_respects_congruence.v
by_prop_BetS_notequal.v		by_prop_BetS_notequal.v
by_prop_Col_ABC_ABD_ABE_CDE.v		by_prop_Col_ABC_ABD_ABE_CDE.v
by_prop_Col_ABC_ABD_BCD.v		by_prop_Col_ABC_ABD_BCD.v
by_prop_Col_ABC_BAC.v		by_prop_Col_ABC_BAC.v
by_prop_Col_ABC_BCA.v		by_prop_Col_ABC_BCA.v
by_prop_Col_order.v		by_prop_Col_order.v
by_prop_CongA_ABCequalsCBA.v		by_prop_CongA_ABCequalsCBA.v
by_prop_CongA_NC.v		by_prop_CongA_NC.v
by_prop_CongA_distinct.v		by_prop_CongA_distinct.v
by_prop_CongA_flip.v		by_prop_CongA_flip.v
by_prop_CongA_flip_left.v		by_prop_CongA_flip_left.v
by_prop_CongA_flip_right.v		by_prop_CongA_flip_right.v
by_prop_CongA_helper.v		by_prop_CongA_helper.v
by_prop_CongA_reflexive.v		by_prop_CongA_reflexive.v
by_prop_CongA_symmetric.v		by_prop_CongA_symmetric.v
by_prop_CongA_transitive.v		by_prop_CongA_transitive.v
by_prop_CongTriangles_reflexive.v		by_prop_CongTriangles_reflexive.v
by_prop_Cong_doublereverse.v		by_prop_Cong_doublereverse.v
by_prop_Cong_flip.v		by_prop_Cong_flip.v
by_prop_Cong_symmetric.v		by_prop_Cong_symmetric.v
by_prop_Cong_transitive.v		by_prop_Cong_transitive.v
by_prop_EqAreaQuad_reflexive.v		by_prop_EqAreaQuad_reflexive.v
by_prop_EqAreaTri_reflexive.v		by_prop_EqAreaTri_reflexive.v
by_prop_LtA_respects_congruence.v		by_prop_LtA_respects_congruence.v
by_prop_LtA_respects_congruence_smaller.v		by_prop_LtA_respects_congruence_smaller.v
by_prop_LtA_transitive.v		by_prop_LtA_transitive.v
by_prop_Lt_additive.v		by_prop_Lt_additive.v
by_prop_Lt_asymmetric.v		by_prop_Lt_asymmetric.v
by_prop_Lt_between.v		by_prop_Lt_between.v
by_prop_Lt_congruence.svg		by_prop_Lt_congruence.svg
by_prop_Lt_congruence.v		by_prop_Lt_congruence.v
by_prop_Lt_congruence_smaller.v		by_prop_Lt_congruence_smaller.v
by_prop_Lt_notequal.v		by_prop_Lt_notequal.v
by_prop_Lt_transitive.v		by_prop_Lt_transitive.v
by_prop_Lt_trichotomous.v		by_prop_Lt_trichotomous.v
by_prop_OnRay_ABC_ACB.v		by_prop_OnRay_ABC_ACB.v
by_prop_OnRay_ABC_BAC_BetS_ACB.v		by_prop_OnRay_ABC_BAC_BetS_ACB.v
by_prop_OnRay_assert.v		by_prop_OnRay_assert.v
by_prop_OnRay_betweenness.v		by_prop_OnRay_betweenness.v
by_prop_OnRay_impliescollinear.v		by_prop_OnRay_impliescollinear.v
by_prop_OnRay_neq_A_B.v		by_prop_OnRay_neq_A_B.v
by_prop_OnRay_neq_A_C.v		by_prop_OnRay_neq_A_C.v
by_prop_OnRay_orderofpoints_any.v		by_prop_OnRay_orderofpoints_any.v
by_prop_OnRay_shared_initial_point.v		by_prop_OnRay_shared_initial_point.v
by_prop_OppositeSide_flip.v		by_prop_OppositeSide_flip.v
by_prop_OppositeSide_symmetric.v		by_prop_OppositeSide_symmetric.v
by_prop_Par_NC.v		by_prop_Par_NC.v
by_prop_Par_collinear.v		by_prop_Par_collinear.v
by_prop_Par_collinear2.v		by_prop_Par_collinear2.v
by_prop_Par_flip.v		by_prop_Par_flip.v

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Repository files navigation

Proof Checking Euclid

Reading order

Differences from GeoCoq

Diagrams

How diagrams were generated

About

Uh oh!

Releases

Packages

Languages

License

blin/proof-checking-euclid

Folders and files

Latest commit

History

Repository files navigation

Proof Checking Euclid

Reading order

Differences from GeoCoq

Diagrams

How diagrams were generated

About

Resources

License

Uh oh!

Stars

Watchers

Forks

Releases

Packages 0

Languages

Packages