A (mostly functional) 21st Century CompSci Curriculum

The proof assistant used is the language itself.

• 15-150 Principles of Functional Programming (SML)
  • The terse version
  • Older Assignments & labs here and here
  • We can also try whatever current version of hype for types
  • A very detailed and efficient rewrite of the regex matcher from Harper's SML book for proof directed debugging

Coinduction/Coalgebras are introduced here.

• CS410 Advanced Functional Programming (Agda)
  • Lecture playlist or McBride playlist

This is a typical discrete math course formalized in Lean 4.

• The Mechanics of Proof book by Heather MacBeth

Mathematical Structures for CS an introductory course using the Ask proof assistant.

• Lecture Playlist and second semester
• Books: In-progress draft and Gödel, Escher, Bach: an Eternal Golden Braid by Douglas R. Hofstadter

The most interesting course is Advanced Data Structures by Erik Demaine.

I plan to use the free book Functional Data Structures and Algorithms which verifies complexity and correctness with Isabelle/HOL then will try calf to analyze costs of the same algorithms with different cost models. There's many other books to try in calf like the parallel algorithms in CMU's 15-210 Book that accounts for garbage collection and moving I/O around.

A course you may like is Algorithmic Lower Bounds and draft book because one day you will be working on something which seems to be impossible and you'll want to know is there a similar problem out there someone else has already proved belongs in EXP-hard because it means you are wasting your time. There is many, many problems that can't be solved with an algorithm in any sort of sane polynomial time. This course teaches how an existing problem in some complexity class can be reduced using constraint logic and other methods to whatever it is you're working on to prove you're screwed. Now you can change the goals of what you're trying to do or maybe try known approximation tricks of similar problems in that class to help get better running time.

Proofs are programs.

• Robert Harper's book (abbreviated version) and supplementary materials
• OPLSS 2021 lectures and any other lectures we can find
• All the orig papers on logical relations and parametricity structures
• PLAI a workbook (Racket/Lisp)

HoTT & Univalence

• 15-819 Homotopy Type Theory lectures and book
  • Principles of Dependent Type Theory (draft)
  • Univalent Foundations lecture notes and exercises
  • Programming in MLTT book
  • Intro to Homotopy Type Theory has 200+ exercises

Everything we can find on phase distinctions too and experimental (higher observable) type theories.

Intuitionistic logic is a synonym for “constructive logic” and proof theory is viewing mathematical proofs as finite combinatorial objects or actual things you can construct and show someone.

• Constructive Logic (SML)
• Many OPLSS lectures on YouTube about proof theory
• Many Per Martin-Lof papers
• How to read/use The Edinburgh Logical Framework or LF
  • technical details we have to know

The algebra of proofs/programs.

• MIT course Applied Category Theory
• Programming with Categories a workbook (Haskell)

NJ Wildberger made an excellent Algebraic Topology course which avoids set theory nonsense and focuses on the ideas. This is what we'll need to understand any book on Category Theory.

Watching the first lecture. Some of this is in chapter 1 of the book draft.

This already seems bonkers but reminder what we are actually learning is this taught in Cornell's CS2800 course or Mathematics for Computer Science that old MIT mcs.pdf floating around. McBride has changed the delivery so anyone with no experience can understand it.

Everything in the lectures enter them into an .ask file and don't delete them because we'll need all these definitions later. Ask has to be built up from scratch: "Ask doesn't know anything by default and if you delete things you've removed part of it's brain".

-- Double dash signals a comment!

-- Declare a data type, Number,
-- which gives spuds-and-a-lemon numbers.
data Number
 = Z | S Number

-- Define four to be the number
-- made from four spuds and a lemon
four :: Number
define four = S (S (S (S Z)))

When you run that in emacs by pressing Tab, it will change your current buffer to show 'defined' like in the lecture except on their system the output is shown beside the editor and ours directly changes things. Undo the changes if you make a mistake.

The way addition works is also in the book Chapter 1.2, to add S(SZ) to SZ remove the two S's on the left and once Z is reached substitute it for the other number SZ to get S(S(SZ). Here is the function that does exactly that and if you press tab as you write then Ask fills in all the code for you:

-- define plus
plus :: Number -> Number -> Number
defined plus n m inductively n where
  defined plus n m from n where
    defined plus Z m = m
    defined plus (S x) m = S (plus x m)

Defined inductively means something constructed by a finite amount of applications of a given set of rules. A number has two 'rules' for it's construction: Z or S Number. You make more numbers by applying the constructor S to a Number like S (SZ) to make 2 or SZ to make 1. We're told to imagine a skewer with a lemon added first then spuds attached on the skewer beside the lemon.

Full explanation of the code:

plus :: Number -> Number -> Number

This is a function type signature: plus consumes two inputs of type Number and returns type Number.

define plus n m inductively n where

Prof McBride says to interpret this as n is the input that gets smaller. Recall that anything defined inductively is something constructed from a finite set of applications of a given set of rules that's also what this is code is saying: n was made by such a process so it will have cases to split on.

defined plus n m from n where
 defined plus Z m = m
 defined plus (S x) m = S (plus x m)

The input n is either Z or S Number. The variable x is bound to the Number from S Number. If a Number is S(SZ) then (SZ) is bound to x. This is interpreted as SZ is the successor and Z is the number or if you want 'the rest of the number'. If we keep calling plus again with x which is the rest of the number then the inputs to plus get smaller until Z is reached.

Let's look at how this function returns values.

Set value of n = S(S(S(SZ)))
Set value of m = Z

plus n m returns:
S(plus (S(S(SZ))) m)
S(S(plus (S(SZ)) m))
S(S(S(plus SZ m)))
S(S(S(S(plus Z m))))  
 -- case if Z return m which here m = Z 
S(S(S(SZ)))

Where do the brackets come from in the returns? In the definition of plus: S (plus x m). Execution in purely functional programming is simple substitution like math. Everything in the brackets is replaced by the next return which is another S (plus x m) then the most nested bracket is evaluated first once we reach a Z and recursion stops.

In this lecture is a very illustrative way to tell students to use chat and not email because profs get hundreds of them: "Back in the Soviet days, the KGB guards would wake up the prisoners every morning with a fresh bucket of cold piss. That's how I feel when looking at my email and you sending one is helping to fill up the bucket".

We can't see the other screen but this is just associativity: n + m is n added m times. 2 + 3 is 2 + 2 + 2 and 3 + 2 is 3 + 3 and both are the same result. This is in the book 1.2 Chapter.

Proof by Induction

Inductive reasoning is after you observe all the special cases you make an 'inductive leap' to the general case. It's how theories about the world are found you find a pattern or something in individual examples and make it into a generalized theory.

A proof by induction is similar you prove that some property holds in the base case which here means an input of Z. That property could be that the plus function when given n and m inputs will always compute n + m. Next you inductively assume for all future inputs n that this property still holds. You prove it holds for the successor input and now there is an implication chain as Z implies x implies S x this property always holds. Why can we assume all inputs have the property? The idea is that you've already tested every special case you can think of and now wish to prove it for the general case.

Let's prove Z + a = a using the (+) definition:

(+) :: Number -> Number -> Number
defined x + y inductively x where
  defined x + y from x where
   defined Z + y = y
   defined (S x) + y = S (x + y)

Replace inputs with Z and a:

(+) :: Number -> Number -> Number
defined Z + a inductively Z where
  defined Z + a from Z where
   defined Z + a = a
   ....

Trivial proof. Let's try the other proof:

prove x + Z = x tested where
  prove x + Z = x inductively x where
    prove x + Z = x from x where
      given x = S x prove S x + Z = S x  <--we want to prove this

Replace the code via substitution with the input Sx + Z:

(+) :: Number -> Number -> Number
defined S x + Z inductively S x where
  defined S x + Z from S x where
   defined Z + Z = Z
   defined (S x) + Z = S (x + Z)  

In the proof we assumed x + Z = x with "prove x + Z = x inductively x" and can rewrite S(x + Z) to S(x). Proof is done: Sx + Z = Sx.

Next proof Sx + y + z = Sx + (y + z):

(+) :: Number -> Number -> Number
defined S x + (y + z) inductively x where
  defined S x + (y + z) from S x where
   defined Z + (y + z) = (y + z)
   defined (S x) + (y + z) = S (x + (y + z)

proven (x + y) + z = x + (y + z) tested where
  proven x + y + z = x + (y + z) inductively x where
    proven x + y + z = x + (y + z) from x where
      given x = S x proven S x + y + z = S x + (y + z) tested

We assumed inductively that x + y + z = x + (y + z):

(+) :: Number -> Number -> Number
defined S x + (y + z) inductively x where
  defined S x + (y + z) from S x where
   defined Z + (y + z) = (y + z)
   defined (S x) + (y + z) = S x + y + z

Watching lecture 2.

We don't have access to the homework but it's not needed. Pause the lecture before the prof starts filling out a definition of a function or a proof and try and figure it out yourself.

Try writing multiply before it's shown in the lecture. Multiplication is defined in math as repeated addition: 3 * 2 is two groups of 3 added or 3 groups of 2 added. Everytime your program looks at the input that is inductively defined to shrink to Z then add an entire copy of the other input.

You should be pressing tab often and having Ask fill out all the code for you. The multiplication definition:

(*) :: Number -> Number -> Number
defined a * b inductively b where
  defined a * b from b where
    defined a * Z = Z
    defined a * S x = a + (a * x)

Prove a * SZ = a. Ask does this for us but we can figure it out ourselves too:

(*) :: Number -> Number -> Number
defined a * S Z inductively b where
  defined a * S Z from S Z where
    defined a * Z = Z
    defined a * S Z = a + (a * Z) 

Reminder the x in SZ is Z. Here a + (a * Z) is returned a + (Z) and we already proved a + Z = a earlier. Proof is done: a * SZ = a.

Next prove SZ * b = b and replace all the inputs again:

(*) :: Number -> Number -> Number
defined SZ * b inductively b where
  defined SZ * b from b where
    defined SZ * Z = Z
    defined SZ * S x = SZ + (SZ * x)

The Ask proof inductively assumed SZ * b = b and we can rewrite:

(*) :: Number -> Number -> Number
defined SZ * b inductively b where
  defined SZ * b from b where
    defined SZ * Z = Z
    defined SZ * S x = SZ + x

SZ + x is really 1 + x making x into a successor or Sx. Proof is done: SZ * Sx = Sx.

Watching lecture 3

prove (a * b) * c = a * (b * c) inductively c where
  prove a * b * c = a * (b * c) from c where
    given c = S x prove a * b * S x = a * (b * S x) tested where
      prove a * b + a * b * x = a * (b + b * x) ?

Where did Ask come up with that? We should collect a list of everything proven so far because that is what Ask uses as well.

proven Z + b = b 
proven x + Z = x 
proven (x + y) + z = x + (y + z) 
proven a * (S Z) = a 
proven S Z * b = b
defined (S x) + y = S (x + y)
defined a * S x = a + (a * x)

Try (a * b) * S x as that is (a * b) * Sc:

(*) :: Number -> Number -> Number
defined a * b inductively S x where
  defined S x from S x where
    defined (a * b) * Z = Z
    defined (a * b) * S x = (a * b) + ((a * b) * x)

In our list of proofs we already defined a * Sx = a + (a * x) and if you squint (a * b) * S x is (value) * S x:

define (a * b) + ((a * b) * x) = (a * b) + ((a * b) * x)

Ask did something similar it just grouped them differently because it applied the distributive law turning ab + a(bx) into a(b + bx).

prove (a * b) * c = a * (b * c) inductively c where
  prove a * b * c = a * (b * c) from c where
    given c = S x prove a * b * S x = a * (b * S x) tested where
      prove a * b + a * b * x = a * (b + b * x)
       by Route(a * b + a * (b * x)) where
        proven a * b + a * b * x = a * b + a * (b * x)
         under (+)
        prove a * b + a * (b * x) = a * (b + b * x) ?

The inductive assumption abc = a(bc) was used here for route taking ab + abx and changing it to ab + a(bx). Sx is the successor of c and x is c letting us take advantage of the inductive assumption.

We can't directly prove x = z but we can prove x = y and y = z then x = z hence why this is called 'Route' we are taking a route indirectly. Once the tactic under + is used which we're told means to step each side and do comparison addition, one part of the route is finished. Proof is finished in the next lecture.

Watching lecture 4.

proven (a * b) + (a * c) = a * (b + c) inductively b where
  proven a * b + a * c = a * (b + c) from b where
    given b = S x proven a * S x + a * c = a * (S x + c) tested where
      proven a + a * x + a * c = a + a * (x + c)
       by Route (a + ((a * x) + (a * c))) where
        proven a + (a * x + a * c) = a + a * (x + c)
         under (+)

First notice b is the x. Ask asked us to prove a + ax + ac = a + a(x + c). The solution was to feed the entire left side into Route() but group with brackets the inductive hypothesis (a)b + (ac). The result of Route(a + ((ax) + (ac)) was a + (ax + ac) and now that can be compared with under(+) and when run ask finishes the proof. The insight was once again feed the inductive hypothesis into Route() with the extra terms outside the hypothesis brackets.

TODO

Lean uses an undecidable type theory so it's proof-checker (kernel) is incomplete meaning if you aren't experienced in Lean tactics to avoid these issues you could get blown out by Kurt Godel and think this is a software bug when it's incompleteness. It is popular because they were the only proof assistant to care about user experience you could get Lean running quickly in VSCode and start proving things immediately. The Mathlib is gigantic so whatever subject you are working in chances are there already exists verified theorems you can readily use from the library. That's of course assuming they aren't dumping AI slop directly into Mathlib and are hopefully keeping all that as seperate libraries but I have no idea honestly. It will work well enough for this book anyway.

VS Code

To install this course locally:

• install Lean which also has you install VS Code
• install git if needed
• in terminal type: git clone the book repo
• go into math2001 directory
• 'code .' to start from present directory

You should get a right panel in VS code called 'Lean Infoview' that displays the state of goals as you click around the source code.

Emacs

I had to run in the math2001 directory:

• lake exe cache get
  • it downloads 3972+ files

Install lean4-mode and Ctrl-c Ctrl-i opens the lean view in a new window showing goals.

Reading 1.1 Proving equalities from Mechanics of Proof. The .lean files to do these examples are in the Math2001 directory you cloned from github. The goal here is to make both sides equal at first with the right side finessed using algebra so it can be rewritten by the hypothesis a - b = 4 in the first example.

1.2.x Proving equalities in Lean make a proof skeleton first:

-- 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
  _ = 0 := _

The Lean docs suggest using underscore to keep the calc structure balanced while working on the proof that way we will get helpful error messages and not excessive red squiggles errors. That code declares 6 variables of type Int, h1 and h2 are assumptions/hypothesis, and we want to prove d(af - be) = 0. Calc is an environment like activating a mode.

-- 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 * e * b) := by ring -- reorder to match h1/h2
   _ = (b * c * f) - (c * f * b) := by rw [h1, h2] -- rewrite using h1/h2
   _ = 0 := by ring

I tried avoiding the reorder at first and skipping directly to rw but the pattern couldn't be detected by Lean unless I manually made it identical to the hypothesis.

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

Try the 1.3.11 exercises:

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

example {a b : ℤ} (h : a - b = 0) : a = b :=
  calc
  a = a - 0 := by ring
  _ = a - (a - b) := by rw [h]
  _ = b := by ring

example {x y : ℤ} (h1 : x - 3 * y = 5) (h2 : y = 3) : x = 14 :=
  calc
  x = x - (3 * y) + (3 * y) := by ring
  _ = 5 + (3 * 3) := by rw [h1, h2]
  _ = 14 := by ring

example {p q : ℚ} (h1 : p - 2 * q = 1) (h2 : q = -1) : p = -1 :=
  calc
  p = p - (2 * q) + (2 * q) := by ring
  _ = 1 + (2 * -1) := by rw [h1, h2]
  _ = -1 := by ring

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

example {p q : ℤ} (h1 : p + 4 * q = 1) (h2 : q - 1 = 2) : p = -11 :=
  calc
  p = p + 4 * q - 4 * (q - 1) - 4 := by ring
  _ = 1 - 4 * 2 - 4 := by rw [h1, h2]
  _ = -11 := by ring

example {a b c : ℝ} (h1 : a + 2 * b + 3 * c = 7) (h2 : b + 2 * c = 3)
  (h3 : c = 1) : a = 2 :=
  calc
  a = (a + 2 * b + 3 * c) - 2 * (b + 2 * c) + c  := by ring
  _ = 7 - 2 * 3 + 1 := by rw [h1, h2, h3]
  _ = 2 := by ring

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 {c : ℚ} (h1 : 4 * c + 1 = 3 * c - 2) : c = -3 :=
  calc
  c =  4 * c + 1 - 3 * c - 1 := by ring
  _ = 3 * c - 2 - 3 * c - 1 := by rw [h1]
  _ = -3 := 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

example {x y : ℤ} (h1 : 2 * x + y = 4) (h2 : x + y = 1) : x = 3 :=
  calc
  x = 2 * x + y - 1 * (x + y) := by ring
  _ = 4 - 1 * 1 := by rw [h1, h2]
  _ = 3 := by ring

example {a b : ℝ} (h1 : a + 2 * b = 4) (h2 : a - b = 1) : a = 2 :=
  calc
  a = (a + 2 * b + 2 * (a - b)) / 3 := by ring
  _ = (4 + 2 * 1)/3 := by rw [h1, h2] 
  _ = 6/3 := by ring
  _ = 2 := 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)^2 + (u + 1) - 1 := by ring -- must use brackets or rw fails
  _ = v^2 + v - 1 := by rw [h1] 

 -- use symbolab.com or similar site 
 -- this is directly from one of the examples in the book
example {t : ℚ} (ht : t ^ 2 - 4 = 0) :
    t ^ 4 + 3 * t ^ 3 - 3 * t ^ 2 - 2 * t - 2 = 10 * t + 2 :=
    calc
    t^4 + 3* t^3 - 3* t^2 - 2 * t - 2 =
    (t^2 + 3 * t + 1) * (t^2 - 4) + 10 * t + 2 := by ring
    _ = (t^2 + 3 * t + 1) * 0 + 10 * t + 2 := by rw [ht]
    _ = 10 * t + 2 := by ring

Exercise 15 I changed the hypothesis and this worked:

example {x y : ℝ} (h1 : x = 2) (h2 : y * x = 2 * x ) : y = 2 :=
 calc
  y = y * 2/2 := by ring 
  _ = y * x/x := by rw [h1]
  _ = (2 * x)/x := by rw [h2]
  _ = (2 * 2)/2 := by rw [h1]
  _ = 2 := by ring

Exercise 16 is of course impossible (no rational number exists that when squared is negative) but lean will let you prove it anyway using rewrites. If you want more exercises there's homework for this book/course in the git repository.

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
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
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 in the Index of Lean tactics as "extra checks an inequality whose two sides differ by the addition of a positive quantity".

-- Example 1.4.9
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 the 14.11 exercises:

example {x y : ℤ} (h1 : x + 3 ≥ 2 * y) (h2 : 1 ≤ y) : x ≥ -1 :=
  calc
  x = x + 3 - 3 := by ring
  _ ≥ 2 * y - 3 := by rel [h1]
  _ ≥ 2 * 1 - 3 := by rel [h2]
  _ ≥ -1 := by numbers 

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
  
example {n : ℤ} (h1 : n ≥ 5) : n ^ 2 - 2 * n + 3 > 14 :=
  calc
  n^2 - 2 * n + 3 =
  n * n - 2 * n + 3 := by ring
  _ ≥ 5 * n - 2 * n + 3 := by rel [h1]
  _ = 3 * n + 3 := by ring
  _ ≥ 3 * 5 + 3 := by rel [h1]
  _ > 14 := by numbers

example {x : ℚ} : x ^ 2 - 2 * x ≥ -1 :=
 calc
  x ^ 2 - (2 * x) ≥ x ^ 2 - (2  * x) := by extra
  _ = (x - 1)^2 - 1 := by ring
  _ ≥ -1 := by extra
  
example (a b : ℝ) (h1 : c < (a + b)/2) : a ^ 2 + b ^ 2 ≥ 2 * a * b :=
  calc
  a^2 + b^2 ≥ a^2 + b^2 := by extra
  _ = (a - b)^2 + (2 * a * b) := by ring
  _ ≥ (2 * a * b) := by extra

Read the next section on addarith, it's a purposely weakened version of linarith the usual mathlib tactic in Lean because linarith performs magic you don't even to tell it which hypotheses to use.

We finally learn what the infoview does besides telling us 'goals accomplished'. 2.1.5 example is a little hard to follow if you don't plug it into lean:

• a² = b² + 1 and a >= 1
• a² >= 1 by extra
  • recall extra is a tactic for inequalities when one side differs by a positive qty
• a² = 1² by ring because 1² is 1
• the cancel tactic
• a >= 1

The cancel tactic removes a common factor from both sides so x² = 2² will not cancel as lean doesn't know if 2 is divisible by x unless you already proved it has 2 for a factor. Of course x² = 0 works because 0 divided by anything is 0. Every number has 1 for a factor so x² = 1² will cancel. You can however force a cancel if you cast everything to inequalities by using an extra statement in the calc proof that x² >= 2² but the goal if it's an equality will be unfinished.

There's many times I have to put brackets around something for the rewriter to pick it up, tried to see if I could replicate the problem in VS Code on a laptop and same issue. Just have to be specific sometimes to the rewriter what you want. 2.1.7 example the hint was that Lean can infer from the have declarations that this quantity is positive and I interpret this as scope where the have declarations are outside calc:

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

2.1.8 example is similar:

example (a b : ℝ) (h : a ≤ b) : a ^ 3 ≤ b ^ 3 := by
  have h1 : 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
    _ ≤ b^3 := by extra

2.1.9 exercises took forever because of scope issues with the lean viewer it works like Python you have to be aware of white spacing/indents:

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

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

example (x y : ℚ) (h : x * y = 1) (h2 : x ≥ 1) : y ≤ 1 := by
 have h4 :=
 calc 
    x * y = x * y := by ring
    _ = 1 := by rw [h]
    _ > 0 := by extra
 cancel x at h4
 calc -- cancel kills the calc block have to start another
   1 = x * y := by rw [h] 
   _ ≥ 1 * y := by rel [h2]
   _ = y := by ring

Applying lemmas you look at the goals and that now drives the proof:

example {y : ℝ} : y ^ 2 + 1 ≠ 0 := by
  apply ne_of_gt
  calc
   y^2 + 1 = y^2 + 1 := by ring
   _  > 0 := by extra

/-! # Exercises -/

example {m : ℤ} (hm : m + 1 = 5) : 3 * m ≠ 6 := by
  apply ne_of_gt
  calc
  3 * m = 3 * m + 1 - 1 := by ring
  _ = 2 * m + (m + 1) - 1 := by ring
  _ = 2 * m + 5 - 1 := by rw [hm]
  _ = m + (m + 1) + 4 - 1 := by ring
  _ = m + 5 + 4 - 1 := by rw [hm]
  _ = (m + 1) + 4 + 4 - 1 := by ring
  _ = 5 + 4 + 4 - 1 := by rw [hm]
  _ > 6 := by numbers
 
example {s : ℚ} (h1 : 3 * s ≤ -6) (h2 : 2 * s ≥ -4) : s = -2 := by
  apply le_antisymm
  have h3 :=
   calc
    3 * s ≤ -6 := by rel [h1]
    _ = 3 * -2 := by ring
  cancel 3 at h3
  have h4 :=
   calc 
   2 * s ≥ -4 := by rel [h2]
   _ = 2 * -2 := by ring
  cancel 2 at h4