Update to lean v4.12.0

Auto/Embedding/LamBase.lean

@@ -3781,7 +3781,7 @@ def LamWF.bvarApps
           rw [List.length_reverse]; apply Nat.le_refl
         dsimp [lctxr]; rw [← List.reverseAux, List.reverseAux_eq]
         rw [pushLCtxs_lt (by rw [List.length_append]; apply Nat.le_trans exlt (Nat.le_add_right _ _))]
-        rw [List.getD_eq_getElem?_getD]; rw [List.getElem?_append exlt];
+        rw [List.getD_eq_getElem?_getD]; rw [List.getElem?_append];
         rw [List.getElem?_reverse (by dsimp [List.length]; apply Nat.le_refl _)]
         dsimp [List.length]; simp
       conv => enter [2, 3]; rw [tyeq]

Auto/Embedding/LamBitVec.lean

@@ -101,7 +101,7 @@ namespace BVLems
     apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_of_le_right (.step .refl) h)
 
   theorem msb_equiv_lt (a : BitVec n) : !a.msb ↔ a.toNat < 2 ^ (n - 1) := by
-    dsimp [BitVec.msb, BitVec.getMsb, BitVec.getLsb]
+    dsimp [BitVec.msb, getMsbD, getLsbD]
     cases n
     case zero => simp
     case succ n =>
@@ -133,7 +133,7 @@ namespace BVLems
         rw [Nat.sub_one, Nat.pred_lt_iff_le (Nat.two_pow_pos _)]
         apply Nat.le_trans (Nat.sub_le _ _) (Nat.pow_le_pow_of_le_right (.step .refl) h)
       apply eq_of_val_eq; rw [toNat_ofNatLt, hzero]
-      rw [toNat_neg, Int.mod_def', Int.emod]; dsimp only;
+      rw [toNat_neg, Int.mod_def', Int.emod];
       rw [Nat.zero_mod, Int.natAbs_ofNat, Nat.succ_eq_add_one, Nat.zero_add]
       rw [Int.subNatNat_of_sub_eq_zero ((Nat.sub_eq_zero_iff_le).mpr (Nat.two_pow_pos _))]
       rw [Int.toNat_ofNat, BitVec.toNat_ofNat]

Auto/Embedding/LamSystem.lean

@@ -209,7 +209,7 @@ theorem LamTerm.rwGenAllWith_lam : rwGenAllWith conv rty (.lam s body) =
   | .none =>
     match rty with
     | .func _ resTy => (rwGenAllWith conv resTy body).bind (LamTerm.lam s ·)
-    | _ => .none := by simp [rwGenAllWith]
+    | _ => .none := by delta rwGenAllWith; simp only
 
 theorem LamTerm.rwGenAllWith_app : rwGenAllWith conv rty (.app s fn arg) =
   match conv rty (.app s fn arg) with
@@ -1492,7 +1492,7 @@ theorem LamTerm.evarBounded_rwGenAllWith (H : ∀ s, evarBounded (conv s) bound)
     case none.refl => apply Nat.le_max_right
     case some.refl => apply H _ _ _ h
   case lam s' body IH =>
-    simp [LamTerm.rwGenAllWith]
+    rw [LamTerm.rwGenAllWith_lam]
     match h₁ : conv s (.lam s' body) with
     | .some t' => intro h₂; cases h₂; apply H _ _ _ h₁
     | .none =>
@@ -1547,7 +1547,7 @@ theorem LamTerm.evarEquiv_rwGenAllWith (H : ∀ s, evarEquiv (conv s)) :
     case none.refl => rfl
     case some.refl => apply H _ _ _ h
   case lam s' body IH =>
-    simp [LamTerm.rwGenAllWith]
+    rw [LamTerm.rwGenAllWith_lam]
     match h₁ : conv s (.lam s' body) with
     | .some t' => intro h₂; cases h₂; apply H _ _ _ h₁
     | .none =>
@@ -1592,7 +1592,7 @@ theorem LamGenConvWith.rwGenAllWith (H : LamGenConvWith lval conv) : LamGenConvW
     case none.refl => apply LamGenEquivWith.refl
     case some.refl => apply H _ _ _ h
   case lam s' body IH =>
-    simp [LamTerm.rwGenAllWith]
+    rw [LamTerm.rwGenAllWith_lam]
     match h₁ : conv s (.lam s' body) with
     | .some t' => intro h₂; cases h₂; apply H _ _ _ h₁
     | .none =>

Auto/Lib/BinTree.lean

@@ -260,7 +260,11 @@ theorem insert'Aux.equiv (bt : BinTree α) (n : Nat) (x : α) (rd : Nat) :
   case succ rd' IH =>
     match n with
     | 0 => rw [insert'Aux, insert'WF]
-    | 1 => rw [insert'Aux, insert'WF]
+    | 1 =>
+      simp only [eq_def]
+      cases bt
+      . simp only [insert'WF]
+      . simp only [insert'WF]
     | n' + 2 =>
       dsimp [insert'Aux];
       rw [insert'WF.succSucc];
@@ -313,7 +317,7 @@ theorem insert'.correct₁ (bt : BinTree β) (n : Nat) (x : β) : n ≠ 0 → ge
     have hne' : (n + 2) / 2 ≠ 0 := by
       rw [Nat.add_div_right _ (.step .refl)]; intro h; cases h
     let IH' := fun bt => IH bt hne'
-    rw [get?'_succSucc, insert'.succSucc, left!, right!]
+    rw [get?'_succSucc, insert'.succSucc, left!.eq_def, right!.eq_def]
     cases (n + 2) % 2 <;> cases bt <;> dsimp <;> rw [IH']
 
 theorem insert.correct₁ (bt : BinTree β) (n : Nat) (x : β) : get? (insert bt n x) n = .some x :=
@@ -338,7 +342,7 @@ theorem insert'.correct₂ (bt : BinTree β) (n₁ n₂ : Nat) (x : β) : n₁ 
     | 0 => cases bt <;> rfl
     | 1 => cases bt <;> rfl
     | n₁ + 2 =>
-      rw [insert'.succSucc, left!, right!]
+      rw [insert'.succSucc, left!.eq_def, right!.eq_def]
       have hne' : (n₁ + 2) % 2 = (n₂ + 2) % 2 → (n₁ + 2) / 2 ≠ (n₂ + 2) / 2 := by
         intro heq h; apply hne;
         rw [← Nat.div_add_mod (n₁ + 2) 2, ← Nat.div_add_mod (n₂ + 2) 2]

Auto/Translation/Preprocessing.lean

@@ -60,7 +60,7 @@ def elabDefEq (name : Name) : TacticM (Array Lemma) := do
     addRecAsLemma val
   | some (.defnInfo _) =>
     -- Generate definitional equation for (possibly recursive) declaration
-    match ← getEqnsFor? name (nonRec := true) with
+    match ← getEqnsFor? name with
     | some eqns => eqns.mapIdxM fun i eq =>
       do elabLemma (← `($(mkIdent eq))) (.leaf s!"defeq {i.val} {name}")
     | none => return #[]

lake-manifest.json

@@ -1,4 +1,4 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages": [],
  "name": "auto",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.11.0
+leanprover/lean4:v4.12.0