Theorem Proving in Lean 3 (outdated)

• 1. Introduction
  • 1.1. Computers and Theorem Proving
  • 1.2. About Lean
  • 1.3. About this Book
  • 1.4. Acknowledgments
• 2. Dependent Type Theory
  • 2.1. Simple Type Theory
  • 2.2. Types as Objects
  • 2.3. Function Abstraction and Evaluation
  • 2.4. Introducing Definitions
  • 2.5. Local Definitions
  • 2.6. Variables and Sections
  • 2.7. Namespaces
  • 2.8. Dependent Types
  • 2.9. Implicit Arguments
  • 2.10. Exercises
• 3. Propositions and Proofs
  • 3.1. Propositions as Types
  • 3.2. Working with Propositions as Types
  • 3.3. Propositional Logic
  • 3.4. Introducing Auxiliary Subgoals
  • 3.5. Classical Logic
  • 3.6. Examples of Propositional Validities
  • 3.7. Exercises
• 4. Quantifiers and Equality
  • 4.1. The Universal Quantifier
  • 4.2. Equality
  • 4.3. Calculational Proofs
  • 4.4. The Existential Quantifier
  • 4.5. More on the Proof Language
  • 4.6. Exercises
• 5. Tactics
  • 5.1. Entering Tactic Mode
  • 5.2. Basic Tactics
  • 5.3. More Tactics
  • 5.4. Structuring Tactic Proofs
  • 5.5. Tactic Combinators
  • 5.6. Rewriting
  • 5.7. Using the Simplifier
  • 5.8. Exercises
• 6. Interacting with Lean
  • 6.1. Importing Files
  • 6.2. More on Sections
  • 6.3. More on Namespaces
  • 6.4. Attributes
  • 6.5. More on Implicit Arguments
  • 6.6. Notation
  • 6.7. Coercions
  • 6.8. Displaying Information
  • 6.9. Setting Options
  • 6.10. Elaboration Hints
  • 6.11. Using the Library
• 7. Inductive Types
  • 7.1. Enumerated Types
  • 7.2. Constructors with Arguments
  • 7.3. Inductively Defined Propositions
  • 7.4. Defining the Natural Numbers
  • 7.5. Other Recursive Data Types
  • 7.6. Tactics for Inductive Types
  • 7.7. Inductive Families
  • 7.8. Axiomatic Details
  • 7.9. Mutual and Nested Inductive Types
  • 7.10. Exercises
• 8. Induction and Recursion
  • 8.1. Pattern Matching
  • 8.2. Wildcards and Overlapping Patterns
  • 8.3. Structural Recursion and Induction
  • 8.4. Well-Founded Recursion and Induction
  • 8.5. Mutual Recursion
  • 8.6. Dependent Pattern Matching
  • 8.7. Inaccessible Terms
  • 8.8. Match Expressions
  • 8.9. Exercises
• 9. Structures and Records
  • 9.1. Declaring Structures
  • 9.2. Objects
  • 9.3. Inheritance
• 10. Type Classes
  • 10.1. Type Classes and Instances
  • 10.2. Chaining Instances
  • 10.3. Inferring Notation
  • 10.4. Decidable Propositions
  • 10.5. Managing Type Class Inference
  • 10.6. Coercions using Type Classes
• 11. Axioms and Computation
  • 11.1. Historical and Philosophical Context
  • 11.2. Propositional Extensionality
  • 11.3. Function Extensionality
  • 11.4. Quotients
  • 11.5. Choice
  • 11.6. The Law of the Excluded Middle