diff --git a/Veir/Rewriter/GetSet/CreateOp.lean b/Veir/Rewriter/GetSet/CreateOp.lean index 6c9d4dd9a..ee3122333 100644 --- a/Veir/Rewriter/GetSet/CreateOp.lean +++ b/Veir/Rewriter/GetSet/CreateOp.lean @@ -397,21 +397,51 @@ theorem BlockPtr.prev!_createOp {block : BlockPtr} : Rewriter.createOp ctx opType resultTypes operands blockOperands regions properties insertionPoint h₁ h₂ h₃ h₄ h₅ = some (ctx', newOp) → (block.get! ctx').prev = (block.get! ctx).prev := by - grind (gen := 20) + simp only [Rewriter.createOp] + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset @[simp, grind =>, simp_getset] theorem BlockPtr.next!_createOp {block : BlockPtr} : Rewriter.createOp ctx opType resultTypes operands blockOperands regions properties insertionPoint h₁ h₂ h₃ h₄ h₅ = some (ctx', newOp) → (block.get! ctx').next = (block.get! ctx).next := by - grind (gen := 20) + simp only [Rewriter.createOp] + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset @[simp, grind =>, simp_getset] theorem BlockPtr.parent!_createOp {block : BlockPtr} : Rewriter.createOp ctx opType resultTypes operands blockOperands regions properties insertionPoint h₁ h₂ h₃ h₄ h₅ = some (ctx', newOp) → (block.get! ctx').parent = (block.get! ctx).parent := by - grind (gen := 20) + simp only [Rewriter.createOp] + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset @[grind =>, simp_getset] theorem BlockPtr.firstOp!_createOp {block : BlockPtr} : @@ -424,7 +454,27 @@ theorem BlockPtr.firstOp!_createOp {block : BlockPtr} : else (block.get! ctx).firstOp | none => (block.get! ctx).firstOp := by simp only [Rewriter.createOp] - grind (gen := 20) (instances := 2000) [cases InsertPoint] + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + cases insertPoint + case before op => + simp only [InsertPoint.block!_before_eq, InsertPoint.prev!_before_eq] + simp_getset + by_cases hop : op = newOpPtr + · subst newOpPtr + grind + · simp [hop] + case atEnd block => + simp only [InsertPoint.block!_atEnd_eq, Option.some.injEq, InsertPoint.prev_atEnd_eq] + grind + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset @[grind =>, simp_getset] theorem BlockPtr.lastOp!_createOp {block : BlockPtr} : @@ -437,7 +487,25 @@ theorem BlockPtr.lastOp!_createOp {block : BlockPtr} : else (block.get! ctx).lastOp | none => (block.get! ctx).lastOp := by simp only [Rewriter.createOp] - grind (gen := 20) [cases InsertPoint] + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + cases insertPoint + case before op => + simp only [InsertPoint.block!_before_eq] + simp_getset + by_cases hop : op = newOpPtr + · subst newOpPtr + grind + · simp [hop] + case atEnd block => simp + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset @[grind =>, simp_getset] theorem OperationPtr.prev!_createOp {operation : OperationPtr} : @@ -452,7 +520,30 @@ theorem OperationPtr.prev!_createOp {operation : OperationPtr} : | none => if operation = newOp then none else (operation.get! ctx).prev := by simp only [Rewriter.createOp] - grind (gen := 20) [cases InsertPoint] + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + cases insertPoint + case before op => + simp only [InsertPoint.next_before_eq, Option.some.injEq, InsertPoint.prev!_before_eq] + simp_getset + by_cases hop : op = newOpPtr; grind + simp only [hop, ↓reduceIte] + by_cases hop' : operation = op; simp_all + simp [hop'] + by_cases hop'' : operation = newOpPtr <;> simp_all + case atEnd block => + simp only [InsertPoint.next_atEnd_eq, reduceCtorEq, ↓reduceIte, InsertPoint.prev_atEnd_eq, + BlockPtr.lastOp!_initBlockOperands, BlockPtr.lastOp!_initOpOperands] + by_cases hop : operation = newOpPtr <;> simp_all + simp_getset + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset @[grind =>, simp_getset] theorem OperationPtr.next!_createOp {operation : OperationPtr} : @@ -467,7 +558,41 @@ theorem OperationPtr.next!_createOp {operation : OperationPtr} : | none => if operation = newOp then none else (operation.get! ctx).next := by simp only [Rewriter.createOp] - grind (gen := 20) (splits := 20) (instances := 2000) [cases InsertPoint] + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + cases insertPoint + case before op => + simp only [InsertPoint.prev!_before_eq, prev!_initBlockOperands, prev!_initOpOperands, + InsertPoint.next_before_eq] + simp_getset + by_cases hop : op = newOpPtr + · subst newOpPtr + simp only [↓reduceIte, reduceCtorEq] + by_cases hop' : operation = op; simp [hop', ↓reduceIte] + simp only [hop', ↓reduceIte, right_eq_ite_iff] + grind + · simp only [hop, ↓reduceIte] + by_cases hop' : some operation = (op.get! ctx).prev + · simp only [hop', ↓reduceIte, right_eq_ite_iff, Option.some.injEq] + grind + · simp only [hop', ↓reduceIte] + by_cases hop'' : operation = newOpPtr <;> simp_all + case atEnd block => + simp only [InsertPoint.prev_atEnd_eq, BlockPtr.lastOp!_initBlockOperands, + BlockPtr.lastOp!_initOpOperands, InsertPoint.next_atEnd_eq] + by_cases hop : some operation = (block.get! ctx₂).lastOp; grind + simp only [hop, ↓reduceIte] + by_cases hop' : operation = newOpPtr; simp_all + simp only [hop', ↓reduceIte, right_eq_ite_iff] + grind + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset @[grind =>, simp_getset] theorem OperationPtr.parent!_createOp {operation : OperationPtr} : @@ -480,7 +605,27 @@ theorem OperationPtr.parent!_createOp {operation : OperationPtr} : | none => none else (operation.get! ctx).parent := by simp only [Rewriter.createOp] - grind (gen := 20) [cases InsertPoint, Operation.empty] + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + cases insertPoint + case before op => + simp only [InsertPoint.block!_before_eq, parent!_initBlockOperands, parent!_initOpOperands] + simp_getset + by_cases hop : operation = newOpPtr + · simp only [hop, ↓reduceIte, ite_eq_right_iff] + grind + · simp only [hop, ↓reduceIte] + case atEnd block => + simp only [InsertPoint.block!_atEnd_eq] + by_cases hop : operation = newOpPtr <;> simp [hop] + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset @[grind =>, simp_getset] theorem OperationPtr.getOpType!_createOp {operation : OperationPtr} : @@ -489,7 +634,16 @@ theorem OperationPtr.getOpType!_createOp {operation : OperationPtr} : operation.getOpType! ctx' = if operation = newOp then ofDialect OpInfo opType else operation.getOpType! ctx := by simp only [Rewriter.createOp] - grind (gen := 20) + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset @[grind =>, simp_getset] theorem OperationPtr.attrs!_createOp {operation : OperationPtr} : @@ -498,7 +652,16 @@ theorem OperationPtr.attrs!_createOp {operation : OperationPtr} : (operation.get! ctx').attrs = if operation = newOp then DictionaryAttr.empty else (operation.get! ctx).attrs := by simp only [Rewriter.createOp] - grind (gen := 20) + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset @[grind =>, simp_getset] theorem OperationPtr.getProperties!_createOp {operation : OperationPtr} : @@ -512,7 +675,16 @@ theorem OperationPtr.getProperties!_createOp {operation : OperationPtr} : else operation.getProperties! ctx dialectOpType := by simp only [Rewriter.createOp] - grind (gen := 20) + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset @[grind =>, simp_getset] theorem OperationPtr.getNumResults!_createOp {operation : OperationPtr} : @@ -521,7 +693,18 @@ theorem OperationPtr.getNumResults!_createOp {operation : OperationPtr} : operation.getNumResults! ctx' = if operation = newOp then resultTypes.size else operation.getNumResults! ctx := by simp only [Rewriter.createOp] - grind (gen := 20) + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + by_cases hop : operation = newOpPtr <;> simp [hop] + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset + by_cases hop : operation = newOpPtr <;> simp [hop] /- OpResultPtr.get!_createOp is too complex to be expressed, and should not be needed in practice, @@ -535,7 +718,18 @@ theorem OperationPtr.getNumOperands!_createOp {operation : OperationPtr} : operation.getNumOperands! ctx' = if operation = newOp then operands.size else operation.getNumOperands! ctx := by simp only [Rewriter.createOp] - grind (gen := 20) + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + by_cases hop : operation = newOpPtr <;> simp [hop] + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset + by_cases hop : operation = newOpPtr <;> simp [hop] /- OpOperandPtr.get!_createOp is too complex to be expressed, and should not be needed in practice, @@ -549,7 +743,18 @@ theorem OperationPtr.getOperands!_createOp {operation : OperationPtr} : operation.getOperands! ctx' = if operation = newOp then operands else operation.getOperands! ctx := by simp only [Rewriter.createOp] - grind (gen := 20) + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + by_cases hop : operation = newOpPtr <;> simp [hop] + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset + by_cases hop : operation = newOpPtr <;> simp [hop] @[grind =>, simp_getset] theorem OperationPtr.getNumSuccessors!_createOp {operation : OperationPtr} : @@ -557,7 +762,19 @@ theorem OperationPtr.getNumSuccessors!_createOp {operation : OperationPtr} : insertionPoint h₁ h₂ h₃ h₄ h₅ = some (ctx', newOp) → operation.getNumSuccessors! ctx' = if operation = newOp then blockOperands.size else operation.getNumSuccessors! ctx := by - grind (gen := 20) + simp only [Rewriter.createOp] + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + by_cases hop : operation = newOpPtr <;> simp [hop] + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset + by_cases hop : operation = newOpPtr <;> simp [hop] /- BlockOperandPtr.get!_createOp is too complex to be expressed, and should not be needed in practice, @@ -572,7 +789,18 @@ theorem OperationPtr.getSuccessor!_createOp {operation : OperationPtr} : if operation = newOp then blockOperands[index]! else operation.getSuccessor! ctx index := by simp only [Rewriter.createOp] - grind (gen := 20) + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + by_cases hop : operation = newOpPtr <;> simp [hop] + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset + by_cases hop : operation = newOpPtr <;> simp [hop] @[grind =>, simp_getset] theorem OperationPtr.getSuccessors!_createOp {operation : OperationPtr} : @@ -580,7 +808,19 @@ theorem OperationPtr.getSuccessors!_createOp {operation : OperationPtr} : insertionPoint h₁ h₂ h₃ h₄ h₅ = some (ctx', newOp) → operation.getSuccessors! ctx' = if operation = newOp then blockOperands else operation.getSuccessors! ctx := by - grind (gen := 20) + simp only [Rewriter.createOp] + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + by_cases hop : operation = newOpPtr <;> simp [hop] + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset + by_cases hop : operation = newOpPtr <;> simp [hop] @[grind =>, simp_getset] theorem OperationPtr.getNumRegions!_createOp {operation : OperationPtr} : @@ -588,7 +828,27 @@ theorem OperationPtr.getNumRegions!_createOp {operation : OperationPtr} : insertionPoint h₁ h₂ h₃ h₄ h₅ = some (ctx', newOp) → operation.getNumRegions! ctx' = if operation = newOp then regions.size else operation.getNumRegions! ctx := by - grind (gen := 20) + simp only [Rewriter.createOp] + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + by_cases hop : operation = newOpPtr; rotate_left; simp [hop] + subst newOpPtr; simp only [↓reduceIte, Nat.zero_add] + rw [← OperationPtr.getNumRegions!_eq_getNumRegions (by grind)] + simp_getset + simp + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset + by_cases hop : operation = newOpPtr; rotate_left; simp [hop] + rw [← OperationPtr.getNumRegions!_eq_getNumRegions (by grind)] + simp only [hop, ↓reduceIte, getNumRegions!_initOpResults, Nat.zero_add] + simp_getset + simp @[grind =>, simp_getset] theorem OperationPtr.getRegion!_createOp {operation : OperationPtr} : @@ -597,7 +857,19 @@ theorem OperationPtr.getRegion!_createOp {operation : OperationPtr} : operation.getRegion! ctx' idx = if _ : operation = newOp ∧ idx < regions.size then regions[idx] else operation.getRegion! ctx idx := by - grind (gen := 20) + simp only [Rewriter.createOp] + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + by_cases hop : operation = newOpPtr <;> simp [hop] + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset + by_cases hop : operation = newOpPtr <;> simp [hop] /- BlockOperandPtrPtr.get!_createOp is too complex to be expressed, and should not be needed in practice, @@ -609,7 +881,17 @@ theorem BlockPtr.getNumArguments!_createOp {block : BlockPtr} : Rewriter.createOp ctx opType resultTypes operands blockOperands regions properties insertionPoint h₁ h₂ h₃ h₄ h₅ = some (ctx', newOp) → block.getNumArguments! ctx' = block.getNumArguments! ctx := by - grind (gen := 20) + simp only [Rewriter.createOp] + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset /- BlockArgumentPtr.get!_createOp is too complex to be expressed, and should not be needed in practice, @@ -621,14 +903,34 @@ theorem RegionPtr.firstBlock!_createOp {region : RegionPtr} : Rewriter.createOp ctx opType resultTypes operands blockOperands regions properties insertionPoint h₁ h₂ h₃ h₄ h₅ = some (ctx', newOp) → (region.get! ctx').firstBlock = (region.get! ctx).firstBlock := by - grind (gen := 20) + simp only [Rewriter.createOp] + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset @[simp, grind =>, simp_getset] theorem RegionPtr.lastBlock!_createOp {region : RegionPtr} : Rewriter.createOp ctx opType resultTypes operands blockOperands regions properties insertionPoint h₁ h₂ h₃ h₄ h₅ = some (ctx', newOp) → (region.get! ctx').lastBlock = (region.get! ctx).lastBlock := by - grind (gen := 20) + simp only [Rewriter.createOp] + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset @[simp, grind =>, simp_getset] theorem RegionPtr.parent!_createOp {region : RegionPtr} : @@ -636,7 +938,31 @@ theorem RegionPtr.parent!_createOp {region : RegionPtr} : insertionPoint h₁ h₂ h₃ h₄ h₅ = some (ctx', newOp) → (region.get! ctx').parent = if region ∈ regions then some newOp else (region.get! ctx).parent := by - grind (gen := 20) + simp only [Rewriter.createOp] + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + rw [←OperationPtr.getNumRegions!_eq_getNumRegions (by grind)] + simp_getset + simp only [↓reduceIte, Nat.zero_le, true_and] + congr + have := Array.exists_mem_iff_exists_getElem (xs := regions) (P := fun r => r = region) + simp only [exists_eq_right] at this + simp [this] + · simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset + rw [←OperationPtr.getNumRegions!_eq_getNumRegions (by grind)] + simp_getset + simp only [↓reduceIte, Nat.zero_le, true_and] + congr + have := Array.exists_mem_iff_exists_getElem (xs := regions) (P := fun r => r = region) + simp only [exists_eq_right] at this + simp [this] /- ValuePtr.getFirstUse!_createOp is too complex to be expressed, and should not be needed in practice, @@ -654,7 +980,21 @@ theorem ValuePtr.getType!_createOp {value : ValuePtr} : resultTypes[opRes.index] else value.getType! ctx | .blockArgument _ => value.getType! ctx := by - grind (gen := 20) + simp only [Rewriter.createOp] + split; simp; next ctx₁ newOpPtr hCreateEmpty => + split; simp; next rename_i ctx₂ hInitRegions => + split + next insertPoint => + split; simp; next ctx₃ hInsert => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp]; intro rfl rfl + simp_getset + simp only [↓reduceIte, Nat.zero_le, and_true] + cases value <;> simp + next => + simp only [Option.some.injEq, Prod.mk.injEq, and_imp] + intro rfl rfl + simp_getset + cases value <;> simp /- OpOperandPtrPtr.get!_createOp is too complex to be expressed, and should not be needed in practice, @@ -697,16 +1037,53 @@ theorem Rewriter.createOp_inBounds (ptr : GenericPtr) blockOperandPtr.InBounds ctx | _ => ptr.InBounds ctx ∨ ptr = .operation newOp := by simp only [createOp] at h + split at h; simp at h + rename_i ctx₁ newOpPtr hnew + split at h; simp at h + rename_i ctx₂ hreg split at h - · simp at h - · rename_i ctx₁ newOpPtr hnew - split at h - · simp at h - · rename_i ctx₂ hreg - split at h - · split at h - · simp at h - · cases ptr <;> grind [createEmptyOp] - · cases ptr <;> grind [createEmptyOp] + · split at h; simp at h; rename_i ctx₂ hctx₂ + simp only [Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨h₁, h₂⟩ := h + subst h₁ h₂ + simp only [insertOp_inBounds_mono _ hctx₂, Rewriter.initBlockOperands_inBounds] + simp_getset + simp only [↓reduceIte, Nat.zero_add] + cases ptr <;> simp only [← initOpRegions_inBounds hreg, initOpResults_inBounds, + Rewriter.createEmptyOp_genericPtr_mono _ hnew] + case opResult => simp_getset; simp + case opOperand => simp + case blockOperand => simp + case blockOperandPtr opPtr => cases opPtr <;> simp + case value ptr => + cases ptr + · simp_getset; simp + · simp + case opOperandPtr opPtr => + rcases opPtr with _ | ⟨_ | _⟩ + · simp + · simp_getset; simp + · simp + · simp only [Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨h₁, h₂⟩ := h + subst h₁ h₂ + simp only [Rewriter.initBlockOperands_inBounds] + simp_getset + simp only [↓reduceIte, Nat.zero_add] + cases ptr <;> simp only [← initOpRegions_inBounds hreg, initOpResults_inBounds, + Rewriter.createEmptyOp_genericPtr_mono _ hnew] + case opResult => simp_getset; simp + case opOperand => simp + case blockOperand => simp + case blockOperandPtr opPtr => cases opPtr <;> simp + case value ptr => + cases ptr + · simp_getset; simp + · simp + case opOperandPtr opPtr => + rcases opPtr with _ | ⟨_ | _⟩ + · simp + · simp_getset; simp + · simp end Veir