research-article

Public Access

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

Authors:

Bohua ZhanAuthors Info & Claims

CPP 2019: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs

Pages 65 - 77

https://doi.org/10.1145/3293880.3294093

Published: 14 January 2019 Publication History

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 existing libraries for topology and analysis. The existing library for linear algebra is not flexible enough for our needs. We therefore set up the first systematic and large scale application of ``types to sets''. It allows us to automatically transform the existing (type based) library of linear algebra to one with explicit carrier sets.

References

[1]

Glen E. Bredon. 1993. Topology and Geometry. Springer, New York.

[2]

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.

[3]

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.

Digital Library

[4]

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.

Digital Library

[5]

Morris W. Hirsch. 1976. Differential Topology. Springer, New York.

[6]

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.

Digital Library

[7]

Alexei Averchenko (https://math.stackexchange.com/users/3793/alexei averchenko). 2011. An example of a derivation at a point on a C k -manifold which is not a tangent vector. Mathematics Stack Exchange. https://math.stackexchange.com/q/73677

[8]

Pedro (https://math.stackexchange.com/users/9921/pedro). 2014. C k -manifolds: how and why? Mathematics Stack Exchange. https://math. stackexchange.com/q/914790

[9]

Fabian Immler and Bohua Zhan. 2018. Smooth Manifolds. Archive of Formal Proofs (Oct. 2018). http://isa-afp.org/entries/Smooth_ Manifolds.html, Formal proof development.

[10]

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

[11]

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).

[12]

John M. Lee. 2012. Introduction to Smooth Manifolds. Springer, New York.

[13]

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.

Digital Library

[14]

Barrett O’Neill. 1983. Semi-Riemannian geometry, with applications to relativity. Academic Press, San Diego.

[15]

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.

[16]

Karol Pąk. 2014. Topological Manifolds. Formalized Mathematics 22, 2 (2014), 179 – 186.

[17]

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

[18]

Michael Spivak. 1965. Calculus on Manifolds: A Modern Approach to Classical Theorems of Advanced Calculus. Addison-Wesley, Reading, Massachusetts.

[19]

Michael Spivak. 1999. A Comprehensive Introduction to Differential Geometry, Volume One. Publish or Perich Inc., Houston.

Cited By

Bordg ADoña Mateo AKrebbers RTraytel DPientka BZdancewic S(2023)Encoding Dependently-Typed Constructions into Simple Type TheoryProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3573105.3575679(78-89)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3573105.3575679
Popescu ATraytel D(2023)Admissible Types-to-PERs Relativization in Higher-Order LogicProceedings of the ACM on Programming Languages10.1145/35712357:POPL(1214-1245)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1145/3571235
Milehins MPopescu AZdancewic S(2022)An extension of the framework types-to-sets for Isabelle/HOLProceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3497775.3503674(180-196)Online publication date: 17-Jan-2022
https://dl.acm.org/doi/10.1145/3497775.3503674
Show More Cited By

Index Terms

Smooth manifolds and types to sets for linear algebra in Isabelle/HOL
1. Mathematics of computing
  1. Continuous mathematics
    1. Topology
      1. Geometric topology
2. Theory of computation
  1. Logic
    1. Higher order logic
    2. Logic and verification

Recommendations

An extension of the framework types-to-sets for Isabelle/HOL
CPP 2022: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs

In their article titled From Types to Sets by Local Type Definitions in Higher-Order Logic and published in the proceedings of the conference Interactive Theorem Proving in 2016, Ondřej Kunčar and Andrei Popescu propose an extension of the logic ...
Programming and verifying a declarative first-order prover in Isabelle/HOL

We certify in the proof assistant Isabelle/HOL the soundness of a declarative first-order prover with equality. The LCF-style prover is a translation we have made, to Standard ML, of a prover in John Harrison’s Handbook of Practical Logic and Automated ...
A Formalization and Proof Checker for Isabelle’s Metalogic
Abstract
Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP 2019: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 2019

261 pages

ISBN:9781450362221

DOI:10.1145/3293880

Program Chairs:
Assia Mahboubi
INRIA, France
,
Magnus O. Myreen
Chalmers University of Technology, Sweden

Copyright © 2019 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGLOG: ACM Special Interest Group on Logic and Computation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

CPP '19

Sponsor:

SIGPLAN

CPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 14 - 15, 2019

Cascais, Portugal

Acceptance Rates

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
382
Total Downloads

Downloads (Last 12 months)61
Downloads (Last 6 weeks)6

Reflects downloads up to 17 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bordg ADoña Mateo AKrebbers RTraytel DPientka BZdancewic S(2023)Encoding Dependently-Typed Constructions into Simple Type TheoryProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3573105.3575679(78-89)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3573105.3575679
Popescu ATraytel D(2023)Admissible Types-to-PERs Relativization in Higher-Order LogicProceedings of the ACM on Programming Languages10.1145/35712357:POPL(1214-1245)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1145/3571235
Milehins MPopescu AZdancewic S(2022)An extension of the framework types-to-sets for Isabelle/HOLProceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3497775.3503674(180-196)Online publication date: 17-Jan-2022
https://dl.acm.org/doi/10.1145/3497775.3503674
The mathlib Community Blanchette JHriţcu C(2020)The lean mathematical libraryProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3372885.3373824(367-381)Online publication date: 20-Jan-2020
https://dl.acm.org/doi/10.1145/3372885.3373824
Guttmann W(2020)Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOLAutomated Reasoning10.1007/978-3-030-51054-1_14(236-253)Online publication date: 24-Jun-2020
https://doi.org/10.1007/978-3-030-51054-1_14

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents