Sorry about the explosion surrounding my implementation of a simple reverse function in class. Working with theorem provers can be humbling as undoubtedly you are discovering.
The problem was quite subtle. Will discovered the issue after he and I poked around a bit after class. Here is the definition we were working with:
Fixpoint rev (T:Type) (l:list T) : list T :=
match l with
| nil _ => nil T
| (cons _ h t) => (app T (rev T t) (cons T h (nil T)))
end.
Other than the wildcards for type variables, this definition should make pretty good sense to you. It did when I was working with it, but I could not get it to type check much less execute.
As Will discovered, the problem is not in the definition of rev but un the
definition of app. nil and cons are both defined by our new definition of
polymorphic lists. rev is the function under consideration. We’ve written
a version of app previously that is still in scope. However, that app was
written before our polymorphic list definition in Lists.v. When we tried to
use it in the definition of rev, of course it did not type check. If type
checking had thrown an error that app did not exist we would have caught it
immediately.
I’m happy to go through this in class if anyone is interested in seeing it, but
if you simply write a polymorphic version of app before the polymorphic
version of rev, everything works perfectly.
I’ve posted the interpreter from yesterday’s class at AE with a few updates. First, I’ve renamed expDenote to
eval. No functionality changes or changes to proofs, I just think
that eval is clearer. Second, I fixed the first proof we attempted
to use auto. We’ve not covered that in class yet, but will in the
next couple of days.
Following is a source listing for convenience.
From Stdlib Require Bool Arith List.
From Stdlib Require Lia.
Set Implicit Arguments.
Module AE.
(** Simple abstract syntax for an expression language, [exp], with a
constant value constructed with [Num] and binary operations [Plus] and
[Mult].
*)
Inductive exp : Type :=
| Num : nat -> exp
| Plus : exp -> exp -> exp
| Mult : exp -> exp -> exp.
Check exp_ind.
Check (Num 3).
Check (Plus (Num 2) (Num 3)).
Check (Mult (Num 2) (Num 3)).
(** Recursive function that evaluates an [exp] to a [nat]. [Num n] evaluates
to [n]. [Plus e1 e2] evaluates to the operation [plus] applied
to the evaluation of [e1] and [e2].
*)
Fixpoint eval (e:exp) : nat :=
match e with
| Num n => n
| Plus e1 e2 => (plus (eval e1) (eval e2))
| Mult e1 e2 => (mult (eval e1) (eval e2))
end.
(** An experiment to show [eval] working as an interpreter *)
Compute eval (Mult (Plus (Num 2) (Num 4)) (Num 5)).
Check eval (Mult (Plus (Num 2) (Num 4)) (Num 5)).
(* 5*(2+4) *)
(** A theorem over addition of natural numbers *)
Theorem ex0: forall x, (eval (Plus (Num x) (Num 4))) >= 4.
Proof.
simpl. induction x.
- simpl. auto.
- simpl. auto.
Qed.
(* * Verifying a simple optimization that replaces [0+x] with [x]. In [expOpt]
we replace [0+x] by [x] using pattern matching and leave everything else
alone. *)
Fixpoint expOpt (e:exp) : exp :=
match e with
| Num n => Num n
| Plus (Num 0) e2 => (expOpt e2)
| Plus e1 e2 => (Plus (expOpt e1) (expOpt e2))
| Mult e1 e2 => (Mult (expOpt e1) (expOpt e2))
end.
(* * The correctness theorem simply says that evaluating an expression has the
same value as evaluating its optimization. Note that in the proof we're only
using commands learned so far. Heavy use of induction hypotheses and a nested
[destruct] structure the verification. *)
Theorem optimize_correct: forall e,
(eval e) = ((eval (expOpt e))).
Proof.
intros e. induction e.
- reflexivity.
- simpl. rewrite IHe1. rewrite IHe2. destruct e1.
destruct n.
+ reflexivity.
+ reflexivity.
+ reflexivity.
+ reflexivity.
- simpl. rewrite <- IHe1. rewrite <- IHe2. reflexivity.
Qed.
End AE.
If you are using the links to Rocq source files embedded in the class
schedule, please download Induction.v and InductionTest.v
again. Will pointed out after class that I did not update links
embedded in the schedule to point to the 2025 version of the
book. Some of your submissions for Basics.v used old versions of the
file. Not to worry, we will figure this out. However, please download
a new version of Induction.v and InductionTest.v if you used links
on the schedule. Differences are minor, so it should not cost you any
time.
If you are using files downloaded directly from the Software Foundations website, you already have the correct versions and do not need to download again.
Let’s Face It by The Mighty Mighty Bosstones
The Mighty Mighty Bosstones’ 1997 masterpiece Let’s Face It represents the absolute peak of third-wave ska’s mainstream crossover potential. This album took the Boston band’s distinctive “skacore” sound—a ferocious blend of ska, punk, and hardcore—and refined it into something both accessible and uncompromising.
Built around the massive hit “The Impression That I Get,” the album showcases the Bosstones at their most confident and cohesive. Dicky Barrett’s gravelly vocals and Tim Burton’s tie-wearing stage presence became iconic, while the band’s eight-piece lineup created a wall of sound that was simultaneously raucous and tight. The rhythm section locked into ska’s characteristic upstroke with punk’s driving intensity, while the horn section added layers of melody and chaos.
Beyond the radio-friendly opener, tracks like “The Rascal King” and “Nevermind Me” demonstrate the band’s range, moving from political commentary to personal introspection without losing their essential energy. “Royal Oil” and “Break So Easily” showcase their ability to slow things down without sacrificing emotional impact, while “Numbered Days” brings back the full-throttle assault that made them legends in the underground.
The album’s production, handled by Paul Q. Kolderie and Sean Slade, captures the band’s live energy while giving each instrument room to breathe. The result feels like being in the middle of a sweaty ska pit while still being able to appreciate the sophisticated songcraft underneath the mayhem.
Let’s Face It went platinum and helped define an era, but more importantly, it stands as a testament to a band that never compromised their vision even as they conquered the mainstream.
Listen to Let’s Face It on Tidal
Donald Fagen’s 1982 solo debut The Nightfly stands as one of the most sophisticated and immaculately crafted albums of the early 1980s. Coming off the dissolution of Steely Dan, Fagen channeled his obsession with jazz harmony, pristine production, and wry social commentary into a deeply personal yet universally resonant work.
The album functions as both nostalgic reverie and sharp-eyed critique, with Fagen drawing on memories of late-night radio, Cold War paranoia, and the optimistic futurism of the early 1960s. From the opening title track’s smooth groove to the closing melancholy of “The Goodbye Look,” every song showcases Fagen’s gift for wrapping complex emotions in deceptively accessible melodies.
Standout tracks like “I.G.Y.” (International Geophysical Year) and “New Frontier” perfectly capture the album’s central tension between technological promise and human frailty. Fagen’s vocals, delivered with his characteristic detached cool, float over arrangements that are both lush and precise, featuring contributions from jazz luminaries like Chuck Rainey and Jeff “Skunk” Baxter.
The production, handled by Fagen with Gary Katz, remains a high-water mark for early digital recording techniques. Every instrument sits perfectly in the mix, creating a sonic landscape that feels both intimate and expansive.
The Nightfly endures not just as a technical achievement, but as a meditation on American dreams deferred and the bittersweet passage of time.
Listen to The Nightfly on Tidal
Aja represents Steely Dan at their absolute peak—a masterclass in studio perfectionism that elevated the craft of record-making to high art. Released in 1977, Donald Fagen and Walter Becker’s sixth album stands as perhaps the most sonically immaculate recording of the rock era.
The album’s seven tracks unfold like a series of meticulously arranged vignettes, each one a testament to the duo’s obsessive attention to detail. The title track alone features some of the most sophisticated jazz-rock fusion ever recorded, with Chuck Rainey’s bass work and Steve Gadd’s drumming providing the foundation for layers of pristine instrumentation.
“Peg” became their biggest hit, built around a groove so infectious it masks the underlying harmonic complexity. Meanwhile, “Deacon Blues” serves as perhaps their greatest achievement—a wry meditation on romantic failure wrapped in lush orchestration and punctuated by Pete Christlieb’s unforgettable saxophone solo.
What sets Aja apart isn’t just the technical excellence, but how Fagen and Becker’s cynical worldview finds perfect expression in the album’s polished surfaces. These aren’t songs about transcendence or rebellion, but about the quiet compromises and small defeats of middle-class American life, delivered with wit so sharp it cuts.
The production, handled by Gary Katz, remains a benchmark for clarity and depth. Every element sits perfectly in the mix, from the intricate guitar work to the sophisticated vocal arrangements. It’s music for audiophiles that never sacrifices emotional content for sonic perfection.
Aja endures because it captures something essential about American sophistication—beautiful, knowing, and slightly hollow at its core.
The over-arching recommendation I have for a clean and quick Rocq install is:
opam installed (and properly initialized), just run opam install coq.9.0.0opam support for Windows natively is very new and relatively buggy. You might find yourself up against cases of “sorry you just can’t do that on Windows with opam currently”wsl
Navigate to some folder you care about putting the Rocq code in:
cd ~/Rocq/2025/lf # navigate to folder
code . # Launches vscode
From there, make sure you have the right Rocq extension installed (see below)
Use VSCode… alternatives exist, but they are not well-supported or have hardly any features.
In particular, I use the coq-lsp vscode extension.
Others also have great success with vsrocq.
Both will involve you using opam to install a language server. Thus, the importance of using opam.
Try searching online, it might be a common issue with a fix. Otherwise, come to office hours.
The first week of classes is underway! Here are a few important updates and reminders:
Make sure you have Coq (now called Rocq) installed and working. You can use:
The first homework assignment covering Basics.v and BasicsTest.v is
tentatively assigned Monday, August 25th. Remember:
Basics.v file through CanvasDon’t forget that office hours are MW 2:50-4:00 in 3048 Eaton Hall, or by appointment. Please don’t hesitate to come by if you’re having trouble with the proof system or course concepts.
Good luck with your first week!
In fact a proven truth, to be precise, is not a truth at all - it’s just the sum of proofs. ~Joseph Brodsky, Homage to Yalta
Welcome to the course website!
Here you’ll find all the resources you need to stay up to date and successfully navigate this semester — from lecture notes and homework assignments to announcements and helpful links.
Please check back frequently for updates, and don’t hesitate to reach out if you have any questions. We’re looking forward to a great semester together!