From 7bafe6f8df0a5600e4a22add3b5fc0f1e0928de9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 19 Nov 2024 17:51:31 -0800 Subject: [PATCH] chore: fix stage2 issue chore: fix stage2 issues --- src/Init/Data/Array/Basic.lean | 2 +- src/Init/Data/List/Impl.lean | 2 +- src/Lean/Data/RArray.lean | 2 +- src/Lean/Elab/PatternVar.lean | 2 +- src/Std/Sat/AIG/Basic.lean | 6 +++--- src/Std/Sat/AIG/CNF.lean | 6 +++--- src/Std/Sat/AIG/Relabel.lean | 2 +- .../BVDecide/LRAT/Internal/Formula/RatAddResult.lean | 2 +- .../BVDecide/LRAT/Internal/Formula/RupAddResult.lean | 9 ++++----- src/Std/Time/Date/ValidDate.lean | 2 +- 10 files changed, 17 insertions(+), 18 deletions(-) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index cdda587895e7..56be906c8cc1 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -798,7 +798,7 @@ decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ h induction a, i, h using Array.eraseIdx.induct with | @case1 a i h h' a' ih => unfold eraseIdx - simp [h', a', ih] + simp +zetaDelta [h', a', ih] | case2 a i h h' => unfold eraseIdx simp [h'] diff --git a/src/Init/Data/List/Impl.lean b/src/Init/Data/List/Impl.lean index e01f04335392..5fb32bf0b59c 100644 --- a/src/Init/Data/List/Impl.lean +++ b/src/Init/Data/List/Impl.lean @@ -332,7 +332,7 @@ def enumFromTR (n : Nat) (l : List α) : List (Nat × α) := rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as] simp [enumFrom, f] rw [← Array.foldr_toList] - simp [go] + simp +zetaDelta [go] /-! ## Other list operations -/ diff --git a/src/Lean/Data/RArray.lean b/src/Lean/Data/RArray.lean index c58f07fe1078..8ed71a5c57d0 100644 --- a/src/Lean/Data/RArray.lean +++ b/src/Lean/Data/RArray.lean @@ -55,7 +55,7 @@ where go lb ub h1 h2 : (ofFn.go f lb ub h1 h2).size = ub - lb := by induction lb, ub, h1, h2 using RArray.ofFn.go.induct (f := f) (n := n) case case1 => simp [ofFn.go, size]; omega - case case2 ih1 ih2 hiu => rw [ofFn.go]; simp [size, *]; omega + case case2 ih1 ih2 hiu => rw [ofFn.go]; simp +zetaDelta [size, *]; omega section Meta open Lean diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean index 75ee2565a430..3aec810628fb 100644 --- a/src/Lean/Elab/PatternVar.lean +++ b/src/Lean/Elab/PatternVar.lean @@ -159,7 +159,7 @@ private def processVar (idStx : Syntax) : M Syntax := do private def samePatternsVariables (startingAt : Nat) (s₁ s₂ : State) : Bool := Id.run do if h₁ : s₁.vars.size = s₂.vars.size then for h₂ : i in [startingAt:s₁.vars.size] do - if s₁.vars[i] != s₂.vars[i]'(by obtain ⟨_, y⟩ := h₂; simp_all) then return false + if s₁.vars[i] != s₂.vars[i]'(by obtain ⟨_, y⟩ := h₂; simp_all +zetaDelta) then return false true else false diff --git a/src/Std/Sat/AIG/Basic.lean b/src/Std/Sat/AIG/Basic.lean index cf12873255e3..4a12ef54dce9 100644 --- a/src/Std/Sat/AIG/Basic.lean +++ b/src/Std/Sat/AIG/Basic.lean @@ -471,7 +471,7 @@ def mkGate (aig : AIG α) (input : GateInput aig) : Entrypoint α := have := input.lhs.ref.hgate have := input.rhs.ref.hgate omega - ⟨{ aig with decls, invariant, cache }, ⟨g, by simp [decls]⟩⟩ + ⟨{ aig with decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩ /-- Add a new input node to the AIG in `aig`. Note that this version is only meant for proving, @@ -487,7 +487,7 @@ def mkAtom (aig : AIG α) (n : α) : Entrypoint α := split at h2 · apply aig.invariant <;> assumption · contradiction - ⟨{ decls, invariant, cache }, ⟨g, by simp [decls]⟩⟩ + ⟨{ decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩ /-- Add a new constant node to `aig`. Note that this version is only meant for proving, @@ -503,7 +503,7 @@ def mkConst (aig : AIG α) (val : Bool) : Entrypoint α := split at h2 · apply aig.invariant <;> assumption · contradiction - ⟨{ decls, invariant, cache }, ⟨g, by simp [decls]⟩⟩ + ⟨{ decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩ end AIG diff --git a/src/Std/Sat/AIG/CNF.lean b/src/Std/Sat/AIG/CNF.lean index 95ecaa3ae8d5..b43ced351dff 100644 --- a/src/Std/Sat/AIG/CNF.lean +++ b/src/Std/Sat/AIG/CNF.lean @@ -505,7 +505,7 @@ def State.addConst (state : State aig) (idx : Nat) (h : idx < aig.decls.size) let newCnf := Decl.constToCNF (.inr ⟨idx, h⟩) b have hinv := toCNF.State.Inv_constToCNF htip let ⟨cache, hcache⟩ := cache.addConst idx h htip - ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [hcache]⟩ + ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [newCnf, hcache]⟩ /-- Add the CNF for a `Decl.atom` to the state. @@ -517,7 +517,7 @@ def State.addAtom (state : State aig) (idx : Nat) (h : idx < aig.decls.size) let newCnf := Decl.atomToCNF (.inr ⟨idx, h⟩) (.inl a) have hinv := toCNF.State.Inv_atomToCNF htip let ⟨cache, hcache⟩ := cache.addAtom idx h htip - ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [hcache]⟩ + ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [newCnf, hcache]⟩ /-- Add the CNF for a `Decl.gate` to the state. @@ -537,7 +537,7 @@ def State.addGate (state : State aig) {hlb} {hrb} (idx : Nat) (h : idx < aig.dec rinv have hinv := toCNF.State.Inv_gateToCNF htip let ⟨cache, hcache⟩ := cache.addGate idx h htip hl hr - ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [hcache]⟩ + ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [newCnf, hcache]⟩ /-- Evaluate the CNF contained within the state. diff --git a/src/Std/Sat/AIG/Relabel.lean b/src/Std/Sat/AIG/Relabel.lean index f06433ffaae9..ae33a8346006 100644 --- a/src/Std/Sat/AIG/Relabel.lean +++ b/src/Std/Sat/AIG/Relabel.lean @@ -65,7 +65,7 @@ def relabel (r : α → β) (aig : AIG α) : AIG β := cache, invariant := by intro idx lhs rhs linv rinv hbound hgate - simp [decls] at hgate + simp +zetaDelta [decls] at hgate have := Decl.relabel_gate hgate apply aig.invariant assumption diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean index be25f5ad8be3..ac09debb1f56 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean @@ -224,7 +224,7 @@ theorem ratAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (p have insertRupUnits_rw : (insertRupUnits f (negate c)).1 = ⟨(insertRupUnits f (negate c)).1.clauses, (insertRupUnits f (negate c)).1.rupUnits, (insertRupUnits f (negate c)).1.ratUnits, (insertRupUnits f (negate c)).1.assignments⟩ := rfl - simp only [performRatCheck_fold_formula_eq performRupCheck_res h_performRupCheck_res (Literal.negate p) ratHints, + simp +zetaDelta only [performRatCheck_fold_formula_eq performRupCheck_res h_performRupCheck_res (Literal.negate p) ratHints, clauses_performRupCheck, rupUnits_performRupCheck, ratUnits_performRupCheck, restoreAssignments_performRupCheck fc fc_assignments_size, ← insertRupUnits_rw, clear_insertRup f f_readyForRatAdd.2 (negate c), fc, performRupCheck_res] diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean index 2407b761393e..7de0c5db4a35 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean @@ -111,7 +111,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen ⟨units.size, units_size_lt_updatedUnits_size⟩ have i_gt_zero : i.1 > 0 := by rw [i_eq_l]; exact l.1.2.1 refine ⟨mostRecentUnitIdx, l.2, i_gt_zero, ?_⟩ - simp only [insertUnit, h3, ite_false, Array.getElem_push_eq, i_eq_l, reduceCtorEq] + simp +zetaDelta only [insertUnit, h3, ite_false, Array.getElem_push_eq, i_eq_l, reduceCtorEq] constructor · rfl · constructor @@ -131,7 +131,6 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen exact k_property · intro h simp only [← h, not_true, mostRecentUnitIdx] at hk - exact hk rfl rw [Array.getElem_push_lt _ _ _ k_in_bounds] rw [i_eq_l] at h2 exact h2 ⟨k.1, k_in_bounds⟩ @@ -193,7 +192,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen constructor · rw [Array.getElem_push_lt units l j.1 j.2, h1] · constructor - · simp [i_eq_l, ← hl] + · simp +zetaDelta [i_eq_l, ← hl] rfl · constructor · simp only [i_eq_l] @@ -228,7 +227,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen refine ⟨mostRecentUnitIdx, ⟨j.1, j_lt_updatedUnits_size⟩, i_gt_zero, ?_⟩ simp [insertUnit, h5, ite_false, Array.getElem_push_eq, ne_eq] constructor - · simp [i_eq_l, ← hl] + · simp +zetaDelta [i_eq_l, ← hl] rfl · constructor · rw [Array.getElem_push_lt units l j.1 j.2, h1] @@ -1330,7 +1329,7 @@ theorem rupAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (ru have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by rw [size_assignments_insertRupUnits f (negate c)] exact f_readyForRupAdd.2.1 - simp only [clauses_performRupCheck, rupUnits_performRupCheck, ratUnits_performRupCheck, + simp +zetaDelta only [clauses_performRupCheck, rupUnits_performRupCheck, ratUnits_performRupCheck, restoreAssignments_performRupCheck fc fc_assignments_size, Prod.mk.injEq, and_true] at rupAddSuccess have rupAddSuccess : DefaultFormula.insert (clearRupUnits (insertRupUnits f (negate c)).fst) c = f' := by rw [rupAddSuccess] diff --git a/src/Std/Time/Date/ValidDate.lean b/src/Std/Time/Date/ValidDate.lean index bd38c6520d26..ce74efb4eeba 100644 --- a/src/Std/Time/Date/ValidDate.lean +++ b/src/Std/Time/Date/ValidDate.lean @@ -48,7 +48,7 @@ def ofOrdinal (ordinal : Day.Ordinal.OfYear leap) : ValidDate leap := let bounded := Bounded.LE.mk ordinal.val (And.intro h h₁) |>.sub acc let bounded : Bounded.LE 1 monthDays.val := bounded.cast (by omega) (by omega) let days₁ : Day.Ordinal := ⟨bounded.val, And.intro bounded.property.left (Int.le_trans bounded.property.right monthDays.property.right)⟩ - ⟨⟨idx, days₁⟩, Int.le_trans bounded.property.right (by simp)⟩ + ⟨⟨idx, days₁⟩, Int.le_trans bounded.property.right (by simp +zetaDelta)⟩ else by let h₂ := Int.not_le.mp h₁