formal: a record's reading decomposes by simp; no per-record reading lemma - #382
Merged
Merged
Conversation
…lemma The readings gate demanded `reads_x`/`scoped_x` beside every `CircuitType` instance on the ground that `reads_ofEquiv` matches only the literal `ofEquiv` term. It does not: instances are reducible, and `rw`/`simp only [reads_ofEquiv]` fire through a named instance. What a consumer lacked was the next step — `equivProd x` is not syntactically a tuple, so `reads_prod` never fired — and that is one `@[simps apply]` per decomposition. `Snarky.Encoding.Simps` collects the formers' reading lemmas and the hand-written leaf instances' as the `reads_simps` set (declared in `Snarky.Encoding.ReadsAttr`): with each decomposition's projection lemma, `simp [reads_simps] at h` turns a nested record's `Reads` or `Scoped` into its leaves'. `Pickles.Encoding` is the equivalences with `@[simps apply]` and the one-line instances — 34 lemmas and the `Type1` instance Snarky already has go; the instances are script-surface roots, the projection lemmas the records' API. The gate accepts either style. Its `sed` used a GNU-only `\?`, so on macOS it had checked nothing; portable now, it sees the tree's 22 instances. Closes #380. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
There was a problem hiding this comment.
Your trial has ended. Reactivate Greptile to resume code reviews.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stacked on #379. Closes #380.
The readings gate demanded
reads_x/scoped_xbeside everyCircuitTypeinstance, on the ground thatreads_ofEquivmatches only the literalofEquivterm andsimpwill not look inside a named instance. Probing showed otherwise, and showed what was actually missing.What the probes found
rw [CircuitType.reads_ofEquiv]andsimp only [CircuitType.reads_ofEquiv]fire through a named instance today: instances are reducible.Reads V x astill cannot reach a leaf, becauseequivProd xis not syntactically a tuple andreads_prodnever fires. The load-bearing lemmas in the tree (reads_affinePoint,reads_spongeState, ~130 uses) are componentwise, a different artifact.@[simps apply]on each decomposition, plus the former lemmas as a simp set, andsimp [reads_simps] at hturns a nested record'sReadsorScopedinto its leaves'. Checked end to end onUnfinalizedProof(13 leaves) andWrapStatement.The change
Snarky.Encoding.ReadsAttrdeclaresreads_simps;Snarky.Encoding.Simpsfills it with the formers' reading lemmas and the hand-written leaf instances' (AffinePoint,SpongeState,Type1). Two new modules; nothing existing rebuilds.Pickles/Encoding.lean: each record is its equivalence with@[simps apply]and a one-lineofEquivinstance. The 34 lemmas go, and theType1instance Snarky already has. About 450 lines to 220.check-readings.shaccepts either style: the two lemmas by hand, or an@[simpsdecomposition on theofEquivargument. Itssedused GNU-only\?, so on macOS it had checked nothing; portable now, it sees the tree's 22 instances.-- synthesisscript-surface entries, the 16 projection lemmas as plain roots, as Snarky does forType1.equivCarrier_apply.Untouched, by design: the six hand-written instances and their named lemmas.
Verified
Build, the consumer probe, readings (22 instances), dead-code, shake on the CI list, runLinter on
Snarky/Pickles/PicklesFixture, style, check-cs, a check-halves lane.🤖 Generated with Claude Code