diff --git a/README.md b/README.md deleted file mode 100644 index 520c8ac..0000000 --- a/README.md +++ /dev/null @@ -1,48 +0,0 @@ -# Lean 4 + Programming Language Semantics - -A self-study curriculum for computer scientists who know PL theory and want -to mechanize proofs in Lean 4 — from syntax to soundness of the -Hindley-Milner type system. - -## Structure - -``` -├── README.md ← this file -├── tutorial-01-basics/ ← Lean 4 fundamentals -│ ├── 01-types-and-functions.md -│ ├── 02-inductive-types.md -│ ├── 03-propositions-and-proofs.md -│ ├── 04-quantifiers-and-equality.md -│ ├── 05-advanced-tactics.md -│ ├── 06-structures-type-classes.md -│ └── 07-dependent-types.md -├── tutorial-02-semantics/ ← PL semantics in Lean -│ ├── 08-syntax-representation.md -│ ├── 09-substitution.md -│ ├── 10-small-step-semantics.md -│ ├── 11-stlc-type-system.md -│ ├── 12-type-safety.md -│ ├── 13-hm-declarative.md -│ ├── 14-algorithm-w.md -│ └── 15-soundness-completeness.md -└── references.md ← all cited resources -``` - -## How to Use - -1. Install Lean 4 (VS Code + `lean4` extension): - [lean-lang.org/lean4/doc/quickstart.html](https://lean-lang.org/lean4/doc/quickstart.html) -2. Start with **Tutorial 1**, Unit 1. Each unit is a standalone `.md` file with - inline Lean exercises. -3. Type the exercises into a `.lean` file and make it compile. -4. After Tutorial 1, move to **Tutorial 2** to mechanize STLC and HM. - -## Prerequisites - -- Functional programming (Haskell/OCaml familiarity) -- Basic PL theory (lambda calculus, operational semantics, type systems) -- No prior proof assistant experience required - -## References - -See [references.md](references.md) for the full list of resources. diff --git a/README.org b/README.org new file mode 100644 index 0000000..a45bda8 --- /dev/null +++ b/README.org @@ -0,0 +1,58 @@ +* Lean 4 + Programming Language Semantics +:PROPERTIES: +:CUSTOM_ID: lean-4-programming-language-semantics +:END: +A self-study curriculum for computer scientists who know PL theory and want +to mechanize proofs in Lean 4 --- from syntax to soundness of the +Hindley-Milner type system. + +** Structure +:PROPERTIES: +:CUSTOM_ID: structure +:END: +#+begin_example +├── README.org ← this file +├── tutorial-01-basics/ ← Lean 4 fundamentals +│ ├── 01-types-and-functions.org +│ ├── 02-inductive-types.org +│ ├── 03-propositions-and-proofs.org +│ ├── 04-quantifiers-and-equality.org +│ ├── 05-advanced-tactics.org +│ ├── 06-structures-type-classes.org +│ └── 07-dependent-types.org +├── tutorial-02-semantics/ ← PL semantics in Lean +│ ├── 08-syntax-representation.org +│ ├── 09-substitution.org +│ ├── 10-small-step-semantics.org +│ ├── 11-stlc-type-system.org +│ ├── 12-type-safety.org +│ ├── 13-hm-declarative.org +│ ├── 14-algorithm-w.org +│ └── 15-soundness-completeness.org +└── references.org ← all cited resources +#+end_example + +** How to Use +:PROPERTIES: +:CUSTOM_ID: how-to-use +:END: +1. Install Lean 4 (VS Code + =lean4= extension): + [[https://lean-lang.org/lean4/doc/quickstart.html][lean-lang.org/lean4/doc/quickstart.html]] +2. Start with *Tutorial 1*, Unit 1. Each unit is a standalone =.org= file with + inline Lean exercises. +3. Type the exercises into a =.lean= file and make it compile. +4. After Tutorial 1, move to *Tutorial 2* to mechanize STLC and HM. + +** Prerequisites +:PROPERTIES: +:CUSTOM_ID: prerequisites +:END: +- Functional programming (Haskell/OCaml familiarity) +- Basic PL theory (lambda calculus, operational semantics, type systems) +- No prior proof assistant experience required + +** References +:PROPERTIES: +:CUSTOM_ID: references +:END: +See [[file:references.org]] for the full list of resources. diff --git a/references.md b/references.md deleted file mode 100644 index b7fccf3..0000000 --- a/references.md +++ /dev/null @@ -1,39 +0,0 @@ -# References - -## Primary Learning Resources - -| Abbr | Title | Link | -|------|-------|------| -| FPIL | *Functional Programming in Lean* | https://lean-lang.org/functional_programming_in_lean/ | -| TPIL | *Theorem Proving in Lean 4* | https://leanprover.github.io/theorem_proving_in_lean4/ | -| MiL | *Mathematics in Lean* | https://leanprover-community.github.io/mathematics_in_lean/ | - -## PL Semantics Formalizations in Lean 4 - -| Resource | What it covers | Link | -|----------|---------------|------| -| syndikos/lean4-stlc | STLC: syntax, semantics, typing, metatheory (Progress + Preservation) | https://github.com/syndikos/lean4-stlc | -| chenson2018/LeanScratch | Untyped λ-calculus: de Bruijn + locally nameless, confluence proofs | https://github.com/chenson2018/LeanScratch | -| sdemos/type-inference | STLC + HM type inference, soundness & completeness of W | https://github.com/sdemos/type-inference | -| rami3l/PLFaLean | PLFA Parts 2–3 translated to Lean 4 | https://github.com/rami3l/PLFaLean | - -## PL Theory (Non-Lean) - -| Resource | Format | Link | -|----------|--------|------| -| Software Foundations Vol.2 | Rocq book | https://softwarefoundations.cis.upenn.edu/ | -| PLFA Part 2 | Agda book | https://plfa.github.io/ | -| Chris Henson: Beginner Resources for Formalizing Lambda Calculi | Blog post | https://chrishenson.net/posts/2025-05-10-formalized_lambda_calculus.html | - -## HM Type System - -| Resource | Format | Link | -|----------|--------|------| -| Wikipedia: Hindley-Milner type system | Reference | https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system | -| Jeff Vaughan: "A proof of correctness for the HM type inference algorithm" | PDF (2008) | https://www.jeffvaughan.net/docs/hmproof.pdf | - -## Community - -- Official site: https://lean-lang.org/ -- Zulip chat: https://leanprover.zulipchat.com/ -- Lean 4 docs: https://lean-lang.org/documentation/ diff --git a/references.org b/references.org new file mode 100644 index 0000000..b620f5d --- /dev/null +++ b/references.org @@ -0,0 +1,51 @@ +* References +:PROPERTIES: +:CUSTOM_ID: references +:END: +** Primary Learning Resources +:PROPERTIES: +:CUSTOM_ID: primary-learning-resources +:END: +| Abbr | Title | Link | +|------+----------------------------------+-------------------------------------------------------------| +| FPIL | /Functional Programming in Lean/ | https://lean-lang.org/functional_programming_in_lean/ | +| TPIL | /Theorem Proving in Lean 4/ | https://leanprover.github.io/theorem_proving_in_lean4/ | +| MiL | /Mathematics in Lean/ | https://leanprover-community.github.io/mathematics_in_lean/ | + +** PL Semantics Formalizations in Lean 4 +:PROPERTIES: +:CUSTOM_ID: pl-semantics-formalizations-in-lean-4 +:END: +| Resource | What it covers | Link | +|-------------------------+-----------------------------------------------------------------------+--------------------------------------------| +| syndikos/lean4-stlc | STLC: syntax, semantics, typing, metatheory (Progress + Preservation) | https://github.com/syndikos/lean4-stlc | +| chenson2018/LeanScratch | Untyped λ-calculus: de Bruijn + locally nameless, confluence proofs | https://github.com/chenson2018/LeanScratch | +| sdemos/type-inference | STLC + HM type inference, soundness & completeness of W | https://github.com/sdemos/type-inference | +| rami3l/PLFaLean | PLFA Parts 2--3 translated to Lean 4 | https://github.com/rami3l/PLFaLean | + +** PL Theory (Non-Lean) +:PROPERTIES: +:CUSTOM_ID: pl-theory-non-lean +:END: +| Resource | Format | Link | +|-----------------------------------------------------------------+-----------+--------------------------------------------------------------------------| +| Software Foundations Vol.2 | Rocq book | https://softwarefoundations.cis.upenn.edu/ | +| PLFA Part 2 | Agda book | https://plfa.github.io/ | +| Chris Henson: Beginner Resources for Formalizing Lambda Calculi | Blog post | https://chrishenson.net/posts/2025-05-10-formalized_lambda_calculus.html | + +** HM Type System +:PROPERTIES: +:CUSTOM_ID: hm-type-system +:END: +| Resource | Format | Link | +|----------------------------------------------------------------------------+------------+------------------------------------------------------------------| +| Wikipedia: Hindley-Milner type system | Reference | https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system | +| Jeff Vaughan: "A proof of correctness for the HM type inference algorithm" | PDF (2008) | https://www.jeffvaughan.net/docs/hmproof.pdf | + +** Community +:PROPERTIES: +:CUSTOM_ID: community +:END: +- Official site: https://lean-lang.org/ +- Zulip chat: https://leanprover.zulipchat.com/ +- Lean 4 docs: https://lean-lang.org/documentation/ diff --git a/tutorial-01-basics/01-types-and-functions.md b/tutorial-01-basics/01-types-and-functions.md deleted file mode 100644 index 36fd57b..0000000 --- a/tutorial-01-basics/01-types-and-functions.md +++ /dev/null @@ -1,107 +0,0 @@ -# Unit 1 — Types and Functions - -**Tutorial 1: Lean 4 Fundamentals** · [← Back to README](../README.md) - -## Goals - -- Define functions with `def` and lambda notation -- Understand Lean's basic types: `Nat`, `Int`, `String`, `Bool`, `List`, `Option` -- Use pattern matching and `match` expressions -- Run code with `#eval` - -## Source - -*Functional Programming in Lean* (FPIL), Chapters 1–2 -→ https://lean-lang.org/functional_programming_in_lean/ - -## Concepts - -| Concept | Lean syntax | Example | -|---------|------------|---------| -| Function definition | `def f (x : Nat) : Nat :=` | `def double (x : Nat) : Nat := x + x` | -| Lambda | `fun x => ...` | `fun x => x + 1` | -| Pattern matching | `match e with \| pat => ...` | `match n with \| 0 => "zero" \| _ => "non-zero"` | -| Recursion | `def f ... := match ...` | Structural recursion only (no general fixpoint) | -| `#eval` | `#eval expr` | `#eval double 21` prints `42` | - -## Exercises - -> **How to work**: Create a file `Unit1.lean`. Write each exercise, then -> `#eval` to test it (if it's a function) or just make it compile (if it's a -> proof or definition). Fill in the `sorry` placeholders. - -### Exercise 1.1 — Warm-up functions - -```lean --- (a) Write a function that returns the absolute difference between two nats -def absDiff (a b : Nat) : Nat := - sorry - -#eval absDiff 7 3 -- expected: 4 -#eval absDiff 3 7 -- expected: 4 -#eval absDiff 5 5 -- expected: 0 - --- (b) Write a function that checks whether a list contains an element -def contains [BEq α] (x : α) (xs : List α) : Bool := - sorry - -#eval contains 3 [1, 2, 3, 4] -- expected: true -#eval contains 5 [1, 2, 3, 4] -- expected: false - --- (c) Write `map` (without looking at the standard library) -def myMap (f : α → β) (xs : List α) : List β := - sorry - -#eval myMap (fun x => x * 2) [1, 2, 3] -- expected: [2, 4, 6] -``` - -### Exercise 1.2 — Recursion on lists - -```lean --- (a) Sum of a list -def sumList (xs : List Nat) : Nat := - sorry - -#eval sumList [1, 2, 3, 4] -- expected: 10 - --- (b) Reverse a list (the slow way is fine) -def myReverse (xs : List α) : List α := - sorry - -#eval myReverse [1, 2, 3] -- expected: [3, 2, 1] - --- (c) Filter: keep elements satisfying p -def myFilter (p : α → Bool) (xs : List α) : List α := - sorry - -#eval myFilter (fun x => x % 2 == 0) [1, 2, 3, 4, 5, 6] -- expected: [2, 4, 6] -``` - -### Exercise 1.3 — Option type - -```lean --- (a) Safe head -def safeHead (xs : List α) : Option α := - sorry - -#eval safeHead ([1, 2, 3] : List Nat) -- expected: some 1 -#eval safeHead ([] : List Nat) -- expected: none - --- (b) Safe division -def safeDiv (a b : Nat) : Option Nat := - sorry - -#eval safeDiv 10 2 -- expected: some 5 -#eval safeDiv 10 0 -- expected: none - --- (c) Lookup in an association list -def lookup [BEq α] (key : α) (alist : List (α × β)) : Option β := - sorry - -#eval lookup "b" [("a", 1), ("b", 2), ("c", 3)] -- expected: some 2 -#eval lookup "d" [("a", 1), ("b", 2), ("c", 3)] -- expected: none -``` - ---- - -← [Back to README](../README.md) · Next: [Unit 2 — Inductive Types](02-inductive-types.md) diff --git a/tutorial-01-basics/01-types-and-functions.org b/tutorial-01-basics/01-types-and-functions.org new file mode 100644 index 0000000..60c2eae --- /dev/null +++ b/tutorial-01-basics/01-types-and-functions.org @@ -0,0 +1,126 @@ +* Unit 1 --- Types and Functions +:PROPERTIES: +:CUSTOM_ID: unit-1-types-and-functions +:END: +*Tutorial 1: Lean 4 Fundamentals* · [[../README.org][← Back to README]] + +** Goals +:PROPERTIES: +:CUSTOM_ID: goals +:END: +- Define functions with =def= and lambda notation +- Understand Lean's basic types: =Nat=, =Int=, =String=, =Bool=, =List=, =Option= +- Use pattern matching and =match= expressions +- Run code with =#eval= + +** Source +:PROPERTIES: +:CUSTOM_ID: source +:END: +/Functional Programming in Lean/ (FPIL), Chapters 1--2 +→ https://lean-lang.org/functional_programming_in_lean/ + +** Concepts +:PROPERTIES: +:CUSTOM_ID: concepts +:END: +| Concept | Lean syntax | Example | +|---------------------+------------------------------+--------------------------------------------------| +| Function definition | =def f (x : Nat) : Nat :== | =def double (x : Nat) : Nat := x + x= | +| Lambda | =fun x => ...= | =fun x => x + 1= | +| Pattern matching | =match e with \| pat => ...= | =match n with \| 0 => "zero" \| _ => "non-zero"= | +| Recursion | =def f ... := match ...= | Structural recursion only (no general fixpoint) | +| =#eval= | =#eval expr= | =#eval double 21= prints =42= | + +** Exercises +:PROPERTIES: +:CUSTOM_ID: exercises +:END: + +#+begin_quote +*How to work*: Create a file =Unit1.lean=. Write each exercise, then +=#eval= to test it (if it's a function) or just make it compile (if it's a +proof or definition). Fill in the =sorry= placeholders. +#+end_quote + +*** Exercise 1.1 --- Warm-up functions +:PROPERTIES: +:CUSTOM_ID: exercise-1.1-warm-up-functions +:END: +#+begin_src lean +-- (a) Write a function that returns the absolute difference between two nats +def absDiff (a b : Nat) : Nat := + sorry + +#eval absDiff 7 3 -- expected: 4 +#eval absDiff 3 7 -- expected: 4 +#eval absDiff 5 5 -- expected: 0 + +-- (b) Write a function that checks whether a list contains an element +def contains [BEq α] (x : α) (xs : List α) : Bool := + sorry + +#eval contains 3 [1, 2, 3, 4] -- expected: true +#eval contains 5 [1, 2, 3, 4] -- expected: false + +-- (c) Write `map` (without looking at the standard library) +def myMap (f : α → β) (xs : List α) : List β := + sorry + +#eval myMap (fun x => x * 2) [1, 2, 3] -- expected: [2, 4, 6] +#+end_src + +*** Exercise 1.2 --- Recursion on lists +:PROPERTIES: +:CUSTOM_ID: exercise-1.2-recursion-on-lists +:END: +#+begin_src lean +-- (a) Sum of a list +def sumList (xs : List Nat) : Nat := + sorry + +#eval sumList [1, 2, 3, 4] -- expected: 10 + +-- (b) Reverse a list (the slow way is fine) +def myReverse (xs : List α) : List α := + sorry + +#eval myReverse [1, 2, 3] -- expected: [3, 2, 1] + +-- (c) Filter: keep elements satisfying p +def myFilter (p : α → Bool) (xs : List α) : List α := + sorry + +#eval myFilter (fun x => x % 2 == 0) [1, 2, 3, 4, 5, 6] -- expected: [2, 4, 6] +#+end_src + +*** Exercise 1.3 --- Option type +:PROPERTIES: +:CUSTOM_ID: exercise-1.3-option-type +:END: +#+begin_src lean +-- (a) Safe head +def safeHead (xs : List α) : Option α := + sorry + +#eval safeHead ([1, 2, 3] : List Nat) -- expected: some 1 +#eval safeHead ([] : List Nat) -- expected: none + +-- (b) Safe division +def safeDiv (a b : Nat) : Option Nat := + sorry + +#eval safeDiv 10 2 -- expected: some 5 +#eval safeDiv 10 0 -- expected: none + +-- (c) Lookup in an association list +def lookup [BEq α] (key : α) (alist : List (α × β)) : Option β := + sorry + +#eval lookup "b" [("a", 1), ("b", 2), ("c", 3)] -- expected: some 2 +#eval lookup "d" [("a", 1), ("b", 2), ("c", 3)] -- expected: none +#+end_src + +-------------- + +← [[../README.org][Back to README]] · Next: [[file:02-inductive-types.org][Unit 2 --- Inductive Types]] diff --git a/tutorial-01-basics/02-inductive-types.md b/tutorial-01-basics/02-inductive-types.org similarity index 52% rename from tutorial-01-basics/02-inductive-types.md rename to tutorial-01-basics/02-inductive-types.org index 140fb09..6429c7a 100644 --- a/tutorial-01-basics/02-inductive-types.md +++ b/tutorial-01-basics/02-inductive-types.org @@ -1,34 +1,46 @@ -# Unit 2 — Inductive Types +* Unit 2 --- Inductive Types +:PROPERTIES: +:CUSTOM_ID: unit-2-inductive-types +:END: +*Tutorial 1: Lean 4 Fundamentals* · [[../README.org][← Back to README]] -**Tutorial 1: Lean 4 Fundamentals** · [← Back to README](../README.md) - -## Goals - -- Define inductive data types with the `inductive` keyword +** Goals +:PROPERTIES: +:CUSTOM_ID: goals +:END: +- Define inductive data types with the =inductive= keyword - Understand constructors and pattern matching - Write structurally recursive functions over inductive types -- Define `Nat`, `List`, and `Tree` from scratch +- Define =Nat=, =List=, and =Tree= from scratch -## Sources - -- *Theorem Proving in Lean 4* (TPIL), Chapter 7 "Inductive Types" +** Sources +:PROPERTIES: +:CUSTOM_ID: sources +:END: +- /Theorem Proving in Lean 4/ (TPIL), Chapter 7 "Inductive Types" → https://leanprover.github.io/theorem_proving_in_lean4/ -- *Functional Programming in Lean* (FPIL), Chapter 1 +- /Functional Programming in Lean/ (FPIL), Chapter 1 -## Concepts +** Concepts +:PROPERTIES: +:CUSTOM_ID: concepts +:END: +| Concept | Lean syntax | +|-------------------------------+-----------------------------------------------------------| +| Inductive definition | =inductive Name where \| ctor1 : ... → Name= | +| Pattern matching constructors | =match t with \| ctor1 x => ... \| ctor2 y => ...= | +| Structural recursion | Recursion on /structurally smaller/ subterms only | +| =deriving= clauses | =deriving Repr, BEq, DecidableEq= for auto-generated code | -| Concept | Lean syntax | -|---------|------------| -| Inductive definition | `inductive Name where \| ctor1 : ... → Name` | -| Pattern matching constructors | `match t with \| ctor1 x => ... \| ctor2 y => ...` | -| Structural recursion | Recursion on *structurally smaller* subterms only | -| `deriving` clauses | `deriving Repr, BEq, DecidableEq` for auto-generated code | - -## Exercises - -### Exercise 2.1 — Define `Nat` from scratch - -```lean +** Exercises +:PROPERTIES: +:CUSTOM_ID: exercises +:END: +*** Exercise 2.1 --- Define =Nat= from scratch +:PROPERTIES: +:CUSTOM_ID: exercise-2.1-define-nat-from-scratch +:END: +#+begin_src lean inductive MyNat where | zero : MyNat | succ : MyNat → MyNat @@ -46,11 +58,13 @@ def myMul (a b : MyNat) : MyNat := -- (c) Prove that zero is a right identity: myAdd a MyNat.zero = a -- (We'll do proofs properly in Unit 3, but try `by rfl` for now) -``` +#+end_src -### Exercise 2.2 — Define `List α` from scratch - -```lean +*** Exercise 2.2 --- Define =List α= from scratch +:PROPERTIES: +:CUSTOM_ID: exercise-2.2-define-list-α-from-scratch +:END: +#+begin_src lean inductive MyList (α : Type) where | nil : MyList α | cons : α → MyList α → MyList α @@ -66,11 +80,13 @@ def myAppend {α : Type} (xs ys : MyList α) : MyList α := -- (c) Prove: myLength (myAppend xs ys) = myLength xs + myLength ys -- (Try this after Unit 4/5) -``` +#+end_src -### Exercise 2.3 — Binary trees - -```lean +*** Exercise 2.3 --- Binary trees +:PROPERTIES: +:CUSTOM_ID: exercise-2.3-binary-trees +:END: +#+begin_src lean inductive BinTree (α : Type) where | leaf : BinTree α | node : BinTree α → α → BinTree α → BinTree α @@ -99,8 +115,8 @@ def inorder {α : Type} (t : BinTree α) : List α := -- Hint: you may want a helper with min/max bounds. def isBST (t : BinTree Int) : Bool := sorry -``` +#+end_src ---- +-------------- -← [Previous: Unit 1](01-types-and-functions.md) · Next: [Unit 3 — Propositions and Proofs](03-propositions-and-proofs.md) +← [[file:01-types-and-functions.org][Previous: Unit 1]] · Next: [[file:03-propositions-and-proofs.org][Unit 3 --- Propositions and Proofs]] diff --git a/tutorial-01-basics/03-propositions-and-proofs.md b/tutorial-01-basics/03-propositions-and-proofs.md deleted file mode 100644 index 552e472..0000000 --- a/tutorial-01-basics/03-propositions-and-proofs.md +++ /dev/null @@ -1,90 +0,0 @@ -# Unit 3 — Propositions and Proofs - -**Tutorial 1: Lean 4 Fundamentals** · [← Back to README](../README.md) - -## Goals - -- Understand propositions as types (Curry-Howard) -- Write basic proofs using `example` and `theorem` -- Use the tactic language: `intro`, `apply`, `exact`, `have` - -## Source - -*Theorem Proving in Lean 4* (TPIL), Chapters 2–3 -→ https://leanprover.github.io/theorem_proving_in_lean4/ - -## Concepts - -| Concept | Lean | -|---------|------| -| Proposition | `P : Prop` — a type whose terms are proofs | -| Implication `P → Q` | Function from proofs of `P` to proofs of `Q` | -| Conjunction `P ∧ Q` | `And.intro` (constructor), `.left` / `.right` (projections) | -| Disjunction `P ∨ Q` | `Or.inl` / `Or.inr` | -| Negation `¬ P` | `P → False` | -| Tactics | `intro`, `apply`, `exact`, `have`, `assumption` | - -## Exercises - -### Exercise 3.1 — Implicational logic - -```lean --- (a) Identity -theorem id_prop (A : Prop) : A → A := - by - intro h - exact h - --- (b) Composition -theorem compose (A B C : Prop) : (A → B) → (B → C) → (A → C) := - by - sorry - --- (c) Currying -theorem curry (A B C : Prop) : (A → B → C) → (A ∧ B → C) := - by - sorry -``` - -### Exercise 3.2 — Conjunction and disjunction - -```lean --- (a) Swap conjuncts -theorem and_comm (A B : Prop) : A ∧ B → B ∧ A := - by - sorry - --- (b) Disjunction is symmetric -theorem or_comm (A B : Prop) : A ∨ B → B ∨ A := - by - sorry - --- (c) Forward reasoning with `have` -theorem forward_example (A B C : Prop) (h1 : A → B) (h2 : B → C) (ha : A) : C := - by - have hb : B := h1 ha - sorry -``` - -### Exercise 3.3 — Negation - -```lean --- (a) Contradiction -theorem contrapositive (A B : Prop) : (A → B) → (¬ B → ¬ A) := - by - sorry - --- (b) Double negation introduction -theorem double_neg_intro (A : Prop) : A → ¬ ¬ A := - by - sorry - --- (c) Ex falso quodlibet -theorem ex_falso (A : Prop) : False → A := - by - sorry -``` - ---- - -← [Previous: Unit 2](02-inductive-types.md) · Next: [Unit 4 — Quantifiers and Equality](04-quantifiers-and-equality.md) diff --git a/tutorial-01-basics/03-propositions-and-proofs.org b/tutorial-01-basics/03-propositions-and-proofs.org new file mode 100644 index 0000000..f171061 --- /dev/null +++ b/tutorial-01-basics/03-propositions-and-proofs.org @@ -0,0 +1,106 @@ +* Unit 3 --- Propositions and Proofs +:PROPERTIES: +:CUSTOM_ID: unit-3-propositions-and-proofs +:END: +*Tutorial 1: Lean 4 Fundamentals* · [[../README.org][← Back to README]] + +** Goals +:PROPERTIES: +:CUSTOM_ID: goals +:END: +- Understand propositions as types (Curry-Howard) +- Write basic proofs using =example= and =theorem= +- Use the tactic language: =intro=, =apply=, =exact=, =have= + +** Source +:PROPERTIES: +:CUSTOM_ID: source +:END: +/Theorem Proving in Lean 4/ (TPIL), Chapters 2--3 +→ https://leanprover.github.io/theorem_proving_in_lean4/ + +** Concepts +:PROPERTIES: +:CUSTOM_ID: concepts +:END: +| Concept | Lean | +|---------------------+-------------------------------------------------------------| +| Proposition | =P : Prop= --- a type whose terms are proofs | +| Implication =P → Q= | Function from proofs of =P= to proofs of =Q= | +| Conjunction =P ∧ Q= | =And.intro= (constructor), =.left= / =.right= (projections) | +| Disjunction =P ∨ Q= | =Or.inl= / =Or.inr= | +| Negation =¬ P= | =P → False= | +| Tactics | =intro=, =apply=, =exact=, =have=, =assumption= | + +** Exercises +:PROPERTIES: +:CUSTOM_ID: exercises +:END: +*** Exercise 3.1 --- Implicational logic +:PROPERTIES: +:CUSTOM_ID: exercise-3.1-implicational-logic +:END: +#+begin_src lean +-- (a) Identity +theorem id_prop (A : Prop) : A → A := + by + intro h + exact h + +-- (b) Composition +theorem compose (A B C : Prop) : (A → B) → (B → C) → (A → C) := + by + sorry + +-- (c) Currying +theorem curry (A B C : Prop) : (A → B → C) → (A ∧ B → C) := + by + sorry +#+end_src + +*** Exercise 3.2 --- Conjunction and disjunction +:PROPERTIES: +:CUSTOM_ID: exercise-3.2-conjunction-and-disjunction +:END: +#+begin_src lean +-- (a) Swap conjuncts +theorem and_comm (A B : Prop) : A ∧ B → B ∧ A := + by + sorry + +-- (b) Disjunction is symmetric +theorem or_comm (A B : Prop) : A ∨ B → B ∨ A := + by + sorry + +-- (c) Forward reasoning with `have` +theorem forward_example (A B C : Prop) (h1 : A → B) (h2 : B → C) (ha : A) : C := + by + have hb : B := h1 ha + sorry +#+end_src + +*** Exercise 3.3 --- Negation +:PROPERTIES: +:CUSTOM_ID: exercise-3.3-negation +:END: +#+begin_src lean +-- (a) Contradiction +theorem contrapositive (A B : Prop) : (A → B) → (¬ B → ¬ A) := + by + sorry + +-- (b) Double negation introduction +theorem double_neg_intro (A : Prop) : A → ¬ ¬ A := + by + sorry + +-- (c) Ex falso quodlibet +theorem ex_falso (A : Prop) : False → A := + by + sorry +#+end_src + +-------------- + +← [[file:02-inductive-types.org][Previous: Unit 2]] · Next: [[file:04-quantifiers-and-equality.org][Unit 4 --- Quantifiers and Equality]] diff --git a/tutorial-01-basics/04-quantifiers-and-equality.md b/tutorial-01-basics/04-quantifiers-and-equality.org similarity index 51% rename from tutorial-01-basics/04-quantifiers-and-equality.md rename to tutorial-01-basics/04-quantifiers-and-equality.org index a4e73bd..ba8e827 100644 --- a/tutorial-01-basics/04-quantifiers-and-equality.md +++ b/tutorial-01-basics/04-quantifiers-and-equality.org @@ -1,32 +1,44 @@ -# Unit 4 — Quantifiers and Equality +* Unit 4 --- Quantifiers and Equality +:PROPERTIES: +:CUSTOM_ID: unit-4-quantifiers-and-equality +:END: +*Tutorial 1: Lean 4 Fundamentals* · [[../README.org][← Back to README]] -**Tutorial 1: Lean 4 Fundamentals** · [← Back to README](../README.md) - -## Goals - -- Use `∀` (forall) and `∃` (exists) quantifiers -- Manipulate equality with `rfl`, `rw`, `calc` +** Goals +:PROPERTIES: +:CUSTOM_ID: goals +:END: +- Use =∀= (forall) and =∃= (exists) quantifiers +- Manipulate equality with =rfl=, =rw=, =calc= - Combine quantifiers with logical connectives -## Source - -*Theorem Proving in Lean 4* (TPIL), Chapter 4 +** Source +:PROPERTIES: +:CUSTOM_ID: source +:END: +/Theorem Proving in Lean 4/ (TPIL), Chapter 4 → https://leanprover.github.io/theorem_proving_in_lean4/ -## Concepts +** Concepts +:PROPERTIES: +:CUSTOM_ID: concepts +:END: +| Concept | Lean | +|------------------------+------------------------------------------------------| +| Universal =∀ x, P x= | =intro x= to prove; =h x= or =apply h= to use | +| Existential =∃ x, P x= | =⟨x, h⟩= to prove; =rcases h with ⟨x, hx⟩= to use | +| Equality =a = b= | =rfl= when definitional; =rw [h]= when propositional | +| =calc= block | Chain equalities: =calc a = b := h1; _ = c := h2= | -| Concept | Lean | -|---------|------| -| Universal `∀ x, P x` | `intro x` to prove; `h x` or `apply h` to use | -| Existential `∃ x, P x` | `⟨x, h⟩` to prove; `rcases h with ⟨x, hx⟩` to use | -| Equality `a = b` | `rfl` when definitional; `rw [h]` when propositional | -| `calc` block | Chain equalities: `calc a = b := h1; _ = c := h2` | - -## Exercises - -### Exercise 4.1 — Universal quantifier - -```lean +** Exercises +:PROPERTIES: +:CUSTOM_ID: exercises +:END: +*** Exercise 4.1 --- Universal quantifier +:PROPERTIES: +:CUSTOM_ID: exercise-4.1-universal-quantifier +:END: +#+begin_src lean -- (a) Prove a simple forall theorem all_imp (P Q : Nat → Prop) (h : ∀ n, P n → Q n) (x : Nat) (hp : P x) : Q x := by @@ -46,11 +58,13 @@ def Even (n : Nat) : Prop := ∃ k, n = 2 * k theorem all_even_implies_42 : (∀ n, Even n) → Even 42 := by sorry -``` +#+end_src -### Exercise 4.2 — Existential quantifier - -```lean +*** Exercise 4.2 --- Existential quantifier +:PROPERTIES: +:CUSTOM_ID: exercise-4.2-existential-quantifier +:END: +#+begin_src lean -- (a) Prove existence theorem exists_square (a : Nat) : ∃ n, n = a * a := by @@ -67,11 +81,13 @@ theorem exists_or_distrib (P Q : Nat → Prop) : (∃ n, P n ∨ Q n) ↔ (∃ n theorem even_and_gt10_implies_gt5 : (∃ n, Even n ∧ n > 10) → (∃ n, n > 5) := by sorry -``` +#+end_src -### Exercise 4.3 — Equality and rewriting - -```lean +*** Exercise 4.3 --- Equality and rewriting +:PROPERTIES: +:CUSTOM_ID: exercise-4.3-equality-and-rewriting +:END: +#+begin_src lean -- (a) Prove symmetry and transitivity of equality (without using `symm`/`trans`) theorem eq_symm {α : Type} (a b : α) (h : a = b) : b = a := by @@ -90,8 +106,8 @@ theorem calc_example (a b c d : Nat) (h1 : a = b) (h2 : b = c + 1) (h3 : c + 1 = theorem rewrite_example (a b : Nat) (h : a = b + 1) : a * 2 = (b + 1) * 2 := by sorry -``` +#+end_src ---- +-------------- -← [Previous: Unit 3](03-propositions-and-proofs.md) · Next: [Unit 5 — Advanced Tactics](05-advanced-tactics.md) +← [[file:03-propositions-and-proofs.org][Previous: Unit 3]] · Next: [[file:05-advanced-tactics.org][Unit 5 --- Advanced Tactics]] diff --git a/tutorial-01-basics/05-advanced-tactics.md b/tutorial-01-basics/05-advanced-tactics.md deleted file mode 100644 index a5eea88..0000000 --- a/tutorial-01-basics/05-advanced-tactics.md +++ /dev/null @@ -1,52 +0,0 @@ -# Unit 5 — Advanced Tactics - -**Tutorial 1: Lean 4 Fundamentals** · [← Back to README](../README.md) - -## Goals - -- Prove properties by induction with `induction` -- Use `simp`, `ring`, `omega` for automation -- Use `rcases` and `obtain` for case analysis -- Work with `Nat` arithmetic proofs - -## Sources - -- TPIL Chapters 5–6 → https://leanprover.github.io/theorem_proving_in_lean4/ -- *Mathematics in Lean* (MiL), Chapter 1 → https://leanprover-community.github.io/mathematics_in_lean/ - -## Exercises - -```lean -open Nat - --- 5.1 — Induction on naturals -theorem add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) := by - sorry - -theorem add_comm (a b : Nat) : a + b = b + a := by - sorry - -theorem mul_comm (a b : Nat) : a * b = b * a := by - sorry - -theorem zero_mul (n : Nat) : 0 * n = 0 := by - sorry - --- 5.2 — Induction on lists -theorem reverse_reverse (xs : List α) : xs.reverse.reverse = xs := by - sorry - -theorem length_append (xs ys : List α) : (xs ++ ys).length = xs.length + ys.length := by - sorry - -theorem map_id (xs : List α) : xs.map id = xs := by - sorry - --- 5.3 — Using `simp` and `ring` -theorem square_sum (a b : Nat) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by - sorry -``` - ---- - -← [Previous: Unit 4](04-quantifiers-and-equality.md) · Next: [Unit 6 — Structures and Type Classes](06-structures-type-classes.md) diff --git a/tutorial-01-basics/05-advanced-tactics.org b/tutorial-01-basics/05-advanced-tactics.org new file mode 100644 index 0000000..1c79cc1 --- /dev/null +++ b/tutorial-01-basics/05-advanced-tactics.org @@ -0,0 +1,60 @@ +* Unit 5 --- Advanced Tactics +:PROPERTIES: +:CUSTOM_ID: unit-5-advanced-tactics +:END: +*Tutorial 1: Lean 4 Fundamentals* · [[../README.org][← Back to README]] + +** Goals +:PROPERTIES: +:CUSTOM_ID: goals +:END: +- Prove properties by induction with =induction= +- Use =simp=, =ring=, =omega= for automation +- Use =rcases= and =obtain= for case analysis +- Work with =Nat= arithmetic proofs + +** Sources +:PROPERTIES: +:CUSTOM_ID: sources +:END: +- TPIL Chapters 5--6 → https://leanprover.github.io/theorem_proving_in_lean4/ +- /Mathematics in Lean/ (MiL), Chapter 1 → https://leanprover-community.github.io/mathematics_in_lean/ + +** Exercises +:PROPERTIES: +:CUSTOM_ID: exercises +:END: +#+begin_src lean +open Nat + +-- 5.1 — Induction on naturals +theorem add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) := by + sorry + +theorem add_comm (a b : Nat) : a + b = b + a := by + sorry + +theorem mul_comm (a b : Nat) : a * b = b * a := by + sorry + +theorem zero_mul (n : Nat) : 0 * n = 0 := by + sorry + +-- 5.2 — Induction on lists +theorem reverse_reverse (xs : List α) : xs.reverse.reverse = xs := by + sorry + +theorem length_append (xs ys : List α) : (xs ++ ys).length = xs.length + ys.length := by + sorry + +theorem map_id (xs : List α) : xs.map id = xs := by + sorry + +-- 5.3 — Using `simp` and `ring` +theorem square_sum (a b : Nat) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by + sorry +#+end_src + +-------------- + +← [[file:04-quantifiers-and-equality.org][Previous: Unit 4]] · Next: [[file:06-structures-type-classes.org][Unit 6 --- Structures and Type Classes]] diff --git a/tutorial-01-basics/06-structures-type-classes.md b/tutorial-01-basics/06-structures-type-classes.org similarity index 63% rename from tutorial-01-basics/06-structures-type-classes.md rename to tutorial-01-basics/06-structures-type-classes.org index 3f307d1..c524e2c 100644 --- a/tutorial-01-basics/06-structures-type-classes.md +++ b/tutorial-01-basics/06-structures-type-classes.org @@ -1,22 +1,30 @@ -# Unit 6 — Structures and Type Classes +* Unit 6 --- Structures and Type Classes +:PROPERTIES: +:CUSTOM_ID: unit-6-structures-and-type-classes +:END: +*Tutorial 1: Lean 4 Fundamentals* · [[../README.org][← Back to README]] -**Tutorial 1: Lean 4 Fundamentals** · [← Back to README](../README.md) - -## Goals - -- Define `structure` for records with named fields +** Goals +:PROPERTIES: +:CUSTOM_ID: goals +:END: +- Define =structure= for records with named fields - Understand type classes as structures + instance resolution -- Use `deriving` for `Repr`, `BEq`, `Inhabited` -- Write monadic code with `do` notation - -## Sources +- Use =deriving= for =Repr=, =BEq=, =Inhabited= +- Write monadic code with =do= notation +** Sources +:PROPERTIES: +:CUSTOM_ID: sources +:END: - TPIL Chapter 9 (Structures), Chapter 10 (Type Classes) -- FPIL Chapters 3–5 (overloading, monads) +- FPIL Chapters 3--5 (overloading, monads) -## Exercises - -```lean +** Exercises +:PROPERTIES: +:CUSTOM_ID: exercises +:END: +#+begin_src lean -- 6.1 — Structures structure Point where x : Float @@ -61,8 +69,8 @@ def compute (x y z : Nat) : Option Nat := #eval compute 10 2 3 -- expected: some 2 #eval compute 10 0 3 -- expected: none -``` +#+end_src ---- +-------------- -← [Previous: Unit 5](05-advanced-tactics.md) · Next: [Unit 7 — Dependent Types](07-dependent-types.md) +← [[file:05-advanced-tactics.org][Previous: Unit 5]] · Next: [[file:07-dependent-types.org][Unit 7 --- Dependent Types]] diff --git a/tutorial-01-basics/07-dependent-types.md b/tutorial-01-basics/07-dependent-types.org similarity index 57% rename from tutorial-01-basics/07-dependent-types.md rename to tutorial-01-basics/07-dependent-types.org index f0715a2..f3d4cd0 100644 --- a/tutorial-01-basics/07-dependent-types.md +++ b/tutorial-01-basics/07-dependent-types.org @@ -1,33 +1,43 @@ -# Unit 7 — Dependent Types - -**Tutorial 1: Lean 4 Fundamentals** · [← Back to README](../README.md) - -## Goals +* Unit 7 --- Dependent Types +:PROPERTIES: +:CUSTOM_ID: unit-7-dependent-types +:END: +*Tutorial 1: Lean 4 Fundamentals* · [[../README.org][← Back to README]] +** Goals +:PROPERTIES: +:CUSTOM_ID: goals +:END: - Understand types that depend on values -- Work with `Fin n` (numbers < n), `Vector α n` (fixed-length lists) +- Work with =Fin n= (numbers < n), =Vector α n= (fixed-length lists) - Write functions whose return type depends on input - See why dependent types matter for PL semantics -## Sources - +** Sources +:PROPERTIES: +:CUSTOM_ID: sources +:END: - TPIL Chapter 2 "Dependent Type Theory" - FPIL Chapter 7 "Programming with Dependent Types" - Henson 2025: "Beginner Resources for Formalizing Lambda Calculi" -## Concepts +** Concepts +:PROPERTIES: +:CUSTOM_ID: concepts +:END: +| Concept | Lean | +|---------------------------+-----------------------------------------------------| +| Pi type =(x : α) → β x= | Function where return type depends on argument | +| Sigma type =Σ x : α, β x= | Dependent pair: value + property | +| =Fin n= | Natural numbers =< n= | +| =Vector α n= | Lists with length tracked in the type | +| =h : a = b → ...= | Equality can rewrite types (substitution principle) | -| Concept | Lean | -|---------|------| -| Pi type `(x : α) → β x` | Function where return type depends on argument | -| Sigma type `Σ x : α, β x` | Dependent pair: value + property | -| `Fin n` | Natural numbers `< n` | -| `Vector α n` | Lists with length tracked in the type | -| `h : a = b → ...` | Equality can rewrite types (substitution principle) | - -## Exercises - -```lean +** Exercises +:PROPERTIES: +:CUSTOM_ID: exercises +:END: +#+begin_src lean -- 7.1 — Fin n -- Define a safe nth function for lists that *cannot* fail at runtime def safeNth {α : Type} (xs : List α) (i : Fin xs.length) : α := @@ -70,8 +80,8 @@ inductive HasType : Expr → Ty → Prop where theorem isZero_returns_bool (e : Expr) : HasType (Expr.isZero e) Ty.nat → HasType e Ty.nat := by sorry -``` +#+end_src ---- +-------------- -← [Previous: Unit 6](06-structures-type-classes.md) · [← Tutorial 1 Index](./) · Next: [Tutorial 2 — Unit 8](../tutorial-02-semantics/08-syntax-representation.md) +← [[file:06-structures-type-classes.org][Previous: Unit 6]] · [[./][← Tutorial 1 Index]] · Next: [[../tutorial-02-semantics/08-syntax-representation.org][Tutorial 2 --- Unit 8]] diff --git a/tutorial-02-semantics/08-syntax-representation.md b/tutorial-02-semantics/08-syntax-representation.org similarity index 66% rename from tutorial-02-semantics/08-syntax-representation.md rename to tutorial-02-semantics/08-syntax-representation.org index 189eb81..0f31386 100644 --- a/tutorial-02-semantics/08-syntax-representation.md +++ b/tutorial-02-semantics/08-syntax-representation.org @@ -1,28 +1,36 @@ -# Unit 8 — Representing Syntax - -**Tutorial 2: PL Semantics in Lean** · [← Back to README](../README.md) - -## Goals +* Unit 8 --- Representing Syntax +:PROPERTIES: +:CUSTOM_ID: unit-8-representing-syntax +:END: +*Tutorial 2: PL Semantics in Lean* · [[../README.org][← Back to README]] +** Goals +:PROPERTIES: +:CUSTOM_ID: goals +:END: - Encode lambda calculus terms as an inductive type - Understand three binding representations: - 1. **Named** (strings — simple, but α-equiv isn't definitional) - 2. **de Bruijn indices** (numbers — α-equiv is free, shifting is painful) - 3. **Locally nameless** (free vars named, bound vars indexed — compromise) + 1. *Named* (strings --- simple, but α-equiv isn't definitional) + 2. *de Bruijn indices* (numbers --- α-equiv is free, shifting is painful) + 3. *Locally nameless* (free vars named, bound vars indexed --- compromise) We'll use de Bruijn indices (the "heavy lifter") for the rest of this tutorial, with locally nameless for comparison. -## Sources - -- syndikos/lean4-stlc `Syntax.lean`: https://github.com/syndikos/lean4-stlc +** Sources +:PROPERTIES: +:CUSTOM_ID: sources +:END: +- syndikos/lean4-stlc =Syntax.lean=: https://github.com/syndikos/lean4-stlc - Chris Henson 2025: https://chrishenson.net/posts/2025-05-10-formalized_lambda_calculus.html - chenson2018/LeanScratch: https://github.com/chenson2018/LeanScratch - Software Foundations Vol.2: https://softwarefoundations.cis.upenn.edu/ -## Exercises - -```lean +** Exercises +:PROPERTIES: +:CUSTOM_ID: exercises +:END: +#+begin_src lean -- 8.1 — Named representation inductive NamedTerm where | var (x : String) @@ -68,15 +76,17 @@ inductive LNTerm where | lam (body : LNTerm) -- binder | app (f arg : LNTerm) deriving Repr -``` +#+end_src -### Key insight for PL semantics - -When we encode **typing contexts** `Γ = x₁:τ₁, x₂:τ₂, ...`, de Bruijn indices +*** Key insight for PL semantics +:PROPERTIES: +:CUSTOM_ID: key-insight-for-pl-semantics +:END: +When we encode *typing contexts* =Γ = x₁:τ₁, x₂:τ₂, ...=, de Bruijn indices give us "index into the context" for free. The last binding is index 0, the -second-last is index 1, etc. This makes the typing rules elegant in Lean — +second-last is index 1, etc. This makes the typing rules elegant in Lean --- no name-clash avoidance needed. ---- +-------------- -← [Tutorial 1 — Unit 7](../tutorial-01-basics/07-dependent-types.md) · Next: [Unit 9 — Substitution](09-substitution.md) +← [[../tutorial-01-basics/07-dependent-types.org][Tutorial 1 --- Unit 7]] · Next: [[file:09-substitution.org][Unit 9 --- Substitution]] diff --git a/tutorial-02-semantics/09-substitution.md b/tutorial-02-semantics/09-substitution.org similarity index 75% rename from tutorial-02-semantics/09-substitution.md rename to tutorial-02-semantics/09-substitution.org index 02bfcd8..6dee846 100644 --- a/tutorial-02-semantics/09-substitution.md +++ b/tutorial-02-semantics/09-substitution.org @@ -1,22 +1,30 @@ -# Unit 9 — Substitution and α-Equivalence +* Unit 9 --- Substitution and α-Equivalence +:PROPERTIES: +:CUSTOM_ID: unit-9-substitution-and-α-equivalence +:END: +*Tutorial 2: PL Semantics in Lean* · [[../README.org][← Back to README]] -**Tutorial 2: PL Semantics in Lean** · [← Back to README](../README.md) - -## Goals - -- Implement `subst` (substitution) for de Bruijn terms -- Implement `lift` (index shifting) — the key operation that avoids capture +** Goals +:PROPERTIES: +:CUSTOM_ID: goals +:END: +- Implement =subst= (substitution) for de Bruijn terms +- Implement =lift= (index shifting) --- the key operation that avoids capture - Prove fundamental substitution lemmas -## Sources - -- syndikos/lean4-stlc `Syntax.lean` and `Reduction.lean` +** Sources +:PROPERTIES: +:CUSTOM_ID: sources +:END: +- syndikos/lean4-stlc =Syntax.lean= and =Reduction.lean= - chenson2018/LeanScratch: https://github.com/chenson2018/LeanScratch - PLFA Part 2: https://plfa.github.io/ -## Exercises - -```lean +** Exercises +:PROPERTIES: +:CUSTOM_ID: exercises +:END: +#+begin_src lean open DBTerm -- from Unit 8 -- 9.1 — Lift: shift all *free* variables above a cutoff by k @@ -67,15 +75,17 @@ lemma subst_lift_commute (t s : DBTerm) (n : Nat) : -- This lemma is *critical* for proving preservation/type safety later. -- It says that shifting before and after substitution agree. -``` - -### Why this matters +#+end_src +*** Why this matters +:PROPERTIES: +:CUSTOM_ID: why-this-matters +:END: Substitution is the core operation of operational semantics. Doing it right (no variable capture) is the hardest part of formalizing lambda calculi. -de Bruijn indices make capture impossible — the arithmetic is mechanical. +de Bruijn indices make capture impossible --- the arithmetic is mechanical. The lemmas here are boilerplate you prove once, then reuse everywhere. ---- +-------------- -← [Previous: Unit 8](08-syntax-representation.md) · Next: [Unit 10 — Small-Step Semantics](10-small-step-semantics.md) +← [[file:08-syntax-representation.org][Previous: Unit 8]] · Next: [[file:10-small-step-semantics.org][Unit 10 --- Small-Step Semantics]] diff --git a/tutorial-02-semantics/10-small-step-semantics.md b/tutorial-02-semantics/10-small-step-semantics.org similarity index 75% rename from tutorial-02-semantics/10-small-step-semantics.md rename to tutorial-02-semantics/10-small-step-semantics.org index 3da5232..ba5728a 100644 --- a/tutorial-02-semantics/10-small-step-semantics.md +++ b/tutorial-02-semantics/10-small-step-semantics.org @@ -1,22 +1,30 @@ -# Unit 10 — Small-Step Operational Semantics +* Unit 10 --- Small-Step Operational Semantics +:PROPERTIES: +:CUSTOM_ID: unit-10-small-step-operational-semantics +:END: +*Tutorial 2: PL Semantics in Lean* · [[../README.org][← Back to README]] -**Tutorial 2: PL Semantics in Lean** · [← Back to README](../README.md) +** Goals +:PROPERTIES: +:CUSTOM_ID: goals +:END: +- Define single-step reduction =→= for call-by-value λ-calculus +- Define reflexive-transitive closure =→*= +- Prove determinism: =t → t₁ ∧ t → t₂ ⇒ t₁ = t₂= -## Goals - -- Define single-step reduction `→` for call-by-value λ-calculus -- Define reflexive-transitive closure `→*` -- Prove determinism: `t → t₁ ∧ t → t₂ ⇒ t₁ = t₂` - -## Sources - -- syndikos/lean4-stlc `Reduction.lean`, `Semantics.lean` +** Sources +:PROPERTIES: +:CUSTOM_ID: sources +:END: +- syndikos/lean4-stlc =Reduction.lean=, =Semantics.lean= - Software Foundations Vol.2 "Smallstep" - PLFA Part 2 -## Exercises - -```lean +** Exercises +:PROPERTIES: +:CUSTOM_ID: exercises +:END: +#+begin_src lean open DBTerm -- 10.1 — Single-step cbv reduction @@ -62,4 +70,4 @@ def stuckExample : DBTerm := app (var 0) (var 1) -- a free variable applied to another free variable -- Show it's stuck (you'll prove something similar in Unit 12 with types) -``` +#+end_src diff --git a/tutorial-02-semantics/11-stlc-type-system.md b/tutorial-02-semantics/11-stlc-type-system.org similarity index 81% rename from tutorial-02-semantics/11-stlc-type-system.md rename to tutorial-02-semantics/11-stlc-type-system.org index bc1bfd0..c6347fa 100644 --- a/tutorial-02-semantics/11-stlc-type-system.md +++ b/tutorial-02-semantics/11-stlc-type-system.org @@ -1,22 +1,30 @@ -# Unit 11 — STLC Type System +* Unit 11 --- STLC Type System +:PROPERTIES: +:CUSTOM_ID: unit-11-stlc-type-system +:END: +*Tutorial 2: PL Semantics in Lean* · [[../README.org][← Back to README]] -**Tutorial 2: PL Semantics in Lean** · [← Back to README](../README.md) +** Goals +:PROPERTIES: +:CUSTOM_ID: goals +:END: +- Define simple types (=Nat → Bool=, etc.) +- Define typing contexts =Γ= as lists of types +- Encode the STLC typing judgment =Γ ⊢ t : τ= -## Goals - -- Define simple types (`Nat → Bool`, etc.) -- Define typing contexts `Γ` as lists of types -- Encode the STLC typing judgment `Γ ⊢ t : τ` - -## Sources - -- syndikos/lean4-stlc `Typing.lean` +** Sources +:PROPERTIES: +:CUSTOM_ID: sources +:END: +- syndikos/lean4-stlc =Typing.lean= - Software Foundations Vol.2 "Types" - sdemos/type-inference for type inference perspective -## Exercises - -```lean +** Exercises +:PROPERTIES: +:CUSTOM_ID: exercises +:END: +#+begin_src lean open DBTerm -- 11.1 — Types @@ -75,4 +83,4 @@ theorem weakening (Γ Δ : Ctx) (t : DBTerm) (τ : Ty) (h : HasType Γ t τ) (hsub : ∀ i, lookup Γ i = lookup (Δ ++ Γ) i) : HasType (Δ ++ Γ) t τ := by sorry -``` +#+end_src diff --git a/tutorial-02-semantics/12-type-safety.md b/tutorial-02-semantics/12-type-safety.org similarity index 79% rename from tutorial-02-semantics/12-type-safety.md rename to tutorial-02-semantics/12-type-safety.org index ace5170..59d9d11 100644 --- a/tutorial-02-semantics/12-type-safety.md +++ b/tutorial-02-semantics/12-type-safety.org @@ -1,22 +1,30 @@ -# Unit 12 — Type Safety (Progress + Preservation) +* Unit 12 --- Type Safety (Progress + Preservation) +:PROPERTIES: +:CUSTOM_ID: unit-12-type-safety-progress-preservation +:END: +*Tutorial 2: PL Semantics in Lean* · [[../README.org][← Back to README]] -**Tutorial 2: PL Semantics in Lean** · [← Back to README](../README.md) +** Goals +:PROPERTIES: +:CUSTOM_ID: goals +:END: +- Prove *Progress*: well-typed terms are either values or can step +- Prove *Preservation* (Subject Reduction): types survive reduction +- Combine them: *Type Soundness* = well-typed programs don't get stuck -## Goals - -- Prove **Progress**: well-typed terms are either values or can step -- Prove **Preservation** (Subject Reduction): types survive reduction -- Combine them: **Type Soundness** = well-typed programs don't get stuck - -## Sources - -- syndikos/lean4-stlc `Metatheory.lean` +** Sources +:PROPERTIES: +:CUSTOM_ID: sources +:END: +- syndikos/lean4-stlc =Metatheory.lean= - Software Foundations Vol.2 - PLFA Part 2: DeBruijn chapter -## Key Lemmas - -``` +** Key Lemmas +:PROPERTIES: +:CUSTOM_ID: key-lemmas +:END: +#+begin_example Canonical Forms: If [] ⊢ v : τ₁ ⇒ τ₂ and v is a value, then v = λ.t @@ -28,11 +36,13 @@ Preservation: Progress: If [] ⊢ t : τ, then either Value t or ∃ t', t → t' -``` +#+end_example -## Exercises - -```lean +** Exercises +:PROPERTIES: +:CUSTOM_ID: exercises +:END: +#+begin_src lean open DBTerm open Step open HasType @@ -101,4 +111,4 @@ theorem soundness {t : DBTerm} {τ : Ty} (h : HasType [] t τ) : · exact hnotval hv · apply hnostep exact hstep -``` +#+end_src diff --git a/tutorial-02-semantics/13-hm-declarative.md b/tutorial-02-semantics/13-hm-declarative.org similarity index 74% rename from tutorial-02-semantics/13-hm-declarative.md rename to tutorial-02-semantics/13-hm-declarative.org index e6a7880..058f4c9 100644 --- a/tutorial-02-semantics/13-hm-declarative.md +++ b/tutorial-02-semantics/13-hm-declarative.org @@ -1,43 +1,56 @@ -# Unit 13 — Hindley-Milner Declarative Typing Rules +* Unit 13 --- Hindley-Milner Declarative Typing Rules +:PROPERTIES: +:CUSTOM_ID: unit-13-hindley-milner-declarative-typing-rules +:END: +*Tutorial 2: PL Semantics in Lean* · [[../README.org][← Back to README]] -**Tutorial 2: PL Semantics in Lean** · [← Back to README](../README.md) - -## Goals - -- Extend STLC with **let-polymorphism** -- Encode HM types with **type schemes** `∀α. τ` +** Goals +:PROPERTIES: +:CUSTOM_ID: goals +:END: +- Extend STLC with *let-polymorphism* +- Encode HM types with *type schemes* =∀α. τ= - Formalize the 6 declarative typing rules (Var, App, Abs, Let, Inst, Gen) -- Understand the distinction between monomorphic (`τ`) and polymorphic (`σ = ∀α.τ`) types +- Understand the distinction between monomorphic (=τ=) and polymorphic (=σ = ∀α.τ=) types -## Sources +** Sources +:PROPERTIES: +:CUSTOM_ID: sources +:END: +- [[https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system][Wikipedia: Hindley-Milner type system]] +- [[https://www.jeffvaughan.net/docs/hmproof.pdf][Vaughan 2008]] (declarative rules, §2) +- [[https://github.com/sdemos/type-inference][sdemos/type-inference]] (Lean formalization) -- [Wikipedia: Hindley-Milner type system](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system) -- [Vaughan 2008](https://www.jeffvaughan.net/docs/hmproof.pdf) (declarative rules, §2) -- [sdemos/type-inference](https://github.com/sdemos/type-inference) (Lean formalization) +** Background +:PROPERTIES: +:CUSTOM_ID: background +:END: +HM adds *let-polymorphism* to STLC: -## Background - -HM adds **let-polymorphism** to STLC: -``` +#+begin_example let x = e₁ in e₂ -``` -In STLC, `x` would have a single monomorphic type. In HM, `x` gets a type -*scheme* — e.g., `∀α. α → α` for the identity function — and each use of `x` +#+end_example + +In STLC, =x= would have a single monomorphic type. In HM, =x= gets a type +/scheme/ --- e.g., =∀α. α → α= for the identity function --- and each use of =x= instantiates the scheme with fresh type variables. The declarative rules: -``` + +#+begin_example Var: Γ, x:σ ⊢ x : σ App: Γ ⊢ e₁ : τ₁ → τ₂ Γ ⊢ e₂ : τ₁ ⇛ Γ ⊢ e₁ e₂ : τ₂ Abs: Γ, x:τ₁ ⊢ e : τ₂ ⇛ Γ ⊢ λx.e : τ₁ → τ₂ Let: Γ ⊢ e₁ : σ Γ, x:σ ⊢ e₂ : τ ⇛ Γ ⊢ let x = e₁ in e₂ : τ Inst: Γ ⊢ e : ∀α.τ ⇛ Γ ⊢ e : τ[α := τ'] Gen: Γ ⊢ e : τ ∧ α ∉ ftv(Γ) ⇛ Γ ⊢ e : ∀α.τ -``` +#+end_example -## Exercises - -```lean +** Exercises +:PROPERTIES: +:CUSTOM_ID: exercises +:END: +#+begin_src lean -- 13.1 — Types and type schemes inductive MonoType where | tvar (id : Nat) -- type variable α @@ -112,8 +125,8 @@ theorem self_app_id_typed (τ : MonoType) : HMTyping [] self_app_id {vars := [], body := τ ⇒ τ} := by sorry -``` +#+end_src ---- +-------------- -← [Previous: Unit 12](12-type-safety.md) · Next: [Unit 14 — Algorithm W](14-algorithm-w.md) +← [[file:12-type-safety.org][Previous: Unit 12]] · Next: [[file:14-algorithm-w.org][Unit 14 --- Algorithm W]] diff --git a/tutorial-02-semantics/14-algorithm-w.md b/tutorial-02-semantics/14-algorithm-w.org similarity index 79% rename from tutorial-02-semantics/14-algorithm-w.md rename to tutorial-02-semantics/14-algorithm-w.org index f981e28..c88f951 100644 --- a/tutorial-02-semantics/14-algorithm-w.md +++ b/tutorial-02-semantics/14-algorithm-w.org @@ -1,39 +1,49 @@ -# Unit 14 — Algorithm W (Hindley-Milner Type Inference) - -**Tutorial 2: PL Semantics in Lean** · [← Back to README](../README.md) - -## Goals +* Unit 14 --- Algorithm W (Hindley-Milner Type Inference) +:PROPERTIES: +:CUSTOM_ID: unit-14-algorithm-w-hindley-milner-type-inference +:END: +*Tutorial 2: PL Semantics in Lean* · [[../README.org][← Back to README]] +** Goals +:PROPERTIES: +:CUSTOM_ID: goals +:END: - Understand type inference as solving unification constraints -- Implement **Algorithm W**: the classic HM inference algorithm -- Write `unify` (Robinson's unification) -- Write `infer` (the main inference loop) +- Implement *Algorithm W*: the classic HM inference algorithm +- Write =unify= (Robinson's unification) +- Write =infer= (the main inference loop) -## Sources - -- [Vaughan 2008, §3](https://www.jeffvaughan.net/docs/hmproof.pdf) -- [sdemos/type-inference](https://github.com/sdemos/type-inference) -- [Wikipedia: Algorithm W](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Algorithm_W) - -## Background +** Sources +:PROPERTIES: +:CUSTOM_ID: sources +:END: +- [[https://www.jeffvaughan.net/docs/hmproof.pdf][Vaughan 2008, §3]] +- [[https://github.com/sdemos/type-inference][sdemos/type-inference]] +- [[https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Algorithm_W][Wikipedia: Algorithm W]] +** Background +:PROPERTIES: +:CUSTOM_ID: background +:END: Algorithm W takes an expression and returns a substitution + type: -``` +#+begin_example infer(Γ, e) = (S, τ) -``` +#+end_example -- `Γ` maps variables to type schemes -- `e` is the expression to type -- `S` is a type substitution (unifies constraints found during inference) -- `τ` is the inferred monotype +- =Γ= maps variables to type schemes +- =e= is the expression to type +- =S= is a type substitution (unifies constraints found during inference) +- =τ= is the inferred monotype -The algorithm uses a supply of *fresh type variables* to build constraints, +The algorithm uses a supply of /fresh type variables/ to build constraints, then unifies them. -## Exercises - -```lean +** Exercises +:PROPERTIES: +:CUSTOM_ID: exercises +:END: +#+begin_src lean open MonoType open HMExpr open TypeScheme @@ -149,8 +159,8 @@ def infer_id : Option (Subst × MonoType × Nat) := -- 14.7 — Exercise: infer the type of let x = λy. y in x x def infer_self_app : Option (Subst × MonoType × Nat) := inferW [] self_app_id 0 -``` +#+end_src ---- +-------------- -← [Previous: Unit 13](13-hm-declarative.md) · Next: [Unit 15 — Soundness and Completeness](15-soundness-completeness.md) +← [[file:13-hm-declarative.org][Previous: Unit 13]] · Next: [[file:15-soundness-completeness.org][Unit 15 --- Soundness and Completeness]] diff --git a/tutorial-02-semantics/15-soundness-completeness.md b/tutorial-02-semantics/15-soundness-completeness.org similarity index 63% rename from tutorial-02-semantics/15-soundness-completeness.md rename to tutorial-02-semantics/15-soundness-completeness.org index dd4bbac..328f71d 100644 --- a/tutorial-02-semantics/15-soundness-completeness.md +++ b/tutorial-02-semantics/15-soundness-completeness.org @@ -1,28 +1,38 @@ -# Unit 15 — Soundness and Completeness of Algorithm W +* Unit 15 --- Soundness and Completeness of Algorithm W +:PROPERTIES: +:CUSTOM_ID: unit-15-soundness-and-completeness-of-algorithm-w +:END: +*Tutorial 2: PL Semantics in Lean* · [[../README.org][← Back to README]] -**Tutorial 2: PL Semantics in Lean** · [← Back to README](../README.md) - -## Goals - -- Prove that Algorithm W is **sound**: every inferred type is derivable in the declarative system -- Prove that Algorithm W is **complete**: every derivable type can be inferred (up to generalization) +** Goals +:PROPERTIES: +:CUSTOM_ID: goals +:END: +- Prove that Algorithm W is *sound*: every inferred type is derivable in the declarative system +- Prove that Algorithm W is *complete*: every derivable type can be inferred (up to generalization) - Understand the relationship between inference and declarative rules -## Sources +** Sources +:PROPERTIES: +:CUSTOM_ID: sources +:END: +- [[https://www.jeffvaughan.net/docs/hmproof.pdf][Vaughan 2008, §4]] +- [[https://github.com/sdemos/type-inference][sdemos/type-inference]] =Soundness.lean=, =Completeness.lean= -- [Vaughan 2008, §4](https://www.jeffvaughan.net/docs/hmproof.pdf) -- [sdemos/type-inference](https://github.com/sdemos/type-inference) `Soundness.lean`, `Completeness.lean` +** The Theorems +:PROPERTIES: +:CUSTOM_ID: the-theorems +:END: +*Soundness*: If =infer(Γ, e) = (S, τ)=, then =Γ ⊢ e : τ= declaratively. -## The Theorems +*Completeness*: If =Γ ⊢ e : τ= declaratively, then there exists =S, τ'= such that +=infer(Γ, e) = (S, τ')= and =τ= is a substitution instance of =τ'= (i.e., W finds the /most general/ type). -**Soundness**: If `infer(Γ, e) = (S, τ)`, then `Γ ⊢ e : τ` declaratively. - -**Completeness**: If `Γ ⊢ e : τ` declaratively, then there exists `S, τ'` such that -`infer(Γ, e) = (S, τ')` and `τ` is a substitution instance of `τ'` (i.e., W finds the *most general* type). - -## Exercises - -```lean +** Exercises +:PROPERTIES: +:CUSTOM_ID: exercises +:END: +#+begin_src lean open HMTyping open MonoType @@ -78,8 +88,8 @@ theorem principal_types (Γ : HMEnv) (e : HMExpr) (σ : TypeScheme) (∃ S', applySubst S' τ_principal = σ.body) := by exact completeness_W Γ e σ h -``` +#+end_src ---- +-------------- -← [Previous: Unit 14](14-algorithm-w.md) · [← Tutorial 2 Index](.) · [← Back to README](../README.md) +← [[file:14-algorithm-w.org][Previous: Unit 14]] · [[file:.][← Tutorial 2 Index]] · [[../README.org][← Back to README]]