Update the Lean tests and fix the proofs

AeneasVerif · Aug 27, 2024 · 367edbb · 367edbb
1 parent b91ecb8
commit 367edbb
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 14 deletions.
diff --git a/backends/lean/lake-manifest.json b/backends/lean/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1d25ec7ec98d6d9fb526c997aa014bcabbad8b72",
+   "rev": "e6d3a32d66252a70fda1d56463e1da975b3b8f53",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "776a5a8f9c789395796e442d78a9d4cb9c4c9d03",
+   "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c9eabb1358d52f6b7dfd1cabdea4e4fa2632b1f3",
+   "rev": "9d7806d77c33a5e19050de8fbdc106a28150ec71",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

diff --git a/tests/lean/Avl/Properties.lean b/tests/lean/Avl/Properties.lean
@@ -800,7 +800,6 @@ theorem Tree.insert_in_opt_node_spec
     split_conjs
     . simp [Node.invAux, Node.balanceFactor]
     . simp [Subtree.inv]
-    . apply Set.ext; simp
   . -- tree = some
     rename Node T => node
     have hNodeInv : Node.inv node := by simp_all

diff --git a/tests/lean/lake-manifest.json b/tests/lean/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c0efc1fd2a0bec51bd55c5b17348af13d7419239",
+   "rev": "e6d3a32d66252a70fda1d56463e1da975b3b8f53",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
+   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cf30d04b6448dbb5a5b30a7d031e3949e74b9dd1",
+   "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,27 +35,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
+   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.39",
+   "inputRev": "v0.0.41",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
+   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c198452b2993c475770cdfa2801ad2a29fd35194",
+   "rev": "9d7806d77c33a5e19050de8fbdc106a28150ec71",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

diff --git a/tests/lean/lean-toolchain b/tests/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.10.0-rc2
+leanprover/lean4:v4.11.0-rc2