A 2024 Computer Science Curriculum

This is a benefit of dependently typed languages your future 'discrete math' intro course that every undergrad teaches can all be done with a proof assistant now.

• The Mechanics of Proof using Lean by Heather MacBeth

• 15-150 Principles of Functional Programming (SML)
  • Older Assignments & labs can be grabbed from here and here
  • TAs wrote helpful docs for 15-150
  • We can also try whatever current version of hype for types
• Programming with Categories a workbook (Haskell)

They are going to fully mechanize 15-210 soon using calf/decalf to prove costs.

• 15-210 Parallel & Sequential Algorithms (SML)
  • Some recitations/review videos here but we won't need them
  • The hw/labs can be found here or here
  • A very detailed rewrite of the regex matcher from Harper's SML book for proof directed debugging but now with efficient backtracking
  • Functional Data Structures by Prof Ragde (OCaml)

• Practical Foundations for Programming Languages book and supplementary materials
• Robert Harper OPLSS 2021 lectures and some earlier OPLSS lectures for his book
  • We have access to older 15-312 assignments (SML)
• PLAI a workbook (Racket/Lisp)

The HoTT seminar explains how univalence works which will be needed to understand how equality works in many new type theories

• 15-819 Homotopy Type Theory and book
  • Programming in MLTT book

Whatever proof theory and categorical logic we can get our hands on

• Constructive Logic (SML)
• How to read/use The Edinburgh Logical Framework or LF
  • technical details we have to know
• Logical relations and LR as types or ParamTT
• 80-514 Categorical Logic

Mac Lane's or Emily Riehl's book is accessible too if we learn some insights into basic algebraic topology.

• MIT course Applied Category Theory
  • Categories for Types by Crole or Awodey's book

Gitpod free tier is easiest. To install Lean locally w/Visual Studio:

• install Lean
• install git
• install code (Visual Studio code) though I use emacs see below
• in terminal type: git clone https://github.com/hrmacbeth/math2001.git
• cd math2001
• in terminal: lake exe cache get
  • it downloads 3972+ files (wtf)
• 'code .' to start from present directory
• install lean4 extension

Click on 01ProofsbyCalculation.lean you should get a right panel opening up in VS code called 'Lean Infoview' that displays tactic state goals and all messages.

Install everything as before then git clone lean4-mode, paste the readme elisp into .emacs or init.el file, restart and open any .lean file. Ctrl-c Ctrl-i opens the lean view in a new window showing goals. If you use vanilla emacs from some distros like Ubuntu you'll have some 'can't verify signature' error which is fixed by updating elpa keyring.

Another way is with gpg:

gpg --homedir ~/.emacs.d/elpa/gnupg --list-keys 

/home/x/.emacs.d/elpa/gnupg/pubring.kbx
-----------------------------------------
pub   dsa2048 2014-09-24 [SC] [expired: 2019-09-23]
      CA442C00F91774F17F59D9B0474F05837FBDEF9B
uid           [ expired] GNU ELPA Signing Agent (2014) <elpasign@elpa.gnu.org>

pub   rsa3072 2019-04-23 [SC] [expires: 2024-04-21]
      C433554766D3DDC64221BFAA066DAFCB81E42C40
uid           [ unknown] GNU ELPA Signing Agent (2019) <elpasign@elpa.gnu.org>

pub   ed25519 2022-12-28 [C] [expires: 2032-12-25]
      AC49B8A5FDED6931F40EE78BF993C03786DE7ECA
uid           [ unknown] GNU ELPA Signing Agent (2023) <elpasign@elpa.gnu.org>
sub   ed25519 2022-12-28 [S] [expires: 2027-12-27]

Update key if your second key is expired:

gpg --homedir ~/.emacs.d/elpa/gnupg --keyserver hkps://keys.openpgp.org --recv-keys 066DAFCB81E42C40

Reading 1.1 Proving equalities from Mechanics of Proof. Any examples you don't understand come back here after writing some Lean proofs you won't get them all immediately. First example expand out (a - b) and notice you need to add 4ab in order to balance both sides. The problem statement tells us (a - b) = 4 so (a - b)² is 16 after substitution.

1.2.x Proving equalities in Lean the .lean files are all included in the Math2001 directory you cloned from github. I had to fight with Lean to get it to accept 1.2.4 so rewrote it exactly like she did with parens:

-- Example 1.2.4.
-- Exercise: type out the whole proof printed in the text as a Lean proof.
example {a b c d e f : ℤ} (h1 : a * d = b * c) (h2 : c * f = d * e) :
    d * (a * f - b * e) = 0 := 
   calc
    d * (a * f - b * e)
      = d * a * f - d * b * e := by ring
    _ = (a * d) * f - d * b * e := by ring
    _ = (b * c) * f - d * b * e := by rw [h1]
    _ = b * (c * f) - d * b * e := by ring
    _ = b * (d * e) - d * b * e := by rw [h2]
    _ = 0 := by ring 

We are using 'calc' in Lean hence the name proof by calculation. I'm guessing the underscore represents the entire left hand side of the equation indicating to the rw (rewrite) pattern matcher to ignore it. There's nothing in the documentation I could easily find but Terence Tao describes the underscore here same way.

Look at the infoview/goals it will tell you when that stage is done by 'goals accomplished', also click around various parts of the proof to see how the infoview changes:

-- Example 1.3.2
example {x : ℤ} (h1 : x + 4 = 2) : x = -2 :=
  calc
  x = (x + 4) - 4 := by ring
  _ = 2 - 4 := by rw [h1]
  _ = -2 := by ring 

I guessed the syntax for rationals in Lean and it worked:

-- Example 1.3.4
example {w : ℚ} (h1 : 3 * w + 1 = 4) : w = 1 :=
  calc
  w = (3 * w + 1)/3 - 1/3 := by ring
  _ = 4/3 - 1/3 := by rw [h1]
  _ = 1 := by ring

1.3.11 you can use Lean to tell you when the sides have been balanced. You did it correctly if goals panel or infoview shows goals accomplished and the linter hasn't added any red squiggle lines or other errors. Some exercises I tried, you can rewrite a line using both hypotheses and eliminate a lot of steps I kept them here for illustration how Lean works:

example {u v : ℚ} (h1 : 4 * u + v = 3) (h2 : v = 2) : u = 1 / 4 :=
  calc
  u = (4 * u + v)/4 - v/4 := by ring
  _ = 3/4 - 2/4 := by rw [h1, h2]
  _ = 1/4 := by ring

example {u v : ℝ} (h1 : u + 1 = v) : u ^ 2 + 3 * u + 1 = v ^ 2 + v - 1 :=
  calc
  u ^ 2 + 3 * u + 1 = (u + 1) * (u + 1) + (u + 1) - 1 := by ring
  _ = v * v + v - 1 := by rw [h1]
  _ = v ^ 2 + v - 1 := by ring

1.3.2 once again we first establish x = x then use the hypothesis to rewrite it

-- Example 1.3.2
example {x : ℤ} (h1 : x + 4 = 2) : x = -2 :=
  calc
  x = (x + 4) - 4 := by ring
  _ = 2 - 4 := by rw [h1]
  _ = -2 := by ring

For the rest of these examples try them yourself going through the 03TipsandTricks.lean file before looking at the solution it's the only way you learn.

-- Example 1.3.5
example {x : ℤ} (h1 : 2 * x + 3 = x) : x = -3 :=
  calc
  x = (2 * x) - x  := by ring
  _ = 2 * x - (2 * x + 3) := by rw [h1]
  _ = -3 := by ring

(╯°□°)╯︵ ┻━┻ if you see calc underlined with a red error it means you forgot an equal sign or _ sign in your chain of rewrites or there is an accidental character floating around in the scope out of view somewhere it took me forever to figure that out as Lean kept giving some cryptic message and I was looking at the signature.

1.3.11 exercises all use the examples we just saw. Look at 1.3.8 example when you try exercise 11 and manipulate it so a = (4 + 2) / 3.

example {x y : ℝ} (h1 : x = 3) (h2 : y = 4 * x - 3) : y = 9 :=
  calc
  y = y := by ring
  _ = 4*x - 3 := by rw [h2]
  _ = 4*3 - 3 := by rw [h1]
  _ = 9 := by ring

example {p : ℝ} (h1 : 5 * p - 3 = 3 * p + 1) : p = 2 :=
  calc
  p = (5*p -3 - 3*p + 1)/2 + 1 := by ring
  _ = (3*p + 1 - 3*p + 1)/2 + 1 := by rw [h1]
  _ = 2/2 + 1 := by ring
  _ = 2 := by ring

We're still doing the proofs by calc chapter.

1.4.1 example copy down some of the general rules

• Inequality preserved if C \(\ge\) 0:
• A \(\ge\) B implies CA \(\ge\) CB
• A \(\ge\) B implies A - C \(\ge\) B - C
• A \(\ge\) B and B > C then A > C

• Reversed inequality:
• A \(\ge\) B implies C - B \(\ge\) C - A
  • 2 \(\ge\) 1 implies 5 - 1 \(\ge\) 5 - 2

To get the full list of the unicode symbols every editor plugin comes with an abbreviations.json file. Place '\' (LaTeX style commands) before any of those symbols on the left of the abbreviations file to see them converted to the symbols on the right. For example \b is converted in the editor to \(\beta\)

\ge greater or equal
\le less than or equal
< and > are just unicode keyboard chars

-- Example 1.4.2
-- Exercise: replace the words "sorry" with the correct Lean justification.
example {r s : ℚ} (h1 : s + 3 ≥ r) (h2 : s + r ≤ 3) : r ≤ 3 :=
  calc
    r = (s + r + r - s) / 2 := by ring
    _ ≤ (3 + (s + 3) - s) / 2 := by rel [h1, h2]
    _ = 3 := by ring

Example 1.4.3 think why is x + y <= x + (x + 5) it's because y <= x + 5 and x is <= to itself.

-- Example 1.4.3
-- Exercise: type out the whole proof printed in the text as a Lean proof.
example {x y : ℝ} (h1 : y ≤ x + 5) (h2 : x ≤ -2) : x + y < 2 :=
  calc
  x + y ≤ x + (x + 5) := by rel [h1]
  _ = 2 * x + 5 := by ring 
  _ ≤ 2 * -2 + 5 := by rel [h2]
  _ < 2 := by numbers

Example 1.4.6 the final tactic is := by extra which is defined if you click on 'Index of Lean tactics' as "extra checks an inequality whose two sides differ by the addition of a positive quantity".

-- Example 1.4.9
-- Exercise: replace the words "sorry" with the correct Lean justification.
example {a b : ℚ} (h1 : a ≥ 0) (h2 : b ≥ 0) (h3 : a + b ≤ 8) :
    3 * a * b + a ≤ 7 * b + 72 :=
  calc
    3 * a * b + a
      ≤ 2 * b ^ 2 + a ^ 2 + (3 * a * b + a) := by extra
    _ = 2 * ((a + b) * b) + (a + b) * a + a := by ring
    _ ≤ 2 * (8 * b) + 8 * a + a := by rel [h3]
    _ = 7 * b + 9 * (a + b) := by ring
    _ ≤ 7 * b + 9 * 8 := by rel [h3]
    _ = 7 * b + 72 := by ring

1.4.10 same tactic used, put left hand side of inequality on right and side, add some positive squares. If you use any symbolic calculator online then the enormous expanded square makes sense as (a⁴ + b⁴ + c⁴)² = a⁸+2a⁴b⁴+2a⁴c⁴+b⁸+2b⁴c⁴+c⁸

Try some 14.11 exercises

example {a b : ℚ} (h1 : 3 ≤ a) (h2 : a + 2 * b ≥ 4) : a + b ≥ 3 :=
  calc
  a + b = a/2 + (a + 2*b)/2 := by ring
      _ ≥ 3/2 + 4/2 := by rel [h1,h2]
      _ ≥ 3 := by numbers

example {x : ℤ} (hx : x ≥ 9) : x ^ 3 - 8 * x ^ 2 + 2 * x ≥ 3 :=
  calc
  x ^ 3 - 8 * x ^ 2 + 2 * x = 
  x * x * x - 8 * x * x + 2 * x := by ring
  _ ≥ 9 * x * x - 8 * x * x + 2 * x := by rel [hx]
  _ = x * x + 2 * x := by ring
  _ ≥ 9 * x + 2 * x := by rel [hx]
  _ = 11 * x := by ring 
  _ ≥ 11 * 9 := by rel [hx]
  _ ≥ 3 := by numbers

example {n : ℤ} (hn : n ≥ 10) : n ^ 4 - 2 * n ^ 2 > 3 * n ^ 3 :=
  calc
  n^4 - 2 * n^2 =  
  n * n^3 - 2 * n^2 := by ring
  _ ≥ 10 * n^3 - 2 * n^2 := by rel [hn]
  _ = 3 * n^3 + 7 * n * n * n - 2 * n * n := by ring
  _ ≥ 3 * n^3 + 7 * 10 * n * n - 2 * n * n := by rel [hn]
  _ = 3 * n^3 + 68 * n * n := by ring
  _ ≥ 3 * n^3 + 68 * 10 * 10 := by rel [hn]
  _ > 3 * n^3 := by extra

Exercise 6 I couldn't figure it out in lean as I don't know enough of the standard library yet as there's no hypothesis to use rel or addarith with and the sig wants a rational number. My attempts using squares with the tactic extra failed too whereas by hand it is easy:

• x² - 2x \(\ge\) -1
• x² - 2x + 1 \(\ge\) -1 + 1
• (x - 1)² \(\ge\) 0
  • which we know is true since squares are always positive

Reading the second chapter.

2.1.2 prove m + 3 = 9 then final tactic is addarith to subtract 3 from both sides and show m = 9 - 3 or 6.

2.1.5 example remember extra checks an inequality whose two sides differ by the addition of a positive quantity and the square b² is always positive.

Another example is 2.1.7 of extra since positive quantities

example (a b : ℝ) (h1 : -b ≤ a) (h2 : a ≤ b) : a ^ 2 ≤ b ^ 2 := by
  have h3 : 0 ≤ b + a := by addarith [h1]
  have h4 : 0 ≤ b - a := by addarith [h2]
  calc
  a^2 ≤ a^2 + (b + a) * (b - a) := by extra
  _ = b^2 := by ring

2.1.8 extra tactic again:

example (a b : ℝ) (h : a ≤ b) : a ^ 3 ≤ b ^ 3 := by
  have h2 : 0 ≤ b - a := by addarith [h]
  calc
  a^3 ≤ a^3 + ((b-a)*((b-a)^2 + 3*(b + a)^2)/4) := by extra
  _ = b^3 := by ring

The cancel tactic is defined as follows if you look at the code it's another tactic written for this book to simplify the regular lean libraries which are all abstract algebra we haven't learned yet.

'Cancel 2 at h' means

• 2x = 2y cancel to x = y
• 2x < 2y cancel to x < y
• x² = y² cancel to x = y
• 0 < 2x cancel to 0 < x
• x² = 0 cancel to x = 0

However in the exercises I couldn't get it work.

Example Ex 2.1.9 this is what I want to do but it won't let me despite x already being x > 1 so no possible way (x + 2) could be (-2 + 2) or 0:

example {x : ℚ} (h1 : x ^ 2 = 4) (h2 : 1 < x) : x = 2 := by
  have h3 :=
  calc
  x * (x + 2) = 2 * (x ^ 2 + 2 * x)/2 := by ring
  _ = 2 * (4 + 2 * x)/2 := by rw [h1]
  _ = 2 * (x + 2) := by ring
  cancel (x + 2) at h3  

Another example from 2.1.9 that doesn't work, I tried after to manually add in (h : n > 0) and still fails:

example {n : ℤ} (hn : n ^ 2 + 4 = 4 * n) : n = 2 := by
  have hm : 0 = n ^ 2 - 4 * n + 4 := by addarith [hn]
  have h1 :=
  calc
  0 = n ^ 2 - 4 * n + 4 := by rw [hm]
  _ = (n - 2)^2 := by ring
  cancel 2 at h1 
  addarith [h1]

Others have had problems too and filed an issue for a possible bug or maybe I don't understand how Lean4 tactics work we'll have to skip these and try them again later when the author replies.

TODO

Watching the first lecture. According to Robert Harper and Shriram Krishnamurthi so-called 'programming paradigms' like imperative, object-oriented or functional are vague descriptors of the same thing which is just programming. We'll work through both their books PFPL and PLAI after this course. The professor he talks about ~45m we're doing his constructive logic course after this too. @51m LaTeX is how you generate symbols like \(\implies\) for books/papers. Don Knuth invented the original program TeX (annoyingly pronounced 'tek') to write TAOCP.

If you want to follow what he's doing in the REPL try SOSML the online interpreter. The type annotations are optional in SML you can enter 'fun double n = n + n' though I would always use them in the beginning just to remember what you're doing.