# Smooth manifolds and types to sets for linear algebra in Isabelle/HOL

CPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs Cascais Portugal January, 2019, pp. 65-77, 2019.

EI

Keywords:

Weibo:

Abstract:

We formalize the definition and basic properties of smooth manifolds in Isabelle/HOL. Concepts covered include partition of unity, tangent and cotangent spaces, and the fundamental theorem for line integrals. We also construct some concrete manifolds such as spheres and projective spaces. The formalization makes extensive use of the exist...More

Code:

Data:

Introduction

- Smooth manifolds is one of the most important concepts in modern mathematics and physics.
- Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL.
- The existing Isabelle library on linear algebra has theorems mostly about vector spaces defined on the entire type.

Highlights

- Smooth manifolds is one of the most important concepts in modern mathematics and physics
- We describe how to formalize the basic concepts of smooth manifolds in Isabelle/HOL
- We discuss some of the difficulties and lessons learned during our work
- We divide this into two parts: mathematical difficulties related to imprecise exposition in textbooks, and difficulties related to limitations of Isabelle/HOL’s simple type theory
- Since the concept of smooth manifolds is long established in mathematics, we do not expect to discover any problems with the foundations during the formalization process
- While none of the problems are serious, it still shows that in advanced mathematics, definitions of even basic concepts can be subtle, and formalization can serve as a stringent check on the correctness of these definitions

Results

- Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL CPP ’19, January 14–15, 2019, Cascais, Portugal property of topological spaces, taking about 200 lines of Isar text to prove, and makes use of the second-countability condition.
- There is one peculiar detail about these basic facts: the tangent space tangent_space p is formalized as a set, whereas the library for linear algebra in Isabelle/HOL requires vector spaces to be a type.
- For the endeavor of obtaining set based theorems from a type based formalization, Step 1 is to assume a subspace S of a vector space given by a type ’b::ab_group_add and scaling operation scale::real ⇒ ’b ⇒ ’b.
- This definition of dim makes it possible to define and prove dim_S related to dim with the transfer rule for Hilbert choice (Eps_unique_transfer_lemma) from types to sets.
- The notion of vector space in the Isabelle/HOL analysis library (Section 4.1) relies on a type class constraint ’b::ab_group_add.
- The transfer package proves automatically that this can be transferred from types to sets: lemma vector_space_on_with_transfer: assumes "right_total R" "bi_unique R" shows
- The notion of a linear map from a type ’a to a type ’b involves two vector spaces, which are implicitly given the corresponding scaling functions s1::real ⇒ ’a ⇒ ’a and s2::real ⇒ ’b ⇒ ’b.
- In order to illustrate the whole chain of steps that are performed when translating a theorem from the type based library of linear algebra to a set based statement, the authors will work step by step through one example.

Conclusion

- This leaves them with an additional assumption ∃Rep Abs. type_definition Rep Abs S, and with vector space operations on ’s, namely plus_S, minus_S, uminus_S, zero_S, scale_S, Basis_S defined in terms of Abs and Rep. The authors' initial assumption that S posesses a finite basis yields finite_dimensional_vector_space_on_with UNIV plus_S minus_S uminus_S zero_S scale_S
- 2http://isabelle.in.tum.de/ in theory src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy
- The text incorrectly claims that ψ ◦ f ◦ φ−1 is defined on all of Rn. In O’Neill’s textbook [14, Chapter 1, Definition 6], an additional condition is added stating that ψ ◦ f ◦φ−1 defined on an open set of Rn. In both textbooks, it is claimed that continuity follows immediately from differentiability, without discussing the potential issues.

Summary

- Smooth manifolds is one of the most important concepts in modern mathematics and physics.
- Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL.
- The existing Isabelle library on linear algebra has theorems mostly about vector spaces defined on the entire type.
- Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL CPP ’19, January 14–15, 2019, Cascais, Portugal property of topological spaces, taking about 200 lines of Isar text to prove, and makes use of the second-countability condition.
- There is one peculiar detail about these basic facts: the tangent space tangent_space p is formalized as a set, whereas the library for linear algebra in Isabelle/HOL requires vector spaces to be a type.
- For the endeavor of obtaining set based theorems from a type based formalization, Step 1 is to assume a subspace S of a vector space given by a type ’b::ab_group_add and scaling operation scale::real ⇒ ’b ⇒ ’b.
- This definition of dim makes it possible to define and prove dim_S related to dim with the transfer rule for Hilbert choice (Eps_unique_transfer_lemma) from types to sets.
- The notion of vector space in the Isabelle/HOL analysis library (Section 4.1) relies on a type class constraint ’b::ab_group_add.
- The transfer package proves automatically that this can be transferred from types to sets: lemma vector_space_on_with_transfer: assumes "right_total R" "bi_unique R" shows
- The notion of a linear map from a type ’a to a type ’b involves two vector spaces, which are implicitly given the corresponding scaling functions s1::real ⇒ ’a ⇒ ’a and s2::real ⇒ ’b ⇒ ’b.
- In order to illustrate the whole chain of steps that are performed when translating a theorem from the type based library of linear algebra to a set based statement, the authors will work step by step through one example.
- This leaves them with an additional assumption ∃Rep Abs. type_definition Rep Abs S, and with vector space operations on ’s, namely plus_S, minus_S, uminus_S, zero_S, scale_S, Basis_S defined in terms of Abs and Rep. The authors' initial assumption that S posesses a finite basis yields finite_dimensional_vector_space_on_with UNIV plus_S minus_S uminus_S zero_S scale_S
- 2http://isabelle.in.tum.de/ in theory src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy
- The text incorrectly claims that ψ ◦ f ◦ φ−1 is defined on all of Rn. In O’Neill’s textbook [14, Chapter 1, Definition 6], an additional condition is added stating that ψ ◦ f ◦φ−1 defined on an open set of Rn. In both textbooks, it is claimed that continuity follows immediately from differentiability, without discussing the potential issues.

Funding

- Both authors were supported by Deutsche Forschungsgesellschaft under DFG Kosseleck Grant No NI 491/16-1
- The first author was supported by the Air Force Office of Scientific Research under Grant No FA9550-18-1-0120

Reference

- Glen E. Bredon. 1993. Topology and Geometry. Springer, New York.
- Jose Divasón and Jesús Aransay. 2013. Rank-Nullity Theorem in Linear Algebra. Archive of Formal Proofs (Jan. 2013). http://isa-afp.org/entries/ Rank_Nullity_Theorem.html, Formal proof development.
- Florian Haftmann and Makarius Wenzel. 2009. Local Theory Specifications in Isabelle/Isar. In Types for Proofs and Programs, Stefano Berardi, Ferruccio Damiani, and Ugo de’Liguoro (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 153–168.
- John Harrison. 2005. A HOL Theory of Euclidean Space. In Theorem Proving in Higher Order Logics, Joe Hurd and Tom Melham (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 114–129.
- Morris W. Hirsch. 1976. Differential Topology. Springer, New York.
- Johannes Hölzl, Fabian Immler, and Brian Huffman. 2013. Type Classes and Filters for Mathematical Analysis in Isabelle/HOL. In Interactive Theorem Proving, Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.). Springer, Berlin, Heidelberg, 279–294.
- Alexei Averchenko (https://math.stackexchange.com/users/3793/alexei averchenko).2011. An example of a derivation at a point on a Ck -manifold which is not a tangent vector. Mathematics Stack Exchange.https://math.stackexchange.com/q/73677
- Pedro (https://math.stackexchange.com/users/9921/pedro).2014. Ck manifolds:how and why? Mathematics Stack Exchange.https://math.stackexchange.com/q/914790
- Fabian Immler and Bohua Zhan. 2018. Smooth Manifolds. Archive of Formal Proofs (Oct. 2018). http://isa-afp.org/entries/Smooth_
- Ondřej Kunčar. 2016. Types, Abstraction and Parametric Polymorphism in Higher-Order Logic. Dissertation. Technische Universität München, München. http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20160408-1285267-1-5
- Ondřej Kunčar and Andrei Popescu. 2018. From Types to Sets by Local Type Definition in Higher-Order Logic. Journal of Automated Reasoning (04 Jun 2018). https://doi.org/10.1007/s10817-018-9464-6
- John M. Lee. 20Introduction to Smooth Manifolds. Springer, New York.
- Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, Vol. 2283. Springer.
- Barrett O’Neill. 1983. Semi-Riemannian geometry, with applications to relativity. Academic Press, San Diego.
- Andrew M. Pitts. 1993. The HOL Logic. In Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, M. J. C. Gordon and T. F. Melham (Eds.). Cambridge University Press, New York, NY, USA, 191–232.
- Karol Pąk. 2014. Topological Manifolds. Formalized Mathematics 22, 2 (2014), 179 – 186.
- Randy Randerson. 2015. Smooth maps (between manifolds) are continuous (comment in Barrett O’Neill’s textbook). Mathematics Stack Exchange. https://math.stackexchange.com/q/1234599
- Michael Spivak. 1965. Calculus on Manifolds: A Modern Approach to Classical Theorems of Advanced Calculus. Addison-Wesley, Reading, Massachusetts.
- Michael Spivak. 1999. A Comprehensive Introduction to Differential Geometry, Volume One. Publish or Perich Inc., Houston.

Full Text

Tags

Comments