doodle

CSE 230: Principles of Programming Languages CSE 230

Resources - Assignments - Schedule - Grading - Policies

Summary

CSE 230 is an introduction to the Semantics of Programming Languages. Unlike most engineering artifacts, programming languages and hence, programs are mathematical objects whose properties can be formalized. The goal of CSE 230 is to to introduce you to the fundamental mental and mechanical tools required to rigorously analyze languages and programs and to expose you to recent developments in and applications of these techniques/

We shall study operational and axiomatic semantics, two different ways of precisely capturing the meaning of programs by characterizing their executions.

We will see how the lambda calculus can be used to distill essence of computation into a few powerful constructs.

We use that as a launching pad to study expressive type systems useful for for analyzing the behavior of programs at compile-time.

We will study all of the above in the context of lean, an interactive proof assistant that will help us precisely formalize and verify our intuitions about languages and their semantics.

Students will be evaluated on the basis of 4-6 programming (proving!) assignments, and a final exam.

Prerequisites

Basic functional programming e.g. as taught in UCSD CSE 130 using languages like Haskell, OCaml, Scala, Rust, and undergraduate level discrete mathematics, i.e. logic, sets, relations.

Basics

  • Lecture: WLH 2005 TuTh 12:30p-1:50p
  • Final Exam: 03/18/2025 Tu 11:30a-2:29p
  • Podcasts: podcast.ucsd.edu
  • Piazza: Piazza

Staff and Office Hours

  • Ranjit Jhala: Tu, Th 2-3p (3110)
  • Nico Lehmann: Th 3:30pm-5:00pm (Zoom), Fr 9:30am-11am (B240A), Zoom link in canvas
  • Naomi Smith: Tu 12pm-3pm (Zoom)
  • Matt Kolosick: Mo 10am-12pm (Zoom), Thursday 10am-11am (Zoom)
  • Mingyao Shen: We 12-1p (B240A)
  • Kyle Thompson: Mo 1-2p (B260A)

Please check the CANVAS calendar before you come in case there have been any changes.

Resources

The course is loosely based on Concrete Semantics but there is no official textbook; we will link to any relevant resources that may be needed to supplement the lecture material.

Some other useful links are:

Assignments

  1. Assignment X - Github/ID due 1/17
  2. Assignment 0 - Induction due 1/22

Schedule

The schedule below outlines topics, due dates, and links to assignments. The schedule of lecture topics might change slightly, but I post a general plan so you can know roughly where we are headed.

Week 1 - Basics and Induction

Week 2 - Expressions and Evidence

Week 3 - Big Step Semantics

  • Induction on Evidence (Ch04)
  • Imperative Programs: States, Commands, Transitions
  • Program Equivalence (Ch07)

Week 4 - Small Step Semantics

  • Preservation and Progress (Ch09)

Week 5, 6 - Axiomatic Semantics

  • Assertions, Floyd-Hoare Logic, Soundness (Ch12)
  • Verification Conditions and Automatic Verification

Week 7, 8 - Simply Typed Lambda Calculus

  • Terms, Types, and Typing Rules
  • Denotational Semantics and Type Soundness

Week 9, 10 - Automated Verification

  • Satisfiability Modulo Theories
  • Flux: Refinement Type based verification for Rust

Grading

Your grade will be calculated from assignments, exam, and participation

  • Participation Quizzes (15%) Most lectures will come with a 1-2 page handout, and you can submit the handout any time up until the start of the next lecture. Credit is given for reasonable effort in engaging with the material from the day on the handout.

  • Programming Assignments (40%) There will be a total of 5-6 programming assigments, to be done in pairs but submitted individually.

  • In Class Exams (45%) We will have three "in-class exams" Th 1/30 and Tu 2/25 and Th 3/13 each worth 15% of the grade.

Comprehensive Exam: For graduate students using this course for a comprehensive exam requirement, you must get "A" achievement on the exams.

Policies

All assignments are Closed collaboration assignments, where you cannot collaborate with others (except your partner). Of course you can ask questions on Piazza, and come to office hours etc. In particular,

  • You cannot look at or use anyone else's code for the assignment
  • You cannot discuss the assignment with other students
  • You cannot post publicly about the assignment on the course message board (or on social media or other forums). Of course, you can still post questions about material from lecture or past assignments!

You should be familiar with the UCSD guidelines on academic integrity as well.

Late Work

You have a total of six late days that you can use throughout the quarter, but no more than four late days per assignment.

  • A late day means anything between 1 second and 23 hours 59 minutes and 59 seconds past a deadline
  • If you submit past the late day limit, you get 0 points for that assignment
  • There is no penalty for submitting late but within the limit

Regrades

Mistakes occur in grading. Once grades are posted for an assignment, we will allow a short period for you to request a fix (announced along with grade release). If you don't make a request in the given period, the grade you were initially given is final.

Laptop/Device Policy in Lecture

There are lots of great reasons to have a laptop, tablet, or phone open during class. You might be taking notes, getting a photo of an important moment on the board, trying out a program that we're developing together, and so on. The main issue with screens and technology in the classroom isn't your own distraction (which is your responsibility to manage), it's the distraction of other students. Anyone sitting behind you cannot help but have your screen in their field of view. Having distracting content on your screen can really harm their learning experience.

With this in mind, the device policy for the course is that if you have a screen open, you either:

  • Have only content onscreen that's directly related to the current lecture.
  • Have unrelated content open and sit in one of the back two rows of the room to mitigate the effects on other students. I may remind you of this policy if I notice you not following it in class. Note that I really don't mind if you want to sit in the back and try to multi-task in various ways while participating in lecture (I may not recommend it, but it's your time!)

Diversity and Inclusion

We are committed to fostering a learning environment for this course that supports a diversity of thoughts, perspectives and experiences, and respects your identities (including race, ethnicity, heritage, gender, sex, class, sexuality, religion, ability, age, educational background, etc.). Our goal is to create a diverse and inclusive learning environment where all students feel comfortable and can thrive.

Our instructional staff will make a concerted effort to be welcoming and inclusive to the wide diversity of students in this course. If there is a way we can make you feel more included please let one of the course staff know, either in person, via email/discussion board, or even in a note under the door. Our learning about diverse perspectives and identities is an ongoing process, and we welcome your perspectives and input.

We also expect that you, as a student in this course, will honor and respect your classmates, abiding by the UCSD Principles of Community (https://ucsd.edu/about/principles.html). Please understand that others’ backgrounds, perspectives and experiences may be different than your own, and help us to build an environment where everyone is respected and feels comfortable.

If you experience any sort of harassment or discrimination, please contact the instructor as soon as possible. If you prefer to speak with someone outside of the course, please contact the Office of Prevention of Harassment and Discrimination: https://ophd.ucsd.edu/.

Assignments

Expressions, Types and Functions

This material is based on sections 1-3 of Functional Programming in Lean

Expressions

In lean, programs are built from expressions which (if well-typed) have a value.

ExpressionValue
1 + 23
3 * 412
1 + 2 * 3 + 411

Lean expressions are mathematical expressions as in Haskell, Ocaml, etc.

  • variables get a "bound" to a single value (no "re-assignment"),
  • expressions always evaluate to the same value ("no side effects")
  • if two expressions have the same value, then replacing one with the other will not cause the program to compute a different result.

To evaluate an expression, write #eval before it in your editor, and see the result by hovering over #eval.

#eval 1 + 2

#eval 3 * 4

#check 1 + 2 * 3 + 4

Types

Every lean expression has a type.

The type tells lean -- without evaluating the expression -- what kind of value it will produce.

Why do Programming Languages need types???

Lean has a very sophisticated type system that we will learn more about soon...

To see the type of an expression, write #check before it in your editor,

Primitive: Nat

Lean has a "primitive" type Nat for natural numbers (0, 1, 2, ...) that we saw in the expressions above.

#check 1      -- Nat (natural number i.e. 0, 1, 2,...)

#check 1 + 2  -- Nat

QUIZ What is the value of the following expression?

#eval (5 - 10 : Int)


/-

(A) 5                 0%
(B) 10                0%
(C) -5                30%
(D) 0                 5%
(E) None of the above 17%

-/

Type Annotations

Sometimes lean can infer the type automatically.

But sometimes we have to (or want to) give it an annotation.

Primitive: Int

#check (1 : Int)      -- Int (..., -2, -1, 0, 1, 2,...)

#check (1 + 2 : Int)  -- Int

QUIZ What is the value of the following expression?

#eval (5 - 10 : Int)

Primitive: Float

#check 1.1      -- Float

#eval 1.1 + 2.2

Primitive: Bool

#eval true
#check true   -- Bool

#eval false
#check false  -- Bool

#eval true  && true
#eval true  && false
#eval false && true
#eval false && false

#eval true  || true
#eval true  || false
#eval false || true
#eval false || false

-- #eval false + 10    -- type error!

Primitive: String

#eval "Hello, " ++ "world!"
#check "Hello, " ++ "world!"  -- String

-- #eval "Hello, " ++ 10   -- type error!

-- #eval "Hello, " ++ world   -- unknown identifier!

Definitions

We can name expressions using the def keyword.

def hello := "hello"
def world := "world"
def one := 1
def two := 2
def five_plus_ten   := 5 + 10
def five_minus_ten  := 5 - 10
def five_minus_ten' : Int := 5 - 10

You can now #check or #eval these definitions.

#check hello
#eval hello
#eval hello ++ world
#eval five_minus_ten
#eval five_minus_ten'

Functions

In lean, functions are also expressions, as in the λ-calculus.

#check (fun (n : Nat) => n + 1)         -- Nat -> Nat
#check (λ (n : Nat) => n + 1)           -- Nat -> Nat

#check (fun (x y : Nat) => x + y)       -- Nat -> (Nat -> Nat)
#check (λ (x y : Nat) => x + y)         -- Nat -> Nat -> Nat
#check (λ (x : Nat) => λ (y: Nat) => x + y)         -- Nat -> Nat -> Nat

QUIZ What is the type of the following expression?

Nat -> Nat -> Bool

#check (fun (x y : Nat) => x > y)

Function Calls

You can call a function by putting the arguments in front

#eval (fun x => x + 1) 10

#eval ((fun x y => x + y) 100) 200

/-
((fun x y => x + y) 100) 200
==
((λ x => (λ y => x + y)) 100) 200
==
(( (λ y => 100 + y))) 200
==
100 + 200
==
300
-/

QUIZ What is the value of the following expression?

#eval (fun x y => x > y) 10 20

Function Definitions

Of course, it is more convenient to name functions as well, using def since naming allows us to reuse the function in many places.

def inc := fun (x : Int)  => x + 1

def inc'(x: Int) := x + 1

#eval inc 10
#eval inc 20
-- #eval inc true  -- type error!

def add := fun (x y : Nat) => x + y
def add' (x y : Nat) := x + y

#eval add 10 20
#eval add' 10 20

It is often convenient to write the parameters of the function to the left

The below definitions of inc' and add' are equivalent to the above definitions of inc and add.

def inc'' (x : Int) : Int := x + 1

#eval inc'' 10     -- 11


def add'' (x y : Nat) : Nat := x + y

#eval add'' 10 20  -- 30

EXERCISE Write a function max that takes two Nats and returns the maximum of the two.

EXERCISE Write a function max3 that takes three Nats and uses max to compute the maximum of all three

EXERCISE Write a function joinStringsWith of type String -> String -> String -> String that creates a new string by placing its first argument between its second and third arguments.

def mymax (x y : Nat) := if x > y then x else y

def mymax3 (x y z : Nat) := mymax x (mymax y z)

#eval mymax 67 92

-- #eval joinStringsWith ", " "this" "that"  -- "this, that"
-- #check joinStringsWith ", " -- **QUIZ** What is the type of the expression on the left?

EXERCISE Write a function volume of type Nat -> Nat -> Nat -> Nat which computes the volume of a brick given height, width, and depth.

Datatypes and Recursion

This material is based on sections 5,6 of Functional Programming in Lean

Datatypes

So far, we saw some "primitive" or "built-in" types like Nat, Bool etc.

The "primitive" Bool type is actually defined as a datatype in the standard library:

The type has two constructors

  • Bool.false
  • Bool.true.

Which you can think of as "enum"-like constructors.

Like all (decent) modern languages, Lean lets you construct new kinds of datatypes. Let's redefine Bool locally, just to see how it's done.

namespace MyBool

inductive Bool : Type where
  | false : Bool
  | true  : Bool
  deriving Repr

#eval Bool.true

Pattern Matching

The constructors let us produce or build values of the datatype.

The only way to get a Bool is by using the Bool.true or Bool.false constructors.

In contrast, pattern-matching lets us consume or use the values of that datatype...

Lets write a function neg that takes a Bool and returns the opposite Bool, that is

  • when given Bool.true, neg should return Bool.false
  • when given Bool.false, neg should return Bool.true
def neg (b: Bool) :=
  match b with
  | Bool.true  => Bool.false
  | Bool.false => Bool.true

Lets test it to make sure the right thing is happening

#eval neg Bool.true
#eval neg Bool.false

Our first "theorem" ... let us prove that neg true is false by

  1. defining a variable neg_true_eq_false (you can call it whatever you like...)
  2. whose type is the proposition neg Bool.true = Bool.false we want to "prove"
  3. whose body is the proof of the proposition.

For now, lets just write by sorry for the "proof".

def neg_b_neq : ∀ (b:Bool), ¬ (neg b = b) := by
  intros b
  cases b <;> simp [neg]

def neg_neg_b_eq : ∀ (b:Bool), neg (neg b) = b := by
  intros b
  cases b <;> simp [neg]

def neg_true_eq_false : neg Bool.true = Bool.false := by
  rfl

foo <;> bar

Goals

How shall we write the proof?

Well, you can see the goal by

  1. putting the cursor next to the by (before sorry)
  2. looking at the Lean Infoview on the right in vscode

Viewing the Goal

A goal always looks like h1, h2, h3, ... ⊢ g where

  • h1, h2, h3 etc. are hypotheses i.e. what we have, and
  • <g> is the goal i.e. what we want to prove.

In this case, the hypotheses are empty and the goal is neg Bool.true = Bool.false.

Tactics

Proofs can be difficult to write (in this case, not so much).

Fortunately, lean will help us build up the proof by

  • giving us the goal that
  • we can gradually simplify, split ...
  • till we get simple enough sub-goals that it can solve automatically.

TACTIC rfl: The most basic tactic is rfl which abbreviates reflexivity, which is a fancy way of saying "evaluate the lhs and rhs and check if they are equal".

EXERCISE: Write down and "prove" the theorem that neg false is true.

EXERCISE What other "facts" can you think up (and prove!) about neg?

Next, lets try to prove a fact about how neg behaves on all Bool values. For example, lets try to prove that when we neg a Bool value b two times we get back b.

def neg_neg : ∀ (b: Bool), neg (neg b) = b := by
  sorry

This time we cannot just use rfl -- try it and see what happens!

In its own way, lean is saying "I can't tell you (evaluate) what neg b is because I don't know what b is!"

TACTIC intros: First, we want to use the intros tactic which will "move" the ∀ (b: Bool) from the goal into a plain b : Bool hypothesis. That is, the intros tactic will change the goal from ∀ (b: Bool), neg (neg b) = b to b : Bool ⊢ neg (neg b) = b, meaning that our task is now to prove that neg (neg b) = b assuming that b is some Bool valued thing.

Of course, we still cannot use rfl because lean does not know what neg b until b itself has some concrete value.

TACTIC cases: The path forward in this case is to use the cases tactic which does a case analysis on b, i.e. tells lean to split cases on each of the possible values of b --- when it is true and when it is false. Now, when you put your cursor next to cases b you see the two subgoals

  • case false which is ⊢ neg (neg Bool.false) = Bool.false
  • case true which is ⊢ neg (neg Bool.true) = Bool.true

Each case (subgoal) can be proved by rfl so you can complete the proof as

def neg_neg_1 : ∀ (b : Bool), neg (neg b) = b := by
  intros b
  cases b
  rfl
  rfl

However, I prefer to make the different subgoals more "explicit" by writing

def neg_neg_2 : ∀ (b : Bool), neg (neg b) = b := by
  intros b
  cases b
  . case false => rfl
  . case true => rfl

Conjunction Lets write an and function that

  • takes two Bools and
  • returns a Bool that is true if both are true and false otherwise.
def and (b1 b2: Bool) : Bool :=
  match b1, b2 with
  | Bool.true, Bool.true => Bool.true
  | _        , _         => Bool.false

and is Commutative Lets try to prove that and is commutative, i.e. and b1 b2 = and b2 b1. You can start off with intros and then use cases as before, but we may have to do case analysis on both the inputs!

theorem and_comm : ∀ (b1 b2 : Bool), and b1 b2 = and b2 b1 := by
  sorry

TACTIC COMBINATOR <;>: It is a bit tedious to repeat the same sub-proof so many times! The foo <;> bar tactic combinator lets you chain tactics together so by first applying foo and then applying bar to each sub-goal generated by foo. We can use <;> to considerably simplify the proof. In the proof below, move your mouse over the cases b1 <;> cases b2 <;> ... line and see how the goals change in the Lean Infoview panel.

theorem and_comm' : ∀ (b1 b2 : Bool), and b1 b2 = and b2 b1 := by
  -- use the <;> tactic combinator
  sorry

Disjunction Lets write an or function that

  • takes two Bools and
  • returns a Bool that is true if either is true and false otherwise.
def or (b1 b2: Bool) : Bool := sorry

EXERCISE Complete the proof of the theorem that or is commutative, i.e. or produces the same result no matter the order of the arguments.

theorem or_comm : ∀ (b1 b2 : Bool), or b1 b2 = or b2 b1 := by
  sorry

end MyBool

Recursion

Bool is a rather simple type that has just two elements --- true and false.

Pretty much all proofs about Bool can be done by splitting cases on the relevant Bool values and then running rfl (i.e. via a giant "case analysis").

Next, lets look at a more interesting type, which has an infinite number of values.

namespace MyNat

inductive Nat where
  | zero : Nat
  | succ : Nat -> Nat
  deriving Repr

open Nat

Zero, One, Two, Three, ... infinity

Unlike Bool there are infinitely many Nat values.

def n0 : Nat :=                  zero
def n1 : Nat :=             succ zero
def n2 : Nat :=       succ (succ zero)
def n3 : Nat := succ (succ (succ zero))

This has two related consequences.

First, we cannot write interesting functions over Nat just by brute-force enumerating the inputs and outputs as we did with and and or; instead we will have to use recursion.

Second, we cannot write interesting proofs over Nat just by brute-force case-splitting over the values as we did with and_comm and or_comm; instead we will have to use induction.

Addition

Lets write a function to add two Nat values.

def add (n m: Nat) : Nat :=
  match n with
  | zero => m
  | succ n' => succ (add n' m)

example : add n1 n2 = n3 := by rfl

Adding Zero

Next, lets try to prove some simple facts about add for example

theorem add_zero_left : ∀ (n: Nat), add zero n = n := by
  intros
  rfl

The proof of add_zero_left is super easy because it is literally (part of) the definition of add which tells lean that it obeys two equations

add zero      m = m
add (succ n') m = succ (add n' m)

So the rfl applies the first equation and boom we're done.

Adding Zero on the Right

However, lets see what happens if we flip the order of the arguments, so that the second argument is zero

theorem add_zero' : ∀ (n: Nat), add n zero = n := by
  intros n
  sorry

Boo! Now the proof fails because the equation does not apply!

"Calculation" or "Equational Reasoning"

In fact, lets us try to see why the theorem is even true, slowly working our way up the Nat numbers.

  add zero  zero
    { by def of add }
    ===> zero                     ... (0)

  add (succ zero) zero
    { by def of add }
    ===> succ (add zero zero)
    { by (0) }
    ===> succ zero                ... (1)

  add (succ (succ (zero))) zero
    { by def }
    ===> succ (add (succ zero) zero)
    { by (1) }
    ===> succ (succ zero)         ... (2)

  add (succ (succ (succ (zero)))) zero
    { by def }
    ===> succ (add (succ (succ zero)) zero)
    { by (2) }
    ===> succ (succ (succ zero))  ... (3)

calc mode

lean has a neat calc mode that lets us write the above proofs (except, they are actually checked!)

theorem add_0 : add zero zero = zero := by
  calc
    add zero zero = zero := by simp [add] -- just apply the

theorem add_1 : add (succ zero) zero = succ zero := by
  calc
    add (succ zero) zero
      = succ (add zero zero) := by simp [add]
    _ = succ zero            := by simp [add_0]

theorem add_2 : add (succ (succ zero)) zero = succ (succ zero) := by
  calc
    add (succ (succ zero)) zero
      = succ (add (succ zero) zero) := by simp [add]
    _ = succ (succ zero)            := by simp [add_1]

theorem add_3 : add (succ (succ (succ zero))) zero = succ (succ (succ zero)) := by
  calc
    add (succ (succ (succ zero))) zero
      = succ (add (succ (succ zero)) zero) := by simp [add]
    _ = succ (succ (succ zero))            := by simp [add_2]

Proof by Induction

Notice that each of the proofs above is basically the same:

To prove the fact add_{n+1} we

  1. apply the definition of add and then
  2. recursively use the fact add_{n}!

Recursion

Lets us define add for each Nat by reusing the definitions on smaller numbers

Induction

Lets us prove add_n for each Nat by reusing the proofs on smaller numbers

theorem add_zero : ∀ (n: Nat), add n zero = n := by
  intros n
  induction n
  . case zero       => simp [add]
  . case succ n' ih => simp [add, ih]

end MyNat

Polymorphism

lean also lets you define polymorphic types and functions.

For example, here is the definition of a List type that can hold any kind of value

namespace MyList

inductive List (α : Type) where
  | nil : List α
  | cons : α -> List α -> List α
  deriving Repr

open List

def this_is_a_list := cons 0 (cons 1 (cons 2 nil))

List constructors

Just like Nat has a

  • "base-case" constructor (zero) and
  • "inductive-case" constructor (succ)

A List α also has two constructors:

  • "base-case" constructor (nil) and
  • "inductive-case" constructor (cons)

NOTE: You can type the α by typing a \ + a

So we can create different types of lists, e.g.

def list0123 : List Int := cons 0 (cons 1 (cons 2 (cons 3 nil)))
def list3210 : List Int := cons 3 (cons 2 (cons 1 (cons 0 nil)))
def listtftf : List Bool := cons true (cons false (cons true (cons false nil)))

Appending Lists

Lets write a small function to append or concatenate two lists

To do so, we match on the cases of the first list xs

  • If xs is nil then the result is just the second list
  • If xs is of the form cons x xs' then we recursively app xs' ys and cons x in front
def app {α : Type} (xs ys: List α) : List α :=
  match xs with
  | nil => ys
  | cons x xs' => cons x (app xs' ys)

Just like with add the above definition tells lean that app satisfies two equations

  1. ∀ ys, app nil ys = ys
  2. ∀ x xs' ys, app (cons x xs') ys = cons x (app xs' ys)
example : app                 nil   (cons 2 (cons 3 nil)) =                 cons 2 (cons 3 nil)   := by rfl
example : app         (cons 1 nil)  (cons 2 (cons 3 nil)) =         cons 1 (cons 2 (cons 3 nil))  := by rfl
example : app (cons 0 (cons 1 nil)) (cons 2 (cons 3 nil)) = cons 0 (cons 1 (cons 2 (cons 3 nil))) := by rfl








Digression: Implicit vs Explicit Parameters

The α -- representing the Type of the list elements -- is itself a parameter for the app function.

  • The {..} tells lean that it is an implicit parameter vs
  • The (..) we usually use for explicit parameters

An implicit parameter, written {...} is a parameter that lean tries to automatically infer at call-sites, based on the context, for example

def add (n : Nat) (m : Nat) : Nat := n + m
#eval add 3 4  -- Must provide both arguments: 7

An explicit parameter, written (...) is the usual kind where you have to provide at call-sites, for example

def singleton {α : Type} (x: α) : List α := cons x nil
#eval singleton 3








Induction on Lists

app is sort of like add but for lists. For example, it is straightforward to prove "by definition" that

theorem app_nil_left: ∀ {α : Type} (xs: List α), app nil xs = xs := by
  intros
  rfl

However, just like add_zero we need to use induction to prove that

theorem app_nil : ∀ {α : Type} (xs: List α), app xs nil = xs := by
  sorry

Because in the cons x xs' case, we require the fact that app_nil holds for the smaller tail xs', i.e that app xs' nil = xs', which the induction tactic will give us as the hypothesis that we can use.

Associativity of Lists

theorem app_assoc : ∀ {α : Type} (xs ys zs: List α), app (app xs ys) zs = app xs (app ys zs) := by
  sorry

end MyList

set_option pp.fieldNotation false

Datatypes and Recursion

This material is based on

namespace MyNat

inductive Nat where
  | zero : Nat
  | succ : Nat -> Nat
  deriving Repr

open Nat

def add (n m : Nat) : Nat :=
  match n with
  | zero => m
  | succ n' => succ (add n' m)

Trick 1: Helper Lemmas

Example add_comm

Let's try to prove that add is commutative; that is, that the order of arguments does not matter.

If we plunge into trying a direct proof-by-induction, we get stuck at two places.

  1. What is the value of add m zero ?
  2. What is the value of add m (succ n) ?

It will be convenient to have helper lemmas that tell us that

  1. ∀ m, add m zero = m
  2. ∀ n m, add n (succ m) = succ (add n m)
theorem add_comm : ∀ (n m: Nat), add n m = add m n := by
  intros n m
  induction n
  sorry

end MyNat

open List

Example rev_rev

Lets look at another example where we will need helper lemmas.

Appending lists

def app {α : Type} (xs ys: List α) : List α :=
  match xs with
  | [] => ys
  | x::xs' => x :: app xs' ys

/-
app [] [3,4,5] = [3,4,5]

app (2::[]) [3,4,5] = [3,4,5]
==>
2 :: [3,4,5]
==>
[2,3,4,5]
-/

example : app [] [3,4,5] = [3,4,5] := rfl
example : app [0,1,2] [3,4,5] = [0,1,2,3,4,5] := rfl

Reversing lists

def rev {α : Type} (xs: List α) : List α :=
 match xs with
  | [] => []
  | x :: xs' => app (rev xs') [x]

example : rev [] = ([] : List Int) := rfl
example : rev [3] = [3] := rfl
example : rev [2,3] = [3,2] := rfl
example : rev [0,1,2,3] = [3,2,1,0] := rfl
example : rev (rev [0,1,2,3]) = [0,1,2,3] := rfl

rev [0,1,2,3] => rev (0 :: [1,2,3]) => app (rev [1,2,3]) [0] => app [3,2,1] [0] => [3,2,1,0]

Now, lets prove that the above was not a fluke: if you reverse a list twice then you get back the original list.

theorem rev_app : ∀ {α : Type} (xs ys : List α),
  rev (app xs ys) = app (rev ys) (rev xs) := by
    sorry

/-
rev (app xs ys) == app (rev ys) (rev xs)
rev (app [x1,x2,x3,...xn] [y1...ym])
== rev [x1...xn, y1...ym]
== [ym ... y1, xn ... x1]
== app [ym ... y1] [xn ... x1]
== app (rev ys) (rev xs)

-- |- rev (app (rev xs') [x]) = x :: xs'
      ==>
      app (rev [x]) (rev (rev xs'))
-/

theorem rev_rev : ∀ {α : Type} (xs: List α), rev (rev xs) = xs := by
  intros α xs
  induction xs
  . case nil =>
    rfl
  . case cons x xs' ih =>
    simp [rev, rev_app, app, ih]

Yikes. We're stuck again. What helper lemmas could we need?

Trick 2: Generalizing the Variables

Consider the below variant of add.

How is it different than the original?

open MyNat.Nat

def itadd (n m: MyNat.Nat) : MyNat.Nat :=
  match n with
  | zero => m
  | succ n' => itadd n' (succ m)

/-
  itadd (s s s z) (s s s s s z)
  =>
  itadd (s s z) (s s s s s s z)
  =>
  itadd (s z) (s s s s s s s z)
  =>
  itadd (z) (s s s s s s s s z)
  =>
  (s s s s s s s s z)
-/


example : itadd (succ (succ zero)) (succ zero) = succ (succ (succ zero)):= by rfl

Lets try to prove that itadd is equivalent to add.

add n' (succ m) == succ (add n' m)

theorem add_succ : ∀ (n m), MyNat.add n (succ m) = succ (MyNat.add n m) := by
 sorry

theorem itadd_eq : ∀ (n m), itadd n m = MyNat.add n m := by
  intros n
  induction n
  . case zero => simp [itadd, MyNat.add]
  . case succ n' ih =>
    simp [MyNat.add, itadd, add_succ, ih]

Ugh! Why does the proof fail???

We are left with the goal

m n' : MyNat.Nat
ih : itadd n' m = MyNat.add n' m
⊢ itadd n' (succ m) = succ (MyNat.add n' m)

IH is too weak

In the goal above, the ih only talks about itadd n m but says nothing about itadd n (succ m). In fact, the IH should be true for all values of m as we do not really care about m in this theorem. That is, we want to tell lean that the ih should be

m n' : MyNat.Nat
ih : ∀ m, itadd n' m = MyNat.add n' m
⊢ itadd n' (succ m) = succ (MyNat.add n' m)

Generalizing We can do so, by using the induction n generalizing m which tells lean that

  • we are doing induction on n and
  • we don't care about the value of m

Now, go and see what the ih looks like in the case succ ...

This time we can actually use the ih and so the proof works.

theorem add_succ : ∀ (n m), MyNat.add n (succ m) = succ (MyNat.add n m) := by
 sorry

theorem itadd_eq' : ∀ (n m: MyNat.Nat), itadd n m = MyNat.add n m := by
  intros n m
  induction n generalizing m
  case zero => simp [MyNat.add, itadd]
  case succ => simp [MyNat.add, MyNat.add_succ, itadd, *]

Trick 3: Generalizing the Induction Hypothesis

Often, the thing you want to prove is not "inductive" by itself. Meaning, that you want to prove a goal ∀n. P(n) but in fact you need to prove something stronger like ∀n. P(n) /\ Q(n) or even ∀n m, Q(n, m) which then implies your goal.

Example: Tail-Recursive sum

sum 3 => 3 + sum 2 => 3 + 2 + sum 1 => 3 + 2 + 1 + sum 0 => 3 + 2 + 1 + 0

def sum (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | n' + 1 => n + sum n'

def loop (n res : Nat) : Nat :=
  match n with
  | 0      => res
  | n' + 1 => loop n' (res + n)

def sum_tr (n: Nat) := loop n 0

-- loop (n' + 1) 0 == sum (n' + 1)
-- loop a 0  == sum a
-- loop n res  == (sum n) + res

theorem loop_sum : ∀ n res, loop n res = (sum n) + res := by
  intros n res
  induction n generalizing res
  . case zero =>
    simp [loop, sum]
  . case succ n' ih =>
    simp_arith [loop, sum, ih]

theorem sum_eq_sum_tr : ∀ n, sum_tr n = sum n := by
  simp [sum_tr, loop_sum]




/-

fn sum(mut n: Nat) -> Nat {
  let mut res = 0
  while let S n' = n {
    res = res + n;
    n   = n';
  }
  res
}
-/

Tail-Recursively Summing

In an iterative language you might write a loop to sum the numbers n + n-1 + ... + 0 e.g.

#![allow(unused)]
fn main() {
fn sum_tr(mut n: Nat) {
  let mut acc = 0;
  while let succ m = n {
    acc += n;
    n = m
  }
  return acc
}
}

We can write the above with tail-recursion

  • The recursive call is the "last thing" the function does
  • That is, the recursive result is returned without any further computation

NOTE: Go and look at itadd; is it tail recursive?

-- def sum_tr (n acc : Nat) : Nat :=
--   match n with
--   | 0 => acc
--   | n' + 1 => sum_tr n' (n + acc)

-- def sum' (n: Nat) := sum_tr n 0

Lets try to prove that sum and sum' always compute the same result.

theorem sum_eq_sum' : ∀ n, sum n = sum' n := by
  intros n
  induction n
  sorry

Oops, we are stuck.

We need to know something about sum_tr n' (n' + 1) but what?

Can you think of a suitable helper lemma, which would let us directly prove sum_eq_sum'?

theorem helper: ∀ n acc, sum_tr n acc = sum n + acc := by ...

theorem sum_eq_sum' : ∀ n, sum' n = sum n := by
  intros
  simp_arith [sum', helper]

open List

Example: Tail-Recursive sum_list

Summing a List*

def sum_list (xs : List Nat) : Nat :=
  match xs with
  | [] => 0
  | x ::xs' => x + sum_list xs'

Tail-Recursively Summing a List*

In an iterative language you might write a loop to sum the elements of a list, e.g.

#![allow(unused)]
fn main() {
fn sum_list(xs: List<Nat>) {
  let mut acc = 0;
  while let cons x ys = xs {
    acc += x;
    xs = ys
  }
  return acc
}
}

We can write the above with tail-recursion (where the recursive call is the "last thing") that the function does. (Hint: Go and look at itadd; is it tail recursive?)

def sum_list_tr (xs : List Nat) (acc : Nat): Nat :=
  match xs with
  | [] => acc
  | x :: ys => sum_list_tr ys (acc + x)

def sum_list' (xs: List Nat) := sum_list_tr xs 0

Can you figure out a suitable helper lemma that would let us complete the proof of sum_list_eq_sum_list' below?

theorem sum_list'_eq : ∀ (xs acc), sum_list_tr xs acc = sum_list xs + acc := by
  sorry

theorem sum_list_eq_sum_list' : ∀ xs, sum_list' xs = sum_list xs := by
  intros xs
  simp_arith [sum_list', sum_list'_eq]

Example: Tail-Recursive Reverse

rev_tr [0,1,2,3] => loop [0,1,2,3] [] => loop [1,2,3] [0] => loop [2,3] [1, 0] => loop [3] [2, 1, 0] => loop [] [3, 2, 1, 0] => [3,2,1,0]

def rev_tr {α : Type} (xs res: List α) : List α :=
  match xs with
  | [] => res
  | x ::xs' => rev_tr xs' (x :: res)

def rev' (xs: List α) := rev_tr xs []

example : rev' [0,1,2,3] = [3,2,1,0] := by rfl

Can you figure out a suitable helper lemma rev_tr_app that would let us complete the proof of rev_eq_rev' below?

rev_tr xs [] == rev xs

rev_tr xs res == [xn, ...x3, x2,x1, 99] == rev xs ++ res

theorem app_nil : ∀ {α : Type} (xs: List α), app xs [] = xs := by
  sorry

theorem rev_tr_helper_theorem : ∀ {α : Type} (xs res : List α),
  rev_tr xs res = app (rev xs) res := by sorry

theorem rev_eq_rev' : ∀ {α : Type} (xs: List α), rev' xs = rev xs := by
  intros α xs
  simp [rev', rev_tr_helper_theorem, app_nil]

Example: Tail-Recursive Evaluator

Arithmetic Expressions

inductive Aexp : Type where
  | const : Nat -> Aexp
  | plus  : Aexp -> Aexp -> Aexp
  deriving Repr

open Aexp

def two_plus_three := plus (const 2) (const 3)

    alice_plus
    /          \
   bob_const   bob_const
   |            |
   2            3

Evaluating Expressions

def eval (e: Aexp) : Nat :=
  match e with
  | const n => n
  | plus e1 e2 => eval e1 + eval e2

#eval eval two_plus_three

def eval_acc (e: Aexp) (res: Nat) : Nat :=
  match e with
  | const n => n + res
  | plus e1 e2 => eval_acc e2 (eval_acc e1 res)

def eval' (e: Aexp) := eval_acc e 0

example : eval' two_plus_three = eval two_plus_three := by rfl

QUIZ: Is eval_acc tail recursive?

Lets try to prove that eval' and eval are "equivalent".

Can you figure out a suitable helper lemma that would let us complete the proof of eval_eq_eval'?

theorem eval'_eq_eval : ∀ e, eval e = eval' e := by
  intros
  simp [eval', eval_acc_eq]

Trick 4: Functional Induction

Based on Joachim Breitner's notes on Functional Induction

def len (xs: List α) : Nat :=
  match xs with
  | [] => 0
  | _::xs' => 1 + len xs'

def alt (xs ys : List α) : List α :=
  match xs, ys with
  | [], ys => ys
  | xs, [] => xs
  | x::xs, y::ys => x :: y :: alt xs ys

#eval alt [1,2,3,4] [10,20,30]

First, lets try a "brute force" proof.

theorem alt_len : ∀ {α : Type} (xs ys : List α), len (alt xs ys) = len xs + len ys := by
  sorry

Instead, it can be easier to do the same induction as mirrors the recursion in alt

theorem alt_len' : ∀ {α : Type} (xs ys : List α), len (alt xs ys) = len xs + len ys := by
  intros α xs ys
  induction xs, ys using alt.induct
  . case case1 => simp [alt, len]
  . case case2 => simp [alt, len]
  . case case3 => simp_arith [alt, len, *]

Stack Machines