Foundations of software

In this session, you will work with natural numbers both on paper and in the Lean theorem prover.

Part 1: Paper Exercises

1. Define addition as a recursive function on inductively defined natural numbers
   • Write out a recursive definition for addition of two numbers (defined as elements of the inductively define set of natural numbers that are composed of 0, and successors)
   • Make sure to specify both the base case and the recursive case
2. Prove the associativity of addition
   • Prove that for all natural numbers a, b, and c: (a + b) + c = a + (b + c)
   • Be explicit about your inductive hypothesis and cases

Part 2: Getting Started with Lean

3. Lean Installation
   • If you haven't already, install Lean on your computer
   • Verify that the installation works correctly
   • Make sure you can create and open a new Lean project in vscode
4. If you have no experience in proof assistants, complete a few levels of the Natural Number Game (https://adam.math.hhu.de/#/g/leanprover-community/nng4). This will help you become familiar with some of Lean's standard tactics and syntax (you can go as far as you want).

Part 3: Lean Exercises

4. Formalization Tasks
   • Formalize the inductively defined set of natural numbers in Lean
   • Define addition for your natural numbers
   • Prove the associativity of addition in Lean
   • Compare your formal proof with your paper proof from Part 1

Tips

• Start with the paper exercises to build intuition
• Don't worry if the Lean formalization seems challenging at first
• Use the Natural Number Game as a way to discover the basics of Lean tactics
• Reach out for help if you get stuck - that's what exercise sessions are for!

Remember: The goal is to understand both the mathematical concepts and how to work with them in a formal system.