Port of erasure theorem (WIP) - #667
Open
maxvistrup wants to merge 5 commits into
Open
Conversation
Adds `rocq_alias` annotations to every top-level definition and theorem that has a Rocq counterpart in `iris_heap_lang/proph_erasure.v`, and refactors `erased_primStep_primStep` and `erased_baseStep_baseStep` using local tactic macros (`erase_simp`, `peel_ki`) and inversion helpers (`eraseExpr_eq_val`, `eraseVal_eq_lit`) to shrink the case enumerations.
Adds a generic `reshapeExpr` on top of `findECtx` that mirrors Rocq's `reshape_expr e tac`: walks decompositions `e = fill K e'` from innermost outward and invokes `tac K e'` on each. The callback sees both K and e', so it can guard on non-empty K or on the last frame's shape (which the existing `findECtx` — parameterized only on e' — cannot do).
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.
This PR contains a port of the erasure theorem from Rocq. I'm not fully happy with it. As I warned in the meeting on Friday, I don't consider this proof production-ready as of yet. I've tried various things but it remains significantly longer than the upstream proof: 1912 lines vs 860 lines. Let me explain the main reasons why that is:
Reason 1:
reshape_expr. In the Rocq proof,reshape_expris useful for handling the many cases from destructingKiinnon_resolve_prim_step_matched_by_erased_steps_ectx_item. It is not immediately obvious to me how to best get the same convenience in Lean. As partial progress, I have portedreshape_expras a small wrapper around @ayhon'sextractAllEctxItems. That part is all fine. However, to my knowledge, you can't match every goal of a certain shape in Lean. Thus, unlike Rocq, you can't easily go over all the unlabeled cases and extract theKito pass as argument toreshape_expr. Thus, some more creative metaprogramming options are necessary. For now, I leave it unaddressed here to solicit some suggestions from those more experienced in Lean metaprogramming. Is this a familiar pattern? Can I match on the shape of goals?Reason 2:
repeat match goal. Another closely related issue is appears in the proof oferased_baseStep_baseStepwhich is significantly longer than its Rocq parallelerased_base_step_base_step. The latter relies on some creative proof engineering usingrepeat match goalto destruct the relevant parameter unveiled by inverting the step, and then closing all goals byeauto using. The latter step may be within reach in Lean, but it is not clear to me if there is any idiom for doing the first step of singling out certain cases of an inversion.Another point of optimization is
erased_primStep_primStep. This proof inlines the proof corresponding to the Rocq proof ofprim_step_matched_by_erased_steps_ectx_item. In the Rocq proof of this, most of the cases ofdestruct Kicould be discharged tosimplify_eq/=; rewrite fill_app /=.I'm not sure what the Lean analogue would be, but I'm sure something can be done here.Happy to take any input.