The Nuprl Book

Implementing Mathematics

with

The Nuprl Proof Development System

Draft of

By the PRL Group:

Computer Science Department
Cornell University
Ithaca, NY 14853

• Contents
• Overview
  • Brief Description of
  • Highlights of Nuprl
  • Motivations
  • The Nuprl Logical Language
  • Components of the System
    • General
    • Definitions
    • Proof Editing
    • Evaluation
  • Programming Modes
  • Physical Characteristics
  • The ``Feel'' of the System
  • This Document
    • Scope
    • Organization
  • Research Topics
    • Programming Languages
    • Semantics
    • Methodology and Verification
    • Environments
    • Theorem Proving
    • Program Synthesis
    • Artificial Intelligence
  • Related Work
    • Close Relatives
    • Intuitionism and Type Theory
    • Theoretical Background
    • Systems Background
• Introduction to Type Theory
  • The Typed Lambda Calculus
    • A Formal System
    • Computation System
  • Extending the Typed Lambda Calculus
    • Dependent Function Space
    • Cartesian Product
    • Dependent Products
    • Disjoint Union
    • Integers
    • Atoms and Lists
  • Equality and Propositions as Types
    • Propositions as Types
  • Sets and Quotients
  • Semantics
  • Relationship to Set Theory
  • Relationship to Programming Languages
• Statements and Definitions in Nuprl
  • Overview of the Nuprl Environment
    • Windows
    • Commands and Status
    • Starting Up
    • Finishing Up
  • Libraries
    • Entry of Objects
    • Saving Results
  • The Text Editor
    • Entering Text
    • Copying Text
  • Definitions
  • Syntactic Issues
    • Theorems
    • Expressions Formed by Using Type Constructors
  • Stating Theorems
    • Expressing Concepts in the Language of Types
    • Propositions as Types
  • Defining Logics
    • Constructive Logic
    • Classical Logic
    • Other Logical Operators
  • Elementary Number Theory
  • Set Theory
    • The Subset Constructor
    • Intervals
  • Algebra
• Proofs
  • Structure of Proofs
  • Commands Needed for Proofs
  • Examples from Introductory Logic
    • Constructive Propositional Logic
    • Classical Propositional Logic
    • Predicate Logic
  • Example from Elementary Number Theory
• Computation
  • Term Extraction
  • Evaluation
    • Using the Evaluator
    • The Reduction Rules
    • The Reduction Strategy
    • Properties of the Evaluator
  • Computational Content
  • An Example
• Proof Tactics
  • Refinement Tactics
  • Transformation Tactics
  • Writing Simple Tactics
    • The Metalanguage ML
    • Using ML from Nuprl
    • Example Tactics
    • The Auto--tactic
• System Description
  • The Command Language
    • Library Display
    • Manipulating Objects
    • Storing Results
    • General Commands
  • The Library
    • Object Types
    • Library Entries
  • Window Management
    • Mouse Mode
    • Positioning the Mouse Cursor
    • Adjusting and Moving Windows
    • Other Keys in Mouse Mode
  • The Text Editor
    • Tree Cursors, Tree Positions and Bracket Mode
    • Moving the Cursor
    • Adding Text
    • Deleting and Killing Text
    • Copying and Moving Text
  • The Proof Editor
    • Basics of the Proof Editor
    • Motion within a Proof Node
    • Motion within the Proof Tree
    • Initiating a Refinement
    • Showing Goals, Subgoals and Rules
    • Invoking Transformation Tactics
  • Definitions and Definition Objects
• The Rules
  • Semantics
    • Substitution
    • The Computation System
    • The Type System
    • Judgements
  • The Type System in Detail
    • Formal Definition of Equality
    • Typehood and Membership
  • The Rules
    • The Form of a Rule
    • Organization of the Rules
    • Specifying a Rule
    • Optional Parameters and Defaults
    • Hidden Assumptions
    • Shortcuts in the Presentation
  • ATOM
  • VOID
  • INT
  • LESS
  • LIST
  • UNION
  • FUNCTION
  • PRODUCT
  • QUOTIENT
  • SET
  • EQUALITY
  • UNIVERSE
  • MISCELLANEOUS
  • ML Constructors
  • ATOM
  • VOID
  • INT
  • LESS
  • LIST
  • UNION
  • FUNCTION
  • PRODUCT
  • QUOTIENT
  • SET
  • EQUALITY
  • UNIVERSE
  • MISCELLANEOUS
• The Metalanguage
  • An Overview of ML
    • Functional Style
    • Type Definitions
    • Polymorphic Typing
    • Failures
    • Syntax and Semantics
    • Using ML in Nuprl
  • Tactics in ML
  • Basic Types in ML for Nuprl
    • Proofs
    • Rules
    • Declarations
    • Terms
    • Print Representation
    • A Note about Equality
  • Tools for Tactic Writers
    • Tacticals
    • Substitution
    • Unification
  • Example Tactics
    • Example Transformation Tactics
    • A Larger Example
  • Existing Tactics
• Building Theories
  • Proofs
  • Definitions
  • Sets and Quotients
  • Theories
• Mathematics Libraries
  • Basic Definitions
  • Lists and Arrays
  • Cardinality
  • Regular Sets
  • Real Analysis
  • Denotational Semantics
• Recursive Definition
  • Inductive Types
    • Expressiveness and Elegance
  • Details of the Extension
    • Computation System Modification
    • Inductive Type Proof Rules
      • Formation
      • Intro
      • Elim
      • Computation
  • Example Proof
  • Partial Function Types
  • Details of the Extension
    • Computation System Modification
    • Domain Predicate
    • Partial Function Type Proof Rules
      • Formation
      • Intro
      • Elim
      • Computation
• Appendix A: Summary of ML Extensions for
  • General Notes
  • Refinement Functions
  • Rule Constructors
  • Rule Destructors
  • Term Destructors
  • Auto--Tactic
  • Miscellaneous Functions
• Appendix B: Converting to from Lambda--prl
  • Differences in the Logic
    • Introduction Rules
    • Elimination Rules
    • Equality and Simplification Rules
  • Differences in the User Interfaces
  • Simulating Lambda--prl Constructs in Nuprl
    • Logical Operators
    • Lists
    • Primitive Recursive Functions
    • Extraction Terms
• Appendix C: Direct Computation Rules
• References
• Index
• About this document ...