Conversation
Convert compile_correct from the local/get_goal/assembly pattern to the suspend/Resume/Finalise mechanism. The local block with get_goal and compile_correct_tm is replaced by a single Theorem that performs induction and suspends all 17 cases, with each former case theorem becoming a Resume block. compile_Con is split into Con_NONE and Con_SOME to match the separate induction cases. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…ordProps proofs Convert get_goal/setup patterns to HOL4's built-in suspend/Resume/Finalise mechanism in four proof files: - bvl_to_bviProofScript.sml: compile_exps_correct (11 cases) - word_cseProofScript.sml: comp_correct (23 cases) - word_to_stackProofScript.sml: comp_correct (23 cases) - wordPropsScript.sml: evaluate_clock_const + evaluate_clock_with_const (2x18 cases) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Convert 8 pancake proof files from ad-hoc get_goal/setup pattern to HOL4's built-in suspend/Resume/Finalise mechanism. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Convert 4 files from ad-hoc get_goal/setup pattern to HOL4's suspend/Resume/Finalise. Sub-case theorems for App (Eval, Op, Opapp) use nested suspend instead of get_goal. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Replace get_goal/setup pattern with suspend/Resume or inline proofs: - loop_removeProof: delete unused get_goal/ind_goals definitions - pan_globalsProof: inline shared proof into individual Resume blocks - loop_liveProof: extract per-case proofs into Resume blocks - loop_to_wordProof: extract per-case proofs into Resume blocks - wordPropsScript: inline get_goal into local let binding - dafny_wp_calc: convert setup/get_goal/init to suspend/Resume/Finalise Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- bvl_to_bviProof: delete unused val ind_thm - word_cseProof: write goal directly, delete val goal and val ind_thm, use recInduct evaluate_ind instead of match_mp_tac ind_thm Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Write goals directly and use recInduct instead of match_mp_tac ind_thm: - loop_callProof, loop_liveProof, loop_removeProof: recInduct loopSemTheory.evaluate_ind - crep_to_loopProof: recInduct crepSemTheory.evaluate_ind - pan_to_crepProof: recInduct panSemTheory.evaluate_ind, also remove gen_goal Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
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
2 participants
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.
No description provided.