From fea5a37f4a36906a007a1b0708482d153eb095f4 Mon Sep 17 00:00:00 2001 From: John Regehr Date: Sat, 27 Jun 2026 14:07:17 -0600 Subject: [PATCH 1/2] a new theorem --- Veir/Rewriter/WfRewriter/GetSet.lean | 39 ++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/Veir/Rewriter/WfRewriter/GetSet.lean b/Veir/Rewriter/WfRewriter/GetSet.lean index 716b80d65..16389ed04 100644 --- a/Veir/Rewriter/WfRewriter/GetSet.lean +++ b/Veir/Rewriter/WfRewriter/GetSet.lean @@ -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 @@ -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 + 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` -/ From d80b76377773811384e548c3eaedaf86a15e73a7 Mon Sep 17 00:00:00 2001 From: John Regehr Date: Sat, 27 Jun 2026 14:42:17 -0600 Subject: [PATCH 2/2] more theorems --- Veir/PatternRewriter/Basic.lean | 23 +++++++++++++++++++ Veir/Rewriter/WfRewriter/GetSet.lean | 33 ++++++++++++++++++---------- 2 files changed, 45 insertions(+), 11 deletions(-) diff --git a/Veir/PatternRewriter/Basic.lean b/Veir/PatternRewriter/Basic.lean index b74557bb0..37fe2dcf2 100644 --- a/Veir/PatternRewriter/Basic.lean +++ b/Veir/PatternRewriter/Basic.lean @@ -215,6 +215,29 @@ def replaceValue (rewriter: PatternRewriter OpInfo) (oldVal newVal: ValuePtr) let ctx := WfRewriter.replaceValue rewriter.ctx oldVal newVal { rewriter with ctx, hasDoneAction := true} +@[simp, grind =] +theorem replaceValue_ctx {rewriter : PatternRewriter OpInfo} {oldVal newVal : ValuePtr} + {neValues : oldVal ≠ newVal} {oldIn : oldVal.InBounds rewriter.ctx.raw} + {newIn : newVal.InBounds rewriter.ctx.raw} : + (rewriter.replaceValue oldVal newVal neValues oldIn newIn).ctx + = WfRewriter.replaceValue rewriter.ctx oldVal newVal neValues oldIn newIn := by + simp [replaceValue, addUsersInWorklist_same_ctx] + +/-- After replacing `op`'s single result with `newValue`, erasing `op` succeeds: the three +preconditions of `eraseOp` (`op` in bounds, no regions, no uses) hold in the resulting rewriter. -/ +theorem eraseOp_some_after_replace_result0 + (rewriter : PatternRewriter OpInfo) (op : OperationPtr) (newValue : ValuePtr) + (hop : op.InBounds rewriter.ctx.raw) + (hres : (op.getResult 0 : ValuePtr).InBounds rewriter.ctx.raw) + (hnew : newValue.InBounds rewriter.ctx.raw) + (hne : (op.getResult 0 : ValuePtr) ≠ newValue) + (hone : op.getNumResults! rewriter.ctx.raw = 1) + (hregions : op.getNumRegions! rewriter.ctx.raw = 0) : + ∃ rewriter', + (rewriter.replaceValue (op.getResult 0 : ValuePtr) newValue hne hres hnew).eraseOp op + = some rewriter' := + ⟨_, rfl⟩ + def createBlock (rewriter: PatternRewriter OpInfo) (argTypes: Array TypeAttr) (insertPoint : Option BlockInsertPoint) diff --git a/Veir/Rewriter/WfRewriter/GetSet.lean b/Veir/Rewriter/WfRewriter/GetSet.lean index 16389ed04..e0c9a87c3 100644 --- a/Veir/Rewriter/WfRewriter/GetSet.lean +++ b/Veir/Rewriter/WfRewriter/GetSet.lean @@ -882,6 +882,27 @@ theorem ValuePtr.hasUses!_WfRewriter_replaceValue_oldValue : fun_induction WfRewriter.replaceValue <;> grind [Id.run, ValuePtr.hasUses!_def, ValuePtr.getFirstUse!_eq_getFirstUse] +/-- After replacing the (sole) result of `op` with another value, `op` no longer has any uses. -/ +@[grind =] +theorem OperationPtr.hasUses!_WfRewriter_replaceValue_getResult0 + {op : OperationPtr} {newValue : ValuePtr} + {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) : + 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 + +/-- After replacing `op`'s single result with `newValue`, `op` still exists, still has no regions, +and now has no uses — exactly the preconditions required to erase it. -/ theorem OperationPtr.erase_preconditions_after_replace_result0 {op : OperationPtr} {newValue : ValuePtr} (hop : op.InBounds ctx.raw) @@ -902,17 +923,7 @@ theorem OperationPtr.erase_preconditions_after_replace_result0 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⟩ + exact ⟨h1, h2, OperationPtr.hasUses!_WfRewriter_replaceValue_getResult0 hone⟩ end WfRewriter.replaceValue