bump version to v4.11.0

Auto/Embedding/LamBase.lean

@@ -3780,8 +3780,8 @@ 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 _ _))]
-        dsimp [List.getD]; rw [List.get?_append exlt];
-        rw [List.get?_reverse _ (by dsimp [List.length]; apply Nat.le_refl _)]
+        rw [List.getD_eq_getElem?_getD]; rw [List.getElem?_append exlt];
+        rw [List.getElem?_reverse (by dsimp [List.length]; apply Nat.le_refl _)]
         dsimp [List.length]; simp
       conv => enter [2, 3]; rw [tyeq]
       exact .ofBVar _)

Auto/Embedding/LamBitVec.lean

@@ -68,7 +68,10 @@ namespace BVLems
       rw [Nat.mod_eq_of_lt]; rcases a with ⟨⟨a, isLt⟩⟩;
       apply Nat.le_trans isLt; apply Nat.pow_le_pow_of_le_right (Nat.le_step .refl) hle
 
-  theorem toNat_sub (a b : BitVec n) : (a - b).toNat = (a.toNat + (2 ^ n - b.toNat)) % (2 ^ n) := rfl
+  theorem toNat_sub (a b : BitVec n) : (a - b).toNat = (2 ^ n - b.toNat + a.toNat) % (2 ^ n) := rfl
+
+  theorem toNat_sub' (a b : BitVec n) : (a - b).toNat = (a.toNat + (2 ^ n - b.toNat)) % (2 ^ n) := by
+    rw [toNat_sub]; rw [Nat.add_comm]
 
   theorem toNat_neg (a : BitVec n) : (-a).toNat = (2^n - a.toNat) % (2^n) := by
     rw [neg_def]; unfold BitVec.neg; rw [toNat_ofNat]
@@ -168,7 +171,7 @@ namespace BVLems
     case false =>
       have hnlt := of_decide_eq_false hdec; have hle := Nat.le_of_not_lt hnlt
       rw [Bool.ite_eq_false _ _ _ hnlt]; apply eq_of_val_eq
-      rw [toNat_ofNat, toNat_sub, toNat_ofNat, toNat_ofNat]
+      rw [toNat_ofNat, toNat_sub', toNat_ofNat, toNat_ofNat]
       have exc : ∃ c, a = b + c := ⟨a - b, by rw [Nat.add_comm, Nat.sub_add_cancel hle]⟩
       rcases exc with ⟨c, ⟨⟩⟩
       rw [Nat.add_sub_cancel_left, Nat.mod_add_mod, Nat.add_assoc b c]

Auto/Lib/ListExtra.lean

@@ -112,12 +112,11 @@ def List.mergeSort (r : α → α → Prop) [DecidableRel r]  : List α → List
   | [] => []
   | [a] => [a]
   | a :: b :: l => by
-    -- Porting note: rewrote to make `mergeSort_cons_cons` proof easier
-    let ls := (split (a :: b :: l))
-    have e : split (a :: b :: l) = ⟨ls.1, ls.2⟩ := rfl
+    let ls := split l
+    have e : split (a :: b :: l) = ⟨a :: ls.1, b :: ls.2⟩ := rfl
     have h := length_split_lt e
-    have := h.1
-    have := h.2
+    have : (split l).fst.length < l.length + 2 := Nat.le_of_lt h.1
+    have : (split l).snd.length < l.length + 2 := Nat.le_of_lt h.2
     exact merge r (mergeSort r ls.1) (mergeSort r ls.2)
   termination_by l => List.length l
 

Auto/Translation/LamReif.lean

@@ -1157,8 +1157,12 @@ def processSimpleApp (fn arg : Expr) : ReifM (Option LamTerm) := do
       if lvls.length != 1 then
         throwError "processSimpleApp :: Attribute should have one level"
       return .some (.base (.ocst (.smtAttr1T attrName (← reifType arg) (.base .prop))))
-      -- `arg` is the original (un-lifted) type
     if let .some tcon := reifMapIL.find? name then
+      if name == ``Embedding.forallF then
+        let [lvl₁, lvl₂] := lvls
+          | throwError "processSimpleApp :: Auto.Embedding.forallF should have two levels"
+        if !(← Meta.isLevelDefEq lvl₁ .zero) || !(← Meta.isLevelDefEq lvl₂ .zero) then
+          return .none
       return .some (.base (tcon (← reifType arg)))
     return .none
   | [arg₁, arg₂] =>

lean-toolchain

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