A HOL Theory of Euclidean space

John Harrison.

Proceedings of TPHOLs 2005: 18th International Conference on Theorem Proving in Higher Order Logics. Springer LNCS 3603, pp. 114-129.

Abstract:

We describe a formalization of the elementary algebra, topology and analysis of finite-dimensional Euclidean space in the HOL Light theorem prover. (Euclidean space is R^N with the usual notion of distance.) A notable feature is that the HOL type system is used to encode the dimension N in a simple and useful way, even though HOL does not permit dependent types. In the resulting theory the HOL type system, far from getting in the way, naturally imposes the correct dimensional constraints, e.g. checking compatibility in matrix multiplication. Among the interesting later developments of the theory are a partial decision procedure for the theory of vector spaces (based on a more general algorithm due to Solovay) and a formal proof of various classic theorems of topology and analysis for arbitrary N-dimensional Euclidean space, e.g. Brouwer's fixpoint theorem and the differentiability of inverse functions.

DVI, PostScript or PDF

Bibtex entry:

@INPROCEEDINGS{harrison-euclidean,                                            
        author          = JRH,                                                
        title           = "A {HOL} Theory of {E}uclidean space",
        booktitle       = "Theorem Proving in Higher Order Logics,            
                           18th International Conference, TPHOLs 2005",        
        editor          = "Joe Hurd and Tom Melham",                     
        address         = "Oxford, UK",                                   
        date            = "August 2005",                              
        publisher       = "Springer-Verlag",
        series          = "Lecture Notes in Computer Science",
        volume          = 3603,                                          
        year            = 2005}
        pages           = "114--129"}