Initial work porting TS/Types by mwhicks1 · Pull Request #86 · plclub/sf-in-lean

mwhicks1 · 2026-07-15T18:09:44Z

Initial pass at TS/Types.lean. This is a draft because it's not close to merging yet. But wanted to get it up rather than keep it on my machine. No need for anyone to comment, but feel free to look.

Worth noting:

In SF for Rocq, Types follows Smallstep, which follows Imp. There are dependencies to both. For now I've inlined the definitions in Smallstep that are needed (a small handful) but the bigger problem is the text/commentary, which assumes the reader is familiar with concepts not really covered in SFL's current LF. My current thinking is a pared down Smallstep that is at the start of both HL and TS, so that if you go from HL to TS or vice versa you can skip Smallstep the second time through.
The notation is maybe risky. The basic approach (as used in Imp) doesn't allow for defining notation for a type and then using it in the type's (inductive) definition. Claude figured out a way and that's what's here, but it breaks hygiene selectively. Needs review (and suggestions for alternatives).
Much of the text has not been touched, neither proofs etc. Just getting the definitions down for now and will come back to this.

Slang is the simple expression language (Aexp/Bexp with big-step evaluation and the optimize0plus optimization), extracted from HL/Imp's opening and shared as the common foundation for the HL and TS paths. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

The chapter's opening (~810 lines: variable-free Aexp/Bexp, evaluation, optimization, and evaluation-as-a-relation) duplicated the new Slang chapter. Remove it and add a short bridge telling the reader to read Slang first, then resume here with variables and commands. - Delete the # Arithmetic and Boolean Expressions / # Optimizing Booleans / # Evaluation as a Relation sections (Warmup, AevalRDivision, AevalRExtended). - No import of TS.Slang: nothing here uses it in code, and importing would make HL depend on a TS-volume module, against the independent-paths goal. - Reference Slang in prose (plain text; a live cross-book link isn't supported across separate books yet). - Redirect the two Warmup back-references to Slang. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

# Conflicts: # HL/Imp.lean

- Promote dev-note urgencies/authors to directive args (SOONER -> BeforeNextRelease, LATER -> PotentialImprovement; mwhicks1/chenson2018 -> author strings). - GRADE_THEOREM blocks -> :::gradeTheorem (GRADE_MANUAL stays :::grade). - Add :::quizSolution answer blocks to the two quizzes. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Small-step operational semantics (toy Tm language, typed arithmetic build-up, and the Slang-based arithmetic/boolean small-step + stack machine). Builds on the Slang chapter. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

- Cut the boolean toy language (Temp4/Temp5), the Combined arith+bool language, and the normalize-tactic section: redundant now that the chapter builds on Slang (which already has arithmetic and boolean expressions). The Combined language's stuck-terms lesson is picked up in the Types chapter. - Rename the Slang small-step section to 'Small-Step Slang' and move Nondeterministic Evaluation after Boolean Expressions. - Add astep_deterministic / bstep_deterministic exercises, proved as compact <;>-driven tactic chains with a single uniform closer. - Use Unicode operators (¬, ∧, −, ×) in the boolean/arithmetic inference rules. - Resolve in-file TODOs; drop stale dev/port-status notes; prose + formatting. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

- Dev-note urgencies/authors -> directive args (SOONER/LATER/TODO -> BeforeNextRelease/PotentialImprovement/NOW; mwhicks1/MRC -> author strings); the bare 'Additional Exercises' TODO -> :::dev NOW. - GRADE_THEOREM -> :::gradeTheorem (GRADE_MANUAL stays :::grade). - :::quizSolution for all 8 quizzes (5 converted from :::instructors answers, 3 bare quizzes given computed answers). - compiler_is_correct: (level := Advanced) (Rocq EX3A). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Types of a typed arithmetic language (progress, preservation, soundness), building on the Smallstep chapter's generic vocabulary. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

The Smallstep chapter drops the Combined-language exercises combined_step_deterministic / combined_strong_progress (two-sorted Slang can't express stuck terms). Add a dev reminder at the stuck-terms section that this chapter's single-sorted Tm language is their successor and should cover both angles (step_deterministic; some_term_is_stuck). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

#97 makes non-canonical :::dev urgencies a hard build error; update the cross-check note's argument to the canonical spelling. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

- GRADE_THEOREM (progress/preservation/preservation') -> :::gradeTheorem (six GRADE_MANUAL stay :::grade). - :::quizSolution for all 11 quizzes (6 converted from :::answer, 5 bare quizzes given computed answers). - Exercise flags from Rocq Types.v: variation1/variation2/remove_pred0 (manual := true); prog_pres_bigstep EX4AM -> (level := Advanced) (manual := true). - Promote the two single-note dev urgencies to canonical args. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Address xhalo32's review comment: use named binders for the recursive hypotheses in Tm.Step and Tm.HasType (matching Imp.lean and the existing Tm.IsNValue) rather than arrow-form hypotheses. The constructors are identical, so nothing downstream changes. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

The variation quizzes/exercises displayed proposed rules using Rocq-style names (ST_PredTrue, ST_Funny1..3, T_IfFunny, T_SuccBool, T_Funny4/5). Rename to our inductive-rule convention (predTrue/predFalse, funny1..5, ifFunny, succBool), matching the actual Tm.Step/Tm.HasType constructor names; also fixes prose that mixed 'ifTrue' with 'ST_Funny1'. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

- Replace <> / <= / ! / && with ≠ / ≤ / ¬ / ∧ in the imp_bexp grammar, macro_rules, and boolean delaborator - Update examples and the #check expected-output annotation to match

- Strip trailing whitespace across prose and dev-note lines - Use * rather than × in the arithmetic BNF for consistency

…space cleanup # Conflicts: # TS/Slang.lean

berberman left a GitHub comment about not using induction principles directly, and preferring the fun_induction tactic. I asked Claude to help me update the proof to do that, and then adjusted the text accordingly, leaving a note that we should either update Automation to add this tactic, or introduce it here.

This approach follows a suggestion from Vtec234, and was implemented by Claude for `Tm.Step` and `Tm.AltStep`. TBD: Whether to do something similar for typing.

bcpierce00

This is going to need a couple of line-by-line proofreading passes once it stabilizes, but from a quick pass it seems good so far. I left some comments inline.

bcpierce00

Oops -- I seem to have marked this as "Ready for review," but I don't know how to unmark it!

KihongHeo · 2026-07-23T13:35:37Z

Silly question: how to type ⦂? Hovering over the symbol does not give any message. \typecolon does not work.

chenson2018 · 2026-07-23T13:46:39Z

Silly question: how to type ⦂? Hovering over the symbol does not give any message. \typecolon does not work.

Not a silly question, as there is not an abbreviation. It should be added to settings .vscode/settings.json.

(Note that \: is already an abbreviation for ∶, another Unicode colon. I didn't suggest it because it is probably confusing in being very hard to tell apart from the usual colon.)

mwhicks1 changed the base branch from main to mwh-imp-proofs July 15, 2026 18:19

chenson2018 reviewed Jul 15, 2026

View reviewed changes

Comment thread TS/Types.lean Outdated

mwhicks1 force-pushed the mwh-imp-proofs branch 2 times, most recently from dd0eb26 to a1dd33a Compare July 15, 2026 20:10

Base automatically changed from mwh-imp-proofs to main July 15, 2026 20:53

xhalo32 reviewed Jul 16, 2026

View reviewed changes

Comment thread TS/Types.lean Outdated

xhalo32 reviewed Jul 16, 2026

View reviewed changes

Comment thread TS/Types.lean

xhalo32 reviewed Jul 16, 2026

View reviewed changes

Comment thread TS/Types.lean

mwhicks1 and others added 13 commits July 18, 2026 09:06

Merge branch 'main' into mwh-slang

414360b

# Conflicts: # HL/Imp.lean

TS: add the versified Smallstep chapter

08dfca4

Small-step operational semantics (toy Tm language, typed arithmetic build-up, and the Slang-based arithmetic/boolean small-step + stack machine). Builds on the Slang chapter. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

TS: add the Types chapter

6b442c4

Types of a typed arithmetic language (progress, preservation, soundness), building on the Smallstep chapter's generic vocabulary. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

TS/Types: canonical dev urgency for #97 (LATER -> PotentialImprovement)

6743e57

#97 makes non-canonical :::dev urgencies a hard build error; update the cross-check note's argument to the canonical spelling. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

mwhicks1 force-pushed the mwh-ts branch from 26c9bbd to 360b857 Compare July 18, 2026 19:22

mwhicks1 changed the base branch from main to mwh-slang-smallstep July 18, 2026 19:23

mwhicks1 mentioned this pull request Jul 18, 2026

Work in progress (tracking meta-issue) #25

Open

Benjamin Pierce and others added 6 commits July 20, 2026 19:49

Comments / polishing on Slang chapter.

ad40be5

One more

fd25c54

HL/Imp: use Unicode notation in Imp concrete syntax

c4dbb11

- Replace <> / <= / ! / && with ≠ / ≤ / ¬ / ∧ in the imp_bexp grammar, macro_rules, and boolean delaborator - Update examples and the #check expected-output annotation to match

Comments / polishing on Slang chapter.

8260c03

One more

d30e0c0

TS/Slang: trailing-whitespace cleanup and × → * in BNF grammar

20fcebe

- Strip trailing whitespace across prose and dev-note lines - Use * rather than × in the arithmetic BNF for consistency

mwhicks1 added 6 commits July 20, 2026 18:08

Merge mwh-slang: Imp Unicode notation + Pierce's Slang polish + white…

0bb9c3d

…space cleanup # Conflicts: # TS/Slang.lean

Merge branch 'main' into mwh-slang

c3ae0e5

Merge branch 'mwh-slang' into mwh-slang-smallstep

3b2995a

Merge branch 'mwh-slang-smallstep' into mwh-ts

d387e29

Update notation so it's available in the inductive definition.

466131f

This approach follows a suggestion from Vtec234, and was implemented by Claude for `Tm.Step` and `Tm.AltStep`. TBD: Whether to do something similar for typing.

mwhicks1 mentioned this pull request Jul 21, 2026

Allowing independent paths from LF to TS and LF to HL #87

Closed

Base automatically changed from mwh-slang-smallstep to main July 22, 2026 23:49

bcpierce00 reviewed Jul 23, 2026

View reviewed changes

Comments

63da06f

bcpierce00 self-assigned this Jul 23, 2026

bcpierce00 marked this pull request as ready for review July 23, 2026 12:12

bcpierce00 requested a review from a team as a code owner July 23, 2026 12:12

bcpierce00 reviewed Jul 23, 2026

View reviewed changes

mwhicks1 added 4 commits July 23, 2026 08:15

Merge branch 'main' into mwh-ts

b5e8b52

Merge branch 'mwh-ts' of github.com:plclub/sf-in-lean into mwh-ts

c01f43a

relocate comment (broke build)

e3df64b

addressed a couple of bcpierce00 comments

7c446bd

mwhicks1 added 3 commits July 23, 2026 13:06

macro hygeine trick, applied to typing syntax

5cb1419

key mapping for typechecking colon is \tc

0f83a72

Merge branch 'main' into mwh-ts

64c4d82

mwhicks1 merged commit 3d020c3 into main Jul 23, 2026
1 check passed

mwhicks1 deleted the mwh-ts branch July 23, 2026 17:30

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Initial work porting TS/Types#86

Initial work porting TS/Types#86
mwhicks1 merged 33 commits into
mainfrom
mwh-ts

mwhicks1 commented Jul 15, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

bcpierce00 left a comment

Uh oh!

bcpierce00 left a comment

Uh oh!

KihongHeo commented Jul 23, 2026

Uh oh!

chenson2018 commented Jul 23, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

Uh oh!

Conversation

mwhicks1 commented Jul 15, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

bcpierce00 left a comment

Choose a reason for hiding this comment

Uh oh!

bcpierce00 left a comment

Choose a reason for hiding this comment

Uh oh!

KihongHeo commented Jul 23, 2026

Uh oh!

chenson2018 commented Jul 23, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants