chore: update to nightly-testing-2024-12-14 (#904)

SSA/Core/Framework.lean

@@ -1307,7 +1307,7 @@ theorem Lets.denote_getPureExprAux [LawfulMonad d.m] {Γ₁ Γ₂ : Ctxt d.Ty} {
       specialize ih he f'
       simp only [Ctxt.Diff.Valid, Ctxt.get?, Expr.denote_changeVars,
         EffectKind.return_impure_toMonad_eq, bind_assoc] at ih
-      simp [denote, ← ih]
+      simp +zetaDelta [denote, ← ih]
     | last =>
       simp only [getPureExprAux, eq_rec_constant, Var.casesOn_last,
         Option.mem_def, Option.some.injEq] at he

SSA/Experimental/Bits/AutoStructs/Constructions.lean

@@ -951,9 +951,9 @@ def CNFA.proj_tr (m : CNFA n₂) (f : Fin n₁ → Fin n₂) :
     constructor
     · rintro (hin | ⟨a', hin, heq, hin'⟩)
       · use t.2
-        simp only [Prod.mk.eta, Array.mem_iff_getElem, Array.getElem_take, Array.size_take,
+        simp +zetaDelta only [Prod.mk.eta, Array.mem_iff_getElem, Array.getElem_take, Array.size_take,
           lt_inf_iff, and_self, and_true, hin]
-        use i.val, by simp
+        use i.val, by simp +zetaDelta
       · use a'; simp [heq, hin']
         simp only [Array.mem_iff_getElem, Array.getElem_take, Array.size_take, Fin.is_le',
           inf_of_le_left, lt_inf_iff] at hin ⊢

SSA/Experimental/Bits/AutoStructs/Defs.lean

@@ -349,15 +349,15 @@ lemma formula_language_case_atom :
     simp at h
     unfold lrel l1 l2 at h
     obtain ⟨⟨hrel, h1⟩, h2⟩ := h
-    have _ : n+1 < bvsb.bvs.length := by simp_all [n]
-    have _ : n < bvsb.bvs.length := by simp_all [n]
+    have _ : n+1 < bvsb.bvs.length := by simp +zetaDelta [n]
+    have _ : n < bvsb.bvs.length := by simp +zetaDelta [n]
     have hrel : evalRelation rel (bvsb.bvs.get n) (bvsb.bvs.get (Fin.last (n + 1))) := by
       simp at hrel
       apply hrel
     have ht1 : bvsb.bvs.get n = t1.evalFin fun n => bvsb.bvs.get n := by
       unfold Term.language at h1
       simp [Mathlib.Vector.transport, liftMaxSucc1] at h1
-      unfold n; simp; rw [←h1]
+      unfold n; simp +zetaDelta; rw [←h1]
       congr; ext1 k
       split_ifs with h
       · exfalso
@@ -368,7 +368,7 @@ lemma formula_language_case_atom :
     have ht2 : bvsb.bvs.get (Fin.last (n+1)) = t2.evalFin fun n => bvsb.bvs.get n := by
       unfold Term.language at h2
       simp [Mathlib.Vector.transport, liftMaxSucc2] at h2
-      unfold n; simp only [Formula.arity, Fin.natCast_self]; rw [←h2]
+      unfold n; simp +zetaDelta only [Formula.arity, Fin.natCast_self]; rw [←h2]
       congr; ext1 k
       split_ifs with h
       · exfalso

SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean

@@ -921,7 +921,7 @@ theorem decision_procedure_is_correct {w} (φ : Formula) (env : Nat → BitVec w
   extract_lets bvs at hx
   suffices hin : bvs ∈ (⊤ : Set _) by
     rw [←h] at hin
-    simp [Set.instMembership, Set.Mem] at hin; assumption
+    simp +zetaDelta [Set.instMembership, Set.Mem] at hin; assumption
   simp
 
 -- -- For testing the comparison operators.

SSA/Experimental/Bits/AutoStructs/Worklist.lean

@@ -222,16 +222,16 @@ where go (st0 : worklist.St A S) : RawCNFA A :=
         constructor
         { constructor
           { apply Array.mem_of_back?_eq_some at heq'; apply st0.worklist_incl; assumption }
-          { apply Array.not_elem_back_pop at heq' <;> simp_all [Array.pop, wl] } }
+          { apply Array.not_elem_back_pop at heq' <;> simp_all +zetaDelta [Array.pop, wl] } }
         constructor
         { right; apply Array.mem_of_back?_eq_some at heq'; assumption }
         rintro sa hh; rcases hh with hnin | hin
-        { simp [hnin] }
+        { simp +zetaDelta [hnin] }
         right
         exact Array.mem_of_mem_pop st0.worklist sa hin
       have : st2.meas ≤ st1.meas := by
         apply Finset.card_le_card
-        simp [worklist.St.meas, Finset.subset_iff]
+        simp +zetaDelta [worklist.St.meas, Finset.subset_iff]
         intros sa' h
         rcases h with hnin | hin
         { left; simp [st1] at hincl; intros hc; apply hnin; apply hincl; assumption }
@@ -251,7 +251,7 @@ where go (st0 : worklist.St A S) : RawCNFA A :=
           apply hdisj
           { simp_all [Std.HashMap.mem_keys_iff_mem]; apply hnew }
           { apply hc }
-        rcases hin with ⟨hin⟩; simp_all
+        rcases hin with ⟨hin⟩; simp_all +zetaDelta
       have : st2.meas < st0.meas := by omega
       go st2
     else
@@ -387,7 +387,7 @@ lemma worklistRun'_go_wf :
     simp [hsa]
     have heq := Option.eq_none_iff_forall_not_mem.mpr hmap
     simp_all
-    split <;> simp_all
+    split <;> simp_all +zetaDelta
   case case4 sa? hnone =>
     unfold worklistRun'.go sa? at *
     simp; simp_all
@@ -408,7 +408,7 @@ lemma worklistRun'_go_wf :
     suffices hccl : motive as.size (Array.foldl (processOneElem A S final s) st1 as) by
       rcases hccl with ⟨hwf, hst', _⟩; constructor <;> assumption
     apply Array.foldl_induction motive
-    · simp_all [motive]; constructor
+    · simp_all +zetaDelta [motive]; constructor
       · apply hst _ _ hs
       · apply hst
     . simp [motive]; intros i st hwf hsin hst
@@ -850,7 +850,7 @@ def worklistGo_spec {st : worklist.St A S} (inv : StInv A S st.m st.map) :
       subst_eqs
       split
       next _ s' hmap =>
-        have _ : s' = s := by simp_all
+        have _ : s' = s := by simp_all +zetaDelta
         subst_eqs
         rw [heq] at hsome; subst_eqs
         suffices hccl : processOneElem_mot inits final f s sa (f sa).size (Array.foldl (processOneElem A S final s) st1 (f sa)) by
@@ -859,7 +859,7 @@ def worklistGo_spec {st : worklist.St A S} (inv : StInv A S st.m st.map) :
             ext sa'; simp_all; rintro rfl k hge hsome
             suffices hccl : (f sa'.1)[k]? = none by simp_all
             apply Array.getElem?_size_le; assumption
-          simp_all only [ge_iff_le, st2]
+          simp_all +zetaDelta only [ge_iff_le, st2]
         apply Array.foldl_induction
         { simp only [st1, wl']
           unfold processOneElem_mot
@@ -895,7 +895,7 @@ def worklistGo_spec {st : worklist.St A S} (inv : StInv A S st.m st.map) :
         have hnin : sa ∉ st.map := by
           intros hin
           suffices ex : ∃ s, st.map[sa]? = some s by simp_all
-          simp_all
+          simp_all +zetaDelta
         exfalso; apply hnin; apply st.worklist_incl; exact Array.mem_of_back?_eq_some hsome
     next hnone =>
       simp only [Array.back?, Array.getElem?_eq_none_iff] at *

SSA/Experimental/Bits/Fast/Circuit.lean

@@ -721,7 +721,7 @@ def nonemptyAux [DecidableEq α] :
       ⟨b₁ || b₂, by
         simp only [eval_eq_evalv, Bool.or_eq_true, eq_iff_iff]
         rw [← b₁.prop, ← b₂.prop]
-        simp! only [(eval_assignVars)]
+        simp +zetaDelta only [(eval_assignVars)]
         constructor
         · rintro ⟨x, hx⟩
           cases hi : x i
@@ -769,7 +769,7 @@ instance [DecidableEq α] : DecidableRel ((· ≤· ) : Circuit α → Circuit 
     by simp [always_true_iff, le_def, or_iff_not_imp_left]
 
 /-- Negate the value of the circuit -/
-def not {α : Type u} (c : Circuit α) : Circuit α := 
+def not {α : Type u} (c : Circuit α) : Circuit α :=
   c ^^^ .tru
 
 end Circuit

SSA/Projects/FullyHomomorphicEncryption/Syntax.lean

@@ -84,12 +84,12 @@ def ROfZComputable_impl (z : ℤ) : R q n :=
           constructor
           · intros ha
             simp at ha
-            simp [ha]
+            simp +zetaDelta [ha]
           · intros hb
             simp at hb
             obtain ⟨ha, hz⟩ := hb
             subst ha
-            simp [hz]
+            simp +zetaDelta [hz]
         )
       : (ZMod q)[X]
   }

lake-manifest.json

@@ -25,10 +25,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "24a956e927a627c16a104adc19ceca8b33569ea7",
+   "rev": "ddcb85bddebd7fa5b7316dab25b7eae6e0ff1fbb",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing-2024-12-13",
+   "inputRev": "nightly-testing-2024-12-14",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
@@ -75,10 +75,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "43bcb1964528411e47bfa4edd0c87d1face1fce4",
+   "rev": "6dd5eb5a3aeb43f710a35e7fe4fa3f85649ac9a4",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "nightly-testing",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "590ac59af9f55fbb429e3615a25a10d36d723d48",
+   "rev": "13c202289cae0db69d997904de3c4d43c9222ea8",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",

lakefile.toml

@@ -4,7 +4,7 @@ defaultTargets = ["SSA"]
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "nightly-testing-2024-12-13"
+rev = "nightly-testing-2024-12-14"
 
 [[require]]
 name = "Cli"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-12-13
+leanprover/lean4:nightly-2024-12-14