chore: bump Lean to v4.9.0 (#119)

* bump Lean to v4.9.0

* Fix compilation of Smt.Real

* Fix expected outputs of most test cases

* import Real.Star instead of Real.Basic

* Revert import Real.Star -> Real.Basic, update test case to reflect failure

Smt/Data/Sexp.lean

@@ -83,9 +83,9 @@ partial def parseOneAux : List Substring → Except ParseError (Sexp × List Sub
       return (atom tk.toString, tks)
   | [] => throw <| .incomplete "expected a token, got none"
 
-partial def parseManyAux :=
+partial def parseManyAux : List Substring → Except ParseError (Array Sexp × List Substring) :=
   go #[]
-where go (stk : Array Sexp) : List Substring → Except ParseError (Array Sexp × List Substring)
+where go (stk : Array Sexp)
   | tk :: tks => do
     if tk.front == ')' then .ok (stk, tk :: tks)
     else

Smt/Reconstruct/Real/Polynorm.lean

@@ -6,6 +6,7 @@ Authors: Abdalrhman Mohamed
 -/
 
 import Mathlib.Data.Real.Basic
+import Mathlib.Tactic.Ring.RingNF
 
 namespace Smt.Reconstruct.Real
 

Test/BitVec/Shift.expected

@@ -9,8 +9,8 @@ Test/BitVec/Shift.lean:5:8: warning: declaration uses 'sorry'
 goal: x ++ y = zeroExtend 6 x <<< 3#2 ||| zeroExtend 6 y
 
 query:
-(declare-const y (_ BitVec 3))
 (declare-const x (_ BitVec 3))
+(declare-const y (_ BitVec 3))
 (assert (distinct (concat x y) (bvor (bvshl ((_ zero_extend 3) x) #b11) ((_ zero_extend 3) y))))
 (check-sat)
 Test/BitVec/Shift.lean:10:8: warning: declaration uses 'sorry'

Test/Int/Binders.expected

@@ -1,7 +1,7 @@
 goal: curryAdd a b = curryAdd b a
 
 query:
-(define-fun curryAdd (([email protected]._hyg.3 Int) ([email protected]._hyg.5 Int)) Int (+ [email protected]._hyg.3 [email protected]._hyg.5))
+(define-fun curryAdd (([email protected]._hyg.4 Int) ([email protected]._hyg.6 Int)) Int (+ [email protected]._hyg.4 [email protected]._hyg.6))
 (declare-const b Int)
 (declare-const a Int)
 (assert (distinct (curryAdd a b) (curryAdd b a)))
@@ -10,7 +10,7 @@ Test/Int/Binders.lean:5:0: warning: declaration uses 'sorry'
 goal: partCurryAdd a b = partCurryAdd b a
 
 query:
-(define-fun partCurryAdd ((a Int) ([email protected]._hyg.33 Int)) Int (+ a [email protected]._hyg.33))
+(define-fun partCurryAdd ((a Int) ([email protected]._hyg.36 Int)) Int (+ a [email protected]._hyg.36))
 (declare-const b Int)
 (declare-const a Int)
 (assert (distinct (partCurryAdd a b) (partCurryAdd b a)))
@@ -19,7 +19,7 @@ Test/Int/Binders.lean:11:0: warning: declaration uses 'sorry'
 goal: partCurryAdd' a b = partCurryAdd' b a
 
 query:
-(define-fun |partCurryAdd'| ((a Int) ([email protected]._hyg.2347 Int)) Int (+ a [email protected]._hyg.2347))
+(define-fun |partCurryAdd'| ((a Int) ([email protected]._hyg.2495 Int)) Int (+ a [email protected]._hyg.2495))
 (declare-const b Int)
 (declare-const a Int)
 (assert (distinct (+ a b) (+ b a)))
@@ -29,8 +29,8 @@ goal: mismatchNamesAdd a b = mismatchNamesAdd b a
 
 query:
 (define-fun mismatchNamesAdd ((a Int) (b Int)) Int (+ a b))
-(declare-const a Int)
 (declare-const b Int)
+(declare-const a Int)
 (assert (distinct (mismatchNamesAdd a b) (mismatchNamesAdd b a)))
 (check-sat)
 Test/Int/Binders.lean:25:0: warning: declaration uses 'sorry'

Test/Int/Let.expected

@@ -19,7 +19,7 @@ goal: z 3 = 10
 
 query:
 (declare-fun f (Int) Int)
-(define-fun z (([email protected]._hyg.295 Int)) Int (f 10))
+(define-fun z (([email protected]._hyg.300 Int)) Int (f 10))
 (assert (= (f 10) 10))
 (assert (distinct (z 3) 10))
 (check-sat)

Test/Nat/Cong.expected

@@ -3,7 +3,7 @@ goal: x = y → f x = f y
 query:
 (define-sort Nat () Int)
 (declare-fun f (Nat) Nat)
-(assert (forall ((_uniq.1521 Nat)) (=> (>= _uniq.1521 0) (>= (f _uniq.1521) 0))))
+(assert (forall ((_uniq.1520 Nat)) (=> (>= _uniq.1520 0) (>= (f _uniq.1520) 0))))
 (declare-const x Nat)
 (assert (>= x 0))
 (declare-const y Nat)

Test/Nat/Sum'.expected

@@ -1,6 +1,6 @@
 Test/Nat/Sum'.lean:7:12: error: tactic 'assumption' failed
 case zero.a
-_uniq✝¹¹⁶⁰³⁻⁰ :
+_uniq✝⁹⁹³⁹⁻⁰ :
   ¬((∀ (n : Int), sum n = if n = 0 then 0 else n + sum (if 1 ≤ n then n - 1 else 0)) ∧
       (∀ («_uniq.4976» : Int), «_uniq.4976» ≥ 0 → sum «_uniq.4976» ≥ 0) ∧ Smt.Reconstruct.Builtin.distinct [sum 0, 0])
 ⊢ ¬Smt.Reconstruct.andN' [Nat → Nat] ¬sum 0 = 0 * (0 + 1) / 2
@@ -11,7 +11,7 @@ query:
 (declare-const n Nat)
 (assert (>= n 0))
 (define-fun-rec sum ((n Nat)) Nat (ite (= n 0) 0 (+ n (sum (ite (<= 1 n) (- n 1) 0)))))
-(assert (forall ((_uniq.13678 Nat)) (=> (>= _uniq.13678 0) (>= (sum _uniq.13678) 0))))
+(assert (forall ((_uniq.12014 Nat)) (=> (>= _uniq.12014 0) (>= (sum _uniq.12014) 0))))
 (assert (= (sum n) (div (* n (+ n 1)) 2)))
 (assert (distinct (sum (+ n 1)) (div (* (+ n 1) (+ (+ n 1) 1)) 2)))
 (check-sat)

Test/Real/Density.expected

@@ -6,3 +6,5 @@ query:
 (assert (not (=> (< x z) (exists ((y Real)) (and (< x y) (< y z))))))
 (check-sat)
 Test/Real/Density.lean:4:8: warning: declaration uses 'sorry'
+Test/Real/Density.lean:5:2: warning: 'smt_show' tactic does nothing
+note: this linter can be disabled with `set_option linter.unusedTactic false`

Test/Real/Inverse.expected

@@ -5,3 +5,5 @@ query:
 (assert (not (=> (distinct x 0.0) (exists ((y Real)) (= (* x y) 1.0)))))
 (check-sat)
 Test/Real/Inverse.lean:4:8: warning: declaration uses 'sorry'
+Test/Real/Inverse.lean:5:2: warning: 'smt_show' tactic does nothing
+note: this linter can be disabled with `set_option linter.unusedTactic false`

Test/linarith.expected

@@ -15,6 +15,7 @@ Test/linarith.lean:125:9: warning: unused variable `a`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
 Test/linarith.lean:125:13: warning: unused variable `c`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
+Test/linarith.lean:146:2: error: [arithPolyNorm]: could not prove x - y = -x + y
 Test/linarith.lean:168:34: warning: unused variable `z`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
 Test/linarith.lean:169:5: warning: unused variable `h5`

lake-manifest.json

@@ -1,4 +1,4 @@
-{"version": 7,
+{"version": "1.0.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/abdoo8080/lean-cvc5.git",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "551ff2d7dffd7af914cdbd01abbd449fe3e3d428",
+   "rev": "54bb04c3119f24fde14b9068c4b2e69db52a1450",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
+   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,7 +31,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "53ba96ad7666d4a2515292974631629b5ea5dfee",
+   "rev": "06cca4bd36b2af743d4858c5cc31604aa9da26bc",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -40,10 +40,10 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
+   "rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.36",
+   "inputRev": "v0.0.38",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "77e081815b30b0d30707e1c5b0c6a6761f7a2404",
+   "rev": "c29c3cdce415240e9dcec5c583ad5d36f83f9c71",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -67,10 +67,10 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "b5eba595428809e96f3ed113bc7ba776c5f801ac",
+   "rev": "f0957a7575317490107578ebaee9efaf8e62a4ab",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.8.0",
+   "inputRev": "v4.9.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "smt",

lakefile.lean

@@ -6,7 +6,7 @@ require cvc5 from
   git "https://github.com/abdoo8080/lean-cvc5.git" @ "main"
 
 require mathlib from
-  git "https://github.com/leanprover-community/mathlib4.git" @ "v4.8.0"
+  git "https://github.com/leanprover-community/mathlib4.git" @ "v4.9.0"
 
 def libcpp : String :=
   if System.Platform.isWindows then "libstdc++-6.dll"

lean-toolchain

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