Skip to main content
Springer Nature Link
Log in

Formalizing Some “Small” Finite Models of Projective Geometry in Coq

  • Conference paper
  • First Online:
Artificial Intelligence and Symbolic Computation (AISC 2018)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 11110))

  • 599 Accesses

Abstract

We study two different descriptions of incidence projective geometry: a synthetic, mathematics-oriented one and a more practical, computation-oriented one, based on the combinatorial concept of rank of a set of points. Using both axiom systems, we prove that some specific finite planes (resp. spaces) verify the axioms of projective plane (resp. space) geometry and Desargues’ property. It requires using repeated case analysis on all variables of some finite inductive data-types and leads to numerous (sub-)goals in the Coq proof assistant. We thus investigate to what extend Coq can deal with such a combinatorial explosion in the number of cases to handle. We propose some easy-to-implement but relevant proof optimizations which, combined together, lead to an efficient way to deal with such large proofs.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
€32.70 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (France)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 42.79
Price includes VAT (France)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 52.74
Price includes VAT (France)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    The perspector is the point at which the three lines connecting the vertices of two perspective triangles concur.

  2. 2.

    Computer setup: Intel(R) Core(TM) i5-4460 CPU @ 3.20 GHz with 16G of memory.

  3. 3.

    An interactive representation of pg(3, 2) can be viewed on wolfram web site: http://demonstrations.wolfram.com/15PointProjectiveSpace/.

  4. 4.

    Fully-specified functions can be automatically defined using the proof search capabilities of Coq.

References

  1. Armand, M., Grégoire, G., Keller, B., Théry, L., Werner, B.: Verifying SAT and SMT in Coq for a fully automated decision procedure. In: International Workshop on Proof-Search in Axiomatic Theories and Type Theories (PSATTT 2011) (2011)

    Google Scholar 

  2. Batten, L.M.: Combinatorics of Finite Geometries. Cambridge University Press, Cambridge (1997)

    Book  Google Scholar 

  3. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development, Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-662-07964-5

    Book  MATH  Google Scholar 

  4. Braun, D., Magaud, N., Schreck, P.: An equivalence proof between rank theory and incidence projective geometry. In: Automated Deduction in Geometry (ADG 2016), pp. 62–77 (2016)

    Google Scholar 

  5. Buekenhout, F. (ed.): Handbook of Incidence Geometry. North Holland, Amsterdam (1995)

    MATH  Google Scholar 

  6. Coq Development Team: The Coq Proof Assistant Reference Manual, Version 8.6. LogiCal Project (2017)

    Google Scholar 

  7. Coxeter, H.S.M.: Projective Geometry. Springer, New York (2003)

    MATH  Google Scholar 

  8. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  9. Hall, M.: Projective planes. Trans. Am. Math. Soc. 54(2), 229–277 (1943)

    Article  MathSciNet  Google Scholar 

  10. Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_1

    Chapter  Google Scholar 

  11. Magaud, N., Narboux, J., Schreck, P.: Formalizing projective plane geometry in Coq. In: Sturm, T., Zengler, C. (eds.) ADG 2008. LNCS (LNAI), vol. 6301, pp. 141–162. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21046-4_7

    Chapter  MATH  Google Scholar 

  12. Magaud, N., Narboux, J., Schreck, P.: A case study in formalizing projective geometry in Coq: Desargues theorem. Comput. Geom.: Theor. Appl. 45(8), 406–424 (2012)

    Article  MathSciNet  Google Scholar 

  13. Mahboubi, A., Tassi, E.: Mathematical Components. Draft (2016)

    Google Scholar 

  14. Michelucci, D., Schreck, P.: Incidence constraints: a combinatorial approach. Int. J. Comput. Geom. Appl. 16(5), 443–460 (2006)

    Article  MathSciNet  Google Scholar 

  15. Moulton, F.R.: A simple non-desarguesian plane geometry. Trans. Am. Math. Soc. 3(2), 192–195 (1902)

    Article  MathSciNet  Google Scholar 

  16. Oxley, J.G.: Matroid Theory, vol. 3. Oxford University Press, Oxford (2006)

    MATH  Google Scholar 

  17. Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 43(4), 337 (2009)

    Article  MathSciNet  Google Scholar 

  18. Tebbi, T., Gross, J.: A profiler for Ltac. In: Coq PL Workshop 2015 (2015)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Icube UMR 7357 CNRS - Université de Strasbourg (IGG), Illkirch Cedex, France

    David Braun, Nicolas Magaud & Pascal Schreck

Authors
  1. David Braun
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nicolas Magaud
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Pascal Schreck
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nicolas Magaud .

Editor information

Editors and Affiliations

  1. University of Edinburgh, Edinburgh, United Kingdom

    Jacques Fleuriot

  2. Beihang University, Beijing, China

    Dongming Wang

  3. Karlsruhe Institute of Technology, Karlsruhe, Germany

    Jacques Calmet

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Braun, D., Magaud, N., Schreck, P. (2018). Formalizing Some “Small” Finite Models of Projective Geometry in Coq. In: Fleuriot, J., Wang, D., Calmet, J. (eds) Artificial Intelligence and Symbolic Computation. AISC 2018. Lecture Notes in Computer Science(), vol 11110. Springer, Cham. https://doi.org/10.1007/978-3-319-99957-9_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-99957-9_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-99956-2

  • Online ISBN: 978-3-319-99957-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation