From 409cbe1da9584df23486ef057f609372d6ae9843 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 13 Sep 2025 21:44:55 -0700 Subject: [PATCH] fix: make `rw` collect only new goals, occurs check (#10306) This PR fixes a few bugs in the `rw` tactic: it could "steal" goals because they appear in the type of the rewrite, it did not do an occurs check, and new proof goals would not be synthetic opaque. This PR also lets the `rfl` tactic assign synthetic opaque metavariables so that it is equivalent to `exact rfl`. Implementation note: filtering old vs new is not sufficient. This PR partially addresses the bug where the rw tactic creates natural metavariables for each of the goals; now new proof goals are synthetic opaque. Metaprogramming API: Instead of `Lean.MVarId.rewrite` prefer `Lean.Elab.Tactic.elabRewrite` for elaborating rewrite theorems and applying rewrites to expressions. Closes #10172 --- src/Init/Data/Array/Lemmas.lean | 6 +- src/Init/Data/Fin/Fold.lean | 2 +- src/Init/Data/List/Lemmas.lean | 6 +- src/Init/Data/List/Nat/TakeDrop.lean | 5 +- src/Lean/Elab/Tactic/BuiltinTactic.lean | 3 +- src/Lean/Elab/Tactic/Conv/Rewrite.lean | 13 +- src/Lean/Elab/Tactic/Rewrite.lean | 50 +++++-- src/Lean/Meta/Tactic/Rewrite.lean | 3 +- src/Std/Data/DTreeMap/Internal/Lemmas.lean | 4 +- src/Std/Sat/AIG/CachedGatesLemmas.lean | 8 +- src/Std/Sat/AIG/If.lean | 18 ++- src/Std/Sat/AIG/RefVecOperator/Map.lean | 20 ++- src/Std/Sat/AIG/RefVecOperator/Zip.lean | 14 +- .../Bitblast/BVExpr/Circuit/Impl/Expr.lean | 18 +-- .../BVExpr/Circuit/Impl/Operations/Add.lean | 20 +-- .../Bitblast/BVExpr/Circuit/Lemmas.lean | 16 ++- .../Bitblast/BVExpr/Circuit/Lemmas/Const.lean | 4 +- .../Bitblast/BVExpr/Circuit/Lemmas/Expr.lean | 8 +- .../BVExpr/Circuit/Lemmas/Operations/Add.lean | 20 ++- .../Circuit/Lemmas/Operations/Extract.lean | 4 +- .../BVExpr/Circuit/Lemmas/Operations/Mul.lean | 19 ++- .../Circuit/Lemmas/Operations/Replicate.lean | 3 +- .../Circuit/Lemmas/Operations/RotateLeft.lean | 8 +- .../Lemmas/Operations/RotateRight.lean | 8 +- .../Circuit/Lemmas/Operations/ShiftLeft.lean | 14 +- .../Circuit/Lemmas/Operations/ShiftRight.lean | 26 ++-- .../Circuit/Lemmas/Operations/Udiv.lean | 133 ++++++++++++++---- .../BVExpr/Circuit/Lemmas/Operations/Ult.lean | 3 +- .../Circuit/Lemmas/Operations/Umod.lean | 9 +- .../Circuit/Lemmas/Operations/ZeroExtend.lean | 12 +- .../Bitblast/BVExpr/Circuit/Lemmas/Var.lean | 9 +- .../LRAT/Internal/Formula/RupAddResult.lean | 6 +- tests/lean/run/10172.lean | 33 +++++ 33 files changed, 339 insertions(+), 186 deletions(-) create mode 100644 tests/lean/run/10172.lean diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 57364dac39..5faeff7aec 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -1478,7 +1478,7 @@ theorem forall_mem_filter {p : α → Bool} {xs : Array α} {P : α → Prop} : theorem getElem?_filter {xs : Array α} {p : α → Bool} {i : Nat} (h : i < (xs.filter p).size) (w : (xs.filter p)[i]? = some a) : p a := by - rw [getElem?_eq_getElem] at w + rw [getElem?_eq_getElem h] at w simp only [Option.some.injEq] at w rw [← w] apply getElem_filter h @@ -4470,10 +4470,10 @@ theorem back!_eq_back? [Inhabited α] {xs : Array α} : xs.back! = xs.back?.getD theorem getElem?_push_lt {xs : Array α} {x : α} {i : Nat} (h : i < xs.size) : (xs.push x)[i]? = some xs[i] := by - rw [getElem?_pos, getElem_push_lt] + rw [getElem?_pos (xs.push x) i (size_push _ ▸ Nat.lt_succ_of_lt h), getElem_push_lt] theorem getElem?_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size]? = some x := by - rw [getElem?_pos, getElem_push_eq] + rw [getElem?_pos (xs.push x) xs.size (size_push _ ▸ Nat.lt_succ_self xs.size), getElem_push_eq] @[simp] theorem getElem?_size {xs : Array α} : xs[xs.size]? = none := by simp only [getElem?_def, Nat.lt_irrefl, dite_false] diff --git a/src/Init/Data/Fin/Fold.lean b/src/Init/Data/Fin/Fold.lean index 1b6b9722f1..5b6c9fdb29 100644 --- a/src/Init/Data/Fin/Fold.lean +++ b/src/Init/Data/Fin/Fold.lean @@ -122,7 +122,7 @@ private theorem foldlM_loop [Monad m] (f : α → Fin (n+1) → m α) (x) (h : i rw [foldlM_loop_lt _ _ h', foldlM_loop]; rfl else cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h') - rw [foldlM_loop_lt] + rw [foldlM_loop_lt _ _ h] congr; funext rw [foldlM_loop_eq, foldlM_loop_eq] termination_by n - i diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 3a33e1a81f..1e3a671b76 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -939,8 +939,8 @@ theorem getLast!_eq_getElem! [Inhabited α] {l : List α} : l.getLast! = l[l.len | nil => simp | cons _ _ => apply getLast!_of_getLast? - rw [getElem!_pos, getElem_cons_length (h := by simp)] - rfl + rw [getLast?_eq_getElem?] + simp /-! ## Head and tail -/ @@ -1344,7 +1344,7 @@ grind_pattern getElem_filter => (xs.filter p)[i] theorem getElem?_filter {xs : List α} {p : α → Bool} {i : Nat} (h : i < (xs.filter p).length) (w : (xs.filter p)[i]? = some a) : p a := by - rw [getElem?_eq_getElem] at w + rw [getElem?_eq_getElem h] at w simp only [Option.some.injEq] at w rw [← w] apply getElem_filter h diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean index 440b952232..06e3c2b1ce 100644 --- a/src/Init/Data/List/Nat/TakeDrop.lean +++ b/src/Init/Data/List/Nat/TakeDrop.lean @@ -567,9 +567,10 @@ theorem getElem_zipWith {f : α → β → γ} {l : List α} {l' : List β} f (l[i]'(lt_length_left_of_zipWith h)) (l'[i]'(lt_length_right_of_zipWith h)) := by rw [← Option.some_inj, ← getElem?_eq_getElem, getElem?_zipWith_eq_some] + have := lt_length_right_of_zipWith h exact - ⟨l[i]'(lt_length_left_of_zipWith h), l'[i]'(lt_length_right_of_zipWith h), - by rw [getElem?_eq_getElem], by rw [getElem?_eq_getElem]; exact ⟨rfl, rfl⟩⟩ + ⟨l[i]'(lt_length_left_of_zipWith h), l'[i], + by rw [getElem?_eq_getElem], by rw [getElem?_eq_getElem this]; exact ⟨rfl, rfl⟩⟩ theorem zipWith_eq_zipWith_take_min : ∀ {l₁ : List α} {l₂ : List β}, zipWith f l₁ l₂ = zipWith f (l₁.take (min l₁.length l₂.length)) (l₂.take (min l₁.length l₂.length)) diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index 7d2cb96d14..4a0fd95340 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -284,7 +284,8 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit := liftMetaTactic fun mvarId => do mvarId.contradiction; pure [] @[builtin_tactic Lean.Parser.Tactic.eqRefl] def evalRefl : Tactic := fun _ => - liftMetaTactic fun mvarId => do mvarId.refl; pure [] + -- Allow assigning synthetic opaque so that it is as capable as `exact rfl`. + liftMetaTactic fun mvarId => do withAssignableSyntheticOpaque mvarId.refl; pure [] @[builtin_tactic Lean.Parser.Tactic.intro] def evalIntro : Tactic := fun stx => do match stx with diff --git a/src/Lean/Elab/Tactic/Conv/Rewrite.lean b/src/Lean/Elab/Tactic/Conv/Rewrite.lean index fa535095d1..934530d415 100644 --- a/src/Lean/Elab/Tactic/Conv/Rewrite.lean +++ b/src/Lean/Elab/Tactic/Conv/Rewrite.lean @@ -6,7 +6,6 @@ Authors: Leonardo de Moura module prelude -public import Lean.Meta.Tactic.Rewrite public import Lean.Elab.Tactic.Rewrite public import Lean.Elab.Tactic.Conv.Basic @@ -17,11 +16,11 @@ open Meta @[builtin_tactic Lean.Parser.Tactic.Conv.rewrite] def evalRewrite : Tactic := fun stx => do let config ← Tactic.elabRewriteConfig stx[1] - withRWRulesSeq stx[0] stx[2] fun symm term => do - Term.withSynthesize <| withMainContext do - let e ← elabTerm term none true - let r ← (← getMainGoal).rewrite (← getLhs) e symm (config := config) - updateLhs r.eNew r.eqProof - replaceMainGoal ((← getMainGoal) :: r.mvarIds) + withRWRulesSeq stx[0] stx[2] fun symm term => withMainContext do + let r ← Term.withSynthesize do + elabRewrite (← getMainGoal) (← getLhs) term symm (config := config) + let r ← finishElabRewrite r + updateLhs r.eNew r.eqProof + replaceMainGoal ((← getMainGoal) :: r.mvarIds) end Lean.Elab.Tactic.Conv diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean index f0a4ca1358..04274f20e4 100644 --- a/src/Lean/Elab/Tactic/Rewrite.lean +++ b/src/Lean/Elab/Tactic/Rewrite.lean @@ -17,25 +17,53 @@ public section namespace Lean.Elab.Tactic open Meta +/-- +Runs `Lean.MVarId.rewrite`, and also handles filtering out the old metavariables in the rewrite result. +This should be used from within `withSynthesize`. +Use `finishElabRewrite` once elaboration is complete to make final updates to `RewriteResult`. +-/ +def elabRewrite (mvarId : MVarId) (e : Expr) (stx : Syntax) + (symm : Bool := false) (config := { : Rewrite.Config }) : TacticM RewriteResult := do + let mvarCounterSaved := (← getMCtx).mvarCounter + let thm ← elabTerm stx none true + if thm.hasSyntheticSorry then + throwAbortTactic + unless ← occursCheck mvarId thm do + throwErrorAt stx "Occurs check failed: Expression{indentExpr thm}\ncontains the goal {Expr.mvar mvarId}" + let r ← mvarId.rewrite e thm symm (config := config) + let mctx ← getMCtx + let mvarIds := r.mvarIds.filter fun mvarId => (mctx.getDecl mvarId |>.index) >= mvarCounterSaved + + return { r with mvarIds } + +/-- +Makes new goals be synthetic opaque, to be done once elaboration of the rewrite theorem is complete. + +Workaround note: we are only doing this for proof goals, not data goals, +since there are many downstream cases of tactic proofs that later assign data goals by unification. +-/ +def finishElabRewrite (r : RewriteResult) : MetaM RewriteResult := do + let mvarIds ← r.mvarIds.filterM (not <$> ·.isAssigned) + mvarIds.forM fun newMVarId => newMVarId.withContext do + if ← Meta.isProp (← newMVarId.getType) then + newMVarId.setKind .syntheticOpaque + return { r with mvarIds } + def rewriteTarget (stx : Syntax) (symm : Bool) (config : Rewrite.Config := {}) : TacticM Unit := do - Term.withSynthesize <| withMainContext do - let e ← elabTerm stx none true - if e.hasSyntheticSorry then - throwAbortTactic - let r ← (← getMainGoal).rewrite (← getMainTarget) e symm (config := config) - let mvarId' ← (← getMainGoal).replaceTargetEq r.eNew r.eqProof - replaceMainGoal (mvarId' :: r.mvarIds) + let r ← Term.withSynthesize <| withMainContext do + elabRewrite (← getMainGoal) (← getMainTarget) stx symm (config := config) + let r ← finishElabRewrite r + let mvarId' ← (← getMainGoal).replaceTargetEq r.eNew r.eqProof + replaceMainGoal (mvarId' :: r.mvarIds) def rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Rewrite.Config := {}) : TacticM Unit := withMainContext do -- Note: we cannot execute `replaceLocalDecl` inside `Term.withSynthesize`. -- See issues #2711 and #2727. let rwResult ← Term.withSynthesize <| withMainContext do - let e ← elabTerm stx none true - if e.hasSyntheticSorry then - throwAbortTactic let localDecl ← fvarId.getDecl - (← getMainGoal).rewrite localDecl.type e symm (config := config) + elabRewrite (← getMainGoal) localDecl.type stx symm (config := config) + let rwResult ← finishElabRewrite rwResult let replaceResult ← (← getMainGoal).replaceLocalDecl fvarId rwResult.eNew rwResult.eqProof replaceMainGoal (replaceResult.mvarId :: rwResult.mvarIds) diff --git a/src/Lean/Meta/Tactic/Rewrite.lean b/src/Lean/Meta/Tactic/Rewrite.lean index 531c51120b..723b3ced35 100644 --- a/src/Lean/Meta/Tactic/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Rewrite.lean @@ -24,7 +24,8 @@ structure RewriteResult where mvarIds : List MVarId -- new goals /-- -Rewrite goal `mvarId` +Rewrite `e` using `heq` in the context of `mvarId`. +Returns the result of the rewrite, the metavariable `mvarId` is not assigned. -/ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr) (symm : Bool := false) (config := { : Rewrite.Config }) : MetaM RewriteResult := diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index 98ad00628b..2757c188ae 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -394,7 +394,7 @@ theorem containsThenInsert_fst [TransOrd α] (h : t.WF) {k : α} {v : β k} : theorem containsThenInsert!_fst [TransOrd α] (h : t.WF) {k : α} {v : β k} : (t.containsThenInsert! k v).1 = t.contains k := by - rw [containsThenInsert!_fst_eq_containsThenInsert_fst, containsThenInsert_fst h] + rw [containsThenInsert!_fst_eq_containsThenInsert_fst _ h.balanced, containsThenInsert_fst h] theorem containsThenInsert_snd [TransOrd α] (h : t.WF) {k : α} {v : β k} : (t.containsThenInsert k v h.balanced).2.impl = (t.insert k v h.balanced).impl := by @@ -411,7 +411,7 @@ theorem containsThenInsertIfNew_fst [TransOrd α] (h : t.WF) {k : α} {v : β k} theorem containsThenInsertIfNew!_fst [TransOrd α] (h : t.WF) {k : α} {v : β k} : (t.containsThenInsertIfNew! k v).1 = t.contains k := by - rw [containsThenInsertIfNew!_fst_eq_containsThenInsertIfNew_fst, containsThenInsertIfNew_fst h] + rw [containsThenInsertIfNew!_fst_eq_containsThenInsertIfNew_fst _ h.balanced, containsThenInsertIfNew_fst h] theorem containsThenInsertIfNew_snd [TransOrd α] (h : t.WF) {k : α} {v : β k} : (t.containsThenInsertIfNew k v h.balanced).2.impl = (t.insertIfNew k v h.balanced).impl := by diff --git a/src/Std/Sat/AIG/CachedGatesLemmas.lean b/src/Std/Sat/AIG/CachedGatesLemmas.lean index d3ae258b8a..c39d853c88 100644 --- a/src/Std/Sat/AIG/CachedGatesLemmas.lean +++ b/src/Std/Sat/AIG/CachedGatesLemmas.lean @@ -124,8 +124,8 @@ theorem mkXorCached_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : id simp only [mkXorCached] rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)] rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)] - · rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)] - apply LawfulOperator.lt_size_of_lt_aig_size + rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)] + · apply LawfulOperator.lt_size_of_lt_aig_size assumption · apply LawfulOperator.lt_size_of_lt_aig_size apply LawfulOperator.lt_size_of_lt_aig_size @@ -159,8 +159,8 @@ theorem mkBEqCached_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : id simp only [mkBEqCached] rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)] rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)] - · rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)] - apply LawfulOperator.lt_size_of_lt_aig_size + rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)] + · apply LawfulOperator.lt_size_of_lt_aig_size assumption · apply LawfulOperator.lt_size_of_lt_aig_size apply LawfulOperator.lt_size_of_lt_aig_size diff --git a/src/Std/Sat/AIG/If.lean b/src/Std/Sat/AIG/If.lean index 767a58207e..1d81490302 100644 --- a/src/Std/Sat/AIG/If.lean +++ b/src/Std/Sat/AIG/If.lean @@ -103,12 +103,12 @@ theorem denote_mkIfCached {aig : AIG α} {input : TernaryInput aig} : simp only [TernaryInput.cast, Ref.cast_eq, denote_mkOrCached, denote_projected_entry, denote_mkAndCached, denote_mkNotCached] congr 2 - · rw [LawfulOperator.denote_mem_prefix] + · rw [LawfulOperator.denote_mem_prefix (LawfulOperator.lt_size ..)] rw [LawfulOperator.denote_mem_prefix] · simp · simp [Ref.hgate] · rw [LawfulOperator.denote_mem_prefix] - · rw [LawfulOperator.denote_mem_prefix] + · rw [LawfulOperator.denote_mem_prefix (LawfulOperator.lt_size_of_lt_aig_size _ _ input.rhs.hgate)] rw [LawfulOperator.denote_mem_prefix] namespace RefVec @@ -198,13 +198,11 @@ theorem go_get_aux {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (d split at hgo · rw [← hgo] intros - rw [go_get_aux] - rw [AIG.RefVec.get_push_ref_lt] - · simp only [Ref.cast, Ref.mk.injEq] - rw [AIG.RefVec.get_cast] - · simp - · assumption - · apply go_le_size + rw [go_get_aux (hidx := Nat.lt_succ_of_lt hidx) (hfoo := go_le_size ..)] + rw [AIG.RefVec.get_push_ref_lt (hidx := hidx)] + simp only [Ref.cast, Ref.mk.injEq] + rw [AIG.RefVec.get_cast] + simp · rw [← hgo] simp only [Nat.le_refl, get] have : curr = w := by omega @@ -261,7 +259,7 @@ theorem denote_go {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (di | inl heq => subst heq rw [← hgo] - rw [go_get] + rw [go_get]; case hidx => omega rw [AIG.RefVec.get_push_ref_eq'] · rw [go_denote_mem_prefix] · simp diff --git a/src/Std/Sat/AIG/RefVecOperator/Map.lean b/src/Std/Sat/AIG/RefVecOperator/Map.lean index 2826d86994..d3bdb9c2f2 100644 --- a/src/Std/Sat/AIG/RefVecOperator/Map.lean +++ b/src/Std/Sat/AIG/RefVecOperator/Map.lean @@ -148,12 +148,11 @@ theorem go_get_aux {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVe · dsimp only at hgo rw [← hgo] intro hfoo - rw [go_get_aux] - rw [AIG.RefVec.get_push_ref_lt] + rw [go_get_aux]; case hidx => omega + rw [AIG.RefVec.get_push_ref_lt (hidx := hidx)] · simp only [Ref.cast, Ref.mk.injEq] rw [AIG.RefVec.get_cast] - · simp - · assumption + simp · apply go_le_size · dsimp only at hgo rw [← hgo] @@ -209,13 +208,12 @@ theorem denote_go {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVec cases Nat.eq_or_lt_of_le hidx2 with | inl heq => rw [← hgo] - rw [go_get] - rw [AIG.RefVec.get_push_ref_eq'] - · simp only [← heq] - rw [go_denote_mem_prefix] - · simp - · simp [Ref.hgate] - · rw [heq] + rw [go_get]; case hidx => omega + rw [AIG.RefVec.get_push_ref_eq' (hidx := heq.symm)] + simp only [← heq] + rw [go_denote_mem_prefix] + · simp + · simp [Ref.hgate] | inr hlt => rw [← hgo] rw [denote_go] diff --git a/src/Std/Sat/AIG/RefVecOperator/Zip.lean b/src/Std/Sat/AIG/RefVecOperator/Zip.lean index 61d6973715..d6663baf49 100644 --- a/src/Std/Sat/AIG/RefVecOperator/Zip.lean +++ b/src/Std/Sat/AIG/RefVecOperator/Zip.lean @@ -197,13 +197,11 @@ theorem go_get_aux {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVe · dsimp only at hgo rw [← hgo] intro hfoo - rw [go_get_aux] - rw [AIG.RefVec.get_push_ref_lt] - · simp only [Ref.cast, Ref.mk.injEq] - rw [AIG.RefVec.get_cast] - · simp - · assumption - · apply go_le_size + rw [go_get_aux (hfoo := go_le_size ..)]; case hidx => omega + rw [AIG.RefVec.get_push_ref_lt (hidx := hidx)] + simp only [Ref.cast, Ref.mk.injEq] + rw [AIG.RefVec.get_cast] + simp · dsimp only at hgo rw [← hgo] simp only [Nat.le_refl, get, Ref.cast_eq, Ref.mk.injEq, true_implies] @@ -262,7 +260,7 @@ theorem denote_go {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVec cases Nat.eq_or_lt_of_le hidx2 with | inl heq => rw [← hgo] - rw [go_get] + rw [go_get]; case hidx => omega rw [AIG.RefVec.get_push_ref_eq'] · simp only [← heq] rw [go_denote_mem_prefix] diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean index 82b38302c0..9be7f49fee 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean @@ -333,14 +333,14 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : | .and | .or | .xor => rw [AIG.RefVec.zip_decl_eq] rw [goCache_decl_eq, goCache_decl_eq] - · omega + · exact Nat.lt_of_lt_of_le h1 hl · apply Nat.lt_of_lt_of_le · exact h1 · apply Nat.le_trans <;> assumption | .add | .mul | .udiv | .umod => rw [AIG.LawfulVecOperator.decl_eq] rw [goCache_decl_eq, goCache_decl_eq] - · omega + · exact Nat.lt_of_lt_of_le h1 hl · apply Nat.lt_of_lt_of_le · exact h1 · apply Nat.le_trans <;> assumption @@ -350,13 +350,13 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : rw [AIG.LawfulVecOperator.decl_eq] rw [goCache_decl_eq] have := (goCache aig expr cache).result.property - omega + exact Nat.lt_of_lt_of_le h1 this next lhsExpr rhsExpr h => have hl := (goCache aig lhsExpr cache).result.property have hr := (goCache (goCache aig lhsExpr cache).1.1.aig rhsExpr (goCache aig lhsExpr cache).cache).result.property rw [AIG.LawfulVecOperator.decl_eq] rw [goCache_decl_eq, goCache_decl_eq] - · omega + · exact Nat.lt_of_lt_of_le h1 hl · apply Nat.lt_of_lt_of_le · exact h1 · apply Nat.le_trans <;> assumption @@ -364,18 +364,18 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : rw [AIG.LawfulVecOperator.decl_eq (f := blastReplicate)] rw [goCache_decl_eq] have := (goCache aig inner cache).result.property - omega + exact Nat.lt_of_lt_of_le h1 this next hi lo inner => rw [AIG.LawfulVecOperator.decl_eq (f := blastExtract)] rw [goCache_decl_eq] have := (goCache aig inner cache).result.property - omega + exact Nat.lt_of_lt_of_le h1 this next rhsExpr lhsExpr => have hl := (goCache aig lhsExpr cache).result.property have hr := (goCache (goCache aig lhsExpr cache).1.1.aig rhsExpr (goCache aig lhsExpr cache).cache).result.property rw [AIG.LawfulVecOperator.decl_eq (f := blastShiftLeft)] rw [goCache_decl_eq, goCache_decl_eq] - · omega + · exact Nat.lt_of_lt_of_le h1 hl · apply Nat.lt_of_lt_of_le · exact h1 · apply Nat.le_trans <;> assumption @@ -384,7 +384,7 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : have hr := (goCache (goCache aig lhsExpr cache).1.1.aig rhsExpr (goCache aig lhsExpr cache).cache).result.property rw [AIG.LawfulVecOperator.decl_eq (f := blastShiftRight)] rw [goCache_decl_eq, goCache_decl_eq] - · omega + · exact Nat.lt_of_lt_of_le h1 hl · apply Nat.lt_of_lt_of_le · exact h1 · apply Nat.le_trans <;> assumption @@ -393,7 +393,7 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : have hr := (goCache (goCache aig lhsExpr cache).1.1.aig rhsExpr (goCache aig lhsExpr cache).cache).result.property rw [AIG.LawfulVecOperator.decl_eq (f := blastArithShiftRight)] rw [goCache_decl_eq, goCache_decl_eq] - · omega + · exact Nat.lt_of_lt_of_le h1 hl · apply Nat.lt_of_lt_of_le · exact h1 · apply Nat.le_trans <;> assumption diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean index 6fd4874e8f..4a43303a78 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean @@ -220,17 +220,19 @@ theorem go_decl_eq (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : AIG.R unfold go at hgo dsimp only at hgo split at hgo - · rw [← hgo] - intros - rw [go_decl_eq] + next h => + rw [← hgo] + intro idx h1 h2 + have h3 : idx < (mkFullAdderOut aig { lhs := lhs.get curr h, rhs := rhs.get curr h, cin := cin }).aig.decls.size := by + apply AIG.LawfulOperator.lt_size_of_lt_aig_size + exact h1 + have h4 : idx < (mkFullAdder aig { lhs := lhs.get curr h, rhs := rhs.get curr h, cin := cin }).aig.decls.size := by + apply AIG.LawfulOperator.lt_size_of_lt_aig_size + exact h3 + rw [go_decl_eq (w := w) (curr := curr + 1) (h1 := h4)] unfold mkFullAdder - rw [AIG.LawfulOperator.decl_eq (f := mkFullAdderCarry)] + rw [AIG.LawfulOperator.decl_eq (f := mkFullAdderCarry) (h1 := h3)] rw [AIG.LawfulOperator.decl_eq (f := mkFullAdderOut)] - · apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderOut) - assumption - · apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderCarry) - apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderOut) - assumption · simp [← hgo] termination_by w - curr diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean index fa1d2e9f82..a9bf1c6dcf 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean @@ -82,7 +82,7 @@ theorem go_eval_eq_eval (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExp all_goals simp [go, Gate.eval] congr 1 - · rw [go_denote_mem_prefix] + · rw [go_denote_mem_prefix (hstart := Ref.hgate _)] apply lih exact hinv · apply rih @@ -92,13 +92,15 @@ theorem go_eval_eq_eval (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExp simp only [go, Ref.cast_eq, denote_mkIfCached, denote_projected_entry, eval_ite, Bool.ite_eq_cond_iff] apply ite_congr - · rw [go_denote_mem_prefix] - rw [go_denote_mem_prefix] - · specialize dih _ _ hinv - simp [dih] - · simp [Ref.hgate] + · rw [go_denote_mem_prefix (hstart := ?h)] + case h => + apply go_lt_size_of_lt_aig_size + exact Ref.hgate _ + rw [go_denote_mem_prefix (hstart := Ref.hgate _)] + specialize dih _ _ hinv + simp [dih] · intro h - rw [go_denote_mem_prefix] + rw [go_denote_mem_prefix (hstart := Ref.hgate _)] apply lih apply go_Inv_of_Inv exact hinv diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean index 03f1058bbd..4636917ba2 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean @@ -41,7 +41,7 @@ theorem go_get_aux (aig : AIG α) (c : BitVec w) (curr : Nat) (hcurr : curr ≤ · dsimp only at hgo rw [← hgo] intro hfoo - rw [go_get_aux] + rw [go_get_aux (hfoo := hfoo) (hidx := Nat.lt_succ_of_lt hidx)] rw [AIG.RefVec.get_push_ref_lt] · dsimp only at hgo rw [← hgo] @@ -74,7 +74,7 @@ theorem go_denote_eq (aig : AIG α) (c : BitVec w) (assign : α → Bool) cases Nat.eq_or_lt_of_le hidx2 with | inl heq => rw [← hgo] - rw [go_get] + rw [go_get]; case hidx => omega rw [AIG.RefVec.get_push_ref_eq'] · rw [← heq] simp diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean index 4d27259e15..38e30ca329 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean @@ -313,7 +313,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) simp only [RefVec.denote_zip, RefVec.get_cast, Ref.cast_eq, denote_mkAndCached, eval_bin, BVBinOp.eval_and, BitVec.getLsbD_and] congr 1 - · rw [goCache_denote_mem_prefix] + · rw [goCache_denote_mem_prefix (hstart := Ref.hgate _)] rw [goCache_denote_eq] exact hinv · rw [goCache_denote_eq] @@ -323,7 +323,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) simp only [RefVec.denote_zip, RefVec.get_cast, Ref.cast_eq, denote_mkOrCached, eval_bin, BVBinOp.eval_or, BitVec.getLsbD_or] congr 1 - · rw [goCache_denote_mem_prefix] + · rw [goCache_denote_mem_prefix (hstart := Ref.hgate _)] rw [goCache_denote_eq] exact hinv · rw [goCache_denote_eq] @@ -333,7 +333,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) simp only [RefVec.denote_zip, RefVec.get_cast, Ref.cast_eq, denote_mkXorCached, eval_bin, BVBinOp.eval_xor, BitVec.getLsbD_xor] congr 1 - · rw [goCache_denote_mem_prefix] + · rw [goCache_denote_mem_prefix (hstart := Ref.hgate _)] rw [goCache_denote_eq] exact hinv · rw [goCache_denote_eq] @@ -444,7 +444,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) · rw [goCache_denote_eq] apply goCache_Inv_of_Inv exact hinv - · rw [goCache_denote_mem_prefix] + · rw [goCache_denote_mem_prefix (hstart := Ref.hgate _)] rw [goCache_denote_eq] exact hinv next h => diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean index 52f67b9797..6d1c306c6f 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean @@ -75,7 +75,7 @@ theorem mkFullAdder_denote_mem_prefix (aig : AIG α) (input : FullAdderInput aig ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by unfold mkFullAdder dsimp only - rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)] + rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry) (LawfulOperator.lt_size_of_lt_aig_size aig input hstart)] rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderOut)] theorem go_denote_mem_prefix (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref aig) @@ -110,13 +110,11 @@ theorem go_get_aux (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref a split at hgo · rw [← hgo] intro hfoo - rw [go_get_aux] - rw [AIG.RefVec.get_push_ref_lt] - · simp only [Ref.cast, Ref.mk.injEq] - rw [AIG.RefVec.get_cast] - · simp - · assumption - · apply go_le_size + rw [go_get_aux (hidx := Nat.lt_succ_of_lt hidx) (hfoo := go_le_size ..)] + rw [AIG.RefVec.get_push_ref_lt (hidx := hidx)] + simp only [Ref.cast, Ref.mk.injEq] + rw [AIG.RefVec.get_cast] + simp · rw [← hgo] simp only [Nat.le_refl] obtain rfl : curr = w := by omega @@ -196,9 +194,9 @@ theorem go_denote_eq (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref simp only [Ref.cast_eq, denote_projected_entry, denote_mkFullAdderCarry, FullAdderInput.lhs_cast, FullAdderInput.rhs_cast, FullAdderInput.cin_cast, BitVec.carry_succ] - rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderOut)] - rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderOut)] - rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderOut)] + rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderOut) (h := Ref.hgate _)] + rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderOut) (h := Ref.hgate _)] + rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderOut) (h := Ref.hgate _)] rw [hleft, hright, hcin] simp [atLeastTwo_eq_halfAdder] · omega diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean index d8c4f28172..6241193f62 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean @@ -37,7 +37,7 @@ theorem go_get_aux (aig : AIG α) (input : RefVec aig w) (lo : Nat) (curr : Nat) split at hgo · dsimp only at hgo rw [← hgo] - rw [go_get_aux] + rw [go_get_aux]; case hidx1 => omega rw [AIG.RefVec.get_push_ref_lt] · dsimp only at hgo rw [← hgo] @@ -62,7 +62,7 @@ theorem go_get (aig : AIG α) (input : RefVec aig w) (lo : Nat) (curr : Nat) · rw [← hgo] cases Nat.eq_or_lt_of_le hidx2 with | inl heq => - rw [go_get_aux] + rw [go_get_aux]; case hidx1 => omega rw [AIG.RefVec.get_push_ref_eq'] · simp [heq] · simp [heq] diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean index 7bfebb9856..d7e7b94940 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean @@ -61,7 +61,7 @@ theorem go_denote_eq {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr + 1 ≤ · intro idx hidx rw [BitVec.mulRec_succ_eq] have : rexpr.getLsbD (curr + 1) = false := by - rw [← hright] + rw [← hright _ ‹curr + 1 < w›] exact of_isConstant hconstant simp [this, hacc] · dsimp only at hgo @@ -74,12 +74,18 @@ theorem go_denote_eq {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr + 1 ≤ rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastAdd)] rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)] rw [hleft] + all_goals + repeat apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + exact Ref.hgate _ · intro idx hidx simp only [RefVec.get_cast, Ref.cast_eq] rw [AIG.LawfulVecOperator.denote_mem_prefix (f := RefVec.ite)] rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastAdd)] rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)] rw [hright] + all_goals + repeat apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + exact Ref.hgate _ · intro idx hidx rw [BitVec.mulRec_succ_eq] simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq, BitVec.ofNat_eq_ofNat] @@ -90,11 +96,14 @@ theorem go_denote_eq {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr + 1 ≤ rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)] at hdiscr rw [hright] at hdiscr exact hdiscr + all_goals + repeat apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + exact Ref.hgate _ simp only [this, ↓reduceIte] rw [denote_blastAdd] · intros simp only [RefVec.get_cast, Ref.cast_eq] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst) (h := Ref.hgate _)] rw [hacc] · intros simp only [denote_blastShiftLeftConst, BitVec.getLsbD_shiftLeft] @@ -109,10 +118,16 @@ theorem go_denote_eq {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr + 1 ≤ rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)] at hdiscr rw [hright] at hdiscr simp [hdiscr] + all_goals + repeat apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + exact Ref.hgate _ simp only [this, Bool.false_eq_true, ↓reduceIte, BitVec.add_zero] rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastAdd)] rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)] rw [hacc] + all_goals + repeat apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + exact Ref.hgate _ · have : curr + 1 = w := by omega subst this rw [← hgo] diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean index fa8c6c2484..9b1abb6d16 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean @@ -59,10 +59,9 @@ theorem go_get_aux (aig : AIG α) (n : Nat) (curr : Nat) (hcurr : curr ≤ n) unfold go split · dsimp only - rw [go_get_aux] + rw [go_get_aux]; case hidx => rw [Nat.mul_add]; omega rw [AIG.RefVec.get_append] simp only [hidx, ↓reduceDIte] - omega · dsimp only simp only [RefVec.get, Ref.mk.injEq] have : curr = n := by omega diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateLeft.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateLeft.lean index 6e4cc79cd2..237a651f03 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateLeft.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateLeft.lean @@ -39,9 +39,9 @@ theorem go_get_aux (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w) split · dsimp only split - · rw [go_get_aux] + · rw [go_get_aux]; case hidx => omega rw [AIG.RefVec.get_push_ref_lt] - · rw [go_get_aux] + · rw [go_get_aux]; case hidx => omega rw [AIG.RefVec.get_push_ref_lt] · dsimp only simp only [RefVec.get, Ref.mk.injEq] @@ -69,14 +69,14 @@ theorem go_get (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w) | inl heq => split · split - · rw [go_get_aux] + · rw [go_get_aux]; case hidx => omega rw [AIG.RefVec.get_push_ref_eq'] · simp [heq] · omega · omega · split · omega - · rw [go_get_aux] + · rw [go_get_aux]; case hidx => omega rw [AIG.RefVec.get_push_ref_eq'] · simp [heq] · omega diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateRight.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateRight.lean index 407e9738c8..fa6f5dcf29 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateRight.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateRight.lean @@ -39,9 +39,9 @@ theorem go_get_aux (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w) split · dsimp only split - · rw [go_get_aux] + · rw [go_get_aux]; case hidx => omega rw [AIG.RefVec.get_push_ref_lt] - · rw [go_get_aux] + · rw [go_get_aux]; case hidx => omega rw [AIG.RefVec.get_push_ref_lt] · dsimp only simp only [RefVec.get, Ref.mk.injEq] @@ -70,14 +70,14 @@ theorem go_get (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w) | inl heq => split · split - · rw [go_get_aux] + · rw [go_get_aux]; case hidx => omega rw [AIG.RefVec.get_push_ref_eq'] · simp [heq] · omega · omega · split · omega - · rw [go_get_aux] + · rw [go_get_aux]; case hidx => omega rw [AIG.RefVec.get_push_ref_eq'] · simp [heq] · omega diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean index 8ef4025859..166926819f 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean @@ -43,11 +43,11 @@ theorem go_get_aux (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w) split at hgo · rw [← hgo] intros - rw [go_get_aux] + rw [go_get_aux (hidx := Nat.lt_succ_of_lt hidx) (hfoo := ‹_›)] rw [AIG.RefVec.get_push_ref_lt] · rw [← hgo] intros - rw [go_get_aux] + rw [go_get_aux (hidx := Nat.lt_succ_of_lt hidx) (hfoo := ‹_›)] rw [AIG.RefVec.get_push_ref_lt] · dsimp only at hgo rw [← hgo] @@ -107,7 +107,7 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w) split at hgo · split · rw [← hgo] - rw [go_get] + rw [go_get]; case hidx => omega rw [AIG.RefVec.get_push_ref_eq'] · rw [go_denote_mem_prefix] · simp only [Ref.cast_eq] @@ -118,7 +118,7 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w) · split · omega · rw [← hgo] - rw [go_get] + rw [go_get]; case hidx => omega rw [AIG.RefVec.get_push_ref_eq'] · rw [go_denote_mem_prefix] · simp [heq] @@ -195,7 +195,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : rw [← hg] simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq, denote_blastShiftLeftConst] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst) (h := Ref.hgate _)] rw [hright] simp only [hif1, ↓reduceIte] have hmod : 2 ^ pow % 2 ^ n = 2 ^ pow := by @@ -218,10 +218,10 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : rw [← hg] simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq, denote_blastShiftLeftConst] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst) (h := Ref.hgate _)] rw [hright] simp only [hif1, Bool.false_eq_true, ↓reduceIte] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst) (h := Ref.hgate _)] rw [hleft] simp · have : rhs.getLsbD pow = false := by diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean index 91e36f8801..cc09e862d5 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean @@ -43,11 +43,11 @@ theorem go_get_aux (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w) split at hgo · rw [← hgo] intros - rw [go_get_aux] + rw [go_get_aux (hidx := Nat.lt_succ_of_lt hidx) (hfoo := ‹_›)] rw [AIG.RefVec.get_push_ref_lt] · rw [← hgo] intros - rw [go_get_aux] + rw [go_get_aux (hidx := Nat.lt_succ_of_lt hidx) (hfoo := ‹_›)] rw [AIG.RefVec.get_push_ref_lt] · dsimp only at hgo rw [← hgo] @@ -107,7 +107,7 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w) split at hgo · split · rw [← hgo] - rw [go_get] + rw [go_get]; case hidx => omega rw [AIG.RefVec.get_push_ref_eq'] · rw [go_denote_mem_prefix] · simp [heq] @@ -117,7 +117,7 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w) · split · omega · rw [← hgo] - rw [go_get] + rw [go_get]; case hidx => omega rw [AIG.RefVec.get_push_ref_eq'] · rw [go_denote_mem_prefix] · simp only [Ref.cast_eq] @@ -178,7 +178,7 @@ theorem go_get (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w) split · split all_goals - rw [go_get] + rw [go_get]; case hidx => omega rw [AIG.RefVec.get_push_ref_lt] · simp only have : curr = w := by omega @@ -213,7 +213,7 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w) simp only [hlt, ↓reduceDIte] dsimp only at hgo rw [← hgo] - rw [go_get] + rw [go_get]; case hidx => omega rw [AIG.RefVec.get_push_ref_eq'] · simp [heq] · omega @@ -222,7 +222,7 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w) simp only [hlt, ↓reduceDIte] dsimp only at hgo rw [← hgo] - rw [go_get] + rw [go_get]; case hidx => omega rw [AIG.RefVec.get_push_ref_eq'] · simp [heq] | inr => @@ -285,7 +285,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : rw [← hg] simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq, denote_blastShiftRightConst] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftRightConst)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftRightConst) (h := Ref.hgate _)] rw [hright] simp only [hif1, ↓reduceIte] have hmod : 2 ^ pow % 2 ^ n = 2 ^ pow := by @@ -303,10 +303,10 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : rw [← hg] simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq, denote_blastShiftRightConst] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftRightConst)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftRightConst) (h := Ref.hgate _)] rw [hright] simp only [hif1, Bool.false_eq_true, ↓reduceIte] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftRightConst)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftRightConst) (h := Ref.hgate _)] rw [hleft] simp · have : rhs.getLsbD pow = false := by @@ -418,7 +418,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : rw [← hg] simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq, denote_blastArithShiftRightConst] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastArithShiftRightConst)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastArithShiftRightConst) (h := Ref.hgate _)] rw [hright] simp only [hif1, ↓reduceIte] have hmod : 2 ^ pow % 2 ^ n = 2 ^ pow := by @@ -436,10 +436,10 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : rw [← hg] simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq, denote_blastArithShiftRightConst] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastArithShiftRightConst)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastArithShiftRightConst) (h := Ref.hgate _)] rw [hright] simp only [hif1, Bool.false_eq_true, ↓reduceIte] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastArithShiftRightConst)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastArithShiftRightConst) (h := Ref.hgate _)] rw [hleft] simp · have : rhs.getLsbD pow = false := by diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean index 9864f47499..00817da70c 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean @@ -109,9 +109,16 @@ theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lh · simp [Std.Tactic.BVDecide.Normalize.BitVec.lt_ult] · intro idx hidx simp only [RefVec.get_cast, Ref.cast_eq] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub) (h := ?h)] + case h => + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + exact Ref.hgate _ + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := ?h)] + case h => + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + exact Ref.hgate _ + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := Ref.hgate _)] rw [denote_blastShiftConcat_eq_shiftConcat] · simp [hr] · rw [BVPred.denote_getD_eq_getLsbD] @@ -125,11 +132,21 @@ theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lh rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] · simp [hright] · simp [Ref.hgate] + all_goals + repeat apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + exact Ref.hgate _ · intro h simp only [RefVec.get_cast, Ref.cast_eq] - rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] + rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt) (h := ?h)] + case h => + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + exact Ref.hgate _ + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub) (h := ?h)] + case h => + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + exact Ref.hgate _ + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := Ref.hgate _)] rw [denote_blastShiftConcat_eq_shiftConcat] · intro idx hidx rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] @@ -138,11 +155,18 @@ theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lh · rw [denote_mkConstCached] · intro h simp only [RefVec.get_cast, Ref.cast_eq] - rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)] + rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt) (h := ?h)] + case h => + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + exact Ref.hgate _ + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub) (h := Ref.hgate _)] rw [denote_blastShiftConcat_eq_shiftConcat] · intro idx hidx - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := ?h2)] + case h2 => + simp only [RefVec.get_cast, Ref.cast_eq] + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + exact Ref.hgate _ rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] · simp [hq] · simp [Ref.hgate] @@ -172,11 +196,29 @@ theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lh next hdiscr => rw [← Normalize.BitVec.lt_ult] at hdiscr simp only [Ref.cast_eq, hdiscr, ↓reduceIte] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := AIG.RefVec.ite)] - rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := AIG.RefVec.ite) (h := ?h)] + case h => + apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := BVPred.mkUlt) + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + exact Ref.hgate _ + rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt) (h := ?h)] + case h => + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + exact Ref.hgate _ + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub) (h := ?h)] + case h => + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + exact Ref.hgate _ + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := ?h)] + case h => + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size + exact Ref.hgate _ + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := Ref.hgate _)] rw [denote_blastShiftConcat_eq_shiftConcat] · intro idx hidx simp [hr] @@ -186,27 +228,47 @@ theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lh next hdiscr => rw [← Normalize.BitVec.lt_ult] at hdiscr simp only [Ref.cast_eq, hdiscr, ↓reduceIte] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := AIG.RefVec.ite)] - rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := AIG.RefVec.ite) (h := ?h2)] + case h2 => + apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := BVPred.mkUlt) + exact Ref.hgate _ + rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt) (h := Ref.hgate _)] rw [denote_blastSub] · intro idx hidx simp only [RefVec.get_cast, Ref.cast_eq] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := ?h2)] + case h2 => + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat) + exact Ref.hgate _ + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := Ref.hgate _)] rw [denote_blastShiftConcat_eq_shiftConcat] · simp [hr] · rw [BVPred.denote_getD_eq_getLsbD] · exact hleft · simp · intro idx hidx - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := ?h3)] + case h3 => + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat) + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat) + simp [Ref.hgate] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := ?h3)] + case h3 => + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat) + simp [Ref.hgate] rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] · simp [hright] · simp [Ref.hgate] · intro idx hidx - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub) (h := ?h4)] + case h4 => + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat) + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat) + simp [Ref.hgate] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := ?h4)] + case h4 => + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat) + simp [Ref.hgate] rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] . simp only [Ref.cast_eq, RefVec.get_cast] rw [denote_blastShiftConcat_eq_shiftConcat] @@ -217,9 +279,21 @@ theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lh · simp . simp [Ref.hgate] · intro idx hidx - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub) (h := ?h5)] + case h5 => + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat) + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat) + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat) + simp [Ref.hgate] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := ?h5)] + case h5 => + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat) + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat) + simp [Ref.hgate] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := ?h5)] + case h5 => + apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat) + simp [Ref.hgate] rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)] . simp [hright] . simp [Ref.hgate] @@ -381,12 +455,15 @@ theorem denote_blastUdiv (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bo RefVec.get_cast] split next hdiscr => - rw [blastUdiv.go_denote_mem_prefix] at hdiscr + rw [blastUdiv.go_denote_mem_prefix (hstart := Ref.hgate _)] at hdiscr rw [BVPred.mkEq_denote_eq (lhs := rhs) (rhs := 0#w)] at hdiscr · simp only [beq_iff_eq] at hdiscr rw [hdiscr] rw [blastUdiv.go_denote_mem_prefix] - rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)] + case hstart => + apply LawfulOperator.le_size_of_le_aig_size (f := BVPred.mkEq) + exact Ref.hgate _ + rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq) (h := Ref.hgate _)] rw [denote_blastConst] simp · intro idx hidx @@ -394,7 +471,7 @@ theorem denote_blastUdiv (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bo · intro idx hidx simp next hdiscr => - rw [blastUdiv.go_denote_mem_prefix] at hdiscr + rw [blastUdiv.go_denote_mem_prefix (hstart := Ref.hgate _)] at hdiscr rw [BVPred.mkEq_denote_eq (lhs := rhs) (rhs := 0#w)] at hdiscr · have hzero : 0#w < rhs := by rw [Normalize.BitVec.zero_lt_iff_zero_neq] diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean index e72f91dcef..c7e60a8a00 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean @@ -39,7 +39,8 @@ theorem mkUlt_denote_eq (aig : AIG α) (lhs rhs : BitVec w) (input : BinaryRefVe · simp · dsimp only intro idx hidx - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := BVExpr.bitblast.blastNot)] + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := BVExpr.bitblast.blastNot) (h := ?h)] + case h => simp [Ref.hgate] apply hleft · dsimp only intro idx hidx diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean index 221539fa63..4e3fa65367 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean @@ -147,11 +147,14 @@ theorem denote_blastUmod (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bo RefVec.get_cast] split next hdiscr => - rw [blastUdiv.go_denote_mem_prefix] at hdiscr + rw [blastUdiv.go_denote_mem_prefix (hstart := Ref.hgate _)] at hdiscr rw [BVPred.mkEq_denote_eq (lhs := rhs) (rhs := 0#w)] at hdiscr · simp only [beq_iff_eq] at hdiscr rw [hdiscr] - rw [blastUdiv.go_denote_mem_prefix] + rw [blastUdiv.go_denote_mem_prefix (hstart := ?h)] + case h => + apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := BVPred.mkEq) + exact Ref.hgate _ rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)] · simp [hleft] · simp [Ref.hgate] @@ -162,7 +165,7 @@ theorem denote_blastUmod (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bo rw [denote_blastConst] simp next hdiscr => - rw [blastUdiv.go_denote_mem_prefix] at hdiscr + rw [blastUdiv.go_denote_mem_prefix (hstart := Ref.hgate _)] at hdiscr rw [BVPred.mkEq_denote_eq (lhs := rhs) (rhs := 0#w)] at hdiscr · have hzero : 0#w < rhs := by rw [Normalize.BitVec.zero_lt_iff_zero_neq] diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean index b4b2f61a93..2b720eef66 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean @@ -40,12 +40,12 @@ theorem go_get_aux (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWidth · dsimp only at hgo split at hgo · rw [← hgo] - intros - rw [go_get_aux] + intro hfoo + rw [go_get_aux (hfoo := hfoo)]; case hidx => omega rw [AIG.RefVec.get_push_ref_lt] · rw [← hgo] - intros - rw [go_get_aux] + intro hfoo + rw [go_get_aux (hfoo := hfoo)]; case hidx => omega rw [AIG.RefVec.get_push_ref_lt] · dsimp only at hgo rw [← hgo] @@ -108,7 +108,7 @@ theorem go_denote_eq (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWid rw [heq] at hsplit simp only [hsplit, ↓reduceDIte] rw [← hgo] - rw [go_get] + rw [go_get]; case hidx => omega rw [AIG.RefVec.get_push_ref_eq'] · rw [go_denote_mem_prefix] · simp [heq] @@ -118,7 +118,7 @@ theorem go_denote_eq (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWid rw [heq] at hsplit simp only [hsplit, ↓reduceDIte] rw [← hgo] - rw [go_get] + rw [go_get]; case hidx => omega rw [AIG.RefVec.get_push_ref_eq'] · rw [go_denote_mem_prefix] · simp only [Ref.cast_eq] diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean index a24a5e5a27..42e62b9406 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean @@ -39,12 +39,11 @@ theorem go_get_aux (aig : AIG BVBit) (a : Nat) (curr : Nat) (hcurr : curr ≤ w) · dsimp only at hgo rw [← hgo] intro hfoo - rw [go_get_aux] - rw [AIG.RefVec.get_push_ref_lt] + rw [go_get_aux (hidx := Nat.lt_succ_of_lt hidx)] + rw [AIG.RefVec.get_push_ref_lt (hidx := hidx)] · simp only [Ref.cast, Ref.mk.injEq] rw [AIG.RefVec.get_cast] - · simp - · assumption + simp · apply go_le_size · dsimp only at hgo rw [← hgo] @@ -99,7 +98,7 @@ theorem go_denote_eq (aig : AIG BVBit) (a : Nat) (assign : Assignment) (curr : N cases Nat.eq_or_lt_of_le hidx2 with | inl heq => rw [← hgo] - rw [go_get] + rw [go_get]; case hidx => omega rw [AIG.RefVec.get_push_ref_eq'] · rw [← heq] rw [go_denote_mem_prefix] diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean index aa473f7cc7..400609f9b1 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean @@ -175,7 +175,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, mostRecentUnitIdx, i_gt_zero, ?_⟩ simp only [insertUnit, h5, ite_false, reduceCtorEq] constructor - · rw [Array.getElem_push_lt, h1] + · rw [Array.getElem_push_lt j.2, h1] · constructor · simp +zetaDelta [i_eq_l, ← hl] rfl @@ -215,7 +215,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen · simp +zetaDelta [i_eq_l, ← hl] rfl · constructor - · rw [Array.getElem_push_lt, h1] + · rw [Array.getElem_push_lt j.2, h1] · constructor · simp only [i_eq_l] rw [Array.getElem_modify_self] @@ -258,7 +258,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, b,i_gt_zero, ?_⟩ simp only [insertUnit, h5, ite_false, reduceCtorEq] constructor - · rw [Array.getElem_push_lt, h1] + · rw [Array.getElem_push_lt j.2, h1] · constructor · grind · constructor diff --git a/tests/lean/run/10172.lean b/tests/lean/run/10172.lean new file mode 100644 index 0000000000..d05c5da9fc --- /dev/null +++ b/tests/lean/run/10172.lean @@ -0,0 +1,33 @@ +/-! +# Rewrite tactic "steals" goals +-/ + + +/-! +https://github.com/leanprover/lean4/issues/10172 + +There were two metaprogramming bugs: +- `rw` didn't filter old vs new metavariables when coming up with new goals. +- it also didn't make the new metavariables be synthetic opaque, so the old one was + being assigned, even with old vs new filtering. +-/ +example (l m : List Nat) (i : Nat) (hi' : i < (l ++ m).length) + (hh : ∀ hi, l[i]'hi = 5) : (l ++ m)[i] = 5 := by + rw [List.getElem_append_left] + · rw [hh] -- used to be Error: unsolved goal `i < l.length` + · sorry -- used to be Error: No goals to be solved + +/-! +While we're here, we could address a missing occurs check. + +https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/rewrite.20with.20the.20goal/near/538108360 +-/ +/-- +error: Occurs check failed: Expression + ?k +contains the goal ?k +-/ +#guard_msgs in +example : 1 = 2 := by + refine ?k + rw [?k]