Partially prove Procedure.typeCheckWF (5 of 9 fields)#453
Partially prove Procedure.typeCheckWF (5 of 9 fields)#453tautschnig wants to merge 7 commits intomainfrom
Conversation
Replace the full 'by sorry' with a structured proof that establishes 5 of 9 WFProcedureProp fields from the type checker: - wfstmts: from Statement.typeCheckWF - ioDisjoint: from checkVariableScoping success - inputsNodup: from checkNoDuplicates success - outputsNodup: from checkNoDuplicates success - modNodup: from checkNoDuplicates success The remaining 4 fields (wfloclnd, inputsLocl, outputsLocl, wfspec) are not currently enforced by the type checker and remain as sorry. To enable the proof, checkNoDuplicates and checkVariableScoping in ProcedureType.lean are changed from private to public, with helper lemmas extracting the relevant properties from their success. Kiro spent 21 minutes on this partial proof.
There was a problem hiding this comment.
Pull request overview
This PR replaces a blanket by sorry for Procedure.typeCheckWF with a structured proof that derives several WFProcedureProp fields directly from the successful execution path of Procedure.typeCheck, leaving the remaining fields as sorry because the type checker does not currently enforce them.
Changes:
- Added local helper theorems to extract
Nodupand input/output disjointness properties from successfulcheckNoDuplicates/checkVariableScoping. - Implemented a partial
Procedure.typeCheckWFproof that constructs 5 of 9WFProcedurePropfields, with 4 fields still admitted viasorry. - Changed
checkNoDuplicatesandcheckVariableScopinginProcedureType.leanfromprivateto public to support the proof.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 2 comments.
| File | Description |
|---|---|
Strata/Languages/Core/ProcedureWF.lean |
Adds helper extraction lemmas and a partial Procedure.typeCheckWF proof building a WFProcedureProp. |
Strata/Languages/Core/ProcedureType.lean |
Exposes internal typechecker helper functions (checkNoDuplicates, checkVariableScoping) by removing private. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
The previous commit introduced two issues in Procedure.typeCheckWF: 1. Used 'private lemma' which is not a valid keyword in Lean 4.27.0 (lemma is a Mathlib alias, not available here). 2. The bind-peeling strategy with Except.bind_eq_ok_of_ok only handled 3 of the ~9 sequential binds in Procedure.typeCheck, leaving unsolved goals. Restore the working approach: set_option maxHeartbeats/maxRecDepth with 'repeat (split at H <;> try contradiction)' to handle all binds automatically.
Address PR review comment: restore 'private' on checkNoDuplicates and checkVariableScoping in ProcedureType.lean to reduce module API surface. Move the corresponding _ok theorems (checkNoDuplicates_ok, checkVariableScoping_ok) into ProcedureType.lean where they can access the private defs, and export them as public theorems. ProcedureWF.lean now uses these exported theorems instead of duplicating the proofs.
aqjune-aws
left a comment
aqjune-aws
left a comment
There was a problem hiding this comment.
I approved this pull request because the added theorems looked useful and the partial proofs looked ok (one more approval would be necessary, though).
Address PR comment: everything after 'intro h' in the proof can be replaced with grind.
Address PR comment: maxHeartbeats and maxRecDepth options are not needed for this proof and make things brittle.
|
Generally I'd recommend finishing proofs before submitting PRs. I don't think we waste time reviewing LLM failures to finish tasks. |
What are you taking as an "LLM failure" here? The fact that 4 proofs were left unproven? If so: those actually require changes in the type checker to enable their proof. See #452 for the full resolution, this was just my attempt to break this up into reviewable chunks. If something else is your definition of "LLM failure," then please explain. |
Replace the full 'by sorry' with a structured proof that establishes 5 of 9 WFProcedureProp fields from the type checker:
The remaining 4 fields (wfloclnd, inputsLocl, outputsLocl, wfspec) are not currently enforced by the type checker and remain as sorry.
Kiro spent 21 minutes on this partial proof.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.