Adventures in Type Theory 2 — Coming in Clutch

Published: 2025-08-25

Part of the Adventures in Type Theory series

So, this entry in Adventures in Type Theory has decidedly less type theory, but not none. That is because my freshly installed clutch has decided to give in; it turns out that it was installed incorrectly.

Riding with a slipping clutch is painful, and so we’ll be spending the next day or two here in Alsace while we await repairs at Seedz Motorsport, who have been absolutely wonderful in helping me get back on the road! Until then, hopefully, we’ll have time to do a bit more type theory.

Without further ado, here’s the story so far!

Initialization

Location: L’Emanuella, Isbergues (50.61313, 2.45165)

Time: 2025-08-24T11:49+2

I woke up, and the hosts treated me to a wonderful breakfast.

Then I headed to the supermarket to buy some toothpaste and a toothbrush; I tried to buy gas too, but my (Starling) debit card was not accepted, and they use those auto-pumps here which need you to insert a card before they dispense. I left my other cards at l’Emmanuella.

I see problems on my horizon…

Narrator: there were problems on the horizon

It was time for a little change of pace: we needed to:

• Sit down and figure out what our next stop is on the way to Termini Imerese
• Get some progress in on our TOPLAS paper’s revisions.

There were two primary options for travel:

• Make for Dijon, and cross the Alps the next day
• Make for Milan, and demonstrate the will of an iron donkey by travelling 1000 kilometers in a day

The latter wouldn’t leave much time for type theory… but I wanted to spend more time in Italy, rather than travelling. And all the hotels in the middle ground, namely Switzerland, were painfully expensive.

So, the impulse took hold of me, and I spent the next hour preparing for the long haul to Milan.

• I bought an e-vignette for riding through Switzerland. The official site was surprisingly hard to find through search!
• I made an ill-fated reservation at the Idea Hotel Milano San Siro

Allocating 3 hours time for rest, and pushing the Gladius to the limit, we could make it by 1 AM. So be it.

I put it off with a bit of research — like staring at a heavy barbell you don’t want to lift.

I’m regretting having taken so much time to get started; if I had started right away, we could have made it by 11!

Alright. This will be !!FUN!!, in the Dwarf Fortress sense.

2025-08-24T12:57+2. Forth and onwards!

The Path to Milan

We’re off to a good start. In the exceedingly brief age of the Z650, that liminal space between defeats, a good friend of mine and fellow category theorist implored me to get a windshield, complaining of the windblast from the naked bike.

I responded with, essentially, do u even lift, bro?.

Well, look who has egg on their face now. Well, insects, actually. I’m sure they carry eggs.

We’re off to a roaring start, and I’m getting a real core workout fighting the windblast. I try various positions, and find that sitting upright I need to either use my arms or engage my core and legs, whereas leaning forwards is more in the legs and head.

The strength of the blast is highly nonlinear, so it’s quite relaxing when I’m behind cars just cruising, but becomes a serious exertion when speeding past in the fast lane, so much so that I occasionally stop in the slow lane for a rest. I didn’t realize how bad it was before, because it’s my first really long trip on the Gladius, and I tend to go slower on UK roads. Every bit counts!

I stop for gas and a snack. My credit cards, which are on my phone, are not accepted by the gas pump (but work inside for food!). My other debit card is. After a slight delay, I ride off, but quickly notice, elas ¹, my clutch is slipping once more. The free play at the clutch lever has disappeared, so I pull over to the side of the highway and adjust it once more.

The ride carries on, we get some more gas, and… it’s slipping again! Again, the free play is mostly gone, so we adjust further… There are also nice windmills on the side of the road.

The ride carries on. Clutch is holding just fine. I test it a few times, and even on 6th gear lugging it, the RPM is directly proportional to the speed.

I get some more gas. Can you guess what happened? Yeah.

So I’m stopped at the toll gate, and begin trying to figure out what’s wrong. There’s no more room to adjust at the handlebar. I take off the sprocket cover to take a look at the arm, with the help of my trusty mechanic, ChatGPT, who hopes that it’s just the cable being worn.

During this kerfuffle, I drop the bike. The bike is fine, but the left mirror takes a hit and needs to be straightened, and, more irritatingly, my only power bank breaks. Up to this point, I was riding with the cable coming out of my jacket pocket, which surprisingly can handle the high speeds, since my navigation phone has limited battery capacity.

A friendly biker on a Z900 stops by, and we take a look together. The arm is resting firmly on the stop. It seems that, once more, my freshly installed clutch is cooked.

So.

We continue the ride eastwards, now with a slipping clutch. We’re limited to about 110 km/h, usually below 100, before the clutch stops biting. Stop and get some gas, spend a bit too long resting.

The scenery is beautiful, though, and I wish I had brought a GoPro. Low RPM, low throttle, high gear, lower on slopes, which get more common as we head further east. I gaze upon the great works of man, 5% and 6% grades carved up and down the rolling hills.

At Kekastel, around 10 PM, I stop for gas and decide to call it a night at hotelF1 Saverne Monswiller.

About 35 kilometers left.

Is my bike… dabbing?

The cold begins to set in.

At one point, the road split into two levels, and it looked quite striking at night. I could only find a Google Streetview image taken during the day:

None of these roads are, individually, bona fide megaprojects, and yet, I am always awestruck at the immense labor it must have required to build these structures in totality. There is something larger-than-life, cyclopean, about highways, sized as they are for cars rather than men.

They carved hills as hunters carve beast-flesh. Wild Men think they ate stone for food. They went through Druádan to Rimmon with great wains. They go no longer.

— Ghân-buri-Ghân, The Return of the King

And yet we are on those roads. We are those people.

I see the stars come out.

But I digress.

We arrive. The room is spare, but standard.

I debate writing this post, but hypersleep beckons.

I quickly check my bank balance, on both cards. The second is… almost empty.

Huh?

Turns out each gas station was reserving up to 500 € to pump gas. And I pumped gas often, for safety, and to take a rest from the road, sometimes as little as 4 liters at a time.

Let’s hope they let go of that quickly, as otherwise, we will need to look for gas stations with attendants, which seem rare out here. Like I said, Problems™.

(EDIT: one hold was removed by around 2025-08-25T15:30+2; the others, so far, remain)

Repair in Sarreguemines

Location: hotelF1 Saverne Monswiller (48.75137, 7.38435)

Time: 2025-08-25T10:30+2

I sleep through my alarms, and achieve consciousness at 10:30 AM, 30 minutes before checkout time. I put on some electronic metal to time myself, and get out just in time, having double-checked that I didn’t leave anything behind.

I get downstairs, and call around to see where I can get my bike repaired. Lots of bad luck, little in the way of English speakers. While I am nominally fluent in French, this is one fun way to practice my motorcycle jargon, especially since just yesterday I learned that “my clutch is slipping” is translated “mon embrayage patine.” I just typed in “engage.” As I was saying.

Even more fun was calling shops down in Milan, who primarily spoke Italian. I got in touch with one guy who spoke English, after much Google-translate-fu, over at Japanmoto Milano, who was very helpful. He could probably get me a new Suzuki clutch. But would I want to brave the Alps that day, and get the clutch repaired tomorrow, pre-ordering it? That’s what would be necessary to make the schedule.

At this point, I had called a local garage, I believe it was Magic Racing, which was very nice, but couldn’t help me because they didn’t do road bikes. Thankfully, they called Seedz Motorsport for me, who later called me back, on my UK number no less, as my French phone had run out of battery.

They can fix the clutch, worst case by the day after tomorrow morning (2025-08-27), best case tomorrow evening (2025-08-26).

So.

Naturally, I book the ferry from Genoa to Palermo departing 2025-08-28T22:45+2. As I’m booking, I catch sight of an… interesting… advertisement.

We ride to Seedz, arriving just as they open at 2025-08-25T14:00+2, and they take a quick look. The staff is extremely nice, and let me watch as they open up the sprocket cover. Lots of cool bikes around, too, in various states of disassembly.

Seems the clutch cable is fine, which means they have to open the clutch itself. But later, as they have another bike scheduled. I go get a coffee and a croissant at the nearby patisserie, and start writing.

I finally get a bit of work in on my TOPLAS revisions: I start removing effect annotations from contexts, to simplify the narrative. During the ride, I had some inspiration about how to do SSA in locally nameless style. Excited to start experimenting with that.

I head back to the shop, and the clutch is indeed cooked. I had just gotten a new one installed at Cambridge Motorcycles, and apparently, it was done incorrectly, with the plates in the wrong order and the springs far too soft. An oil line was also disconnected, and half the coolant was missing. So that’s why there was that misting of oil on the engine case. No bueno.

Thankfully, they can get the parts in, hopefully even by tomorrow, as planned, and we can ride off. Until then, I guess we can walk and enjoy the wonderful scenery.

I book accommodation at Alternative Hôtel Proche Sarreguemines, which I walk to, and the room is beautiful.

They’ve even got this nice intro to the hotel, along with a little guide to the local area!

It’s really great. It’s amazing what happens when people care.

I then walk to go get some food. And some more coffee. The river ever calls my kind, and I find myself at Kebab Le Bosphore, writing this up.

And since I’m here and I’ve eaten, let’s start on that locally nameless SSA, then.

Locally Nameless SSA

We begin by setting up our new repository. There’s no Internet here at Le Bosphore, and I want another snack, so, we’ll copy ln-stlc to profit from our already-installed Mathlib:

# In the same directory as ln-stlc, recursively copy its contents into a new directory ln-ssa
cp -r ln-stlc ln-ssa
# Open the new directory
cd ln-ssa
# Rename files
mv LnStlc LnSSA
mv LnStlc.lean LnSSA.lean

Now we just edit the lakefile.toml…

# <snip>

# defaultTargets = ["LnStlc"] -- replace this
defaultTargets = ["LnSSA"]

# <snip>

[[lean_lib]]
# name = "LnStlc" -- replace this
name = "LnSSA" # with this

And replace the contents of LnSSA.lean with

import LnSSA.Basic

and…

lake build

I hope the Lean offline experience improves soon. And that we cache dependencies to save disk space… but I digress.

Alright, we’ve now got a copy of the ln-stlc project. Let’s do a little refactor…

mkdir LnSSA/Expr
mv LnSSA/Basic.lean LnSSA/Expr/Syntax.lean

and in LnSSA.lean

import LnSSA.Expr.Syntax

Let’s comment out Ctx.Deriv and Ctx.Deriv.lc for now. We’ll move the corrected version to another file later.

Recall that our types for STLC were given by

/-- Simple types -/
inductive Ty : Type
/-- The unit type. -/
| unit
/-- A function type `A → B`. -/
| arr (A B : Ty)
/-- A product type `A × B`. -/
| prod (A B : Ty)

Let’s change these to our types for SSA, ignoring base types for now:

/-- Simple types -/
inductive Ty : Type
/-- The unit type. -/
| unit
/-- The empty type. -/
| empty
/-- A product type `A × B`. -/
| prod (A B : Ty)
/-- A coproduct type `A + B`. -/
| coprod (A B : Ty)

So far so good. Now let’s change our set of terms to be the set of SSA terms, again, ignoring operations for now:

/-- Untyped SSA expressions -/
inductive Tm : Type
/-- A named free variable. -/
| fv (x : String)
/-- A bound variable, represented using a de Bruijn index. -/
| bv (i : ℕ)
/-- A unary let-binding -/
| let₁ (p e : Tm)
/-- The unique value of the unit type. -/
| null
/-- A pair `(a, b)`. -/
| pair (lhs rhs : Tm)
/-- A binary let-binding -/
| let₂ (p e : Tm)
/-- A left injection -/
| inl (e : Tm)
/-- A right injection -/
| inr (e : Tm)
/-- A case expression -/
| case (e l r : Tm)

Note that in SSA we use binary let-bindings, rather than projections.

Our definitions for fvs, bvi, wkUnder, and substUnder are now marked as invalid. Let’s start with fixing fvs:

def Tm.fvs : Tm → Finset String
| .fv x => {x}
| .bv _ => ∅
| .null => ∅
| .let₁ p e => fvs p ∪ fvs e
| .pair lhs rhs => fvs lhs ∪ fvs rhs
| .let₂ p e => fvs p ∪ fvs e
| .inl e => fvs e
| .inr e => fvs e
| .case e l r => fvs e ∪ fvs l ∪ fvs r

For bvi, we need to handle the fact that a binary let-binding binds two variables, rather than one. This is straightforward:

def Tm.bvi : Tm → ℕ
| .fv _ => 0
| .bv i => i + 1
| .let₁ _ e => bvi e - 1
| .null => 0
| .pair lhs rhs => bvi lhs ⊔ bvi rhs
| .let₂ _ e => bvi e - 2
| .inl e => bvi e
| .inr e => bvi e
| .case e l r => bvi e ⊔ (bvi l - 1) ⊔ (bvi r - 1)

And likewise for wkUnder and substUnder:

def Tm.wkUnder (n : ℕ) : Tm → Tm
| .fv x => .fv x
| .bv i => if i < n then .bv i else .bv (i + 1)
| .let₁ p e => .let₁ (wkUnder n p) (wkUnder (n + 1) e)
| .null => .null
| .pair lhs rhs => .pair (wkUnder n lhs) (wkUnder n rhs)
| .let₂ p e => .let₂ (wkUnder n p) (wkUnder (n + 2) e)
| .inl e => .inl (wkUnder n e)
| .inr e => .inr (wkUnder n e)
| .case e l r => .case (wkUnder n e) (wkUnder (n + 1) l) (wkUnder (n + 1) r)

prefix:70 "↑₀" => Tm.wkUnder 0

I was expecting the automation to work as-is for everything else, but it turns out, it fails in the case-case. Factoring it out fixes things:

theorem Tm.bvi_le_substUnder_var (n : ℕ) (x : String) (b : Tm)
  : bvi b ≤ (n + 1) ⊔ (bvi (substUnder n x b) + 1)
  := by induction b generalizing n with
  | case => sorry
  | _ => grind [bvi, substUnder, wkUnder]

-- snip

theorem Tm.bvi_substUnder_var_le (n : ℕ) (x : String) (b : Tm)
  : bvi (substUnder n x b) ≤ n ⊔ (bvi b - 1)
  := by induction b generalizing n with
  | case => sorry
  | _ => grind [bvi, substUnder, wkUnder]

But why? Let’s do some detective work. Alright, this works²:

theorem Tm.bvi_le_substUnder_var (n : ℕ) (x : String) (b : Tm)
  : bvi b ≤ (n + 1) ⊔ (bvi (substUnder n x b) + 1)
  := by induction b generalizing n with
  | case =>
    simp only [bvi, substUnder, wkUnder]
    simp only [Nat.max_assoc, Nat.add_max_add_right, sup_le_iff, Nat.sub_le_iff_le_add]
    grind
  | _ => grind [bvi, substUnder, wkUnder]

and…

-- DOES NOT COMPILE
theorem Tm.bvi_le_substUnder_var (n : ℕ) (x : String) (b : Tm)
  : bvi b ≤ (n + 1) ⊔ (bvi (substUnder n x b) + 1)
  := by induction b generalizing n with
  | _ =>
    simp only [bvi, substUnder, wkUnder]
    simp only [Nat.max_assoc, Nat.add_max_add_right, sup_le_iff, Nat.sub_le_iff_le_add]
    grind

No, the bv case fails…

theorem Tm.bvi_le_substUnder_var (n : ℕ) (x : String) (b : Tm)
  : bvi b ≤ (n + 1) ⊔ (bvi (substUnder n x b) + 1)
  := by induction b generalizing n with
  | _ =>
    simp only [bvi, substUnder, wkUnder]
    simp only [Nat.max_assoc, Nat.add_max_add_right, sup_le_iff, Nat.sub_le_iff_le_add]
    grind [bvi]

Cool and good!

-- DOES NOT COMPILE
theorem Tm.bvi_substUnder_var_le (n : ℕ) (x : String) (b : Tm)
  : bvi (substUnder n x b) ≤ n ⊔ (bvi b - 1)
  := by induction b generalizing n with
  | _ =>
    simp only [bvi, substUnder, wkUnder]
    simp only [Nat.max_assoc, Nat.add_max_add_right, sup_le_iff, Nat.sub_le_iff_le_add]
    grind [bvi]

Nope. Worth a try… While we’re at it, let’s clean up the other one

theorem Tm.bvi_le_substUnder_var (n : ℕ) (x : String) (b : Tm)
  : bvi b ≤ (n + 1) ⊔ (bvi (substUnder n x b) + 1)
  := by induction b generalizing n with
  | _ =>
    simp only [
      bvi, substUnder, wkUnder, Nat.max_assoc, Nat.add_max_add_right, sup_le_iff,
      Nat.sub_le_iff_le_add
    ]
    grind [bvi]

Alright…

-- DOES NOT COMPILE
theorem Tm.bvi_substUnder_var_le (n : ℕ) (x : String) (b : Tm)
  : bvi (substUnder n x b) ≤ n ⊔ (bvi b - 1)
  := by induction b generalizing n with
  | case =>
    simp [bvi, substUnder, wkUnder]
    simp at *
    grind
  | _ => stop grind [bvi, substUnder, wkUnder]

Nope. Hmm… I see lots of trash - 1 + 1 in the goal state… and we have the classic lemma (opens mathlib docs, furiously search for sub_add_something)

theorem Nat.sub_add_eq_max (a b : Nat) :
  a - b + b = max a b

and

-- DOES NOT COMPILE
theorem Tm.bvi_substUnder_var_le (n : ℕ) (x : String) (b : Tm)
  : bvi (substUnder n x b) ≤ n ⊔ (bvi b - 1)
  := by induction b generalizing n with
  | case =>
    simp [bvi, substUnder, wkUnder, Nat.sub_add_eq_max]
    simp at *
    grind
  | _ => stop grind [bvi, substUnder, wkUnder]

Nope. It is doing something, though. Let’s try rewriting with le_max_iff… ah, it doesn’t work because we have something of the form trash ≤ (max trash trash) - 1. So let’s pull that minus sign in, using

theorem Nat.sub_max_sub_right (a b c : Nat) :
  max (a - c) (b - c) = max a b - c

yielding

-- DOES NOT COMPILE
theorem Tm.bvi_substUnder_var_le (n : ℕ) (x : String) (b : Tm)
  : bvi (substUnder n x b) ≤ n ⊔ (bvi b - 1)
  := by induction b generalizing n with
  | case =>
    simp [bvi, substUnder, wkUnder, Nat.sub_add_eq_max, <-Nat.sub_max_sub_right, le_max_iff]
    simp at *
    grind
  | _ => stop grind [bvi, substUnder, wkUnder]

Huh. And yet.

theorem Tm.bvi_substUnder_var_le (n : ℕ) (x : String) (b : Tm)
  : bvi (substUnder n x b) ≤ n ⊔ (bvi b - 1)
  := by induction b generalizing n with
  | case =>
    simp [bvi, substUnder, wkUnder, Nat.sub_add_eq_max]
    rw [<-Nat.sub_max_sub_right, le_max_iff]
    simp at *
    grind
  | _ => grind [bvi, substUnder, wkUnder]

Alright, time for a little golf…

-- DOES NOT COMPILE
theorem Tm.bvi_substUnder_var_le (n : ℕ) (x : String) (b : Tm)
  : bvi (substUnder n x b) ≤ n ⊔ (bvi b - 1)
  := by induction b generalizing n with
  | _ =>
    simp [bvi, substUnder, wkUnder, Nat.sub_add_eq_max]
    repeat rw [<-Nat.sub_max_sub_right, le_max_iff]
    try simp only [le_sup_iff] at *
    grind

says “No goals to be solved” because the first simp discharges them, so…

-- DOES NOT COMPILE
theorem Tm.bvi_substUnder_var_le (n : ℕ) (x : String) (b : Tm)
  : bvi (substUnder n x b) ≤ n ⊔ (bvi b - 1)
  := by induction b generalizing n with
  | _ =>
    simp [bvi, substUnder, wkUnder, Nat.sub_add_eq_max] <;> {
      repeat rw [<-Nat.sub_max_sub_right, le_max_iff]
      try simp only [le_sup_iff] at *
      grind
    }

fails the bvi case, so

theorem Tm.bvi_substUnder_var_le (n : ℕ) (x : String) (b : Tm)
  : bvi (substUnder n x b) ≤ n ⊔ (bvi b - 1)
  := by induction b generalizing n with
  | _ =>
    simp [bvi, substUnder, wkUnder, Nat.sub_add_eq_max] <;> {
      repeat rw [<-Nat.sub_max_sub_right, le_max_iff]
      try simp only [le_sup_iff] at *
      grind [bvi]
    }

works.

Alright, I’m tired now! Until next time!

Ah right, let’s fix the git repository! Back in ln-ssa now,

# remove old git data for ln-stlc
rm -rf .git
# new git repo
git init
# set origin
git remote add origin git@github.com:imbrem/ln-ssa.git
# initial commit
git add .
git commit -am "Initial commit"

Right, need to edit the README.md… and…

git commit --amend

Make the new repo and set up GitHub by:

• In Settings/Actions/General, check Allow GitHub Actions to create and approve pull requests
• In Settings/Pages, set Source to GitHub Actions And finally

git push -u origin main

Alright, until next time!