the ergonomics of

PL metatheory in Lean

7 June 2024

the ergonomics of

PL metatheory in Lean

or: I couldn’t convince people to use Agda for metatheory

but maybe I can convince you to try out Lean instead

this talk is about:

this talk is not about:

• tooling and editor support
• language features designed to take advantage of support
• demonstrating this with a real PL metatheory codebase

• how to do metatheory in Lean
• Lean’s type theory
• (okay maybe a little at the end. but I promise no typing rules)

3

Coq and Lean are:

• interactive proof assistants
• based on dependent types (proofs are terms)
• with automation via tactics

4

my issues with Coq

• P1: proof reading is missing ephemeral information
• P2: term writing isn’t incremental
• P3: proof editing is sequential
• P4: information for learning isn’t well integrated

specifically using:

• Coq-LSP
• also applies to VSCoq 1/CoqIDE
• (I don’t use emacs so idk Proof General)

5

P1: proof reading is missing ephemeral information

• Q1: what changes did this tactic make?
• in tac1; tac2, what changes did tac1 make?
• Q2: what is the type of this subexpression?
• what is the context of this subexpression?
• Q3: what case is this subproof for?

6

P1: proof reading is missing ephemeral information

• Q1: what changes did this tactic make?
• in tac1; tac2, what changes did tac1 make?
• Q2: what is the type of this subexpression?
• what is the context of this subexpression?
• Q3: what case is this subproof for?

7

P1: proof reading is missing ephemeral information

• Q1: what changes did this tactic make?
• in tac1; tac2, what changes did tac1 make?
• Q2: what is the type of this subexpression?
• what is the context of this subexpression?
• Q3: what case is this subproof for?

8

P2: term writing isn’t incremental

• Q1: how do I fill in this term later?
• Q2: how do I fill in this term with tactics?
• if I don’t know the exact tactic I need?
• if I need multiple tactics/generate subgoals?

9

P2: term writing isn’t incremental

• Q1: how do I fill in this term later?
• Q2: how do I fill in this term with tactics?
• if I don’t know the exact tactic I need?
• if I need multiple tactics/generate subgoals?

10

P2: term writing isn’t incremental

• Q1: how do I fill in this term later?
• Q2: how do I fill in this term with tactics?
• if I don’t know the exact tactic I need?
• if I need multiple tactics/generate subgoals?

11

P2: term writing isn’t incremental

• Q1: how do I fill in this term later?
• Q2: how do I fill in this term with tactics?
• if I don’t know the exact tactic I need?
• if I need multiple tactics/generate subgoals?

12

P3: proof editing is (more or less) sequential

• Q1: when I change a definition, what proofs are broken?
• did the proofs break in an expected way? or did I change the wrong definition?
• how much work is left? what should I repair next?
• Q2: when I change a definition, what proof cases are broken?
• am I missing a new case?
• is an old case no longer covered by automation?

13

P3: proof editing is (more or less) sequential

• Q1: when I change a definition, what proofs are broken?
• did the proofs break in an expected way? or did I change the wrong definition?
• how much work is left? what should I repair next?
• Q2: when I change a definition, what proof cases are broken?
• am I missing a new case?
• is an old case no longer covered by automation?

14

P3: proof editing is (more or less) sequential

• Q1: when I change a definition, what proofs are broken?
• did the proofs break in an expected way? or did I change the wrong definition?
• how much work is left? what should I repair next?
• Q2: when I change a definition, what proof cases are broken?
• am I missing a new case?
• is an old case no longer covered by automation?

15

P4: information isn’t well integrated

​

• Q1: what does this tactic do?
• Q2: how do I use this syntax?
• let’s see you try to remember full syntax for match off the top of your head

16

claim: Lean’s tooling & design

help solve these problems

P4: information isn’t well integrated

​

• Q1: what does this tactic do?
• Q2: how do I use this syntax?

A: documentation on hover!

• bonus: cross-file ctrl-click navigation

18

P1: proof reading is missing ephemeral information

• Q1: what changes did this tactic make?
• in tac1; tac2, what changes did tac1 make?
• Q2: what is the type of this subexpression?
• what is the context of this subexpression?

A: infoview at cursor!

• Q3: what case is this subproof for?�A3: tagged cases help retain this info

19

P2: term writing isn’t incremental

• Q1: how do I fill in this term later?�A1: with typed holes
• Q2: how do I fill in this term with tactics?�A2: by dropping into proof mode, anywhere

20

P3: proof editing is (more or less) sequential

• Q1: when I change a definition, what proofs are broken?
• did the proofs break in an expected way? or did I change the wrong definition?
• how much work is left? what should I repair next?
• Q2: when I change a definition, what proof cases are broken?
• am I missing a new case?
• is an old case no longer covered by automation?

A: [demo]

21

tactics I enjoy

• split: pushes a goal inside of a match
• calc: explicit equational reasoning
• apply_rules [lem, …]: keep applying lemmas and hypotheses without backtracking (like Coq’s eauto … using …)

22

other tools and libraries

for Coq

for Lean

• SSReflect�
• CoqHammer�
• Mathcomp�
• Psatz

• LeanSSR�https://github.com/verse-lab/lean-ssr
• Aesop�https://github.com/leanprover-community/aesop
• Mathlib�https://github.com/leanprover-community/mathlib4
• (n)linarith (part of Mathlib)

23

my issues with Lean

basically designed specifically targeting mathematics

• no structural recursion on inductive predicates
• inductive propositions are fine. smth abt decreasing measures
• pretty sure this is a bug
• no induction tactic on mutual inductives
• encode mutual inductives as single inductives
• Coq doesn’t have great mutual inductive support anyway
• no coinduction
• RIP itrees folks ig
• no modules
• use typeclasses
• no Agda-style unification
• :(((

24

ported existing development in ~1 week

25

learning Lean

• Zulip (to ask questions): https://leanprover.zulipchat.com/
• Lean in your browser: https://live.lean-lang.org/
• reference manual: https://lean-lang.org/lean4/doc/
• library docs: https://leanprover-community.github.io/mathlib4_docs/
• learning resources: https://leanprover-community.github.io/learn.html

26