6b9ac691cb
Adds three foundation lemmas about `tokenize`:
· tokenize_lparen_cons : tokenize ('(' :: rest) = lparen :: tokenize rest
· tokenize_rparen_cons : tokenize (')' :: rest) = rparen :: tokenize rest
· tokenize_space_cons : tokenize (' ' :: rest) = tokenize rest
These are the trivial cases — pure unfolding of `tokenizeAux` on
single-char-token branches.
The full Phase 3 (`tokenize (toLeanSource v).toList = toTokens v`)
requires four further substantial lemmas:
· readIdent_split : reading an ident sequence followed by a
non-ident-rest char (or end of input) yields
exactly the accumulated string.
· readStrLit_split : reading an escapeStrLit-encoded body until
the closing `"` recovers the original string.
· tokenize_app_clean: tokenize distributes over a concatenation
where the prefix ends "cleanly" (rparen,
whitespace, or strLit close).
· tokenize_render_X: induction over each meta-mirror type using
the above plus IH on sub-values.
Each is multi-page Lean reasoning about `String`/`List Char`/
`readIdent`/`readStrLit` distribution. The proof sketches are
documented inline.
The token-level universal (already proven) plus closed-instance
`decide` tests cover the round-trip operationally. Adding the
Phase 3 universal would let us state
∀ t, fromLeanSource? (toLeanSource t) = some t
without any closed-instance restrictions.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
||
|---|---|---|
| .. | ||
| Comonad | ||
| Foundation | ||
| Comonad.lean | ||
| Foundation.lean | ||
| Test.lean | ||