Skip to main content
SpringerLink
Log in
Book cover

International Conference on Interactive Theorem Proving

ITP 2017: Interactive Theorem Proving pp 28–45Cite as

A Formalization of Convex Polyhedra Based on the Simplex Method

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10499))

Abstract

We present a formalization of convex polyhedra in the proof assistant Coq. The cornerstone of our work is a complete implementation of the simplex method, together with the proof of its correctness and termination. This allows us to define the basic predicates over polyhedra in an effective way (i.e. as programs), and relate them with the corresponding usual logical counterparts. To this end, we make an extensive use of the Boolean reflection methodology. The benefit of this approach is that we can easily derive the proof of several essential results on polyhedra, such as Farkas Lemma, duality theorem of linear programming, and Minkowski Theorem.

The authors were partially supported by the programme “Ingénierie Numérique & Sécurité” of ANR, project “MALTHY”, number ANR-13-INSE-0003, by a public grant as part of the Investissement d’avenir project, reference ANR-11-LABX-0056-LMH, LabEx LMH and by the PGMO program of EDF and FMJH.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • 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

Learn about institutional subscriptions

Notes

  1. 1.

    Available in a git repository at https://github.com/nhojem/Coq-Polyhedra.

  2. 2.

    Finding how small \(\varepsilon \) must be chosen is tedious, and this would make proofs unnecessarily complicated.

  3. 3.

    We make a slight abuse of language, since feasibility usually applies to linear programs. By extension, we apply it to polyhedra: \(\mathcal {P}(A,b)\) is feasible if it is nonempty.

  4. 4.

    We let the reader check that the associated basic point is , where x is the basic point associated with the basis , and that this point is feasible.

References

  1. Avis, D., Fukuda, K.: A pivoting algorithm for convex hulls and vertex enumeration of arrangements and polyhedra. Discrete Comput. Geom. 8(3), 295–313 (1992)

    Article  MathSciNet  Google Scholar 

  2. Barthe, G., Forest, J., Pichardie, D., Rusu, V.: Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. In: Hagiya, M., Wadler, P. (eds.) FLOPS 2006. LNCS, vol. 3945, pp. 114–129. Springer, Heidelberg (2006). doi:10.1007/11737414_9

    Chapter  MATH  Google Scholar 

  3. Besson, F.: Fast reflexive arithmetic tactics the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 48–62. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74464-1_4

    Chapter  MATH  Google Scholar 

  4. Bremner, D., Deza, A., Hua, W., Schewe, L.: More bounds on the diameters of convex polytopes. Optim. Methods Softw. 28(3), 442–450 (2013)

    Article  MathSciNet  Google Scholar 

  5. Cohen, C., Dénès, M., Mörtberg, A.: Refinements for free! In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 147–162. Springer, Cham (2013). doi:10.1007/978-3-319-03545-1_10

  6. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of POPL 1978, Tucson, Arizona. ACM Press (1978)

    Google Scholar 

  7. Dantzig, G.B.: Maximization of a linear function of variables subject to linear inequalities. In: Activity Analysis of Production and Allocation. Wiley (1951)

    Google Scholar 

  8. Dantzig, G.B., Orden, A., Wolfe, P.: The generalized simplex method for minimizing a linear form under linear inequality restraints. Pac. J. Math. 5(2), 183–195 (1955)

    Article  MathSciNet  Google Scholar 

  9. Fouilhe, A., Boulmé, S.: A certifying frontend for (sub)polyhedral abstract domains. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 200–215. Springer, Cham (2014). doi:10.1007/978-3-319-12154-3_13

    Chapter  Google Scholar 

  10. Gonthier, G.: Point-free, set-free concrete linear algebra. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 103–118. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22863-6_10

    Chapter  Google Scholar 

  11. Gonthier, G., Mahboubi, A., Tassi, E.: A small scale reflection extension for the Coq system. Research Report RR-6455, Inria Saclay Ile de France (2016)

    Google Scholar 

  12. Guglielmi, N., Laglia, L., Protasov, V.: Polytope Lyapunov functions for stable and for stabilizable LSS. Found. Comput. Math. 17(2), 567–623 (2017)

    Article  MathSciNet  Google Scholar 

  13. Harrison, J.: The HOL light theory of Euclidean space. J. Autom. Reason. 50, 173–190 (2013)

    Article  MathSciNet  Google Scholar 

  14. Khachiyan, L.: Polynomial algorithms in linear programming. USSR Comput. Math. Math. Phys. 20(1), 53–72 (1980)

    Article  MathSciNet  Google Scholar 

  15. Sakaguchi, K.: VASS (2016). https://github.com/pi8027/vass

  16. Santos, F.: A counterexample to the Hirsch conjecture. Ann. Math. 176(1), 383–412 (2012)

    Article  MathSciNet  Google Scholar 

  17. Smale, S.: Mathematical problems for the next century. Math. Intell. 20, 7–15 (1998)

    Article  MathSciNet  Google Scholar 

  18. Spasić, M., Marić, F.: Formalization of incremental simplex algorithm by stepwise refinement. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 434–449. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32759-9_35

    Chapter  Google Scholar 

Download references

Acknowledgments

The authors are very grateful to A. Mahboubi for her help to improve the presentation of this paper, and to G. Gonthier, F. Hivert and P.-Y. Strub for fruitful discussions. The second author is also grateful to M. Cristiá for introducing him to the topic of automated theorem proving. The authors finally thank the anonymous reviewers for their suggestions and remarks.

Author information

Authors and Affiliations

  1. Inria and CMAP, Ecole Polytechnique, CNRS, Université Paris–Saclay, Paris, France

    Xavier Allamigeon

  2. CIFASIS-CONICET, Rosario, Argentina

    Ricardo D. Katz

Authors
  1. Xavier Allamigeon
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ricardo D. Katz
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Xavier Allamigeon .

Editor information

Editors and Affiliations

  1. University of Brasília, Brasília D.F., Brazil

    Mauricio Ayala-Rincón

  2. NASA, Hampton, VA, USA

    César A. Muñoz

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Allamigeon, X., Katz, R.D. (2017). A Formalization of Convex Polyhedra Based on the Simplex Method. In: Ayala-Rincón, M., Muñoz, C.A. (eds) Interactive Theorem Proving. ITP 2017. Lecture Notes in Computer Science(), vol 10499. Springer, Cham. https://doi.org/10.1007/978-3-319-66107-0_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66107-0_3

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66106-3

  • Online ISBN: 978-3-319-66107-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation