Skip to content

feat(rewriter): RAUW + erase is safe #936

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
regehr wants to merge 2 commits into
base: main
Choose a base branch
from
Open

feat(rewriter): RAUW + erase is safe #936

Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
fea5a37
a new theorem
regehr Jun 27, 2026
d80b763
more theorems
regehr Jun 27, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
39 changes: 39 additions & 0 deletions Veir/Rewriter/WfRewriter/GetSet.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
module

public import Veir.Rewriter.WfRewriter.Basic
public import Veir.Rewriter.WfRewriter.InBounds
public import Veir.Rewriter.GetSet
public import Veir.Rewriter.WfRewriter.GetSetTactic

Expand Down Expand Up @@ -875,6 +876,44 @@ theorem OperationPtr.getResultTypes!_WfRewriter_replaceValue :
· have := @ValuePtr.getType!_WfRewriter_replaceValue _ _ ctx (operation.getResult i)
grind

@[simp, grind =]
theorem ValuePtr.hasUses!_WfRewriter_replaceValue_oldValue :
oldValue.hasUses! (WfRewriter.replaceValue ctx oldValue newValue ne oldIn newIn).raw = false := by
fun_induction WfRewriter.replaceValue <;>
grind [Id.run, ValuePtr.hasUses!_def, ValuePtr.getFirstUse!_eq_getFirstUse]

theorem OperationPtr.erase_preconditions_after_replace_result0
{op : OperationPtr} {newValue : ValuePtr}
(hop : op.InBounds ctx.raw)
(hres : (op.getResult 0 : ValuePtr).InBounds ctx.raw)
(hnew : newValue.InBounds ctx.raw)
(hne : (op.getResult 0 : ValuePtr) ≠ newValue)
(hone : op.getNumResults! ctx.raw = 1)
(hregions : op.getNumRegions! ctx.raw = 0) :
let ctx' :=
WfRewriter.replaceValue ctx (op.getResult 0 : ValuePtr) newValue hne hres hnew
op.InBounds ctx'.raw ∧
op.getNumRegions! ctx'.raw = 0 ∧
op.hasUses! ctx'.raw = false := by
Comment on lines +906 to +918

@math-fehr math-fehr Jun 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure we overall need this theorem?
Mostly because each component is already a simp/grind lemma?

have h1 : op.InBounds
(WfRewriter.replaceValue ctx (op.getResult 0) newValue hne hres hnew).raw := by
rw [← GenericPtr.iff_operation, WfRewriter.replaceValue_inBounds, GenericPtr.iff_operation]
exact hop
have h2 : op.getNumRegions!
(WfRewriter.replaceValue ctx (op.getResult 0) newValue hne hres hnew).raw = 0 := by
rw [OperationPtr.getNumRegions!_WfRewriter_replaceValue]; exact hregions
have h3 : op.hasUses!
(WfRewriter.replaceValue ctx (op.getResult 0) newValue hne hres hnew).raw = false := by
rw [OperationPtr.hasUses!_eq_false_iff_hasUses!_getResult_eq_false]
intro index hindex
have hnum : op.getNumResults!
(WfRewriter.replaceValue ctx (op.getResult 0) newValue hne hres hnew).raw = 1 := by
rw [OperationPtr.getNumResults!_WfRewriter_replaceValue]; exact hone
have hidx0 : index = 0 := by omega
subst hidx0
exact ValuePtr.hasUses!_WfRewriter_replaceValue_oldValue
exact ⟨h1, h2, h3⟩

end WfRewriter.replaceValue

/-! ## `WfRewriter.setType` -/
Expand Down
Loading