Software Foundations (Lean)

Vol 1: Logical Foundations

Contents:

• Preface
  • Welcome
  • Overview
  • Practicalities
  • Note for Instructors
  • Translations
  • Thanks
• Functional Programming in Lean
  • Introduction
  • Data and Functions
  • Proof by Simplification
  • Proof by Rewriting
  • Proof by Case Analysis
  • More Exercises
• Proof by Induction
  • Proof by Induction
  • Proofs Within Proofs
  • Formal vs. Informal Proof
  • More Exercises
• Working with Structured Data
  • Pairs of Numbers
  • Lists of Numbers
  • Reasoning About Lists
  • Options
  • Partial Maps
• Polymorphism and Higher-Order Functions
  • Polymorphism
  • Functions as Data
  • Additional Exercises
• More Basic Tactics
  • The apply Tactic
  • The apply ... with ... Tactic
  • The inversion Tactic
  • Using Tactics on Hypotheses
  • Varying the Induction Hypothesis
  • Unfolding Definitions
  • Using destruct on Compound Expressions
  • Review
  • Additional Exercises
• Logic in Lean
  • Logical Connectives
  • Programming with Propositions
  • Applying Theorems to Arguments
  • Lean vs. Set Theory
• Inductively Defined Propositions
  • Inductively Defined Propositions
  • Using Evidence in Proofs
  • Inductive Relations
  • Case Study: Regular Expressions
  • Case Study: Improving Reflection
  • Additional Exercises
• Total and Partial Maps
  • The Lean Standard Library
  • Identifiers
  • Total Maps
  • Partial Maps
• The Curry-Howard Correspondence
  • Proof Scripts
  • Quantifiers, Implications, Functions
  • Programming with Tactics
  • Logical Connectives as Inductive Types
  • Equality
• Induction Principles
  • Basics
  • Polymorphism
  • Induction Hypotheses
  • More on the induction Tactic
  • Induction Principles in Prop
  • Formal vs. Informal Proofs by Induction
• Properties of Relations
  • Relations
  • Basic Properties
  • Reflexive, Transitive Closure
• Simple Imperative Programs
  • Arithmetic and Boolean Expressions
  • Lean Automation
  • Evaluation as a Relation
  • Expressions With Variables
  • Commands
  • Evaluating Commands
  • Reasoning About Imp Programs
  • Additional Exercises
• Lexing and Parsing in Lean
  • Internals
  • Examples
• An Evaluation Function for Imp
  • A Broken Evaluator
  • A Step-Indexed Evaluator
  • Relational vs. Step-Indexed Evaluation
  • Determinism of Evaluation Again
• Extracting C++ from Lean
  • Basic Extraction
  • Controlling Extraction of Specific Types
  • A Complete Example
  • Discussion
  • Going Further
• More Automation
  • The auto Tactic
  • Searching For Hypotheses
  • The eapply and eauto variants
• Postscript
  • Looking Back
  • Looking Forward
  • Other Sources
• Bibliography
  • Resources Cited in this Volume

Indices and tables

• Index
• Module Index
• Search Page