CS 242: Final: Theorem Proving

Due: Friday, December 14 at 6:30pm
No late submissions!

In this course, I have presented you with very much a programmer’s view of programming languages. That is, understanding the value of theoretical computational constructs through the lens of practical application to the kinds of problems you’ll encounter in every-day programming tasks.

However, the origins of PL theory came much more so from the domain of math and logic. Alonzo Church, inventor of the lambda calculus, was a logician (computer science did not exist in his time). Some of the earliest applications of computing hardware were directed towards solving logic problems, like the Logic Theorist from 1950. Since then, the field of automated theorem proving has only grown in scope and substance. Today, we have dozens of tools and programming languages dedicated to automated creation or verification of mathematical proofs, such as Coq, Isabelle, and Lean.

For your take-home final, your task is to learn the basics of using the Lean theorem prover to prove simple logic theorems. A key part of this assignment is its lack of instruction—the goals will be well-defined, but it is up to you to learn as much or as little as you need in order to accomplish them. Theorem provers are complex beasts, and you will definitely not fully understand them after this final. However, the hope is that the knowledge you have gained from this course will make you more productive in a setting of self-directed learning that involves concepts from PL theory.

Lean

For this final, we have chosen to use the Lean theorem prover, primarily because it has a great tutorial, and I found it pretty usable in practice. You should follow their instructions to download Lean. We strongly recommend using their web editor or another supported editor.

To complete the tasks below, you will need a subset of the concepts in chapters 1-4 and 7 of the tutorial (linked above). We have drawn several of the tasks from the tutorial’s recommended exercises, and they do not require reading everything before completion. The chapter dependencies are marked approrpiately in the source code. As you read the tutorial, there is a fair amount that you will probably find confusing. And that’s fine! Self-directed learning is about maximizing productivity while in a state of semi-understanding. If you are struggling with the theorems provided, try implementing simpler ones to work your way up.

Theorems

In final/proofs.lean (make sure to git pull), we have provided you an unambiguous specification of several theorems which you need to prove. For grading, we have grouped the theorems below into sets of increasing difficulty that are sufficient to get certain grade levels, e.g. minimum work gets you a C, next step is a B, and so on.

Commutativity of AND (17.5%): $P \wedge Q \iff Q \wedge P$
```
theorem and_commutativity : p ∧ q ↔ q ∧ p
```
De Morgan’s law (17.5%): $\neg(P \vee Q) \iff \neg P \wedge \neg Q$
```
theorem demorgans_law : ¬(p ∨ q) ↔ ¬p ∧ ¬q
```
Contraposition (17.5%): $(P \implies Q) \implies (\neg Q \implies \neg P)$
```
theorem contraposition : (p → q) → (¬q → ¬p)
```
Distributivity of AND over forall (17.5%): $(\forall x. P(x) \wedge Q(x)) \iff (\forall x. P(x)) \wedge (\forall x. Q(x))$
```
theorem and_forall_dist : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x)
```
Full points up to here will get you a 70.
Equivalence of foralls with unbound propositions (5%): $(\forall x. P(x) \vee R) \iff (\forall x. P(x)) \vee R$ .
```
theorem unbound_prop : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r
```
Barber paradox (5%): The barber is the “one who shaves all those, and those only, who do not shave themselves.” The question is, does the barber shave himself? $\neg(\forall x : \text{men}~.~\text{shaves}(\text{barber}, x) \iff \neg\text{shaves}(x, x))$
```
theorem barber_paradox : ¬ (∀ x : men, shaves barber x ↔ ¬ shaves x x)
```
Full points up to here will get you an 80.
Inverse of for all (5%): $\forall x. P(x) \iff \neg(\exists x.\neg P(x))$
```
theorem forall_inverse : (∀ x, p x) ↔ ¬ (∃ x, ¬ p x)
```
Logarithm multiplication law (5%): $\forall x : \mathbb{R}. \forall y : \mathbb{R}. \log(x*y) = \log~x + \log~y$
```
theorem log_mul {x y : real} (hx : x > 0) (hy : y > 0) :
  log (x * y) = log x + log y
```
Note that we have provided you a custom definition of real, log, exp, and the set of logarithmic properties needed to prove the multiplication theorem.

Full points up to here will get you a 90.

For the final task, we have translated the simply typed lambda calculus into Lean using inductive types (see tutorial chapter 7). For example, an expression is:

inductive Expr
| Nat : ℕ → Expr
| Add : Expr → Expr → Expr
| Lam : Typ → Expr → Expr
| App : Expr -> Expr -> Expr
| Var : ℕ → Expr

We have defined the typing rules as a series of variable declaration. For example:

def ProofContext := list Typ

variable has_type : ProofContext → Expr → Typ → Prop

variable t_add : ∀ (gamma : ProofContext), ∀ (e1 : Expr), ∀ (e2 : Expr),
  (has_type gamma e1 Typ.Nat) ∧ (has_type gamma e2 Typ.Nat) →
    has_type gamma (Expr.Add e1 e2) Typ.Nat

Your goal is to provide a typing derivation for two expressions (5% each):

def e : Expr := (Expr.Add (Expr.Nat 3) (Expr.Nat 2))
theorem e1_type : has_type [] e Typ.Nat := ...

def e2 : Expr := Expr.Lam Typ.Nat (Expr.Var 0)
theorem e2_type : has_type [] e2 (Typ.Fun Typ.Nat Typ.Nat) := ...

Each proof currently says sorry, which is a placeholder for a proof not yet finished. You should remove the sorry and fill in each proof. Once the proof type-checks, and as no warnings or sorrys, it’s a valid proof and you’re good to go.

Note on grading: this final is intended to be difficult to get a perfect score (it is a final, after all). That said, the final is only 18% of your grade, and most of you do not need a 100 to get an A. To understand how well you need to do, we have provided a script grading.py which you can run to see your current grade, and the minimum needed grade on the final.

$ pip3 install requests beautifulsoup4
$ python3 grading.py
Stanford email: stephchen@stanford.edu
Stanford password:
How many guest lectures did you attend? 3
Grade for Assignment 1: 100.00
Grade for Assignment 2: 93.28
Grade for Assignment 3: 100.00
Grade for Assignment 4: 100.00
Grade for Assignment 5: 98.5
Grade for Assignment 6: 100.00
Grade for Assignment 7: 100.00
Grade for Assignment 8: 90.00
If you got a 70 on the final, your final grade would be 92.49.
If you got a 80 on the final, your final grade would be 94.29.
If you got a 90 on the final, your final grade would be 96.59.
If you got a 100 on the final, your final grade would be 98.39.

Note that the email and password are just passed into a temporary https beautifulsoup session so we can scrape your grades from Gradescope automatically.

Resources

Although this is a final, we will still provide you with (limited) resources to get help as you learn to use Lean. First and foremost, you are allowed to work in groups of two. You must each still submit your solution, alhtough it can be the same file. Clearly mark in a comment at the top of proofs.lean the names of both contributors.

We will also keep Piazza open and host office hours. However, these resources are exclusively for general Lean questions. We will not be providing assistance with any questions/debugging/etc. directly related to the theorems on the final.

Submitting

Create a submission zip by running ./make_submission.sh. Upload submission.zip to Gradescope.

Sections

Lean

Theorems

Resources

Submitting