AeneasVerif · sonmarcho · Jan 21, 2025 · Jan 21, 2025
diff --git a/backends/lean/Aeneas/Diverge/Core.lean b/backends/lean/Aeneas/Diverge/Core.lean
@@ -605,7 +605,7 @@ namespace FixI
           revert iLt
           simp_arith
         let j: Fin tys1.length := ⟨ j, jLt ⟩
-        Eq.mp (by simp) (get_fun tl j)
+        Eq.mp (by norm_cast) (get_fun tl j)
 
   /- Automating the proofs -/
   @[simp] theorem is_valid_p_same
@@ -818,7 +818,7 @@ namespace FixII
           revert iLt
           simp_arith
         let j: Fin tys1.length := ⟨ j, jLt ⟩
-        Eq.mp (by simp) (get_fun tl j)
+        Eq.mp (by norm_cast) (get_fun tl j)
 
   /- Automating the proofs -/
   @[simp] theorem is_valid_p_same

diff --git a/backends/lean/Aeneas/Progress/Progress.lean b/backends/lean/Aeneas/Progress/Progress.lean
@@ -591,7 +591,7 @@ namespace Test
     rw [add]
     intro tot
     progress
-    simp [*]
+    simp [*, tot]
 
   def add1 (x y : U32) : Result U32 := do
     let z ← add x y

diff --git a/backends/lean/Aeneas/Utils.lean b/backends/lean/Aeneas/Utils.lean
@@ -847,8 +847,8 @@ def normCastAtAll : TacticM Unit := do
   withMainContext do
   let ctx ← Lean.MonadLCtx.getLCtx
   let decls ← ctx.getDecls
-  NormCast.normCastTarget
-  decls.forM (fun d => NormCast.normCastHyp d.fvarId)
+  NormCast.normCastTarget {}
+  decls.forM (fun d => NormCast.normCastHyp {} d.fvarId)
 
 @[inline] def tryLiftMetaTactic1 (tactic : MVarId → MetaM (Option MVarId)) (msg : String) : TacticM Unit :=
   withMainContext do

diff --git a/backends/lean/lake-manifest.json b/backends/lean/lake-manifest.json
@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9837ca9d65d9de6fad1ef4381750ca688774e608",
+   "rev": "15f16b1ec50f425147926be1aede7b4baa725380",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5",
+   "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -35,30 +35,30 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9a0b533c2fbd6195df067630be18e11e4349051c",
+   "rev": "f72319c9686788305a8ab059f3c4d8c724785c83",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2b000e02d50394af68cfb4770a291113d94801b5",
+   "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.48",
+   "inputRev": "v0.0.50",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2689851f387bb2cef351e6825fe94a56a304ca13",
+   "rev": "79402ad9ab4be9a2286701a9880697e2351e4955",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -75,10 +75,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
+   "rev": "c104265c34eb8181af14e8dbc14c2f034292cb02",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -91,5 +91,5 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"}],
- "name": "base",
+ "name": "aeneas",
  "lakeDir": ".lake"}
diff --git a/backends/lean/lakefile.lean b/backends/lean/lakefile.lean
@@ -3,7 +3,7 @@ open Lake DSL
 
 -- Important: mathlib imports std4 and quote4: we mustn't add a `require std4` line
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git" @ "v4.15.0"
+  "https://github.com/leanprover-community/mathlib4.git" @ "v4.16.0-rc2"
 
 package «aeneas» {}
 

diff --git a/backends/lean/lean-toolchain b/backends/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.15.0
+leanprover/lean4:v4.16.0-rc2
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
@@ -436,18 +436,18 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
     -- TODO: canonize addition by default? We need a tactic to simplify arithmetic equalities
     -- with addition and substractions ((ℤ, +) is a group or something - there should exist a tactic
     -- somewhere in mathlib?)
-    simp [List.length_flatten_update_as_int_eq, *]
+    simp [List.length_flatten_update_as_int_eq, nhm, *]
     int_tac
 
   split_conjs
   . simp [inv] at *
     split_conjs
     . match h: lookup hm key with
       | none =>
-        simp [h, lookup] at *
+        simp [h, lookup, nhm] at *
         simp_all (config := {maxDischargeDepth := 1})
       | some _ =>
-        simp_all (config := {maxDischargeDepth := 1}) [lookup]
+        simp_all (config := {maxDischargeDepth := 1}) [lookup, nhm]
     . simp [slots_t_inv, slot_t_inv] at *
       intro i _
       have _ := hinv.right.left i (by simp_all (config := {maxDischargeDepth := 1}))
@@ -470,7 +470,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
       scalar_tac
     cases h_hm: k_hash_mod == hash_mod.val <;> simp_all (config := {zetaDelta := true, maxDischargeDepth := 2})
 
-  simp_all (config := {maxDischargeDepth := 1})
+  simp_all (config := {maxDischargeDepth := 1}) [nhm]
 
 private theorem slot_allP_not_key_lookup (slot : AList α) (h : slot.v.allP fun (k', _) => ¬k = k') :
   slot.lookup k = none := by

diff --git a/tests/lean/lake-manifest.json b/tests/lean/lake-manifest.json
@@ -12,20 +12,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9837ca9d65d9de6fad1ef4381750ca688774e608",
+   "rev": "15f16b1ec50f425147926be1aede7b4baa725380",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
-   "inherited": false,
+   "inputRev": "v4.16.0-rc2",
+   "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5",
+   "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -42,30 +42,30 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9a0b533c2fbd6195df067630be18e11e4349051c",
+   "rev": "f72319c9686788305a8ab059f3c4d8c724785c83",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2b000e02d50394af68cfb4770a291113d94801b5",
+   "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.48",
+   "inputRev": "v0.0.50",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2689851f387bb2cef351e6825fe94a56a304ca13",
+   "rev": "79402ad9ab4be9a2286701a9880697e2351e4955",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -82,10 +82,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
+   "rev": "c104265c34eb8181af14e8dbc14c2f034292cb02",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",

diff --git a/tests/lean/lean-toolchain b/tests/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.15.0
+leanprover/lean4:v4.16.0-rc2
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.15.0
		leanprover/lean4:v4.16.0-rc2