Merge branch 'son/update-lean' into son/scalar_tac

AeneasVerif · Jul 3, 2024 · 0efea04 · 0efea04
2 parents 7870acc + 2db905b
commit 0efea04
Show file tree

Hide file tree

Showing 5 changed files with 44 additions and 26 deletions.
diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
@@ -1066,7 +1066,7 @@ namespace Ex3
     ∀ k x, is_valid_p k (λ k => is_even_is_odd_body k x) := by
     intro k x
     simp [is_even_is_odd_body]
-    split <;> (try simp) <;> split <;> try simp
+    split <;> split <;> try simp
     apply is_valid_p_bind; simp
     intros; split <;> simp
     apply is_valid_p_bind; simp
@@ -1159,7 +1159,7 @@ namespace Ex4
     intro k
     apply (Funs.is_valid_p_is_valid_p tys)
     simp [Funs.is_valid_p]
-    (repeat (apply And.intro)) <;> intro x <;> (try simp at x) <;>
+    (repeat (apply And.intro)) <;> intro x <;>
     simp only [is_even_body, is_odd_body]
     -- Prove the validity of the individual bodies
     . split <;> simp
@@ -1301,7 +1301,7 @@ namespace Ex6
     intro k
     apply (Funs.is_valid_p_is_valid_p tys)
     simp [Funs.is_valid_p]
-    (repeat (apply And.intro)); intro x; try simp at x
+    intro x; try simp at x
     simp only [list_nth_body]
     -- Prove the validity of the individual bodies
     intro k x
@@ -1395,7 +1395,7 @@ namespace Ex7
     intro k
     apply (Funs.is_valid_p_is_valid_p tys)
     simp [Funs.is_valid_p]
-    (repeat (apply And.intro)); intro x; try simp at x
+    intro x; try simp at x
     simp only [list_nth_body]
     -- Prove the validity of the individual bodies
     intro k x
@@ -1539,10 +1539,13 @@ namespace Ex9
     simp only [id_body]
     split <;> try simp
     . apply is_valid_p_same
-    . apply is_valid_p_bind <;> try simp [*]
-      -- We have to show that `map k tl` is valid
-      -- Remark: `map_is_valid` doesn't work here, we need the specialized version
-      apply map_is_valid_simple
+    . apply is_valid_p_bind
+      . -- We have to show that `map k tl` is valid
+        -- Remark: `map_is_valid` doesn't work here, we need the specialized version
+        apply map_is_valid_simple
+      . -- TODO: why isn't `is_valid_p_same` automatically applied?
+        intro tl
+        apply is_valid_p_same
 
   def body (k : (i : Fin 1) → (t : ty i) → (x : input_ty i t) → Result (output_ty i t)) (i: Fin 1) :
     (t : ty i) → (x : input_ty i t) → Result (output_ty i t) := get_fun bodies i k

diff --git a/backends/lean/lake-manifest.json b/backends/lean/lake-manifest.json
@@ -1,10 +1,11 @@
-{"version": "1.0.0",
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "555ec79bc6effe7009036184a5f73f7d8d4850ed",
+   "scope": "leanprover-community",
+   "rev": "bba0af6e930ebcbabfacf021b21dd881d58aaa9d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,6 +14,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
+   "scope": "leanprover-community",
    "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
@@ -22,7 +24,8 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "30619d94ce4a3d69cdb87bb1771562ca2e687cfa",
+   "scope": "leanprover-community",
+   "rev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,25 +34,28 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9",
+   "scope": "leanprover-community",
+   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.38",
+   "inputRev": "v0.0.39",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
+   "scope": "",
    "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96",
+   "scope": "leanprover-community",
+   "rev": "d366a602cc4a325a6f9db3a3991dfa6d6cf409c5",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +64,8 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "dfc07f1b6271219de25170e4936fee9443d4234c",
+   "scope": "",
+   "rev": "5d74b273dd4c171c1f57a2d75abc1d3e27d7095a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

diff --git a/backends/lean/lean-toolchain b/backends/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.9.0
+leanprover/lean4:v4.10.0-rc1
diff --git a/tests/lean/lake-manifest.json b/tests/lean/lake-manifest.json
@@ -1,10 +1,11 @@
-{"version": "1.0.0",
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "555ec79bc6effe7009036184a5f73f7d8d4850ed",
+   "scope": "leanprover-community",
+   "rev": "bba0af6e930ebcbabfacf021b21dd881d58aaa9d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,6 +14,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
+   "scope": "leanprover-community",
    "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
@@ -22,7 +24,8 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "30619d94ce4a3d69cdb87bb1771562ca2e687cfa",
+   "scope": "leanprover-community",
+   "rev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,25 +34,28 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9",
+   "scope": "leanprover-community",
+   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.38",
+   "inputRev": "v0.0.39",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
+   "scope": "",
    "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96",
+   "scope": "leanprover-community",
+   "rev": "d366a602cc4a325a6f9db3a3991dfa6d6cf409c5",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,13 +64,15 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "cd9e3a31766a3a445d8bcb7e0203d96e2248e104",
+   "scope": "",
+   "rev": "c4d0126454325b56a077619f507c8ad690a4a0bb",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"type": "path",
+   "scope": "",
    "name": "base",
    "manifestFile": "lake-manifest.json",
    "inherited": false,

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