From 139bf3da7ec9dfcf9a3278417a4b98e1bbe71ed0 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed Date: Sat, 22 Jun 2024 14:51:45 -0500 Subject: [PATCH 1/4] Sync with cvc5 main. (#116) --- Smt/Reconstruct.lean | 1 + Smt/Reconstruct/BitVec.lean | 32 ++++++++++++++++---------------- lake-manifest.json | 2 +- 3 files changed, 18 insertions(+), 17 deletions(-) diff --git a/Smt/Reconstruct.lean b/Smt/Reconstruct.lean index 5ed1e440..eec9e5db 100644 --- a/Smt/Reconstruct.lean +++ b/Smt/Reconstruct.lean @@ -203,6 +203,7 @@ def solve (query : String) (timeout : Option Nat) : MetaM (Except Error cvc5.Pro if r.isUnsat then let ps ← Solver.getProof if h : 0 < ps.size then + trace[smt.solve] "proof:\n{← Solver.proofToString ps[0]}" return ps[0] throw (self := instMonadExceptOfMonadExceptOf _ _) (Error.user_error "something went wrong") diff --git a/Smt/Reconstruct/BitVec.lean b/Smt/Reconstruct/BitVec.lean index fec2dd77..1ccb309a 100644 --- a/Smt/Reconstruct/BitVec.lean +++ b/Smt/Reconstruct/BitVec.lean @@ -47,7 +47,7 @@ partial def synthDecidableInst (t : cvc5.Term) : ReconstructM Expr := do match t return q(@instDecidableEqBitVec $w) let p : Q(Prop) ← reconstructTerm t Meta.synthInstance q(Decidable $p) - | .BITVECTOR_BITOF => + | .BITVECTOR_BIT => let w : Nat := t[0]!.getSort.getBitVectorSize.val let x : Q(BitVec $w) ← reconstructTerm t[0]! let i : Nat := t.getOp[0]!.getIntegerValue.toNat @@ -70,16 +70,6 @@ where let w : Nat := t.getSort.getBitVectorSize.val let v : Nat := (t.getBitVectorValue 10).toNat! return q(BitVec.ofNat $w $v) - | .BITVECTOR_BB_TERM => - let w : Nat := t.getNumChildren - let bs : Q(BitVec 0) := q(.nil) - let f (bs : Expr) (i : Nat) : ReconstructM Expr := do - let p : Q(Prop) ← reconstructTerm t[i]! - let bs : Q(BitVec $i) := bs - let hp : Q(Decidable $p) ← synthDecidableInst t[i]! - return q(@BitVec.cons $i (@decide $p $hp) $bs) - let bs : Q(BitVec $w) ← (List.range w).foldlM f bs - return q($bs) | .BITVECTOR_CONCAT => let n : Nat := t.getNumChildren let w₁ : Nat := t[0]!.getSort.getBitVectorSize.val @@ -192,11 +182,6 @@ where let j : Nat := t.getOp[1]!.getIntegerValue.toNat let x : Q(BitVec $w) ← reconstructTerm t[0]! return q(«$x».extractLsb $i $j) - | .BITVECTOR_BITOF => - let w : Nat := t[0]!.getSort.getBitVectorSize.val - let x : Q(BitVec $w) ← reconstructTerm t[0]! - let i : Nat := t.getOp[0]!.getIntegerValue.toNat - return q(«$x».getLsb $i = true) | .BITVECTOR_REPEAT => let w : Nat := t.getSort.getBitVectorSize.val let n : Nat := t.getOp[0]!.getIntegerValue.toNat @@ -230,6 +215,21 @@ where let w : Nat := t[0]!.getSort.getBitVectorSize.val let x : Q(BitVec $w) ← reconstructTerm t[0]! return q(«$x».toNat) + | .BITVECTOR_FROM_BOOLS => + let w : Nat := t.getNumChildren + let bs : Q(BitVec 0) := q(.nil) + let f (bs : Expr) (i : Nat) : ReconstructM Expr := do + let p : Q(Prop) ← reconstructTerm t[i]! + let bs : Q(BitVec $i) := bs + let hp : Q(Decidable $p) ← synthDecidableInst t[i]! + return q(@BitVec.cons $i (@decide $p $hp) $bs) + let bs : Q(BitVec $w) ← (List.range w).foldlM f bs + return q($bs) + | .BITVECTOR_BIT => + let w : Nat := t[0]!.getSort.getBitVectorSize.val + let x : Q(BitVec $w) ← reconstructTerm t[0]! + let i : Nat := t.getOp[0]!.getIntegerValue.toNat + return q(«$x».getLsb $i = true) | _ => return none where leftAssocOp (op : Expr) (t : cvc5.Term) : ReconstructM Expr := do diff --git a/lake-manifest.json b/lake-manifest.json index 0bf1bf8d..0283d11e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/abdoo8080/lean-cvc5.git", "type": "git", "subDir": null, - "rev": "1088ef5027ca324c83b13bee1d5eb5e3d27e8ce4", + "rev": "b8f4760a168cf2735ba2848d6af9598c2883c129", "name": "cvc5", "manifestFile": "lake-manifest.json", "inputRev": "main", From 921d31e4d5f5167fc376cb65b38f51f98cbfc3fd Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed Date: Sun, 23 Jun 2024 22:11:18 -0500 Subject: [PATCH 2/4] Fix solver tests. (#117) --- Test/Solver/Error.expected | 2 +- Test/Solver/Error.lean | 13 ++++++++++++- Test/Solver/Interactive.lean | 13 ++++++++++++- Test/Solver/Model.lean | 13 ++++++++++++- Test/Solver/Proof.lean | 13 ++++++++++++- Test/Solver/Triv.lean | 13 ++++++++++++- Test/linarith.expected | 1 - 7 files changed, 61 insertions(+), 7 deletions(-) diff --git a/Test/Solver/Error.expected b/Test/Solver/Error.expected index c209b417..038cdd14 100644 --- a/Test/Solver/Error.expected +++ b/Test/Solver/Error.expected @@ -1,2 +1,2 @@ -Test/Solver/Error.lean:15:0: error: Cannot bind x to symbol of type Int, maybe the symbol has already been defined? +Test/Solver/Error.lean:26:0: error: Cannot bind x to symbol of type Int, maybe the symbol has already been defined? diff --git a/Test/Solver/Error.lean b/Test/Solver/Error.lean index f3b3e4a8..d6c563e4 100644 --- a/Test/Solver/Error.lean +++ b/Test/Solver/Error.lean @@ -2,6 +2,17 @@ import Smt.Translate.Solver open Smt Translate Solver +def cvc5.os := + if System.Platform.isWindows then "Win64" + else if System.Platform.isOSX then "macOS" + else "Linux" + +def cvc5.arch := + if System.Platform.target.startsWith "x86_64" then "x86_64" + else "arm64" + +def cvc5.target := s!"{os}-{arch}-static" + def query : SolverM Result := do setLogic "LIA" declareConst "x" (.symbolT "Int") @@ -9,7 +20,7 @@ def query : SolverM Result := do checkSat def main : IO Unit := do - let ss ← createFromKind .cvc5 ".lake/packages/cvc5/.lake/cvc5/bin/cvc5" none + let ss ← createFromKind .cvc5 s!".lake/packages/cvc5/.lake/cvc5-{cvc5.target}/bin/cvc5" none _ ← StateT.run query ss #eval main diff --git a/Test/Solver/Interactive.lean b/Test/Solver/Interactive.lean index 8d4fc706..8aa532af 100644 --- a/Test/Solver/Interactive.lean +++ b/Test/Solver/Interactive.lean @@ -2,6 +2,17 @@ import Smt.Translate.Solver open Smt Translate Solver +def cvc5.os := + if System.Platform.isWindows then "Win64" + else if System.Platform.isOSX then "macOS" + else "Linux" + +def cvc5.arch := + if System.Platform.target.startsWith "x86_64" then "x86_64" + else "arm64" + +def cvc5.target := s!"{os}-{arch}-static" + open Term in def query : SolverM Result := do setLogic "LIA" @@ -17,7 +28,7 @@ def query : SolverM Result := do return res def main : IO Unit := do - let ss ← createFromKind .cvc5 ".lake/packages/cvc5/.lake/cvc5/bin/cvc5" none + let ss ← createFromKind .cvc5 s!".lake/packages/cvc5/.lake/cvc5-{cvc5.target}/bin/cvc5" none let (res, ss) ← StateT.run query ss _ ← StateT.run exit ss println! "query:\n{Command.cmdsAsQuery ss.commands.reverse}\n\nres: {res}" diff --git a/Test/Solver/Model.lean b/Test/Solver/Model.lean index a8eafc07..3c379a81 100644 --- a/Test/Solver/Model.lean +++ b/Test/Solver/Model.lean @@ -2,6 +2,17 @@ import Smt.Translate.Solver open Smt Translate Solver +def cvc5.os := + if System.Platform.isWindows then "Win64" + else if System.Platform.isOSX then "macOS" + else "Linux" + +def cvc5.arch := + if System.Platform.target.startsWith "x86_64" then "x86_64" + else "arm64" + +def cvc5.target := s!"{os}-{arch}-static" + def query : SolverM (Result × Sexp) := do setLogic "LIA" setOption "produce-models" "true" @@ -9,7 +20,7 @@ def query : SolverM (Result × Sexp) := do return (← checkSat, ← getModel) def main : IO Unit := do - let ss ← createFromKind .cvc5 ".lake/packages/cvc5/.lake/cvc5/bin/cvc5" none + let ss ← createFromKind .cvc5 s!".lake/packages/cvc5/.lake/cvc5-{cvc5.target}/bin/cvc5" none let ((res, model), ss) ← StateT.run query ss _ ← StateT.run exit ss println! "query:\n{Command.cmdsAsQuery ss.commands.reverse}\n\nres: {res}\n\nmodel:\n{model}" diff --git a/Test/Solver/Proof.lean b/Test/Solver/Proof.lean index aa7f0301..306e7b0f 100644 --- a/Test/Solver/Proof.lean +++ b/Test/Solver/Proof.lean @@ -2,6 +2,17 @@ import Smt.Translate.Solver open Smt Translate Solver +def cvc5.os := + if System.Platform.isWindows then "Win64" + else if System.Platform.isOSX then "macOS" + else "Linux" + +def cvc5.arch := + if System.Platform.target.startsWith "x86_64" then "x86_64" + else "arm64" + +def cvc5.target := s!"{os}-{arch}-static" + def query : SolverM Sexp := do setLogic "QF_UF" assert (.symbolT "false") @@ -9,7 +20,7 @@ def query : SolverM Sexp := do getProof def main : IO Unit := do - let ss ← createFromKind .cvc5 ".lake/packages/cvc5/.lake/cvc5/bin/cvc5" none + let ss ← createFromKind .cvc5 s!".lake/packages/cvc5/.lake/cvc5-{cvc5.target}/bin/cvc5" none let (res, ss) ← StateT.run query ss _ ← StateT.run exit ss println! "query:\n{Command.cmdsAsQuery ss.commands.reverse}\n\nres: unsat\n\nproof:\n{res}" diff --git a/Test/Solver/Triv.lean b/Test/Solver/Triv.lean index 00ea37b9..c5d9598d 100644 --- a/Test/Solver/Triv.lean +++ b/Test/Solver/Triv.lean @@ -2,10 +2,21 @@ import Smt.Translate.Solver open Smt Translate Solver +def cvc5.os := + if System.Platform.isWindows then "Win64" + else if System.Platform.isOSX then "macOS" + else "Linux" + +def cvc5.arch := + if System.Platform.target.startsWith "x86_64" then "x86_64" + else "arm64" + +def cvc5.target := s!"{os}-{arch}-static" + def query : SolverM Result := checkSat def main : IO Unit := do - let ss ← createFromKind .cvc5 ".lake/packages/cvc5/.lake/cvc5/bin/cvc5" none + let ss ← createFromKind .cvc5 s!".lake/packages/cvc5/.lake/cvc5-{cvc5.target}/bin/cvc5" none let (res, ss) ← StateT.run query ss _ ← StateT.run exit ss println! "query:\n{Command.cmdsAsQuery ss.commands.reverse}\n\nres: {res}" diff --git a/Test/linarith.expected b/Test/linarith.expected index e0eb6602..76436fc4 100644 --- a/Test/linarith.expected +++ b/Test/linarith.expected @@ -15,7 +15,6 @@ Test/linarith.lean:124:9: warning: unused variable `a` note: this linter can be disabled with `set_option linter.unusedVariables false` Test/linarith.lean:124:13: warning: unused variable `c` note: this linter can be disabled with `set_option linter.unusedVariables false` -Test/linarith.lean:145:2: error: [arithPolyNorm]: could not prove x - y = -x + y Test/linarith.lean:167:34: warning: unused variable `z` note: this linter can be disabled with `set_option linter.unusedVariables false` Test/linarith.lean:168:5: warning: unused variable `h5` From 2899f02744cc12636f71c04e200bce0b308f73b5 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed Date: Sun, 23 Jun 2024 22:41:34 -0500 Subject: [PATCH 3/4] Split proof reconstruction for integers and reals. (#112) --- .github/workflows/ci.yml | 1 + Smt.lean | 2 +- Smt/Int.lean | 9 + Smt/Rat.lean | 8 + Smt/Real.lean | 9 + Smt/Reconstruct/Int.lean | 469 +++++++++++++++++++++++ Smt/Reconstruct/Int/Lemmas.lean | 167 ++++---- Smt/Reconstruct/Int/Polynorm.lean | 241 ++++++++++++ Smt/Reconstruct/Int/Rewrites.lean | 7 +- Smt/Reconstruct/Rat.lean | 458 ++++++++++++++++++++++ Smt/Reconstruct/Rat/Core.lean | 23 ++ Smt/Reconstruct/Rat/Lemmas.lean | 210 ++++++++++ Smt/Reconstruct/Rat/Polynorm.lean | 289 ++++++++++++++ Smt/Reconstruct/Rat/Rewrites.lean | 83 ++++ Smt/Reconstruct/Real.lean | 488 ++++++++++++++++++++++++ Smt/Reconstruct/Real/Lemmas.lean | 337 ++++++++++++++++ Smt/Reconstruct/Real/Polynorm.lean | 79 ++++ Smt/Reconstruct/Real/Rewrites.lean | 95 +++++ Test/BitVec/Shift.expected | 2 +- Test/BitVec/XorComm.expected | 4 +- Test/Bool/Assoc.expected | 4 +- Test/Bool/Comm.expected | 2 +- Test/Bool/Cong.expected | 2 +- Test/Bool/Conjunction.expected | 2 +- Test/Bool/DisjunctiveSyllogism.expected | 2 +- Test/Bool/PropExt.expected | 2 +- Test/Bool/Resolution.expected | 2 +- Test/Bool/Trans.expected | 2 +- Test/Int/Arith.expected | 83 +++- Test/Int/Binders.expected | 8 +- Test/Int/Cong.expected | 8 - Test/Int/Cong.lean | 3 +- Test/Int/DefineSort.expected | 2 +- Test/Int/Dvd.expected | 4 +- Test/Int/DvdTimeout.expected | 6 +- Test/Int/Let.expected | 28 +- Test/Int/Let.lean | 4 +- Test/Int/Neg.expected | 9 - Test/Int/Neg.lean | 2 +- Test/Nat/Cong.expected | 2 +- Test/Nat/Forall'.expected | 2 +- Test/Nat/Max.expected | 12 +- Test/Nat/NeqZero.expected | 4 +- Test/Nat/Sum'.expected | 9 +- Test/Nat/ZeroSub'.expected | 6 +- Test/Nat/ZeroSub.lean | 2 +- Test/Real/Density.expected | 2 +- Test/Real/Density.lean | 1 + Test/Real/Inverse.expected | 2 +- Test/Real/Inverse.lean | 1 + Test/String/Length.expected | 2 +- Test/linarith.expected | 22 +- Test/linarith.lean | 1 + lakefile.lean | 14 +- 54 files changed, 3020 insertions(+), 218 deletions(-) create mode 100644 Smt/Int.lean create mode 100644 Smt/Rat.lean create mode 100644 Smt/Real.lean create mode 100644 Smt/Reconstruct/Int.lean create mode 100644 Smt/Reconstruct/Int/Polynorm.lean create mode 100644 Smt/Reconstruct/Rat.lean create mode 100644 Smt/Reconstruct/Rat/Core.lean create mode 100644 Smt/Reconstruct/Rat/Lemmas.lean create mode 100644 Smt/Reconstruct/Rat/Polynorm.lean create mode 100644 Smt/Reconstruct/Rat/Rewrites.lean create mode 100644 Smt/Reconstruct/Real.lean create mode 100644 Smt/Reconstruct/Real/Lemmas.lean create mode 100644 Smt/Reconstruct/Real/Polynorm.lean create mode 100644 Smt/Reconstruct/Real/Rewrites.lean diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 38bf4cad..63d200ae 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -25,5 +25,6 @@ jobs: lake update lake build lake build +Smt:dynlib + lake build +Smt.Real:dynlib - name: Test lean-smt run: lake run test diff --git a/Smt.lean b/Smt.lean index 4f17e0cb..3d20e9b6 100644 --- a/Smt.lean +++ b/Smt.lean @@ -5,10 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Abdalrhman Mohamed -/ -import Smt.Arith import Smt.BitVec import Smt.Bool import Smt.Builtin +import Smt.Int import Smt.Nat import Smt.Options import Smt.Prop diff --git a/Smt/Int.lean b/Smt/Int.lean new file mode 100644 index 00000000..e1ace45e --- /dev/null +++ b/Smt/Int.lean @@ -0,0 +1,9 @@ +/- +Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abdalrhman Mohamed +-/ + +import Smt.Reconstruct.Int +import Smt.Translate.Int diff --git a/Smt/Rat.lean b/Smt/Rat.lean new file mode 100644 index 00000000..f9e2503e --- /dev/null +++ b/Smt/Rat.lean @@ -0,0 +1,8 @@ +/- +Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abdalrhman Mohamed +-/ + +import Smt.Reconstruct.Rat diff --git a/Smt/Real.lean b/Smt/Real.lean new file mode 100644 index 00000000..fb3784a8 --- /dev/null +++ b/Smt/Real.lean @@ -0,0 +1,9 @@ +/- +Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abdalrhman Mohamed +-/ + +import Smt.Reconstruct.Real +import Smt.Translate.Real diff --git a/Smt/Reconstruct/Int.lean b/Smt/Reconstruct/Int.lean new file mode 100644 index 00000000..d45b0f00 --- /dev/null +++ b/Smt/Reconstruct/Int.lean @@ -0,0 +1,469 @@ +/- +Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abdalrhman Mohamed +-/ + +import Smt.Reconstruct +import Smt.Reconstruct.Builtin.Lemmas +import Smt.Reconstruct.Int.Lemmas +import Smt.Reconstruct.Int.Polynorm +import Smt.Reconstruct.Int.Rewrites +import Smt.Reconstruct.Rewrite + +namespace Smt.Reconstruct.Int + +open Lean +open Qq + +@[smt_sort_reconstruct] def reconstructIntSort : SortReconstructor := fun s => do match s.getKind with + | .INTEGER_SORT => return q(Int) + | _ => return none + +@[smt_term_reconstruct] def reconstructInt : TermReconstructor := fun t => do match t.getKind with + | .SKOLEM => match t.getSkolemId with + | .INT_DIV_BY_ZERO => return q(fun (x : Int) => x / 0) + | .MOD_BY_ZERO => return q(fun (x : Int) => x % 0) + | _ => return none + | .CONST_INTEGER => + let x : Int := t.getIntegerValue + let x' : Q(Nat) := mkRawNatLit x.natAbs + if x ≥ 0 then + return q(OfNat.ofNat $x' : Int) + else + return q(-(OfNat.ofNat $x' : Int)) + | .NEG => + if !t.getSort.isInteger then return none + let x : Q(Int) ← reconstructTerm t[0]! + return q(-$x) + | .SUB => + if !t.getSort.isInteger then return none + leftAssocOp q(@HSub.hSub Int Int Int _) t + | .ADD => + if !t.getSort.isInteger then return none + leftAssocOp q(@HAdd.hAdd Int Int Int _) t + | .MULT => + if !t.getSort.isInteger then return none + leftAssocOp q(@HMul.hMul Int Int Int _) t + | .INTS_DIVISION => + leftAssocOp q(@HDiv.hDiv Int Int Int _) t + | .INTS_DIVISION_TOTAL => + leftAssocOp q(@HDiv.hDiv Int Int Int _) t + | .INTS_MODULUS => + let x : Q(Int) ← reconstructTerm t[0]! + let y : Q(Int) ← reconstructTerm t[1]! + return q($x % $y) + | .INTS_MODULUS_TOTAL => + let x : Q(Int) ← reconstructTerm t[0]! + let y : Q(Int) ← reconstructTerm t[1]! + return q($x % $y) + | .ABS => + if !t.getSort.isInteger then return none + let x : Q(Int) ← reconstructTerm t[0]! + return q(if $x < 0 then -$x else $x) + | .LEQ => + if !t[0]!.getSort.isInteger then return none + let x : Q(Int) ← reconstructTerm t[0]! + let y : Q(Int) ← reconstructTerm t[1]! + return q($x ≤ $y) + | .LT => + if !t[0]!.getSort.isInteger then return none + let x : Q(Int) ← reconstructTerm t[0]! + let y : Q(Int) ← reconstructTerm t[1]! + return q($x < $y) + | .GEQ => + if !t[0]!.getSort.isInteger then return none + let x : Q(Int) ← reconstructTerm t[0]! + let y : Q(Int) ← reconstructTerm t[1]! + return q($x ≥ $y) + | .GT => + if !t[0]!.getSort.isInteger then return none + let x : Q(Int) ← reconstructTerm t[0]! + let y : Q(Int) ← reconstructTerm t[1]! + return q($x > $y) + | _ => return none +where + leftAssocOp (op : Expr) (t : cvc5.Term) : ReconstructM Expr := do + let mut curr ← reconstructTerm t[0]! + for i in [1:t.getNumChildren] do + curr := mkApp2 op curr (← reconstructTerm t[i]!) + return curr + +def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do + match pf.getRewriteRule with + | .ARITH_PLUS_ZERO => + if !pf.getArguments[1]![0]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.add_assoc) q(Int.add_zero) q(@Rewrite.plus_zero) args) + | .ARITH_MUL_ONE => + if !pf.getArguments[1]![0]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.mul_assoc) q(Int.mul_one) q(@Rewrite.mul_one) args) + | .ARITH_MUL_ZERO => + if !pf.getArguments[1]![0]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.mul_assoc) q(Int.mul_one) q(@Rewrite.mul_zero) args) + | .ARITH_INT_DIV_TOTAL => + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + let h : Q($s ≠ 0) ← reconstructProof pf.getChildren[0]! + addThm q($t / $s = $t / $s) q(@Rewrite.int_div_total $t $s $h) + | .ARITH_INT_DIV_TOTAL_ONE => + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q($t / 1 = $t) q(@Rewrite.int_div_total_one $t) + | .ARITH_INT_DIV_TOTAL_ZERO => + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q($t / 0 = 0) q(@Rewrite.int_div_total_zero $t) + | .ARITH_INT_MOD_TOTAL => + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + let h : Q($s ≠ 0) ← reconstructProof pf.getChildren[0]! + addThm q($t % $s = $t % $s) q(@Rewrite.int_mod_total $t $s $h) + | .ARITH_INT_MOD_TOTAL_ONE => + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q($t % 1 = 0) q(@Rewrite.int_mod_total_one $t) + | .ARITH_INT_MOD_TOTAL_ZERO => + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q($t % 0 = $t) q(@Rewrite.int_mod_total_zero $t) + | .ARITH_NEG_NEG_ONE => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q(-1 * (-1 * $t) = $t) q(@Rewrite.neg_neg_one $t) + | .ARITH_ELIM_UMINUS => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q(-$t = -1 * $t) q(@Rewrite.elim_uminus $t) + | .ARITH_ELIM_MINUS => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + addThm q($t - $s = $t + -1 * $s) q(@Rewrite.elim_minus $t $s) + | .ARITH_ELIM_GT => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + addThm q(($t > $s) = ¬($t ≤ $s)) q(@Rewrite.elim_gt $t $s) + | .ARITH_ELIM_LT => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + addThm q(($t < $s) = ¬($t ≥ $s)) q(@Rewrite.elim_lt $t $s) + | .ARITH_ELIM_INT_GT => + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + addThm q(($t > $s) = ($t ≥ $s + 1)) q(@Rewrite.elim_int_gt $t $s) + | .ARITH_ELIM_INT_LT => + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + addThm q(($t < $s) = ($s ≥ $t + 1)) q(@Rewrite.elim_int_lt $t $s) + | .ARITH_ELIM_LEQ => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + addThm q(($t ≤ $s) = ($s ≥ $t)) q(@Rewrite.elim_leq $t $s) + | .ARITH_LEQ_NORM => + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + addThm q(($t ≤ $s) = ¬($t ≥ $s + 1)) q(@Rewrite.leq_norm $t $s) + | .ARITH_GEQ_TIGHTEN => + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + addThm q((¬($t ≥ $s)) = ($s ≥ $t + 1)) q(@Rewrite.geq_tighten $t $s) + | .ARITH_GEQ_NORM1 => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + addThm q(($t ≥ $s) = ($t - $s ≥ 0)) q(@Rewrite.geq_norm1 $t $s) + | .ARITH_GEQ_NORM2 => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + let s : Q(Int) ← reconstructTerm pf.getArguments[2]! + addThm q(($t ≥ $s) = (-$t ≤ -$s)) q(@Rewrite.geq_norm2 $t $s) + | .ARITH_REFL_LEQ => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q(($t ≤ $t) = True) q(@Rewrite.refl_leq $t) + | .ARITH_REFL_LT => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q(($t < $t) = False) q(@Rewrite.refl_lt $t) + | .ARITH_REFL_GEQ => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q(($t ≥ $t) = True) q(@Rewrite.refl_geq $t) + | .ARITH_REFL_GT => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q(($t > $t) = False) q(@Rewrite.refl_gt $t) + | .ARITH_PLUS_FLATTEN => + if !pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.add_assoc) q(Int.add_zero) q(@Rewrite.plus_flatten) args) + | .ARITH_MULT_FLATTEN => + if !pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.mul_assoc) q(Int.mul_one) q(@Rewrite.mult_flatten) args) + | .ARITH_MULT_DIST => + if !pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.mul_assoc) q(Int.mul_one) q(@Rewrite.mult_dist) args) + | .ARITH_PLUS_CANCEL1 => + if !pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.mul_assoc) q(Int.mul_one) q(@Rewrite.plus_cancel1) args) + | .ARITH_PLUS_CANCEL2 => + if !pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.add_assoc) q(Int.add_zero) q(@Rewrite.plus_cancel2) args) + | .ARITH_ABS_ELIM => + if !pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Int) ← reconstructTerm pf.getArguments[1]! + addThm q(ite ($t < 0) (-$t) $t = ite ($t < 0) (-$t) $t) q(@Rewrite.abs_elim $t) + | _ => return none +where + reconstructArgs (args : Array cvc5.Term) : ReconstructM (Array (Array Expr)) := do + let mut args' := #[] + for arg in args do + let mut arg' := #[] + for subarg in arg do + arg' := arg'.push (← reconstructTerm subarg) + args' := args'.push arg' + return args' + +def reconstructSumUB (pf : cvc5.Proof) : ReconstructM (Option Expr) := do + let f := fun (ks, ls, rs, hs) p => do + let l : Q(Int) ← reconstructTerm p.getResult[0]! + let r : Q(Int) ← reconstructTerm p.getResult[1]! + let lsl := q($ls + $l) + let rsr := q($rs + $r) + let k := p.getResult.getKind + if ks == .LT && k == .LT then + let hs : Q($ls < $rs) := hs + let h : Q($l < $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Int.sum_ub₁ $hs $h)) + else if ks == .LT && k == .LEQ then + let hs : Q($ls < $rs) := hs + let h : Q($l ≤ $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Int.sum_ub₂ $hs $h)) + else if ks == .LT && k == .EQUAL then + let hs : Q($ls < $rs) := hs + let h : Q($l = $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Int.sum_ub₃ $hs $h)) + else if ks == .LEQ && k == .LT then + let hs : Q($ls ≤ $rs) := hs + let h : Q($l < $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Int.sum_ub₄ $hs $h)) + else if ks == .LEQ && k == .LEQ then + let hs : Q($ls ≤ $rs) := hs + let h : Q($l ≤ $r) ← reconstructProof p + return (.LEQ, lsl, rsr, q(Int.sum_ub₅ $hs $h)) + else if ks == .LEQ && k == .EQUAL then + let hs : Q($ls ≤ $rs) := hs + let h : Q($l = $r) ← reconstructProof p + return (.LEQ, lsl, rsr, q(Int.sum_ub₆ $hs $h)) + else if ks == .EQUAL && k == .LT then + let hs : Q($ls = $rs) := hs + let h : Q($l < $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Int.sum_ub₇ $hs $h)) + else if ks == .EQUAL && k == .LEQ then + let hs : Q($ls = $rs) := hs + let h : Q($l ≤ $r) ← reconstructProof p + return (.LEQ, lsl, rsr, q(Int.sum_ub₈ $hs $h)) + else if ks == .EQUAL && k == .EQUAL then + let hs : Q($ls = $rs) := hs + let h : Q($l = $r) ← reconstructProof p + return (.EQUAL, lsl, rsr, q(Int.sum_ub₉ $hs $h)) + else + throwError "[sum_ub]: invalid kinds: {ks}, {p.getResult.getKind}" + let k := pf.getChildren[0]!.getResult.getKind + let ls : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[0]! + let rs : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[1]! + let hs ← reconstructProof pf.getChildren[0]! + let (_, ls, rs, hs) ← pf.getChildren[1:].foldlM f (k, ls, rs, hs) + addThm q($ls < $rs) hs + +def reconstructMulSign (pf : cvc5.Proof) : ReconstructM (Option Expr) := do + let ts := pf.getResult[0]!.getChildren + let mut hs : Array (Name × (Array Expr → ReconstructM Expr)) := #[] + let mut map : HashMap cvc5.Term Nat := {} + for h : i in [0:ts.size] do + let t := ts[i]'(h.right) + let p : Q(Prop) ← reconstructTerm t + hs := hs.push (Name.num `a i, fun _ => return p) + map := map.insert (if t.getKind == .NOT then t[0]![0]! else t[0]!) i + let t := pf.getResult[1]! + let vs := if t[0]!.getKind == .CONST_INTEGER then t[1]!.getChildren else t[0]!.getChildren + let f t ps := do + let p : Q(Prop) ← reconstructTerm t + return q($p :: $ps) + let ps : Q(List Prop) ← ts.foldrM f q([]) + let q : Q(Prop) ← reconstructTerm t + let h : Q(impliesN $ps $q) ← Meta.withLocalDeclsD hs fun hs => do + let h : Q($q) ← if ts[map.find! vs[0]!]!.getKind == .NOT then + let a : Q(Int) ← reconstructTerm vs[0]! + let ha : Q($a ≠ 0) := hs[map.find! vs[0]!]! + go vs ts hs map .GT q($a * $a) q(Int.mul_sign₀ $ha) 2 + else + let a : Q(Int) ← reconstructTerm vs[0]! + go vs ts hs map ts[map.find! vs[0]!]!.getKind a hs[map.find! vs[0]!]! 1 + Meta.mkLambdaFVars hs h + addThm q(andN $ps → $q) q(Builtin.scopes $h) +where + go vs ts hs map ka (a : Q(Int)) (ha : Expr) i : ReconstructM Expr := do + if hi : i < vs.size then + let b : Q(Int) ← reconstructTerm vs[i] + let k := ts[map.find! vs[i]]!.getKind + if ka == .LT && k == .LT then + let ha : Q($a < 0) := ha + let hb : Q($b < 0) := hs[map.find! vs[i]]! + go vs ts hs map .GT q($a * $b) q(Int.mul_sign₁ $ha $hb) (i + 1) + else if ka == .LT && k == .NOT then + let ha : Q($a < 0) := ha + let hb : Q($b ≠ 0) := hs[map.find! vs[i]]! + go vs ts hs map .LT q($a * $b * $b) q(Int.mul_sign₂ $ha $hb) (i + 2) + else if ka == .LT && k == .GT then + let ha : Q($a < 0) := ha + let hb : Q($b > 0) := hs[map.find! vs[i]]! + go vs ts hs map .LT q($a * $b) q(Int.mul_sign₃ $ha $hb) (i + 1) + else if ka == .GT && k == .LT then + let ha : Q($a > 0) := ha + let hb : Q($b < 0) := hs[map.find! vs[i]]! + go vs ts hs map .LT q($a * $b) q(Int.mul_sign₄ $ha $hb) (i + 1) + else if ka == .GT && k == .NOT then + let ha : Q($a > 0) := ha + let hb : Q($b ≠ 0) := hs[map.find! vs[i]]! + go vs ts hs map .GT q($a * $b * $b) q(Int.mul_sign₅ $ha $hb) (i + 2) + else if ka == .GT && k == .GT then + let ha : Q($a > 0) := ha + let hb : Q($b > 0) := hs[map.find! vs[i]]! + go vs ts hs map .GT q($a * $b) q(Int.mul_sign₆ $ha $hb) (i + 1) + else + throwError "[mul_sign]: invalid kinds: {ka}, {k}" + else + return ha + +@[smt_proof_reconstruct] def reconstructIntProof : ProofReconstructor := fun pf => do match pf.getRule with + | .DSL_REWRITE + | .THEORY_REWRITE => reconstructRewrite pf + | .ARITH_SUM_UB => + if !pf.getResult[0]!.getSort.isInteger then return none + reconstructSumUB pf + | .INT_TIGHT_UB => + if !pf.getResult[0]!.getSort.isInteger then return none + let i : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[0]! + let c : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[1]! + let h : Q($i < $c) ← reconstructProof pf.getChildren[0]! + addThm q($i ≤ $c - 1) q(@Int.int_tight_ub $c $i $h) + | .INT_TIGHT_LB => + if !pf.getResult[0]!.getSort.isInteger then return none + let i : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[0]! + let c : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[1]! + let h : Q($i > $c) ← reconstructProof pf.getChildren[0]! + addThm q($i ≥ $c + 1) q(@Int.int_tight_lb $c $i $h) + | .ARITH_TRICHOTOMY => + if !pf.getResult[0]!.getSort.isInteger then return none + let x : Q(Int) ← reconstructTerm pf.getResult[0]! + let c : Q(Int) ← reconstructTerm pf.getResult[1]! + let k₁ := pf.getChildren[0]!.getResult.getKind + let k₂ := pf.getChildren[1]!.getResult.getKind + if k₁ == .LEQ && k₂ == .NOT then + let h₁ : Q($x ≤ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≠ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x < $c) q(Int.trichotomy₁ $h₁ $h₂) + else if k₁ == .LEQ && k₂ == .GEQ then + let h₁ : Q($x ≤ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≥ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x = $c) q(Int.trichotomy₂ $h₁ $h₂) + else if k₁ == .NOT && k₂ == .LEQ then + let h₁ : Q($x ≠ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≤ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x < $c) q(Int.trichotomy₃ $h₁ $h₂) + else if k₁ == .NOT && k₂ == .GEQ then + let h₁ : Q($x ≠ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≥ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x > $c) q(Int.trichotomy₄ $h₁ $h₂) + else if k₁ == .GEQ && k₂ == .LEQ then + let h₁ : Q($x ≥ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≤ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x = $c) q(Int.trichotomy₅ $h₁ $h₂) + else if k₁ == .GEQ && k₂ == .NOT then + let h₁ : Q($x ≥ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≠ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x > $c) q(Int.trichotomy₆ $h₁ $h₂) + else + return none + | .ARITH_POLY_NORM => + if pf.getResult[0]!.getSort.getKind == .BOOLEAN_SORT then + if !pf.getResult[0]![0]!.getSort.isInteger then return none + let a₁ : Q(Int) ← reconstructTerm pf.getResult[0]![0]! + let a₂ : Q(Int) ← reconstructTerm pf.getResult[0]![1]! + let b₁ : Q(Int) ← reconstructTerm pf.getResult[1]![0]! + let b₂ : Q(Int) ← reconstructTerm pf.getResult[1]![1]! + let (l, es) ← (toPolyNormExpr q($a₁ - $a₂)).run #[] + let (r, _) ← (toPolyNormExpr q($b₁ - $b₂)).run es + let c₁ : Q(Int) := + if h : 0 < r.toPolynomial.length then let n : Nat := r.toPolynomial[0].coeff.natAbs; q(OfNat.ofNat $n) else q(1) + let c₂ : Q(Int) := + if h : 0 < l.toPolynomial.length then let n : Nat := l.toPolynomial[0].coeff.natAbs; q(OfNat.ofNat $n) else q(1) + let hc₁ : Q($c₁ > 0) := .app q(@of_decide_eq_true ($c₁ > 0) _) q(Eq.refl true) + let hc₂ : Q($c₂ > 0) := .app q(@of_decide_eq_true ($c₂ > 0) _) q(Eq.refl true) + let h : Q($c₁ * ($a₁ - $a₂) = $c₂ * ($b₁ - $b₂)) ← Meta.mkFreshExprMVar q($c₁ * ($a₁ - $a₂) = $c₂ * ($b₁ - $b₂)) + Int.polyNorm h.mvarId! + match pf.getResult[0]!.getKind with + | .LT => + addThm q(($a₁ < $a₂) = ($b₁ < $b₂)) q(Int.lt_of_sub_eq $hc₁ $hc₂ $h) + | .LEQ => + addThm q(($a₁ ≤ $a₂) = ($b₁ ≤ $b₂)) q(Int.le_of_sub_eq $hc₁ $hc₂ $h) + | .EQUAL => + addThm q(($a₁ = $a₂) = ($b₁ = $b₂)) q(Int.eq_of_sub_eq $hc₁ $hc₂ $h) + | .GEQ => + addThm q(($a₁ ≥ $a₂) = ($b₁ ≥ $b₂)) q(Int.ge_of_sub_eq $hc₁ $hc₂ $h) + | .GT => + addThm q(($a₁ > $a₂) = ($b₁ > $b₂)) q(Int.gt_of_sub_eq $hc₁ $hc₂ $h) + | _ => return none + else + if !pf.getResult[0]!.getSort.isInteger then return none + let a : Q(Int) ← reconstructTerm pf.getResult[0]! + let b : Q(Int) ← reconstructTerm pf.getResult[1]! + addTac q($a = $b) Int.polyNorm + | .ARITH_MULT_SIGN => + if !pf.getResult[1]![0]!.getSort.isInteger then return none + reconstructMulSign pf + | .ARITH_MULT_POS => + if !pf.getArguments[0]!.getSort.isInteger then return none + let m : Q(Int) ← reconstructTerm pf.getArguments[0]! + let l : Q(Int) ← reconstructTerm pf.getArguments[1]![0]! + let r : Q(Int) ← reconstructTerm pf.getArguments[1]![1]! + match pf.getArguments[1]!.getKind with + | .LT => + addThm q($m > 0 ∧ $l < $r → $m * $l < $m * $r) q(@Int.mul_pos_lt $l $r $m) + | .LEQ => + addThm q($m > 0 ∧ $l ≤ $r → $m * $l ≤ $m * $r) q(@Int.mul_pos_le $l $r $m) + | .EQUAL => + addThm q($m > 0 ∧ $l = $r → $m * $l = $m * $r) q(@Int.mul_pos_eq $l $r $m) + | .GEQ => + addThm q($m > 0 ∧ $l ≥ $r → $m * $l ≥ $m * $r) q(@Int.mul_pos_ge $l $r $m) + | .GT => + addThm q($m > 0 ∧ $l > $r → $m * $l > $m * $r) q(@Int.mul_pos_gt $l $r $m) + | _ => return none + | .ARITH_MULT_NEG => + if !pf.getArguments[0]!.getSort.isInteger then return none + let m : Q(Int) ← reconstructTerm pf.getArguments[0]! + let l : Q(Int) ← reconstructTerm pf.getArguments[1]![0]! + let r : Q(Int) ← reconstructTerm pf.getArguments[1]![1]! + match pf.getArguments[1]!.getKind with + | .LT => + addThm q($m < 0 ∧ $l < $r → $m * $l > $m * $r) q(@Int.mul_neg_lt $l $r $m) + | .LEQ => + addThm q($m < 0 ∧ $l ≤ $r → $m * $l ≥ $m * $r) q(@Int.mul_neg_le $l $r $m) + | .EQUAL => + addThm q($m < 0 ∧ $l = $r → $m * $l = $m * $r) q(@Int.mul_neg_eq $l $r $m) + | .GEQ => + addThm q($m < 0 ∧ $l ≥ $r → $m * $l ≤ $m * $r) q(@Int.mul_neg_ge $l $r $m) + | .GT => + addThm q($m < 0 ∧ $l > $r → $m * $l < $m * $r) q(@Int.mul_neg_gt $l $r $m) + | _ => return none + | _ => return none + +end Smt.Reconstruct.Int diff --git a/Smt/Reconstruct/Int/Lemmas.lean b/Smt/Reconstruct/Int/Lemmas.lean index 448ce906..989f6eee 100644 --- a/Smt/Reconstruct/Int/Lemmas.lean +++ b/Smt/Reconstruct/Int/Lemmas.lean @@ -5,16 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Tomaz Gomes Mascarenhas, Abdalrhman Mohamed -/ -private theorem Nat.mod_two_ne_zero : ¬n % 2 = 0 ↔ n % 2 = 1 := by - cases Nat.mod_two_eq_zero_or_one n <;> rename_i h <;> simp [h] - -private theorem Nat.even_add : (m + n) % 2 = 0 ↔ (m % 2 = 0 ↔ n % 2 = 0) := by - cases Nat.mod_two_eq_zero_or_one m <;> rename_i h₁ <;> cases Nat.mod_two_eq_zero_or_one n <;> rename_i h₂ <;> - simp [h₁, h₂, Nat.add_mod] - -private theorem Nat.even_add_one : (n + 1) % 2 = 0 ↔ n % 2 ≠ 0 := by - simp [Nat.even_add] - private theorem Int.mul_lt_mul_left {c x y : Int} (hc : c > 0) : (c * x < c * y) = (x < y) := by apply propext constructor @@ -33,31 +23,21 @@ private theorem Int.mul_eq_zero_left {x y : Int} (hx : x ≠ 0) (hxy : x * y = 0 private def uncurry {p₁ p₂ p₃ : Prop} : (p₁ → p₂ → p₃) → (p₁ ∧ p₂) → p₃ := by intros h₁ h₂ - have ⟨ ht₁, ht₂ ⟩ := h₂ + have ⟨ht₁, ht₂⟩ := h₂ exact h₁ ht₁ ht₂ namespace Smt.Reconstruct.Int variable {a b c d : Int} -private theorem or_implies_left (hpq : p ∨ q) (hnq : ¬q) : p := by - cases hpq with - | inl hp => exact hp - | inr hq => exact False.elim (hnq hq) - -private theorem or_implies_right (hpq : p ∨ q) (hnp : ¬p) : q := by - cases hpq with - | inl hp => exact False.elim (hnp hp) - | inr hq => exact hq - theorem sum_ub₁ (h₁ : a < b) (h₂ : c < d) : a + c < b + d := by - have r₁: a + c < a + d := Int.add_lt_add_left h₂ a - have r₂: a + d < b + d := Int.add_lt_add_right h₁ d + have r₁ : a + c < a + d := Int.add_lt_add_left h₂ a + have r₂ : a + d < b + d := Int.add_lt_add_right h₁ d exact Int.lt_trans r₁ r₂ theorem sum_ub₂ (h₁ : a < b) (h₂ : c ≤ d) : a + c < b + d := by - have r₁: a + c ≤ a + d := Int.add_le_add_left h₂ a - have r₂: a + d < b + d := Int.add_lt_add_right h₁ d + have r₁ : a + c ≤ a + d := Int.add_le_add_left h₂ a + have r₂ : a + d < b + d := Int.add_lt_add_right h₁ d exact Int.lt_of_le_of_lt r₁ r₂ theorem sum_ub₃ (h₁ : a < b) (h₂ : c = d) : a + c < b + d := by @@ -90,29 +70,35 @@ theorem sum_ub₉ (h₁ : a = b) (h₂ : c = d) : a + c ≤ b + d := by rewrite [h₁, h₂] exact Int.le_refl (b + d) -theorem trichotomy₁ (h₁ : a ≥ b) (h₂ : a ≠ b) : a > b := by +theorem int_tight_ub {i : Int} (h : i < c) : i ≤ c - 1 := + Int.le_sub_one_of_lt h + +theorem int_tight_lb {i : Int} (h : i > c) : i ≥ c + 1 := + h + +theorem trichotomy₁ (h₁ : a ≤ b) (h₂ : a ≠ b) : a < b := by have tr := Int.lt_trichotomy a b - exact or_implies_right (or_implies_right tr (Int.not_lt.mpr h₁)) h₂ + exact Or.resolve_right (Or.resolve_right (or_assoc.mpr tr) (Int.not_lt.mpr h₁)) h₂ -theorem trichotomy₂ (h₁ : a ≠ b) (h₂ : a ≥ b) : a > b := by +theorem trichotomy₂ (h₁ : a ≤ b) (h₂ : a ≥ b) : a = b := by have tr := Int.lt_trichotomy a b - exact or_implies_right (or_implies_right tr (Int.not_lt.mpr h₂)) h₁ + exact Or.resolve_right (Or.resolve_left tr (Int.not_lt.mpr h₂)) (Int.not_lt.mpr h₁) -theorem trichotomy₃ (h₁ : a ≥ b) (h₂ : a ≤ b) : a = b := by +theorem trichotomy₃ (h₁ : a ≠ b) (h₂ : a ≤ b) : a < b := by have tr := Int.lt_trichotomy a b - exact or_implies_left (or_implies_right tr (Int.not_lt.mpr h₁)) (Int.not_lt.mpr h₂) + exact Or.resolve_right (Or.resolve_right (or_assoc.mpr tr) (Int.not_lt.mpr h₂)) h₁ -theorem trichotomy₄ (h₁ : a ≤ b) (h₂ : a ≥ b) : a = b := by +theorem trichotomy₄ (h₁ : a ≠ b) (h₂ : a ≥ b) : a > b := by have tr := Int.lt_trichotomy a b - exact or_implies_left (or_implies_right tr (Int.not_lt.mpr h₂)) (Int.not_lt.mpr h₁) + exact Or.resolve_left (Or.resolve_left tr (Int.not_lt.mpr h₂)) h₁ -theorem trichotomy₅ (h₁ : a ≠ b) (h₂ : a ≤ b) : a < b := by +theorem trichotomy₅ (h₁ : a ≥ b) (h₂ : a ≤ b) : a = b := by have tr := Int.lt_trichotomy a b - exact or_implies_left (or_implies_left (or_assoc.mpr tr) (Int.not_lt.mpr h₂)) h₁ + exact Or.resolve_right (Or.resolve_left tr (Int.not_lt.mpr h₁)) (Int.not_lt.mpr h₂) -theorem trichotomy₆ (h₁ : a ≤ b) (h₂ : a ≠ b) : a < b := by +theorem trichotomy₆ (h₁ : a ≥ b) (h₂ : a ≠ b) : a > b := by have tr := Int.lt_trichotomy a b - exact or_implies_left (or_implies_left (or_assoc.mpr tr) (Int.not_lt.mpr h₁)) h₂ + exact Or.resolve_left (Or.resolve_left tr (Int.not_lt.mpr h₁)) h₂ theorem lt_eq_sub_lt_zero : (a < b) = (a - b < 0) := by apply propext @@ -168,95 +154,72 @@ theorem gt_of_sub_eq {c₁ c₂ : Int} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h rw (config := { occs := .pos [1] }) [← Int.mul_zero c, gt_iff_lt, Int.mul_lt_mul_left hc] rw [gt_eq_sub_gt_zero, @gt_eq_sub_gt_zero b₁, ← this hc₁, ← this hc₂, h] -mutual - -theorem pow_neg_even {k : Nat} {z : Int} (h₁ : z < 0) (h₂ : k % 2 = 0) : z ^ k > 0 := by - cases k with - | zero => simp [Int.pow_zero] - | succ k => - have hodd := Nat.even_add_one.mp h₂ - have mulZ : z * z ^ k > z * 0 := Int.mul_lt_mul_of_neg_left (pow_neg_odd h₁ (Nat.mod_two_ne_zero.mp hodd)) h₁ - simp at mulZ - rw [Int.pow_succ, Int.mul_comm] - exact mulZ - -theorem pow_neg_odd {k : Nat} {z : Int} (h₁ : z < 0) (h₂ : k % 2 = 1) : z ^ k < 0 := by - cases k with - | zero => simp at h₂ - | succ k => - have heven : k % 2 = 0 := Classical.not_not.mp (mt Nat.even_add_one.mpr (Eq.symm h₂ ▸ nofun)) - have mulZ : z * 0 > z * z ^ k := Int.mul_lt_mul_of_neg_left (pow_neg_even h₁ heven) h₁ - simp at mulZ - rw [Int.pow_succ, Int.mul_comm] - exact mulZ - -end - -theorem pow_pos {k : Nat} {z : Int} (h : z > 0) : z ^ k > 0 := by - induction k with - | zero => simp [Int.pow_zero] - | succ k ih => - rw [Int.pow_succ] - have h₂ := Int.mul_lt_mul_of_pos_left h ih - simp at h₂ - exact h₂ - -theorem non_zero_even_pow {k : Nat} {z : Int} (h₁ : z ≠ 0) (h₂ : k % 2 = 0) : z ^ k > 0 := by - match Int.lt_trichotomy z 0 with - | Or.inl hneg => exact pow_neg_even hneg h₂ - | Or.inr (Or.inl hzero) => rw [hzero] at h₁; simp at h₁ - | Or.inr (Or.inr hpos) => exact pow_pos hpos - -theorem combine_signs₁ : a > 0 → b > 0 → b * a > 0 := by - intros h₁ h₂ - have h := Int.mul_lt_mul_of_pos_left h₁ h₂ +theorem mul_sign₁ (ha : a < 0) (hb : b < 0) : a * b > 0 := by + have h := Int.mul_lt_mul_of_neg_right ha hb simp at h exact h -theorem combine_signs₂ : a > 0 → b < 0 → b * a < 0 := by - intros h₁ h₂ - have h := Int.mul_lt_mul_of_pos_right h₂ h₁ +theorem mul_sign₃ (ha : a < 0) (hb : b > 0) : a * b < 0 := by + have h := Int.mul_lt_mul_of_pos_right ha hb simp at h exact h -theorem combine_signs₃ : a < 0 → b > 0 → b * a < 0 := by - intros h₁ h₂ - have h := Int.mul_lt_mul_of_pos_left h₁ h₂ +theorem mul_sign₄ (ha : a > 0) (hb : b < 0) : a * b < 0 := by + have h := Int.mul_lt_mul_of_pos_left hb ha simp at h exact h -theorem combine_signs₄ : a < 0 → b < 0 → b * a > 0 := by - intros h₁ h₂ - have h := Int.mul_lt_mul_of_neg_left h₁ h₂ +theorem mul_sign₆ (ha : a > 0) (hb : b > 0) : a * b > 0 := by + have h := Int.mul_lt_mul_of_pos_left hb ha simp at h exact h -theorem arith_mul_pos_lt : c > 0 ∧ a < b → c * a < c * b := - uncurry (flip Int.mul_lt_mul_of_pos_left) +theorem mul_sign₀ (ha : a ≠ 0) : a * a > 0 := + match Int.lt_trichotomy a 0 with + | .inl hn => mul_sign₁ hn hn + | .inr (.inl hz) => absurd hz ha + | .inr (.inr hp) => mul_sign₆ hp hp + +theorem mul_sign₂ (ha : a < 0) (hb : b ≠ 0) : a * b * b < 0 := + match Int.lt_trichotomy b 0 with + | .inl hn => mul_sign₄ (mul_sign₁ ha hn) hn + | .inr (.inl hz) => absurd hz hb + | .inr (.inr hp) => mul_sign₃ (mul_sign₃ ha hp) hp + +theorem mul_sign₅ (ha : a > 0) (hb : b ≠ 0) : a * b * b > 0 := + match Int.lt_trichotomy b 0 with + | .inl hn => mul_sign₁ (mul_sign₄ ha hn) hn + | .inr (.inl hz) => absurd hz hb + | .inr (.inr hp) => mul_sign₆ (mul_sign₆ ha hp) hp + +theorem mul_pos_lt (h : c > 0 ∧ a < b) : c * a < c * b := + Int.mul_lt_mul_of_pos_left h.2 h.1 -theorem arith_mul_pos_le : c > 0 ∧ a ≤ b → c * a ≤ c * b := λ h => +theorem mul_pos_le (h : c > 0 ∧ a ≤ b) : c * a ≤ c * b := Int.mul_le_mul_of_nonneg_left h.2 (Int.le_of_lt h.1) -theorem arith_mul_pos_gt : c > 0 ∧ a > b → c * a > c * b := arith_mul_pos_lt +theorem mul_pos_gt (h : c > 0 ∧ a > b) : c * a > c * b := + mul_pos_lt h -theorem arith_mul_pos_ge : c > 0 ∧ a ≥ b → c * a ≥ c * b := arith_mul_pos_le +theorem mul_pos_ge (h : c > 0 ∧ a ≥ b) : c * a ≥ c * b := + mul_pos_le h -theorem arith_mul_pos_eq : c > 0 ∧ a = b → c * a = c * b := by - intros h +theorem mul_pos_eq (h : c > 0 ∧ a = b) : c * a = c * b := by rw [h.2] -theorem arith_mul_neg_lt : c < 0 ∧ a < b → c * a > c * b := - uncurry (flip Int.mul_lt_mul_of_neg_left) +theorem mul_neg_lt (h : c < 0 ∧ a < b) : c * a > c * b := + Int.mul_lt_mul_of_neg_left h.2 h.1 -theorem arith_mul_neg_le : c < 0 ∧ a ≤ b → c * a ≥ c * b := λ h => +theorem mul_neg_le (h : c < 0 ∧ a ≤ b) : c * a ≥ c * b := Int.mul_le_mul_of_nonpos_left (Int.le_of_lt h.1) h.2 -theorem arith_mul_neg_gt : c < 0 ∧ a > b → c * a < c * b := arith_mul_neg_lt +theorem mul_neg_gt (h : c < 0 ∧ a > b) : c * a < c * b := + mul_neg_lt h -theorem arith_mul_neg_ge : c < 0 ∧ a ≥ b → c * a ≤ c * b := arith_mul_neg_le +theorem mul_neg_ge (h : c < 0 ∧ a ≥ b) : c * a ≤ c * b := + mul_neg_le h -theorem arith_mul_neg_eq : c < 0 ∧ a = b → c * a = c * b := by - intros h +theorem mul_neg_eq (h : c < 0 ∧ a = b) : c * a = c * b := by rw [h.2] end Smt.Reconstruct.Int diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean new file mode 100644 index 00000000..4673a41c --- /dev/null +++ b/Smt/Reconstruct/Int/Polynorm.lean @@ -0,0 +1,241 @@ +/- +Copyright (c) 2021-2024 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abdalrhman Mohamed +-/ + +import Lean +import Qq + +namespace Smt.Reconstruct.Int.PolyNorm + +abbrev Var := Nat + +def Context := Var → Int + +structure Monomial where + coeff : Int + vars : List Var +deriving Inhabited, Repr + +namespace Monomial + +open Qq in +def toExpr (m : Monomial) (ppCtx : Var → Q(Int)) : Q(Int) := + if h : m.vars = [] then + toExprCoeff m.coeff + else + if m.coeff = 1 then + (m.vars.drop 1).foldl (fun acc v => q($acc * $(ppCtx v))) (ppCtx (m.vars.head h)) + else + m.vars.foldl (fun acc v => q($acc * $(ppCtx v))) (toExprCoeff m.coeff) +where + toExprCoeff (c : Int) : Q(Int) := + let l : Q(Nat) := Lean.mkRawNatLit c.natAbs + if c ≥ 0 then + q(OfNat.ofNat $l : Int) + else + q(-OfNat.ofNat $l : Int) + +def neg (m : Monomial) : Monomial := + { m with coeff := -m.coeff } + +def add (m₁ m₂ : Monomial) (_ : m₁.vars = m₂.vars) : Monomial := + { coeff := m₁.coeff + m₂.coeff, vars := m₁.vars } + +-- Invariant: monomial variables remain sorted. +def mul (m₁ m₂ : Monomial) : Monomial := + let coeff := m₁.coeff * m₂.coeff + let vars := m₁.vars.foldr insert m₂.vars + { coeff, vars } +where + insert (x : Var) : List Var → List Var + | [] => [x] + | y :: ys => if x ≤ y then x :: y :: ys else y :: insert x ys + +def denote (ctx : Context) (m : Monomial) : Int := + m.coeff * m.vars.foldl (fun acc v => acc * ctx v) 1 + +theorem denote_neg {m : Monomial} : m.neg.denote ctx = -m.denote ctx := by + simp only [neg, denote, Int.neg_mul_eq_neg_mul] + +theorem denote_mul {m₁ m₂ : Monomial} : (m₁.mul m₂).denote ctx = m₁.denote ctx * m₂.denote ctx := + sorry + +end Monomial + +abbrev Polynomial := List Monomial + +namespace Polynomial + +open Qq in +def toExpr (p : Polynomial) (ppCtx : Var → Q(Int)) : Q(Int) := + go p +where + go : Polynomial → Q(Int) + | [] => q(0) + | [m] => m.toExpr ppCtx + | m :: ms =>q($(m.toExpr ppCtx) + $(go ms)) + +def neg (p : Polynomial) : Polynomial := + p.map Monomial.neg + +-- NOTE: implementation merges monomials with same variables. +-- Invariant: monomials remain sorted. +def add (p q : Polynomial) : Polynomial := + p.foldr insert q +where + insert (m : Monomial) : Polynomial → Polynomial + | [] => [m] + | n :: ns => + if m.vars < n.vars then + m :: n :: ns + else if h : m.vars = n.vars then + let m' := m.add n h + if m'.coeff = 0 then ns else m' :: ns + else + n :: insert m ns + +def sub (p q : Polynomial) : Polynomial := + p.add q.neg + +-- Invariant: monomials remain sorted. +def mulMonomial (m : Monomial) (p : Polynomial) : Polynomial := + p.foldr (fun n acc => Polynomial.add [m.mul n] acc) [] + +-- Invariant: monomials remain sorted. +def mul (p q : Polynomial) : Polynomial := + p.foldl (fun acc m => (q.mulMonomial m).add acc) [] + +def denote (ctx : Context) (p : Polynomial) : Int := + p.foldl (fun acc m => acc + m.denote ctx) 0 + +theorem denote_neg {p : Polynomial} : p.neg.denote ctx = -p.denote ctx := + sorry + +theorem denote_add {p q : Polynomial} : (p.add q).denote ctx = p.denote ctx + q.denote ctx := + sorry + +theorem denote_sub {p q : Polynomial} : (p.sub q).denote ctx = p.denote ctx - q.denote ctx := by + simp only [sub, denote_neg, denote_add, Int.sub_eq_add_neg] + +theorem denote_mulMonomial {p : Polynomial} : (p.mulMonomial m).denote ctx = m.denote ctx * p.denote ctx := + sorry + +theorem denote_mul {p q : Polynomial} : (p.mul q).denote ctx = p.denote ctx * q.denote ctx := + sorry + +end Polynomial + +inductive Expr where + | val (v : Int) + | var (v : Nat) + | neg (a : Expr) + | add (a b : Expr) + | mul (a b : Expr) + | sub (a b : Expr) +deriving Inhabited, Repr + +namespace Expr + +def toPolynomial : Expr → Polynomial + | val v => if v = 0 then [] else [{ coeff := v, vars := [] }] + | var v => [{ coeff := 1, vars := [v] }] + | neg a => a.toPolynomial.neg + | add a b => Polynomial.add a.toPolynomial b.toPolynomial + | sub a b => Polynomial.sub a.toPolynomial b.toPolynomial + | mul a b => Polynomial.mul a.toPolynomial b.toPolynomial + +def denote (ctx : Context) : Expr → Int + | val v => v + | var v => ctx v + | neg a => -a.denote ctx + | add a b => a.denote ctx + b.denote ctx + | sub a b => a.denote ctx - b.denote ctx + | mul a b => a.denote ctx * b.denote ctx + +theorem denote_toPolynomial {e : Expr} : e.denote ctx = e.toPolynomial.denote ctx := by + induction e with + | val v => + simp only [denote, toPolynomial] + split <;> rename_i hv + · rewrite [hv]; rfl + · simp [Polynomial.denote, Monomial.denote] + | var v => + simp [denote, toPolynomial, Polynomial.denote, Monomial.denote] + | neg a ih => + simp only [denote, toPolynomial, Polynomial.denote_neg, ih] + | add a b ih₁ ih₂ => + simp only [denote, toPolynomial, Polynomial.denote_add, ih₁, ih₂] + | sub a b ih₁ ih₂ => + simp only [denote, toPolynomial, Polynomial.denote_sub, ih₁, ih₂] + | mul a b ih₁ ih₂ => + simp only [denote, toPolynomial, Polynomial.denote_mul, ih₁, ih₂] + +theorem denote_eq_from_toPolynomial_eq {e₁ e₂ : Expr} (h : e₁.toPolynomial = e₂.toPolynomial) : e₁.denote ctx = e₂.denote ctx := by + rw [denote_toPolynomial, denote_toPolynomial, h] + +end PolyNorm.Expr + +open Lean Qq + +abbrev PolyM := StateT (Array Q(Int)) MetaM + +def getIndex (e : Q(Int)) : PolyM Nat := do + let es ← get + if let some i := es.findIdx? (· == e) then + return i + else + let size := es.size + set (es.push e) + return size + +partial def toPolyNormExpr (e : Q(Int)) : PolyM PolyNorm.Expr := do + match e with + | ~q(OfNat.ofNat $x) => pure (.val x.rawNatLit?.get!) + | ~q(-$x) => pure (.neg (← toPolyNormExpr x)) + | ~q($x + $y) => pure (.add (← toPolyNormExpr x) (← toPolyNormExpr y)) + | ~q($x - $y) => pure (.sub (← toPolyNormExpr x) (← toPolyNormExpr y)) + | ~q($x * $y) => pure (.mul (← toPolyNormExpr x) (← toPolyNormExpr y)) + | e => let v : Nat ← getIndex e; pure (.var v) + +partial def toQPolyNormExpr (e : Q(Int)) : PolyM Q(PolyNorm.Expr) := do + match e with + | ~q(OfNat.ofNat $x) => pure q(.val (@OfNat.ofNat Int $x _)) + | ~q(-$x) => pure q(.neg $(← toQPolyNormExpr x)) + | ~q($x + $y) => pure q(.add $(← toQPolyNormExpr x) $(← toQPolyNormExpr y)) + | ~q($x - $y) => pure q(.sub $(← toQPolyNormExpr x) $(← toQPolyNormExpr y)) + | ~q($x * $y) => pure q(.mul $(← toQPolyNormExpr x) $(← toQPolyNormExpr y)) + | e => let v : Nat ← getIndex e; pure q(.var $v) + +def polyNorm (mv : MVarId) : MetaM Unit := do + let some (_, l, r) := (← mv.getType).eq? + | throwError "[poly_norm] expected an equality, got {← mv.getType}" + let (l, es) ← (toQPolyNormExpr l).run #[] + let (r, es) ← (toQPolyNormExpr r).run es + let is : Q(Array Int) := es.foldl (fun acc e => q(«$acc».push $e)) q(#[]) + let ctx : Q(PolyNorm.Context) := q(fun v => if h : v < «$is».size then $is[v] else 0) + let h : Q(«$l».toPolynomial = «$r».toPolynomial) := .app q(@Eq.refl.{1} PolyNorm.Polynomial) q(«$l».toPolynomial) + mv.assign q(@PolyNorm.Expr.denote_eq_from_toPolynomial_eq $ctx $l $r $h) +where + logPolynomial (e : Q(PolyNorm.Expr)) (es : Array Q(Int)) := do + let p ← unsafe Meta.evalExpr PolyNorm.Expr q(PolyNorm.Expr) e + let ppCtx := fun v => if h : v < es.size then es[v] else q(0) + logInfo m!"poly := {PolyNorm.Polynomial.toExpr p.toPolynomial ppCtx}" + +namespace Tactic + +syntax (name := polyNorm) "poly_norm" : tactic + +open Lean.Elab Tactic in +@[tactic polyNorm] def evalPolyNorm : Tactic := fun _ => + withMainContext do + let mv ← Tactic.getMainGoal + Int.polyNorm mv + replaceMainGoal [] + +end Smt.Reconstruct.Int.Tactic + +example (x y z : Int) : 1 * (x + y) * z = z * y + x * z := by + poly_norm diff --git a/Smt/Reconstruct/Int/Rewrites.lean b/Smt/Reconstruct/Int/Rewrites.lean index f2ab4b10..bae255aa 100644 --- a/Smt/Reconstruct/Int/Rewrites.lean +++ b/Smt/Reconstruct/Int/Rewrites.lean @@ -96,10 +96,7 @@ theorem plus_cancel2 : ts + (-1 * x) + ss + x + rs = ts + ss + rs := Int.neg_eq_neg_one_mul x ▸ Int.add_assoc ts (-x) ss ▸ Int.add_assoc ts (-x + ss) x ▸ Int.add_comm (-x) ss ▸ (Int.neg_add_cancel_right ss x).symm ▸ rfl --- theorem abs_elim : |x| = if x < 0 then -x else x := --- if h : x < 0 then --- if_pos h ▸ abs_of_neg h --- else --- if_neg h ▸ abs_of_nonneg (le_of_not_lt h) +theorem abs_elim : (if x < 0 then -x else x) = if x < 0 then -x else x := + rfl end Smt.Reconstruct.Int.Rewrite diff --git a/Smt/Reconstruct/Rat.lean b/Smt/Reconstruct/Rat.lean new file mode 100644 index 00000000..00449f92 --- /dev/null +++ b/Smt/Reconstruct/Rat.lean @@ -0,0 +1,458 @@ +/- +Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abdalrhman Mohamed +-/ + +import Smt.Reconstruct +import Smt.Reconstruct.Builtin.Lemmas +import Smt.Reconstruct.Rat.Core +import Smt.Reconstruct.Rat.Lemmas +import Smt.Reconstruct.Rat.Polynorm +import Smt.Reconstruct.Rat.Rewrites +import Smt.Reconstruct.Rewrite + +namespace Smt.Reconstruct.Rat + +open Lean hiding Rat +open Qq + +@[smt_sort_reconstruct] def reconstructRatSort : SortReconstructor := fun s => do match s.getKind with + | .REAL_SORT => return q(Rat) + | _ => return none + +@[smt_term_reconstruct] def reconstructRat : TermReconstructor := fun t => do match t.getKind with + | .SKOLEM => match t.getSkolemId with + | .DIV_BY_ZERO => return q(fun (x : Rat) => x / 0) + | _ => return none + | .CONST_RATIONAL => + let c : Lean.Rat := t.getRationalValue + let num : Q(Rat) := mkRatLit c.num.natAbs + if c.den == 1 then + if c.num ≥ 0 then + return q($num) + else + return q(-$num) + else + let den : Q(Rat) := mkRatLit c.den + if c.num ≥ 0 then + return q($num / $den) + else + return q(-$num / $den) + | .NEG => + if t.getSort.isInteger then return none + let x : Q(Rat) ← reconstructTerm t[0]! + return q(-$x) + | .SUB => + if t.getSort.isInteger then return none + leftAssocOp q(@HSub.hSub Rat Rat Rat _) t + | .ADD => + if t.getSort.isInteger then return none + leftAssocOp q(@HAdd.hAdd Rat Rat Rat _) t + | .MULT => + if t.getSort.isInteger then return none + leftAssocOp q(@HMul.hMul Rat Rat Rat _) t + | .DIVISION => + leftAssocOp q(@HDiv.hDiv Rat Rat Rat _) t + | .DIVISION_TOTAL => + leftAssocOp q(@HDiv.hDiv Rat Rat Rat _) t + | .ABS => + if t.getSort.isInteger then return none + let x : Q(Rat) ← reconstructTerm t[0]! + return q(if $x < 0 then -$x else $x) + | .LEQ => + if t[0]!.getSort.isInteger then return none + let x : Q(Rat) ← reconstructTerm t[0]! + let y : Q(Rat) ← reconstructTerm t[1]! + return q($x ≤ $y) + | .LT => + if t[0]!.getSort.isInteger then return none + let x : Q(Rat) ← reconstructTerm t[0]! + let y : Q(Rat) ← reconstructTerm t[1]! + return q($x < $y) + | .GEQ => + if t[0]!.getSort.isInteger then return none + let x : Q(Rat) ← reconstructTerm t[0]! + let y : Q(Rat) ← reconstructTerm t[1]! + return q($x ≥ $y) + | .GT => + if t[0]!.getSort.isInteger then return none + let x : Q(Rat) ← reconstructTerm t[0]! + let y : Q(Rat) ← reconstructTerm t[1]! + return q($x > $y) + | .TO_REAL => + let x : Q(Int) ← reconstructTerm t[0]! + return q($x : Rat) + | .TO_INTEGER => + let x : Q(Rat) ← reconstructTerm t[0]! + return q(«$x».floor) + | .IS_INTEGER => + let x : Q(Rat) ← reconstructTerm t[0]! + return q($x = «$x».floor) + | _ => return none +where + mkRatLit (n : Nat) : Q(Rat) := + let lit : Q(Nat) := Lean.mkRawNatLit n + q(OfNat.ofNat $lit) + leftAssocOp (op : Expr) (t : cvc5.Term) : ReconstructM Expr := do + let mut curr ← reconstructTerm t[0]! + for i in [1:t.getNumChildren] do + curr := mkApp2 op curr (← reconstructTerm t[i]!) + return curr + +def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do + match pf.getRewriteRule with + | .ARITH_DIV_BY_CONST_ELIM => + let t : Q(Rat) ← reconstructTerm pf.getResult[0]![0]! + let c : Q(Rat) ← reconstructTerm pf.getResult[0]![1]! + addThm q($t / $c = $t * (1 / $c)) q(@Rewrite.div_by_const_elim $t $c) + | .ARITH_PLUS_ZERO => + if pf.getArguments[1]![0]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.add_assoc) q(Rat.add_zero) q(@Rewrite.plus_zero) args) + | .ARITH_MUL_ONE => + if pf.getArguments[1]![0]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.mul_assoc) q(Rat.mul_one) q(@Rewrite.mul_one) args) + | .ARITH_MUL_ZERO => + if pf.getArguments[1]![0]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.mul_assoc) q(Rat.mul_one) q(@Rewrite.mul_zero) args) + | .ARITH_DIV_TOTAL => + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + let s : Q(Rat) ← reconstructTerm pf.getArguments[2]! + let h : Q($s ≠ 0) ← reconstructProof pf.getChildren[0]! + addThm q($t / $s = $t / $s) q(@Rewrite.div_total $t $s $h) + | .ARITH_NEG_NEG_ONE => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + addThm q(-1 * (-1 * $t) = $t) q(@Rewrite.neg_neg_one $t) + | .ARITH_ELIM_UMINUS => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + addThm q(-$t = -1 * $t) q(@Rewrite.elim_uminus $t) + | .ARITH_ELIM_MINUS => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + let s : Q(Rat) ← reconstructTerm pf.getArguments[2]! + addThm q($t - $s = $t + -1 * $s) q(@Rewrite.elim_minus $t $s) + | .ARITH_ELIM_GT => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + let s : Q(Rat) ← reconstructTerm pf.getArguments[2]! + addThm q(($t > $s) = ¬($t ≤ $s)) q(@Rewrite.elim_gt $t $s) + | .ARITH_ELIM_LT => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + let s : Q(Rat) ← reconstructTerm pf.getArguments[2]! + addThm q(($t < $s) = ¬($t ≥ $s)) q(@Rewrite.elim_lt $t $s) + | .ARITH_ELIM_LEQ => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + let s : Q(Rat) ← reconstructTerm pf.getArguments[2]! + addThm q(($t ≤ $s) = ($s ≥ $t)) q(@Rewrite.elim_leq $t $s) + | .ARITH_GEQ_NORM1 => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + let s : Q(Rat) ← reconstructTerm pf.getArguments[2]! + addThm q(($t ≥ $s) = ($t - $s ≥ 0)) q(@Rewrite.geq_norm1 $t $s) + | .ARITH_GEQ_NORM2 => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + let s : Q(Rat) ← reconstructTerm pf.getArguments[2]! + addThm q(($t ≥ $s) = (-$t ≤ -$s)) q(@Rewrite.geq_norm2 $t $s) + | .ARITH_REFL_LEQ => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + addThm q(($t ≤ $t) = True) q(@Rewrite.refl_leq $t) + | .ARITH_REFL_LT => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + addThm q(($t < $t) = False) q(@Rewrite.refl_lt $t) + | .ARITH_REFL_GEQ => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + addThm q(($t ≥ $t) = True) q(@Rewrite.refl_geq $t) + | .ARITH_REFL_GT => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + addThm q(($t > $t) = False) q(@Rewrite.refl_gt $t) + | .ARITH_PLUS_FLATTEN => + if pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.add_assoc) q(Rat.add_zero) q(@Rewrite.plus_flatten) args) + | .ARITH_MULT_FLATTEN => + if pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.mul_assoc) q(Rat.mul_one) q(@Rewrite.mult_flatten) args) + | .ARITH_MULT_DIST => + if pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.mul_assoc) q(Rat.mul_one) q(@Rewrite.mult_dist) args) + | .ARITH_PLUS_CANCEL1 => + if pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.mul_assoc) q(Rat.mul_one) q(@Rewrite.plus_cancel1) args) + | .ARITH_PLUS_CANCEL2 => + if pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.add_assoc) q(Rat.add_zero) q(@Rewrite.plus_cancel2) args) + | .ARITH_ABS_ELIM => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Rat) ← reconstructTerm pf.getArguments[1]! + addThm q(ite ($t < 0) (-$t) $t = ite ($t < 0) (-$t) $t) q(@Rewrite.abs_elim $t) + | _ => return none +where + reconstructArgs (args : Array cvc5.Term) : ReconstructM (Array (Array Expr)) := do + let mut args' := #[] + for arg in args do + let mut arg' := #[] + for subarg in arg do + arg' := arg'.push (← reconstructTerm subarg) + args' := args'.push arg' + return args' + +def reconstructSumUB (pf : cvc5.Proof) : ReconstructM (Option Expr) := do + let f := fun (ks, ls, rs, hs) p => do + let l : Q(Rat) ← reconstructTerm p.getResult[0]! + let r : Q(Rat) ← reconstructTerm p.getResult[1]! + let lsl := q($ls + $l) + let rsr := q($rs + $r) + let k := p.getResult.getKind + if ks == .LT && k == .LT then + let hs : Q($ls < $rs) := hs + let h : Q($l < $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Rat.sum_ub₁ $hs $h)) + else if ks == .LT && k == .LEQ then + let hs : Q($ls < $rs) := hs + let h : Q($l ≤ $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Rat.sum_ub₂ $hs $h)) + else if ks == .LT && k == .EQUAL then + let hs : Q($ls < $rs) := hs + let h : Q($l = $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Rat.sum_ub₃ $hs $h)) + else if ks == .LEQ && k == .LT then + let hs : Q($ls ≤ $rs) := hs + let h : Q($l < $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Rat.sum_ub₄ $hs $h)) + else if ks == .LEQ && k == .LEQ then + let hs : Q($ls ≤ $rs) := hs + let h : Q($l ≤ $r) ← reconstructProof p + return (.LEQ, lsl, rsr, q(Rat.sum_ub₅ $hs $h)) + else if ks == .LEQ && k == .EQUAL then + let hs : Q($ls ≤ $rs) := hs + let h : Q($l = $r) ← reconstructProof p + return (.LEQ, lsl, rsr, q(Rat.sum_ub₆ $hs $h)) + else if ks == .EQUAL && k == .LT then + let hs : Q($ls = $rs) := hs + let h : Q($l < $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Rat.sum_ub₇ $hs $h)) + else if ks == .EQUAL && k == .LEQ then + let hs : Q($ls = $rs) := hs + let h : Q($l ≤ $r) ← reconstructProof p + return (.LEQ, lsl, rsr, q(Rat.sum_ub₈ $hs $h)) + else if ks == .EQUAL && k == .EQUAL then + let hs : Q($ls = $rs) := hs + let h : Q($l = $r) ← reconstructProof p + return (.EQUAL, lsl, rsr, q(Rat.sum_ub₉ $hs $h)) + else + throwError "[sum_ub]: invalid kinds: {ks}, {p.getResult.getKind}" + let k := pf.getChildren[0]!.getResult.getKind + let ls : Q(Rat) ← reconstructTerm pf.getChildren[0]!.getResult[0]! + let rs : Q(Rat) ← reconstructTerm pf.getChildren[0]!.getResult[1]! + let hs ← reconstructProof pf.getChildren[0]! + let (_, ls, rs, hs) ← pf.getChildren[1:].foldlM f (k, ls, rs, hs) + addThm q($ls < $rs) hs + +def reconstructMulSign (pf : cvc5.Proof) : ReconstructM (Option Expr) := do + let ts := pf.getResult[0]!.getChildren + let mut hs : Array (Name × (Array Expr → ReconstructM Expr)) := #[] + let mut map : HashMap cvc5.Term Nat := {} + for h : i in [0:ts.size] do + let t := ts[i]'(h.right) + let p : Q(Prop) ← reconstructTerm t + hs := hs.push (Name.num `a i, fun _ => return p) + map := map.insert (if t.getKind == .NOT then t[0]![0]! else t[0]!) i + let t := pf.getResult[1]! + let vs := if t[0]!.getKind == .CONST_INTEGER then t[1]!.getChildren else t[0]!.getChildren + let f t ps := do + let p : Q(Prop) ← reconstructTerm t + return q($p :: $ps) + let ps : Q(List Prop) ← ts.foldrM f q([]) + let q : Q(Prop) ← reconstructTerm t + let h : Q(impliesN $ps $q) ← Meta.withLocalDeclsD hs fun hs => do + let h : Q($q) ← if ts[map.find! vs[0]!]!.getKind == .NOT then + let a : Q(Rat) ← reconstructTerm vs[0]! + let ha : Q($a ≠ 0) := hs[map.find! vs[0]!]! + go vs ts hs map .GT q($a * $a) q(Rat.mul_sign₀ $ha) 2 + else + let a : Q(Rat) ← reconstructTerm vs[0]! + go vs ts hs map ts[map.find! vs[0]!]!.getKind a hs[map.find! vs[0]!]! 1 + Meta.mkLambdaFVars hs h + addThm q(andN $ps → $q) q(Builtin.scopes $h) +where + go vs ts hs map ka (a : Q(Rat)) (ha : Expr) i : ReconstructM Expr := do + if hi : i < vs.size then + let b : Q(Rat) ← reconstructTerm vs[i] + let k := ts[map.find! vs[i]]!.getKind + if ka == .LT && k == .LT then + let ha : Q($a < 0) := ha + let hb : Q($b < 0) := hs[map.find! vs[i]]! + go vs ts hs map .GT q($a * $b) q(Rat.mul_sign₁ $ha $hb) (i + 1) + else if ka == .LT && k == .NOT then + let ha : Q($a < 0) := ha + let hb : Q($b ≠ 0) := hs[map.find! vs[i]]! + go vs ts hs map .LT q($a * $b * $b) q(Rat.mul_sign₂ $ha $hb) (i + 2) + else if ka == .LT && k == .GT then + let ha : Q($a < 0) := ha + let hb : Q($b > 0) := hs[map.find! vs[i]]! + go vs ts hs map .LT q($a * $b) q(Rat.mul_sign₃ $ha $hb) (i + 1) + else if ka == .GT && k == .LT then + let ha : Q($a > 0) := ha + let hb : Q($b < 0) := hs[map.find! vs[i]]! + go vs ts hs map .LT q($a * $b) q(Rat.mul_sign₄ $ha $hb) (i + 1) + else if ka == .GT && k == .NOT then + let ha : Q($a > 0) := ha + let hb : Q($b ≠ 0) := hs[map.find! vs[i]]! + go vs ts hs map .GT q($a * $b * $b) q(Rat.mul_sign₅ $ha $hb) (i + 2) + else if ka == .GT && k == .GT then + let ha : Q($a > 0) := ha + let hb : Q($b > 0) := hs[map.find! vs[i]]! + go vs ts hs map .GT q($a * $b) q(Rat.mul_sign₆ $ha $hb) (i + 1) + else + throwError "[mul_sign]: invalid kinds: {ka}, {k}" + else + return ha + +@[smt_proof_reconstruct] def reconstructRatProof : ProofReconstructor := fun pf => do match pf.getRule with + | .DSL_REWRITE + | .THEORY_REWRITE => reconstructRewrite pf + | .ARITH_SUM_UB => + if pf.getResult[0]!.getSort.isInteger then return none + reconstructSumUB pf + | .INT_TIGHT_UB => + let i : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[0]! + let c : Q(Rat) ← reconstructTerm pf.getChildren[0]!.getResult[1]! + let h : Q($i < $c) ← reconstructProof pf.getChildren[0]! + addThm q($i ≤ «$c».floor) q(@Rat.int_tight_ub $c $i $h) + | .INT_TIGHT_LB => + let i : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[0]! + let c : Q(Rat) ← reconstructTerm pf.getChildren[0]!.getResult[1]! + let h : Q($i > $c) ← reconstructProof pf.getChildren[0]! + addThm q($i ≥ «$c».ceil) q(@Rat.int_tight_lb $c $i $h) + | .ARITH_TRICHOTOMY => + if pf.getResult[0]!.getSort.isInteger then return none + let x : Q(Rat) ← reconstructTerm pf.getResult[0]! + let c : Q(Rat) ← reconstructTerm pf.getResult[1]! + let k₁ := pf.getChildren[0]!.getResult.getKind + let k₂ := pf.getChildren[1]!.getResult.getKind + if k₁ == .LEQ && k₂ == .NOT then + let h₁ : Q($x ≤ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≠ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x < $c) q(Rat.trichotomy₁ $h₁ $h₂) + else if k₁ == .LEQ && k₂ == .GEQ then + let h₁ : Q($x ≤ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≥ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x = $c) q(Rat.trichotomy₂ $h₁ $h₂) + else if k₁ == .NOT && k₂ == .LEQ then + let h₁ : Q($x ≠ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≤ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x < $c) q(Rat.trichotomy₃ $h₁ $h₂) + else if k₁ == .NOT && k₂ == .GEQ then + let h₁ : Q($x ≠ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≥ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x > $c) q(Rat.trichotomy₄ $h₁ $h₂) + else if k₁ == .GEQ && k₂ == .LEQ then + let h₁ : Q($x ≥ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≤ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x = $c) q(Rat.trichotomy₅ $h₁ $h₂) + else if k₁ == .GEQ && k₂ == .NOT then + let h₁ : Q($x ≥ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≠ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x > $c) q(Rat.trichotomy₆ $h₁ $h₂) + else + return none + | .ARITH_POLY_NORM => + if pf.getResult[0]!.getSort.getKind == .BOOLEAN_SORT then + if pf.getResult[0]![0]!.getSort.isInteger then return none + let a₁ : Q(Rat) ← reconstructTerm pf.getResult[0]![0]! + let a₂ : Q(Rat) ← reconstructTerm pf.getResult[0]![1]! + let b₁ : Q(Rat) ← reconstructTerm pf.getResult[1]![0]! + let b₂ : Q(Rat) ← reconstructTerm pf.getResult[1]![1]! + let (l, es) ← (toPolyNormExpr q($a₁ - $a₂)).run #[] + let (r, _) ← (toPolyNormExpr q($b₁ - $b₂)).run es + let c₁ : Q(Rat) := + if h : 0 < r.toPolynomial.length then PolyNorm.Monomial.toExpr.toExprCoeff r.toPolynomial[0].coeff.abs else q(1) + let c₂ : Q(Rat) := + if h : 0 < l.toPolynomial.length then PolyNorm.Monomial.toExpr.toExprCoeff l.toPolynomial[0].coeff.abs else q(1) + let hc₁ : Q($c₁ > 0) := .app q(@of_decide_eq_true ($c₁ > 0) _) q(Eq.refl true) + let hc₂ : Q($c₂ > 0) := .app q(@of_decide_eq_true ($c₂ > 0) _) q(Eq.refl true) + let h : Q($c₁ * ($a₁ - $a₂) = $c₂ * ($b₁ - $b₂)) ← Meta.mkFreshExprMVar q($c₁ * ($a₁ - $a₂) = $c₂ * ($b₁ - $b₂)) + Rat.polyNorm h.mvarId! + match pf.getResult[0]!.getKind with + | .LT => + addThm q(($a₁ < $a₂) = ($b₁ < $b₂)) q(Rat.lt_of_sub_eq $hc₁ $hc₂ $h) + | .LEQ => + addThm q(($a₁ ≤ $a₂) = ($b₁ ≤ $b₂)) q(Rat.le_of_sub_eq $hc₁ $hc₂ $h) + | .EQUAL => + addThm q(($a₁ = $a₂) = ($b₁ = $b₂)) q(Rat.eq_of_sub_eq $hc₁ $hc₂ $h) + | .GEQ => + addThm q(($a₁ ≥ $a₂) = ($b₁ ≥ $b₂)) q(Rat.ge_of_sub_eq $hc₁ $hc₂ $h) + | .GT => + addThm q(($a₁ > $a₂) = ($b₁ > $b₂)) q(Rat.gt_of_sub_eq $hc₁ $hc₂ $h) + | _ => return none + else + if pf.getResult[0]!.getSort.isInteger then return none + let a : Q(Int) ← reconstructTerm pf.getResult[0]! + let b : Q(Int) ← reconstructTerm pf.getResult[1]! + addTac q($a = $b) Rat.polyNorm + | .ARITH_MULT_SIGN => + if pf.getResult[1]![0]!.getSort.isInteger then return none + reconstructMulSign pf + | .ARITH_MULT_POS => + if pf.getArguments[0]!.getSort.isInteger then return none + let m : Q(Rat) ← reconstructTerm pf.getArguments[0]! + let l : Q(Rat) ← reconstructTerm pf.getArguments[1]![0]! + let r : Q(Rat) ← reconstructTerm pf.getArguments[1]![1]! + match pf.getArguments[1]!.getKind with + | .LT => + addThm q($m > 0 ∧ $l < $r → $m * $l < $m * $r) q(@Rat.mul_pos_lt $l $r $m) + | .LEQ => + addThm q($m > 0 ∧ $l ≤ $r → $m * $l ≤ $m * $r) q(@Rat.mul_pos_le $l $r $m) + | .EQUAL => + addThm q($m > 0 ∧ $l = $r → $m * $l = $m * $r) q(@Rat.mul_pos_eq $l $r $m) + | .GEQ => + addThm q($m > 0 ∧ $l ≥ $r → $m * $l ≥ $m * $r) q(@Rat.mul_pos_ge $l $r $m) + | .GT => + addThm q($m > 0 ∧ $l > $r → $m * $l > $m * $r) q(@Rat.mul_pos_gt $l $r $m) + | _ => return none + | .ARITH_MULT_NEG => + if pf.getArguments[0]!.getSort.isInteger then return none + let m : Q(Rat) ← reconstructTerm pf.getArguments[0]! + let l : Q(Rat) ← reconstructTerm pf.getArguments[1]![0]! + let r : Q(Rat) ← reconstructTerm pf.getArguments[1]![1]! + match pf.getArguments[1]!.getKind with + | .LT => + addThm q($m < 0 ∧ $l < $r → $m * $l > $m * $r) q(@Rat.mul_neg_lt $l $r $m) + | .LEQ => + addThm q($m < 0 ∧ $l ≤ $r → $m * $l ≥ $m * $r) q(@Rat.mul_neg_le $l $r $m) + | .EQUAL => + addThm q($m < 0 ∧ $l = $r → $m * $l = $m * $r) q(@Rat.mul_neg_eq $l $r $m) + | .GEQ => + addThm q($m < 0 ∧ $l ≥ $r → $m * $l ≤ $m * $r) q(@Rat.mul_neg_ge $l $r $m) + | .GT => + addThm q($m < 0 ∧ $l > $r → $m * $l < $m * $r) q(@Rat.mul_neg_gt $l $r $m) + | _ => return none + | .ARITH_MULT_TANGENT => + let x : Q(Rat) ← reconstructTerm pf.getArguments[0]! + let y : Q(Rat) ← reconstructTerm pf.getArguments[1]! + let a : Q(Rat) ← reconstructTerm pf.getArguments[2]! + let b : Q(Rat) ← reconstructTerm pf.getArguments[3]! + if pf.getArguments[4]!.getIntegerValue == -1 then + addThm q(($x * $y ≤ $b * $x + $a * $y - $a * $b) = ($x ≤ $a ∧ $y ≥ $b ∨ $x ≥ $a ∧ $y ≤ $b)) q(@Rat.mul_tangent_lower_eq $a $b $x $y) + else + addThm q(($x * $y ≥ $b * $x + $a * $y - $a * $b) = ($x ≤ $a ∧ $y ≤ $b ∨ $x ≥ $a ∧ $y ≥ $b)) q(@Rat.mul_tangent_upper_eq $a $b $x $y) + | _ => return none + +end Smt.Reconstruct.Rat diff --git a/Smt/Reconstruct/Rat/Core.lean b/Smt/Reconstruct/Rat/Core.lean new file mode 100644 index 00000000..bf13d7ae --- /dev/null +++ b/Smt/Reconstruct/Rat/Core.lean @@ -0,0 +1,23 @@ +/- +Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abdalrhman Mohamed +-/ + +import Batteries.Data.Rat + +namespace Rat + +def abs (x : Rat) := if x < 0 then -x else x + +protected theorem add_zero : ∀ a : Rat, a + 0 = a := by + sorry + +protected theorem add_assoc : ∀ a b c : Rat, a + b + c = a + (b + c) := by + sorry + +protected theorem mul_assoc (a b c : Rat) : a * b * c = a * (b * c) := by + sorry + +end Rat diff --git a/Smt/Reconstruct/Rat/Lemmas.lean b/Smt/Reconstruct/Rat/Lemmas.lean new file mode 100644 index 00000000..57e6d6b4 --- /dev/null +++ b/Smt/Reconstruct/Rat/Lemmas.lean @@ -0,0 +1,210 @@ +/- +Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tomaz Gomes Mascarenhas, Abdalrhman Mohamed +-/ + +import Batteries.Data.Rat + +private theorem Rat.mul_lt_mul_left {c x y : Rat} (hc : c > 0) : (c * x < c * y) = (x < y) := by + sorry + +private theorem Rat.mul_le_mul_left {c x y : Rat} (hc : c > 0) : (c * x ≤ c * y) = (x ≤ y) := by + sorry + +private theorem Rat.mul_eq_zero_left {x y : Rat} (hx : x ≠ 0) (hxy : x * y = 0) : y = 0 := by + sorry + +private def uncurry {p₁ p₂ p₃ : Prop} : (p₁ → p₂ → p₃) → (p₁ ∧ p₂) → p₃ := by + intros h₁ h₂ + have ⟨ht₁, ht₂⟩ := h₂ + exact h₁ ht₁ ht₂ + +namespace Smt.Reconstruct.Rat + +variable {a b c d : Rat} + +theorem sum_ub₁ (h₁ : a < b) (h₂ : c < d) : a + c < b + d := by + sorry + +theorem sum_ub₂ (h₁ : a < b) (h₂ : c ≤ d) : a + c < b + d := by + sorry + +theorem sum_ub₃ (h₁ : a < b) (h₂ : c = d) : a + c < b + d := by + sorry + +theorem sum_ub₄ (h₁ : a ≤ b) (h₂ : c < d) : a + c < b + d := by + sorry + +theorem sum_ub₅ (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d := by + sorry + +theorem sum_ub₆ (h₁ : a ≤ b) (h₂ : c = d) : a + c ≤ b + d := by + sorry + +theorem sum_ub₇ (h₁ : a = b) (h₂ : c < d) : a + c < b + d := by + sorry + +theorem sum_ub₈ (h₁ : a = b) (h₂ : c ≤ d) : a + c ≤ b + d := by + sorry + +theorem sum_ub₉ (h₁ : a = b) (h₂ : c = d) : a + c ≤ b + d := by + sorry + +theorem neg_lt_neg (h : a < b) : -a > -b := by + sorry + +theorem neg_le_neg (h : a ≤ b) : -a ≥ -b := by + sorry + +theorem int_tight_ub {i : Int} (h : i < c) : i ≤ c.floor := by + sorry + +theorem int_tight_lb {i : Int} (h : i > c) : i ≥ c.ceil := by + sorry + +theorem trichotomy₁ (h₁ : a ≤ b) (h₂ : a ≠ b) : a < b := by + sorry + +theorem trichotomy₂ (h₁ : a ≤ b) (h₂ : a ≥ b) : a = b := by + sorry + +theorem trichotomy₃ (h₁ : a ≠ b) (h₂ : a ≤ b) : a < b := by + sorry + +theorem trichotomy₄ (h₁ : a ≠ b) (h₂ : a ≥ b) : a > b := by + sorry + +theorem trichotomy₅ (h₁ : a ≥ b) (h₂ : a ≤ b) : a = b := by + sorry + +theorem trichotomy₆ (h₁ : a ≥ b) (h₂ : a ≠ b) : a > b := by + sorry + +theorem lt_eq_sub_lt_zero : (a < b) = (a - b < 0) := by + sorry + +theorem le_eq_sub_le_zero : (a ≤ b) = (a - b ≤ 0) := by + sorry + +theorem eq_eq_sub_eq_zero : (a = b) = (a - b = 0) := by + sorry + +theorem ge_eq_sub_ge_zero : (a ≥ b) = (a - b ≥ 0) := by + sorry + +theorem gt_eq_sub_gt_zero : (a > b) = (a - b > 0) := by + sorry + +theorem lt_of_sub_eq {c₁ c₂ : Rat} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ < a₂) = (b₁ < b₂) := by + have {c x y : Rat} (hc : c > 0) : (c * (x - y) < 0) = (x - y < 0) := by + rw (config := { occs := .pos [1] }) [← Rat.mul_zero c, Rat.mul_lt_mul_left hc] + rw [lt_eq_sub_lt_zero, @lt_eq_sub_lt_zero b₁, ← this hc₁, ← this hc₂, h] + +theorem le_of_sub_eq {c₁ c₂ : Rat} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ ≤ a₂) = (b₁ ≤ b₂) := by + have {c x y : Rat} (hc : c > 0) : (c * (x - y) ≤ 0) = (x - y ≤ 0) := by + rw (config := { occs := .pos [1] }) [← Rat.mul_zero c, Rat.mul_le_mul_left hc] + rw [le_eq_sub_le_zero, @le_eq_sub_le_zero b₁, ← this hc₁, ← this hc₂, h] + +theorem eq_of_sub_eq {c₁ c₂ : Rat} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ = a₂) = (b₁ = b₂) := by + have {c x y : Rat} (hc : c > 0) : (c * (x - y) = 0) = (x - y = 0) := by + apply propext; constructor + · apply Rat.mul_eq_zero_left sorry + · intro hxy; rw [hxy, Rat.mul_zero] + rw [@eq_eq_sub_eq_zero a₁, @eq_eq_sub_eq_zero b₁, ← this hc₁, ← this hc₂, h] + +theorem ge_of_sub_eq {c₁ c₂ : Rat} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ ≥ a₂) = (b₁ ≥ b₂) := by + have {c x y : Rat} (hc : c > 0) : (c * (x - y) ≥ 0) = (x - y ≥ 0) := by + rw (config := { occs := .pos [1] }) [← Rat.mul_zero c, ge_iff_le, Rat.mul_le_mul_left hc] + rw [ge_eq_sub_ge_zero, @ge_eq_sub_ge_zero b₁, ← this hc₁, ← this hc₂, h] + +theorem gt_of_sub_eq {c₁ c₂ : Rat} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ > a₂) = (b₁ > b₂) := by + have {c x y : Rat} (hc : c > 0) : (c * (x - y) > 0) = (x - y > 0) := by + rw (config := { occs := .pos [1] }) [← Rat.mul_zero c, gt_iff_lt, Rat.mul_lt_mul_left hc] + rw [gt_eq_sub_gt_zero, @gt_eq_sub_gt_zero b₁, ← this hc₁, ← this hc₂, h] + +theorem mul_sign₁ (ha : a < 0) (hb : b < 0) : a * b > 0 := by + sorry + +theorem mul_sign₃ (ha : a < 0) (hb : b > 0) : a * b < 0 := by + sorry + +theorem mul_sign₄ (ha : a > 0) (hb : b < 0) : a * b < 0 := by + sorry + +theorem mul_sign₆ (ha : a > 0) (hb : b > 0) : a * b > 0 := by + sorry + +theorem mul_sign₀ (ha : a ≠ 0) : a * a > 0 := + sorry + +theorem mul_sign₂ (ha : a < 0) (hb : b ≠ 0) : a * b * b < 0 := + sorry + +theorem mul_sign₅ (ha : a > 0) (hb : b ≠ 0) : a * b * b > 0 := + sorry + +theorem mul_pos_lt (h : c > 0 ∧ a < b) : c * a < c * b := + sorry + +theorem mul_pos_le (h : c > 0 ∧ a ≤ b) : c * a ≤ c * b := + sorry + +theorem mul_pos_gt (h : c > 0 ∧ a > b) : c * a > c * b := + mul_pos_lt h + +theorem mul_pos_ge (h : c > 0 ∧ a ≥ b) : c * a ≥ c * b := + mul_pos_le h + +theorem mul_pos_eq (h : c > 0 ∧ a = b) : c * a = c * b := by + rw [h.2] + +theorem mul_neg_lt (h : c < 0 ∧ a < b) : c * a > c * b := + sorry + +theorem mul_neg_le (h : c < 0 ∧ a ≤ b) : c * a ≥ c * b := + sorry + +theorem mul_neg_gt (h : c < 0 ∧ a > b) : c * a < c * b := + mul_neg_lt h + +theorem mul_neg_ge (h : c < 0 ∧ a ≥ b) : c * a ≤ c * b := + mul_neg_le h + +theorem mul_neg_eq (h : c < 0 ∧ a = b) : c * a = c * b := by + rw [h.2] + +theorem mul_tangent_mp_lower (h : x * y ≤ b * x + a * y - a * b) + : x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b := + sorry + +theorem mul_tangent_mpr_lower (h : x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b) + : x * y ≤ b * x + a * y - a * b := + sorry + +theorem mul_tangent_lower : + x * y ≤ b * x + a * y - a * b ↔ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b := + ⟨mul_tangent_mp_lower, mul_tangent_mpr_lower⟩ + +theorem mul_tangent_lower_eq + : (x * y ≤ b * x + a * y - a * b) = (x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b) := + propext (mul_tangent_lower) + +theorem mul_tangent_mp_upper (h : x * y ≥ b * x + a * y - a * b) + : x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b := + sorry + +theorem mul_tangent_mpr_upper (h : x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b) + : x * y ≥ b * x + a * y - a * b := + sorry + +theorem mul_tangent_upper + : x * y ≥ b * x + a * y - a * b ↔ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b := + ⟨mul_tangent_mp_upper, mul_tangent_mpr_upper⟩ + +theorem mul_tangent_upper_eq + : (x * y ≥ b * x + a * y - a * b) = (x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b) := + propext (mul_tangent_upper) + +end Smt.Reconstruct.Rat diff --git a/Smt/Reconstruct/Rat/Polynorm.lean b/Smt/Reconstruct/Rat/Polynorm.lean new file mode 100644 index 00000000..93ff125e --- /dev/null +++ b/Smt/Reconstruct/Rat/Polynorm.lean @@ -0,0 +1,289 @@ +/- +Copyright (c) 2021-2024 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abdalrhman Mohamed +-/ + +import Batteries.Data.Rat + +import Lean +import Qq + +theorem Rat.neg_mul_eq_neg_mul (a b : Rat) : -(a * b) = -a * b := by + sorry + +@[simp] theorem Rat.zero_add (a : Rat) : 0 + a = a := by + simp [add_def, normalize_eq_mkRat, Int.add_comm, Nat.add_comm, mkRat_self] + +namespace Smt.Reconstruct.Rat.PolyNorm + +abbrev Var := Nat + +def Context := Var → Rat + +structure Monomial where + coeff : Rat + vars : List Var +deriving Inhabited, Repr + +namespace Monomial + +open Qq in +def toExpr (m : Monomial) (ppCtx : Var → Q(Rat)) : Q(Rat) := + if h : m.vars = [] then + toExprCoeff m.coeff + else + if m.coeff = 1 then + (m.vars.drop 1).foldl (fun acc v => q($acc * $(ppCtx v))) (ppCtx (m.vars.head h)) + else + m.vars.foldl (fun acc v => q($acc * $(ppCtx v))) (toExprCoeff m.coeff) +where + toExprCoeff (c : Rat) : Q(Rat) := + let num : Q(Rat) := mkRatLit c.num.natAbs + if c.den == 1 then + if c.num ≥ 0 then + q($num) + else + q(-$num) + else + let den : Q(Rat) := mkRatLit c.den + if c.num ≥ 0 then + q($num / $den) + else + q(-$num / $den) + mkRatLit (n : Nat) : Q(Rat) := + let l : Q(Nat) := Lean.mkRawNatLit n + q(OfNat.ofNat $l) + +def neg (m : Monomial) : Monomial := + { m with coeff := -m.coeff } + +def add (m₁ m₂ : Monomial) (_ : m₁.vars = m₂.vars) : Monomial := + { coeff := m₁.coeff + m₂.coeff, vars := m₁.vars } + +-- Invariant: monomial variables remain sorted. +def mul (m₁ m₂ : Monomial) : Monomial := + let coeff := m₁.coeff * m₂.coeff + let vars := m₁.vars.foldr insert m₂.vars + { coeff, vars } +where + insert (x : Var) : List Var → List Var + | [] => [x] + | y :: ys => if x ≤ y then x :: y :: ys else y :: insert x ys + +def divConst (m : Monomial) (c : Rat) : Monomial := + { m with coeff := m.coeff / c } + +def denote (ctx : Context) (m : Monomial) : Rat := + m.coeff * m.vars.foldl (fun acc v => acc * ctx v) 1 + +theorem denote_neg {m : Monomial} : m.neg.denote ctx = -m.denote ctx := by + simp only [neg, denote, Rat.neg_mul_eq_neg_mul] + +theorem denote_mul {m₁ m₂ : Monomial} : (m₁.mul m₂).denote ctx = m₁.denote ctx * m₂.denote ctx := + sorry + +theorem denote_divConst {m : Monomial} : (m.divConst c).denote ctx = m.denote ctx / c := + sorry + +end Monomial + +abbrev Polynomial := List Monomial + +namespace Polynomial + +open Qq in +def toExpr (p : Polynomial) (ppCtx : Var → Q(Rat)) : Q(Rat) := + go p +where + go : Polynomial → Q(Rat) + | [] => q(0) + | [m] => m.toExpr ppCtx + | m :: ms =>q($(m.toExpr ppCtx) + $(go ms)) + +def neg (p : Polynomial) : Polynomial := + p.map Monomial.neg + +-- NOTE: implementation merges monomials with same variables. +-- Invariant: monomials remain sorted. +def add (p q : Polynomial) : Polynomial := + p.foldr insert q +where + insert (m : Monomial) : Polynomial → Polynomial + | [] => [m] + | n :: ns => + if m.vars < n.vars then + m :: n :: ns + else if h : m.vars = n.vars then + let m' := m.add n h + if m'.coeff = 0 then ns else m' :: ns + else + n :: insert m ns + +def sub (p q : Polynomial) : Polynomial := + p.add q.neg + +-- Invariant: monomials remain sorted. +def mulMonomial (m : Monomial) (p : Polynomial) : Polynomial := + p.foldr (fun n acc => Polynomial.add [m.mul n] acc) [] + +-- Invariant: monomials remain sorted. +def mul (p q : Polynomial) : Polynomial := + p.foldl (fun acc m => (q.mulMonomial m).add acc) [] + +def divConst (p : Polynomial) (c : Rat) : Polynomial := + p.map (·.divConst c) + +def denote (ctx : Context) (p : Polynomial) : Rat := + p.foldl (fun acc m => acc + m.denote ctx) 0 + +theorem denote_neg {p : Polynomial} : p.neg.denote ctx = -p.denote ctx := + sorry + +theorem denote_add {p q : Polynomial} : (p.add q).denote ctx = p.denote ctx + q.denote ctx := + sorry + +theorem denote_sub {p q : Polynomial} : (p.sub q).denote ctx = p.denote ctx - q.denote ctx := by + simp only [sub, denote_neg, denote_add, Rat.sub_eq_add_neg] + +theorem denote_mulMonomial {p : Polynomial} : (p.mulMonomial m).denote ctx = m.denote ctx * p.denote ctx := + sorry + +theorem denote_mul {p q : Polynomial} : (p.mul q).denote ctx = p.denote ctx * q.denote ctx := + sorry + +theorem denote_divConst {p : Polynomial} : (p.divConst c).denote ctx = p.denote ctx / c := by + sorry + +end Polynomial + +inductive Expr where + | val (v : Rat) + | var (v : Nat) + | neg (a : Expr) + | add (a b : Expr) + | sub (a b : Expr) + | mul (a b : Expr) + | divConst (a : Expr) (c : Rat) +deriving Inhabited, Repr + +namespace Expr + +def toPolynomial : Expr → Polynomial + | val v => if v = 0 then [] else [{ coeff := v, vars := [] }] + | var v => [{ coeff := 1, vars := [v] }] + | neg a => a.toPolynomial.neg + | add a b => Polynomial.add a.toPolynomial b.toPolynomial + | sub a b => Polynomial.sub a.toPolynomial b.toPolynomial + | mul a b => Polynomial.mul a.toPolynomial b.toPolynomial + | divConst a c => Polynomial.divConst a.toPolynomial c + +def denote (ctx : Context) : Expr → Rat + | val v => v + | var v => ctx v + | neg a => -a.denote ctx + | add a b => a.denote ctx + b.denote ctx + | sub a b => a.denote ctx - b.denote ctx + | mul a b => a.denote ctx * b.denote ctx + | divConst a c => a.denote ctx / c + +theorem denote_toPolynomial {e : Expr} : e.denote ctx = e.toPolynomial.denote ctx := by + induction e with + | val v => + simp only [denote, toPolynomial] + split <;> rename_i hv + · rewrite [hv]; rfl + · simp [Polynomial.denote, Monomial.denote] + | var v => + simp [denote, toPolynomial, Polynomial.denote, Monomial.denote] + | neg a ih => + simp only [denote, toPolynomial, Polynomial.denote_neg, ih] + | add a b ih₁ ih₂ => + simp only [denote, toPolynomial, Polynomial.denote_add, ih₁, ih₂] + | sub a b ih₁ ih₂ => + simp only [denote, toPolynomial, Polynomial.denote_sub, ih₁, ih₂] + | mul a b ih₁ ih₂ => + simp only [denote, toPolynomial, Polynomial.denote_mul, ih₁, ih₂] + | divConst a c ih => + simp only [denote, toPolynomial, Polynomial.denote_divConst, ih] + +theorem denote_eq_from_toPolynomial_eq {e₁ e₂ : Expr} (h : e₁.toPolynomial = e₂.toPolynomial) : e₁.denote ctx = e₂.denote ctx := by + rw [denote_toPolynomial, denote_toPolynomial, h] + +end PolyNorm.Expr + +open Lean hiding Rat +open Qq + +abbrev PolyM := StateT (Array Q(Rat)) MetaM + +def getIndex (e : Q(Rat)) : PolyM Nat := do + let es ← get + if let some i := es.findIdx? (· == e) then + return i + else + let size := es.size + set (es.push e) + return size + +partial def toRatConst (e : Q(Rat)) : PolyM Rat := do + match e with + | ~q(OfNat.ofNat $n) => pure n.rawNatLit?.get! + | ~q(-$x) => pure (-(← toRatConst x)) + | ~q($x + $y) => pure ((← toRatConst x) + (← toRatConst y)) + | ~q($x - $y) => pure ((← toRatConst x) - (← toRatConst y)) + | ~q($x * $y) => pure ((← toRatConst x) * (← toRatConst y)) + | ~q($x / $y) => pure ((← toRatConst x) / (← toRatConst y)) + | e => throwError "[poly_norm] expected a rational number, got {e}" + +partial def toPolyNormExpr (e : Q(Rat)) : PolyM PolyNorm.Expr := do + match e with + | ~q(OfNat.ofNat $x) => pure (.val x.rawNatLit?.get!) + | ~q(-$x) => pure (.neg (← toPolyNormExpr x)) + | ~q($x + $y) => pure (.add (← toPolyNormExpr x) (← toPolyNormExpr y)) + | ~q($x - $y) => pure (.sub (← toPolyNormExpr x) (← toPolyNormExpr y)) + | ~q($x * $y) => pure (.mul (← toPolyNormExpr x) (← toPolyNormExpr y)) + | ~q($x / $y) => pure (.divConst (← toPolyNormExpr x) (← toRatConst y)) + | e => let v : Nat ← getIndex e; pure (.var v) + +partial def toQPolyNormExpr (e : Q(Rat)) : PolyM Q(PolyNorm.Expr) := do + match e with + | ~q(OfNat.ofNat $n) => pure q(.val (@OfNat.ofNat Rat $n _)) + | ~q(-$x) => pure q(.neg $(← toQPolyNormExpr x)) + | ~q($x + $y) => pure q(.add $(← toQPolyNormExpr x) $(← toQPolyNormExpr y)) + | ~q($x - $y) => pure q(.sub $(← toQPolyNormExpr x) $(← toQPolyNormExpr y)) + | ~q($x * $y) => pure q(.mul $(← toQPolyNormExpr x) $(← toQPolyNormExpr y)) + | ~q($x / $y) => pure q(.divConst $(← toQPolyNormExpr x) $(PolyNorm.Monomial.toExpr.toExprCoeff (← toRatConst y))) + | e => let v : Nat ← getIndex e; pure q(.var $v) + +def polyNorm (mv : MVarId) : MetaM Unit := do + let some (_, l, r) := (← mv.getType).eq? + | throwError "[poly_norm] expected an equality, got {← mv.getType}" + let (l, es) ← (toQPolyNormExpr l).run #[] + let (r, es) ← (toQPolyNormExpr r).run es + let is : Q(Array Rat) := es.foldl (fun acc e => q(«$acc».push $e)) q(#[]) + let ctx : Q(PolyNorm.Context) := q(fun v => if h : v < «$is».size then $is[v] else 0) + let h : Q(«$l».toPolynomial = «$r».toPolynomial) := .app q(@Eq.refl.{1} PolyNorm.Polynomial) q(«$l».toPolynomial) + mv.assign q(@PolyNorm.Expr.denote_eq_from_toPolynomial_eq $ctx $l $r $h) +where + logPolynomial (e : Q(PolyNorm.Expr)) (es : Array Q(Rat)) := do + let p ← unsafe Meta.evalExpr PolyNorm.Expr q(PolyNorm.Expr) e + let ppCtx := fun v => if h : v < es.size then es[v] else q(0) + logInfo m!"poly := {PolyNorm.Polynomial.toExpr p.toPolynomial ppCtx}" + +namespace Tactic + +syntax (name := polyNorm) "poly_norm" : tactic + +open Lean.Elab Tactic in +@[tactic polyNorm] def evalPolyNorm : Tactic := fun _ => + withMainContext do + let mv ← Tactic.getMainGoal + Rat.polyNorm mv + replaceMainGoal [] + +end Smt.Reconstruct.Rat.Tactic + +example (x y z : Rat) : 1 * (x + y) * z / 4 = 1/(2 * 2) * (z * y + x * z) := by + poly_norm diff --git a/Smt/Reconstruct/Rat/Rewrites.lean b/Smt/Reconstruct/Rat/Rewrites.lean new file mode 100644 index 00000000..20eda57d --- /dev/null +++ b/Smt/Reconstruct/Rat/Rewrites.lean @@ -0,0 +1,83 @@ +/- +Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abdalrhman Mohamed +-/ + +import Batteries.Data.Rat + +namespace Smt.Reconstruct.Rat.Rewrite + +open Function + +theorem div_by_const_elim {t c : Rat} : t / c = t * (1 / c) := + sorry + +-- https://github.com/cvc5/cvc5/blob/proof-new/src/theory/arith/rewrites + +variable {t ts x xs : Rat} + +theorem plus_zero : ts + 0 + ss = ts + ss := + sorry + +theorem mul_one : ts * 1 * ss = ts * ss := + (_root_.Rat.mul_one ts).symm ▸ rfl +theorem mul_zero : ts * 0 * ss = 0 := + (_root_.Rat.mul_zero ts).symm ▸ (Rat.zero_mul ss).symm ▸ rfl + +theorem div_total : s ≠ 0 → t / s = t / s := + const _ rfl + +theorem neg_neg_one : -1 * (-1 * t) = t := + sorry + +-- Eliminations + +theorem elim_uminus : -t = -1 * t := + sorry +theorem elim_minus : t - s = t + -1 * s := + sorry +theorem elim_gt : (t > s) = ¬(t ≤ s) := + sorry +theorem elim_lt : (t < s) = ¬(t ≥ s) := + sorry +theorem elim_leq : (t ≤ s) = (s ≥ t) := + propext ge_iff_le + +theorem geq_norm1 : (t ≥ s) = (t - s ≥ 0) := + sorry + +theorem geq_norm2 : (t ≥ s) = (-t ≤ -s) := + sorry + +theorem refl_leq : (t ≤ t) = True := + sorry +theorem refl_lt : (t < t) = False := + sorry +theorem refl_geq : (t ≥ t) = True := + sorry +theorem refl_gt : (t > t) = False := + sorry + +theorem eq_elim : (t = s) = (t ≥ s ∧ t ≤ s) := + sorry + +theorem plus_flatten : xs + (w + ys) + zs = xs + w + ys + zs := + sorry + +theorem mult_flatten : xs * (w * ys) * zs = xs * w * ys * zs := + sorry + +theorem mult_dist : x * (y + z + ws) = x * y + x * (z + ws) := + sorry + +theorem plus_cancel1 : ts + x + ss + (-1 * x) + rs = ts + ss + rs := + sorry +theorem plus_cancel2 : ts + (-1 * x) + ss + x + rs = ts + ss + rs := + sorry + +theorem abs_elim : (if x < 0 then -x else x) = if x < 0 then -x else x := + rfl + +end Smt.Reconstruct.Rat.Rewrite diff --git a/Smt/Reconstruct/Real.lean b/Smt/Reconstruct/Real.lean new file mode 100644 index 00000000..b6d06a9a --- /dev/null +++ b/Smt/Reconstruct/Real.lean @@ -0,0 +1,488 @@ +/- +Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abdalrhman Mohamed +-/ + +import Smt.Reconstruct +import Smt.Reconstruct.Builtin.Lemmas +import Smt.Reconstruct.Real.Lemmas +import Smt.Reconstruct.Real.Polynorm +import Smt.Reconstruct.Real.Rewrites +import Smt.Reconstruct.Rewrite + +namespace Smt.Reconstruct.Real + +open Lean Qq + +@[smt_sort_reconstruct] def reconstructRealSort : SortReconstructor := fun s => do match s.getKind with + | .REAL_SORT => return q(Real) + | _ => return none + +@[smt_term_reconstruct] def reconstructReal : TermReconstructor := fun t => do match t.getKind with + | .SKOLEM => match t.getSkolemId with + | .DIV_BY_ZERO => return q(fun (x : Real) => x / 0) + | _ => return none + | .CONST_RATIONAL => + let c : Lean.Rat := t.getRationalValue + let num : Q(Real) := mkRealLit c.num.natAbs + if c.den == 1 then + if c.num ≥ 0 then + return q($num) + else + return q(-$num) + else + let den : Q(Real) := mkRealLit c.den + if c.num ≥ 0 then + return q($num / $den) + else + return q(-$num / $den) + | .NEG => + if t.getSort.isInteger then return none + let x : Q(Real) ← reconstructTerm t[0]! + return q(-$x) + | .SUB => + if t.getSort.isInteger then return none + leftAssocOp q(@HSub.hSub Real Real Real _) t + | .ADD => + if t.getSort.isInteger then return none + leftAssocOp q(@HAdd.hAdd Real Real Real _) t + | .MULT => + if t.getSort.isInteger then return none + leftAssocOp q(@HMul.hMul Real Real Real _) t + | .DIVISION => + leftAssocOp q(@HDiv.hDiv Real Real Real _) t + | .DIVISION_TOTAL => + leftAssocOp q(@HDiv.hDiv Real Real Real _) t + | .ABS => + if t.getSort.isInteger then return none + let x : Q(Real) ← reconstructTerm t[0]! + return q(if $x < 0 then -$x else $x) + | .LEQ => + if t[0]!.getSort.isInteger then return none + let x : Q(Real) ← reconstructTerm t[0]! + let y : Q(Real) ← reconstructTerm t[1]! + return q($x ≤ $y) + | .LT => + if t[0]!.getSort.isInteger then return none + let x : Q(Real) ← reconstructTerm t[0]! + let y : Q(Real) ← reconstructTerm t[1]! + return q($x < $y) + | .GEQ => + if t[0]!.getSort.isInteger then return none + let x : Q(Real) ← reconstructTerm t[0]! + let y : Q(Real) ← reconstructTerm t[1]! + return q($x ≥ $y) + | .GT => + if t[0]!.getSort.isInteger then return none + let x : Q(Real) ← reconstructTerm t[0]! + let y : Q(Real) ← reconstructTerm t[1]! + return q($x > $y) + | .TO_REAL => + let x : Q(Int) ← reconstructTerm t[0]! + return q($x : Real) + | .TO_INTEGER => + let x : Q(Real) ← reconstructTerm t[0]! + return q(⌊$x⌋) + | .IS_INTEGER => + let x : Q(Real) ← reconstructTerm t[0]! + return q($x = ⌊$x⌋) + | _ => return none +where + mkRealLit (n : Nat) : Q(Real) := match h : n with + | 0 => q(0 : Real) + | 1 => q(1 : Real) + | _ + 2 => + let h : Q(Nat.AtLeastTwo $n) := h ▸ q(instNatAtLeastTwo) + let h := mkApp3 q(@instOfNatAtLeastTwo Real) (mkRawNatLit n) q(Real.instNatCast) h + mkApp2 q(@OfNat.ofNat Real) (mkRawNatLit n) h + leftAssocOp (op : Expr) (t : cvc5.Term) : ReconstructM Expr := do + let mut curr ← reconstructTerm t[0]! + for i in [1:t.getNumChildren] do + curr := mkApp2 op curr (← reconstructTerm t[i]!) + return curr + +def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do + match pf.getRewriteRule with + | .ARITH_DIV_BY_CONST_ELIM => + let t : Q(Real) ← reconstructTerm pf.getResult[0]![0]! + let r := pf.getResult[0]![1]!.getRationalValue + if r.den == 1 then + let c : Q(Real) := reconstructReal.mkRealLit r.num.natAbs + if r.num ≥ 0 then + if r.num == 1 then + addThm q($t / 1 = $t * 1) q(@Rewrite.div_by_const_elim_1_pos $t) + else + addThm q($t / $c = $t * (1 / $c)) q(@Rewrite.div_by_const_elim_num_pos $t $c) + else + if r.num == -1 then + addThm q($t / -1 = $t * -1) q(@Rewrite.div_by_const_elim_1_neg $t) + else + addThm q($t / -$c = $t * (-1 / $c)) q(@Rewrite.div_by_const_elim_num_neg $t $c) + else + let c₁ : Q(Real) := reconstructReal.mkRealLit r.num.natAbs + let c₂ : Q(Real) := reconstructReal.mkRealLit r.den + if r.num ≥ 0 then + addThm q($t / ($c₁ / $c₂) = $t * ($c₂ / $c₁)) q(@Rewrite.div_by_const_elim_real_pos $t $c₁ $c₂) + else + addThm q($t / (-$c₁ / $c₂) = $t * (-$c₂ / $c₁)) q(@Rewrite.div_by_const_elim_real_neg $t $c₁ $c₂) + | .ARITH_PLUS_ZERO => + if pf.getArguments[1]![0]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@add_assoc Real _) q(@add_zero Real _) q(@Rewrite.plus_zero) args) + | .ARITH_MUL_ONE => + if pf.getArguments[1]![0]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@mul_assoc Real _) q(@mul_one Real _) q(@Rewrite.mul_one) args) + | .ARITH_MUL_ZERO => + if pf.getArguments[1]![0]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@mul_assoc Real _) q(@mul_one Real _) q(@Rewrite.mul_zero) args) + | .ARITH_DIV_TOTAL => + let t : Q(Real) ← reconstructTerm pf.getArguments[1]! + let s : Q(Real) ← reconstructTerm pf.getArguments[2]! + let h : Q($s ≠ 0) ← reconstructProof pf.getChildren[0]! + addThm q($t / $s = $t / $s) q(@Rewrite.div_total $t $s $h) + | .ARITH_NEG_NEG_ONE => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Real) ← reconstructTerm pf.getArguments[1]! + addThm q(-1 * (-1 * $t) = $t) q(@Rewrite.neg_neg_one $t) + | .ARITH_ELIM_UMINUS => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Real) ← reconstructTerm pf.getArguments[1]! + addThm q(-$t = -1 * $t) q(@Rewrite.elim_uminus $t) + | .ARITH_ELIM_MINUS => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Real) ← reconstructTerm pf.getArguments[1]! + let s : Q(Real) ← reconstructTerm pf.getArguments[2]! + addThm q($t - $s = $t + -1 * $s) q(@Rewrite.elim_minus $t $s) + | .ARITH_ELIM_GT => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Real) ← reconstructTerm pf.getArguments[1]! + let s : Q(Real) ← reconstructTerm pf.getArguments[2]! + addThm q(($t > $s) = ¬($t ≤ $s)) q(@Rewrite.elim_gt $t $s) + | .ARITH_ELIM_LT => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Real) ← reconstructTerm pf.getArguments[1]! + let s : Q(Real) ← reconstructTerm pf.getArguments[2]! + addThm q(($t < $s) = ¬($t ≥ $s)) q(@Rewrite.elim_lt $t $s) + | .ARITH_ELIM_LEQ => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Real) ← reconstructTerm pf.getArguments[1]! + let s : Q(Real) ← reconstructTerm pf.getArguments[2]! + addThm q(($t ≤ $s) = ($s ≥ $t)) q(@Rewrite.elim_leq $t $s) + | .ARITH_GEQ_NORM1 => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Real) ← reconstructTerm pf.getArguments[1]! + let s : Q(Real) ← reconstructTerm pf.getArguments[2]! + addThm q(($t ≥ $s) = ($t - $s ≥ 0)) q(@Rewrite.geq_norm1 $t $s) + | .ARITH_GEQ_NORM2 => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Real) ← reconstructTerm pf.getArguments[1]! + let s : Q(Real) ← reconstructTerm pf.getArguments[2]! + addThm q(($t ≥ $s) = (-$t ≤ -$s)) q(@Rewrite.geq_norm2 $t $s) + | .ARITH_REFL_LEQ => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Real) ← reconstructTerm pf.getArguments[1]! + addThm q(($t ≤ $t) = True) q(@Rewrite.refl_leq $t) + | .ARITH_REFL_LT => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Real) ← reconstructTerm pf.getArguments[1]! + addThm q(($t < $t) = False) q(@Rewrite.refl_lt $t) + | .ARITH_REFL_GEQ => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Real) ← reconstructTerm pf.getArguments[1]! + addThm q(($t ≥ $t) = True) q(@Rewrite.refl_geq $t) + | .ARITH_REFL_GT => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Real) ← reconstructTerm pf.getArguments[1]! + addThm q(($t > $t) = False) q(@Rewrite.refl_gt $t) + | .ARITH_PLUS_FLATTEN => + if pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@add_assoc Real _) q(@add_zero Real _) q(@Rewrite.plus_flatten) args) + | .ARITH_MULT_FLATTEN => + if pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@mul_assoc Real _) q(@mul_one Real _) q(@Rewrite.mult_flatten) args) + | .ARITH_MULT_DIST => + if pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@mul_assoc Real _) q(@mul_one Real _) q(@Rewrite.mult_dist) args) + | .ARITH_PLUS_CANCEL1 => + if pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@mul_assoc Real _) q(@mul_one Real _) q(@Rewrite.plus_cancel1) args) + | .ARITH_PLUS_CANCEL2 => + if pf.getArguments[2]!.getSort.isInteger then return none + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@add_assoc Real _) q(@add_zero Real _) q(@Rewrite.plus_cancel2) args) + | .ARITH_ABS_ELIM => + if pf.getArguments[1]!.getSort.isInteger then return none + let t : Q(Real) ← reconstructTerm pf.getArguments[1]! + addThm q(ite ($t < 0) (-$t) $t = ite ($t < 0) (-$t) $t) q(@Rewrite.abs_elim $t) + | _ => return none +where + reconstructArgs (args : Array cvc5.Term) : ReconstructM (Array (Array Expr)) := do + let mut args' := #[] + for arg in args do + let mut arg' := #[] + for subarg in arg do + arg' := arg'.push (← reconstructTerm subarg) + args' := args'.push arg' + return args' + +def reconstructSumUB (pf : cvc5.Proof) : ReconstructM (Option Expr) := do + let f := fun (ks, ls, rs, hs) p => do + let l : Q(Real) ← reconstructTerm p.getResult[0]! + let r : Q(Real) ← reconstructTerm p.getResult[1]! + let lsl := q($ls + $l) + let rsr := q($rs + $r) + let k := p.getResult.getKind + if ks == .LT && k == .LT then + let hs : Q($ls < $rs) := hs + let h : Q($l < $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Real.sum_ub₁ $hs $h)) + else if ks == .LT && k == .LEQ then + let hs : Q($ls < $rs) := hs + let h : Q($l ≤ $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Real.sum_ub₂ $hs $h)) + else if ks == .LT && k == .EQUAL then + let hs : Q($ls < $rs) := hs + let h : Q($l = $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Real.sum_ub₃ $hs $h)) + else if ks == .LEQ && k == .LT then + let hs : Q($ls ≤ $rs) := hs + let h : Q($l < $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Real.sum_ub₄ $hs $h)) + else if ks == .LEQ && k == .LEQ then + let hs : Q($ls ≤ $rs) := hs + let h : Q($l ≤ $r) ← reconstructProof p + return (.LEQ, lsl, rsr, q(Real.sum_ub₅ $hs $h)) + else if ks == .LEQ && k == .EQUAL then + let hs : Q($ls ≤ $rs) := hs + let h : Q($l = $r) ← reconstructProof p + return (.LEQ, lsl, rsr, q(Real.sum_ub₆ $hs $h)) + else if ks == .EQUAL && k == .LT then + let hs : Q($ls = $rs) := hs + let h : Q($l < $r) ← reconstructProof p + return (.LT, lsl, rsr, q(Real.sum_ub₇ $hs $h)) + else if ks == .EQUAL && k == .LEQ then + let hs : Q($ls = $rs) := hs + let h : Q($l ≤ $r) ← reconstructProof p + return (.LEQ, lsl, rsr, q(Real.sum_ub₈ $hs $h)) + else if ks == .EQUAL && k == .EQUAL then + let hs : Q($ls = $rs) := hs + let h : Q($l = $r) ← reconstructProof p + return (.EQUAL, lsl, rsr, q(Real.sum_ub₉ $hs $h)) + else + throwError "[sum_ub]: invalid kinds: {ks}, {p.getResult.getKind}" + let k := pf.getChildren[0]!.getResult.getKind + let ls : Q(Real) ← reconstructTerm pf.getChildren[0]!.getResult[0]! + let rs : Q(Real) ← reconstructTerm pf.getChildren[0]!.getResult[1]! + let hs ← reconstructProof pf.getChildren[0]! + let (_, ls, rs, hs) ← pf.getChildren[1:].foldlM f (k, ls, rs, hs) + addThm q($ls < $rs) hs + +def reconstructMulSign (pf : cvc5.Proof) : ReconstructM (Option Expr) := do + let ts := pf.getResult[0]!.getChildren + let mut hs : Array (Name × (Array Expr → ReconstructM Expr)) := #[] + let mut map : HashMap cvc5.Term Nat := {} + for h : i in [0:ts.size] do + let t := ts[i]'(h.right) + let p : Q(Prop) ← reconstructTerm t + hs := hs.push (Name.num `a i, fun _ => return p) + map := map.insert (if t.getKind == .NOT then t[0]![0]! else t[0]!) i + let t := pf.getResult[1]! + let vs := if t[0]!.getKind == .CONST_INTEGER then t[1]!.getChildren else t[0]!.getChildren + let f t ps := do + let p : Q(Prop) ← reconstructTerm t + return q($p :: $ps) + let ps : Q(List Prop) ← ts.foldrM f q([]) + let q : Q(Prop) ← reconstructTerm t + let h : Q(impliesN $ps $q) ← Meta.withLocalDeclsD hs fun hs => do + let h : Q($q) ← if ts[map.find! vs[0]!]!.getKind == .NOT then + let a : Q(Real) ← reconstructTerm vs[0]! + let ha : Q($a ≠ 0) := hs[map.find! vs[0]!]! + go vs ts hs map .GT q($a * $a) q(Real.mul_sign₀ $ha) 2 + else + let a : Q(Real) ← reconstructTerm vs[0]! + go vs ts hs map ts[map.find! vs[0]!]!.getKind a hs[map.find! vs[0]!]! 1 + Meta.mkLambdaFVars hs h + addThm q(andN $ps → $q) q(Builtin.scopes $h) +where + go vs ts hs map ka (a : Q(Real)) (ha : Expr) i : ReconstructM Expr := do + if hi : i < vs.size then + let b : Q(Real) ← reconstructTerm vs[i] + let k := ts[map.find! vs[i]]!.getKind + if ka == .LT && k == .LT then + let ha : Q($a < 0) := ha + let hb : Q($b < 0) := hs[map.find! vs[i]]! + go vs ts hs map .GT q($a * $b) q(Real.mul_sign₁ $ha $hb) (i + 1) + else if ka == .LT && k == .NOT then + let ha : Q($a < 0) := ha + let hb : Q($b ≠ 0) := hs[map.find! vs[i]]! + go vs ts hs map .LT q($a * $b * $b) q(Real.mul_sign₂ $ha $hb) (i + 2) + else if ka == .LT && k == .GT then + let ha : Q($a < 0) := ha + let hb : Q($b > 0) := hs[map.find! vs[i]]! + go vs ts hs map .LT q($a * $b) q(Real.mul_sign₃ $ha $hb) (i + 1) + else if ka == .GT && k == .LT then + let ha : Q($a > 0) := ha + let hb : Q($b < 0) := hs[map.find! vs[i]]! + go vs ts hs map .LT q($a * $b) q(Real.mul_sign₄ $ha $hb) (i + 1) + else if ka == .GT && k == .NOT then + let ha : Q($a > 0) := ha + let hb : Q($b ≠ 0) := hs[map.find! vs[i]]! + go vs ts hs map .GT q($a * $b * $b) q(Real.mul_sign₅ $ha $hb) (i + 2) + else if ka == .GT && k == .GT then + let ha : Q($a > 0) := ha + let hb : Q($b > 0) := hs[map.find! vs[i]]! + go vs ts hs map .GT q($a * $b) q(Real.mul_sign₆ $ha $hb) (i + 1) + else + throwError "[mul_sign]: invalid kinds: {ka}, {k}" + else + return ha + +@[smt_proof_reconstruct] def reconstructRealProof : ProofReconstructor := fun pf => do match pf.getRule with + | .EVALUATE => + let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort + let t : Q($α) ← reconstructTerm pf.getResult[0]! + let t' : Q($α) ← reconstructTerm pf.getResult[1]! + let h : Q(Decidable ($t = $t')) ← Meta.synthInstance q(Decidable ($t = $t')) + if !(h.getUsedConstants.any (isNoncomputable (← getEnv))) then + return none + addTac q($t = $t') Real.normNum + | .DSL_REWRITE + | .THEORY_REWRITE => reconstructRewrite pf + | .ARITH_SUM_UB => + if pf.getResult[0]!.getSort.isInteger then return none + reconstructSumUB pf + | .INT_TIGHT_UB => + let i : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[0]! + let c : Q(Real) ← reconstructTerm pf.getChildren[0]!.getResult[1]! + let h : Q($i < $c) ← reconstructProof pf.getChildren[0]! + addThm q($i ≤ ⌊$c⌋) q(@Real.int_tight_ub $c $i $h) + | .INT_TIGHT_LB => + let i : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[0]! + let c : Q(Real) ← reconstructTerm pf.getChildren[0]!.getResult[1]! + let h : Q($i > $c) ← reconstructProof pf.getChildren[0]! + addThm q($i ≥ ⌈$c⌉) q(@Real.int_tight_lb $c $i $h) + | .ARITH_TRICHOTOMY => + if pf.getResult[0]!.getSort.isInteger then return none + let x : Q(Real) ← reconstructTerm pf.getResult[0]! + let c : Q(Real) ← reconstructTerm pf.getResult[1]! + let k₁ := pf.getChildren[0]!.getResult.getKind + let k₂ := pf.getChildren[1]!.getResult.getKind + if k₁ == .LEQ && k₂ == .NOT then + let h₁ : Q($x ≤ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≠ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x < $c) q(Real.trichotomy₁ $h₁ $h₂) + else if k₁ == .LEQ && k₂ == .GEQ then + let h₁ : Q($x ≤ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≥ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x = $c) q(Real.trichotomy₂ $h₁ $h₂) + else if k₁ == .NOT && k₂ == .LEQ then + let h₁ : Q($x ≠ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≤ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x < $c) q(Real.trichotomy₃ $h₁ $h₂) + else if k₁ == .NOT && k₂ == .GEQ then + let h₁ : Q($x ≠ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≥ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x > $c) q(Real.trichotomy₄ $h₁ $h₂) + else if k₁ == .GEQ && k₂ == .LEQ then + let h₁ : Q($x ≥ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≤ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x = $c) q(Real.trichotomy₅ $h₁ $h₂) + else if k₁ == .GEQ && k₂ == .NOT then + let h₁ : Q($x ≥ $c) ← reconstructProof pf.getChildren[0]! + let h₂ : Q($x ≠ $c) ← reconstructProof pf.getChildren[1]! + addThm q($x > $c) q(Real.trichotomy₆ $h₁ $h₂) + else + return none + | .ARITH_POLY_NORM => + if pf.getResult[0]!.getSort.getKind == .BOOLEAN_SORT then + if pf.getResult[0]![0]!.getSort.isInteger then return none + let a₁ : Q(Real) ← reconstructTerm pf.getResult[0]![0]! + let a₂ : Q(Real) ← reconstructTerm pf.getResult[0]![1]! + let b₁ : Q(Real) ← reconstructTerm pf.getResult[1]![0]! + let b₂ : Q(Real) ← reconstructTerm pf.getResult[1]![1]! + -- ≠ is a hack to avoid closing the goal (if it's true) + let h : Q($a₁ - $a₂ ≠ $b₁ - $b₂) ← Meta.mkFreshExprMVar q($a₁ - $a₂ ≠ $b₁ - $b₂) + let some mv ← polyNormCore h.mvarId! | return none + let t ← mv.getType + let c₁ : Q(Real) ← Real.findConst t.appArg! + let c₂ : Q(Real) ← Real.findConst t.appFn!.appArg! + let hc₁ : Q($c₁ > 0) ← Meta.mkFreshExprMVar q($c₁ > 0) + let hc₂ : Q($c₂ > 0) ← Meta.mkFreshExprMVar q($c₂ > 0) + Real.normNum hc₁.mvarId! + Real.normNum hc₂.mvarId! + let h : Q($c₁ * ($a₁ - $a₂) = $c₂ * ($b₁ - $b₂)) ← Meta.mkFreshExprMVar q($c₁ * ($a₁ - $a₂) = $c₂ * ($b₁ - $b₂)) + Real.polyNorm h.mvarId! + match pf.getResult[0]!.getKind with + | .LT => + addThm q(($a₁ < $a₂) = ($b₁ < $b₂)) q(Real.lt_of_sub_eq $hc₁ $hc₂ $h) + | .LEQ => + addThm q(($a₁ ≤ $a₂) = ($b₁ ≤ $b₂)) q(Real.le_of_sub_eq $hc₁ $hc₂ $h) + | .EQUAL => + addThm q(($a₁ = $a₂) = ($b₁ = $b₂)) q(Real.eq_of_sub_eq $hc₁ $hc₂ $h) + | .GEQ => + addThm q(($a₁ ≥ $a₂) = ($b₁ ≥ $b₂)) q(Real.ge_of_sub_eq $hc₁ $hc₂ $h) + | .GT => + addThm q(($a₁ > $a₂) = ($b₁ > $b₂)) q(Real.gt_of_sub_eq $hc₁ $hc₂ $h) + | _ => return none + else + if pf.getResult[0]!.getSort.isInteger then return none + let a : Q(Real) ← reconstructTerm pf.getResult[0]! + let b : Q(Real) ← reconstructTerm pf.getResult[1]! + addTac q($a = $b) Real.polyNorm + | .ARITH_MULT_SIGN => + if pf.getResult[1]![0]!.getSort.isInteger then return none + reconstructMulSign pf + | .ARITH_MULT_POS => + if pf.getArguments[0]!.getSort.isInteger then return none + let m : Q(Real) ← reconstructTerm pf.getArguments[0]! + let l : Q(Real) ← reconstructTerm pf.getArguments[1]![0]! + let r : Q(Real) ← reconstructTerm pf.getArguments[1]![1]! + match pf.getArguments[1]!.getKind with + | .LT => + addThm q($m > 0 ∧ $l < $r → $m * $l < $m * $r) q(@Real.mul_pos_lt $l $r $m) + | .LEQ => + addThm q($m > 0 ∧ $l ≤ $r → $m * $l ≤ $m * $r) q(@Real.mul_pos_le $l $r $m) + | .EQUAL => + addThm q($m > 0 ∧ $l = $r → $m * $l = $m * $r) q(@Real.mul_pos_eq $l $r $m) + | .GEQ => + addThm q($m > 0 ∧ $l ≥ $r → $m * $l ≥ $m * $r) q(@Real.mul_pos_ge $l $r $m) + | .GT => + addThm q($m > 0 ∧ $l > $r → $m * $l > $m * $r) q(@Real.mul_pos_gt $l $r $m) + | _ => return none + | .ARITH_MULT_NEG => + if pf.getArguments[0]!.getSort.isInteger then return none + let m : Q(Real) ← reconstructTerm pf.getArguments[0]! + let l : Q(Real) ← reconstructTerm pf.getArguments[1]![0]! + let r : Q(Real) ← reconstructTerm pf.getArguments[1]![1]! + match pf.getArguments[1]!.getKind with + | .LT => + addThm q($m < 0 ∧ $l < $r → $m * $l > $m * $r) q(@Real.mul_neg_lt $l $r $m) + | .LEQ => + addThm q($m < 0 ∧ $l ≤ $r → $m * $l ≥ $m * $r) q(@Real.mul_neg_le $l $r $m) + | .EQUAL => + addThm q($m < 0 ∧ $l = $r → $m * $l = $m * $r) q(@Real.mul_neg_eq $l $r $m) + | .GEQ => + addThm q($m < 0 ∧ $l ≥ $r → $m * $l ≤ $m * $r) q(@Real.mul_neg_ge $l $r $m) + | .GT => + addThm q($m < 0 ∧ $l > $r → $m * $l < $m * $r) q(@Real.mul_neg_gt $l $r $m) + | _ => return none + | .ARITH_MULT_TANGENT => + let x : Q(Real) ← reconstructTerm pf.getArguments[0]! + let y : Q(Real) ← reconstructTerm pf.getArguments[1]! + let a : Q(Real) ← reconstructTerm pf.getArguments[2]! + let b : Q(Real) ← reconstructTerm pf.getArguments[3]! + if pf.getArguments[4]!.getIntegerValue == -1 then + addThm q(($x * $y ≤ $b * $x + $a * $y - $a * $b) = ($x ≤ $a ∧ $y ≥ $b ∨ $x ≥ $a ∧ $y ≤ $b)) q(@Real.mul_tangent_lower_eq $a $b $x $y) + else + addThm q(($x * $y ≥ $b * $x + $a * $y - $a * $b) = ($x ≤ $a ∧ $y ≤ $b ∨ $x ≥ $a ∧ $y ≥ $b)) q(@Real.mul_tangent_upper_eq $a $b $x $y) + | _ => return none + +end Smt.Reconstruct.Real diff --git a/Smt/Reconstruct/Real/Lemmas.lean b/Smt/Reconstruct/Real/Lemmas.lean new file mode 100644 index 00000000..0b907b55 --- /dev/null +++ b/Smt/Reconstruct/Real/Lemmas.lean @@ -0,0 +1,337 @@ +/- +Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tomaz Gomes Mascarenhas, Abdalrhman Mohamed +-/ + +import Mathlib.Data.Real.Archimedean + +private def uncurry {p₁ p₂ p₃ : Prop} : (p₁ → p₂ → p₃) → (p₁ ∧ p₂) → p₃ := by + intros h₁ h₂ + have ⟨ht₁, ht₂⟩ := h₂ + exact h₁ ht₁ ht₂ + +namespace Smt.Reconstruct.Real + +variable {a b c d : Real} + +theorem sum_ub₁ (h₁ : a < b) (h₂ : c < d) : a + c < b + d := by + have r₁ : a + c < a + d := add_lt_add_left h₂ a + have r₂ : a + d < b + d := add_lt_add_right h₁ d + exact lt_trans r₁ r₂ + +theorem sum_ub₂ (h₁ : a < b) (h₂ : c ≤ d) : a + c < b + d := by + have r₁ : a + c ≤ a + d := add_le_add_left h₂ a + have r₂ : a + d < b + d := add_lt_add_right h₁ d + exact lt_of_le_of_lt r₁ r₂ + +theorem sum_ub₃ (h₁ : a < b) (h₂ : c = d) : a + c < b + d := by + rewrite [h₂] + exact add_lt_add_right h₁ d + +theorem sum_ub₄ (h₁ : a ≤ b) (h₂ : c < d) : a + c < b + d := by + have r₁ : a + c < a + d := add_lt_add_left h₂ a + have r₂ : a + d ≤ b + d := add_le_add_right h₁ d + exact lt_of_lt_of_le r₁ r₂ + +theorem sum_ub₅ (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d := by + have r₁ : a + c ≤ a + d := add_le_add_left h₂ a + have r₂ : a + d ≤ b + d := add_le_add_right h₁ d + exact le_trans r₁ r₂ + +theorem sum_ub₆ (h₁ : a ≤ b) (h₂ : c = d) : a + c ≤ b + d := by + rewrite [h₂] + exact add_le_add_right h₁ d + +theorem sum_ub₇ (h₁ : a = b) (h₂ : c < d) : a + c < b + d := by + rewrite [h₁] + exact add_lt_add_left h₂ b + +theorem sum_ub₈ (h₁ : a = b) (h₂ : c ≤ d) : a + c ≤ b + d := by + rewrite [h₁] + exact add_le_add_left h₂ b + +theorem sum_ub₉ (h₁ : a = b) (h₂ : c = d) : a + c ≤ b + d := by + rewrite [h₁, h₂] + exact le_refl (b + d) + +theorem int_tight_ub {i : Int} (h : i < c) : i ≤ ⌊c⌋ := + Int.le_floor.mpr (le_of_lt h) + +theorem int_tight_lb {i : Int} (h : i > c) : i ≥ ⌈c⌉ := + Int.ceil_le.mpr (le_of_lt h) + +theorem trichotomy₁ (h₁ : a ≤ b) (h₂ : a ≠ b) : a < b := by + have tr := lt_trichotomy a b + exact Or.resolve_right (Or.resolve_right (or_assoc.mpr tr) (not_lt.mpr h₁)) h₂ + +theorem trichotomy₂ (h₁ : a ≤ b) (h₂ : a ≥ b) : a = b := by + have tr := lt_trichotomy a b + exact Or.resolve_right (Or.resolve_left tr (not_lt.mpr h₂)) (not_lt.mpr h₁) + +theorem trichotomy₃ (h₁ : a ≠ b) (h₂ : a ≤ b) : a < b := by + have tr := lt_trichotomy a b + exact Or.resolve_right (Or.resolve_right (or_assoc.mpr tr) (not_lt.mpr h₂)) h₁ + +theorem trichotomy₄ (h₁ : a ≠ b) (h₂ : a ≥ b) : a > b := by + have tr := lt_trichotomy a b + exact Or.resolve_left (Or.resolve_left tr (not_lt.mpr h₂)) h₁ + +theorem trichotomy₅ (h₁ : a ≥ b) (h₂ : a ≤ b) : a = b := by + have tr := lt_trichotomy a b + exact Or.resolve_right (Or.resolve_left tr (not_lt.mpr h₁)) (not_lt.mpr h₂) + +theorem trichotomy₆ (h₁ : a ≥ b) (h₂ : a ≠ b) : a > b := by + have tr := lt_trichotomy a b + exact Or.resolve_left (Or.resolve_left tr (not_lt.mpr h₁)) h₂ + +theorem lt_eq_sub_lt_zero : (a < b) = (a - b < 0) := by + apply propext + constructor + · apply sub_neg_of_lt + · apply lt_of_sub_neg + +theorem le_eq_sub_le_zero : (a ≤ b) = (a - b ≤ 0) := by + apply propext + constructor + · exact sub_nonpos_of_le + · exact le_of_sub_nonpos + +theorem eq_eq_sub_eq_zero : (a = b) = (a - b = 0) := by + simp only [sub_eq_zero] + +theorem ge_eq_sub_ge_zero : (a ≥ b) = (a - b ≥ 0) := by + simp only [ge_iff_le, eq_iff_iff] + constructor + · exact sub_nonneg_of_le + · exact le_of_sub_nonneg + +theorem gt_eq_sub_gt_zero : (a > b) = (a - b > 0) := by + simp only [gt_iff_lt, eq_iff_iff] + constructor + · exact sub_pos_of_lt + · exact lt_of_sub_pos + +theorem lt_of_sub_eq {c₁ c₂ : Real} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ < a₂) = (b₁ < b₂) := by + have {c x y : Real} (hc : c > 0) : (c * (x - y) < 0) = (x - y < 0) := by + rw (config := { occs := .pos [1] }) [← mul_zero c, mul_lt_mul_left hc] + rw [lt_eq_sub_lt_zero, @lt_eq_sub_lt_zero b₁, ← this hc₁, ← this hc₂, h] + +theorem le_of_sub_eq {c₁ c₂ : Real} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ ≤ a₂) = (b₁ ≤ b₂) := by + have {c x y : Real} (hc : c > 0) : (c * (x - y) ≤ 0) = (x - y ≤ 0) := by + rw (config := { occs := .pos [1] }) [← mul_zero c, mul_le_mul_left hc] + rw [le_eq_sub_le_zero, @le_eq_sub_le_zero b₁, ← this hc₁, ← this hc₂, h] + +theorem eq_of_sub_eq {c₁ c₂ : Real} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ = a₂) = (b₁ = b₂) := by + have {c x y : Real} (hc : c > 0) : (c * (x - y) = 0) = (x - y = 0) := by + rw (config := { occs := .pos [1] }) [← mul_zero c, mul_right_inj' (ne_of_gt hc)] + rw [@eq_eq_sub_eq_zero a₁, @eq_eq_sub_eq_zero b₁, ← this hc₁, ← this hc₂, h] + +theorem ge_of_sub_eq {c₁ c₂ : Real} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ ≥ a₂) = (b₁ ≥ b₂) := by + have {c x y : Real} (hc : c > 0) : (c * (x - y) ≥ 0) = (x - y ≥ 0) := by + rw (config := { occs := .pos [1] }) [← mul_zero c, ge_iff_le, mul_le_mul_left hc] + rw [ge_eq_sub_ge_zero, @ge_eq_sub_ge_zero b₁, ← this hc₁, ← this hc₂, h] + +theorem gt_of_sub_eq {c₁ c₂ : Real} (hc₁ : c₁ > 0) (hc₂ : c₂ > 0) (h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)) : (a₁ > a₂) = (b₁ > b₂) := by + have {c x y : Real} (hc : c > 0) : (c * (x - y) > 0) = (x - y > 0) := by + rw (config := { occs := .pos [1] }) [← mul_zero c, gt_iff_lt, mul_lt_mul_left hc] + rw [gt_eq_sub_gt_zero, @gt_eq_sub_gt_zero b₁, ← this hc₁, ← this hc₂, h] + +theorem mul_sign₁ (ha : a < 0) (hb : b < 0) : a * b > 0 := by + have h := mul_lt_mul_of_neg_right ha hb + simp at h + exact h + +theorem mul_sign₃ (ha : a < 0) (hb : b > 0) : a * b < 0 := by + have h := mul_lt_mul_of_pos_right ha hb + simp at h + exact h + +theorem mul_sign₄ (ha : a > 0) (hb : b < 0) : a * b < 0 := by + have h := mul_lt_mul_of_pos_left hb ha + simp at h + exact h + +theorem mul_sign₆ (ha : a > 0) (hb : b > 0) : a * b > 0 := by + have h := mul_lt_mul_of_pos_left hb ha + simp at h + exact h + +theorem mul_sign₀ (ha : a ≠ 0) : a * a > 0 := + match lt_trichotomy a 0 with + | .inl hn => mul_sign₁ hn hn + | .inr (.inl hz) => absurd hz ha + | .inr (.inr hp) => mul_sign₆ hp hp + +theorem mul_sign₂ (ha : a < 0) (hb : b ≠ 0) : a * b * b < 0 := + match lt_trichotomy b 0 with + | .inl hn => mul_sign₄ (mul_sign₁ ha hn) hn + | .inr (.inl hz) => absurd hz hb + | .inr (.inr hp) => mul_sign₃ (mul_sign₃ ha hp) hp + +theorem mul_sign₅ (ha : a > 0) (hb : b ≠ 0) : a * b * b > 0 := + match lt_trichotomy b 0 with + | .inl hn => mul_sign₁ (mul_sign₄ ha hn) hn + | .inr (.inl hz) => absurd hz hb + | .inr (.inr hp) => mul_sign₆ (mul_sign₆ ha hp) hp + +theorem mul_pos_lt (h : c > 0 ∧ a < b) : c * a < c * b := + mul_lt_mul_of_pos_left h.2 h.1 + +theorem mul_pos_le (h : c > 0 ∧ a ≤ b) : c * a ≤ c * b := + mul_le_mul_of_nonneg_left h.2 (le_of_lt h.1) + +theorem mul_pos_gt (h : c > 0 ∧ a > b) : c * a > c * b := + mul_pos_lt h + +theorem mul_pos_ge (h : c > 0 ∧ a ≥ b) : c * a ≥ c * b := + mul_pos_le h + +theorem mul_pos_eq (h : c > 0 ∧ a = b) : c * a = c * b := by + rw [h.2] + +theorem mul_neg_lt (h : c < 0 ∧ a < b) : c * a > c * b := + mul_lt_mul_of_neg_left h.2 h.1 + +theorem mul_neg_le (h : c < 0 ∧ a ≤ b) : c * a ≥ c * b := + mul_le_mul_of_nonpos_left h.2 (le_of_lt h.1) + +theorem mul_neg_gt (h : c < 0 ∧ a > b) : c * a < c * b := + mul_neg_lt h + +theorem mul_neg_ge (h : c < 0 ∧ a ≥ b) : c * a ≤ c * b := + mul_neg_le h + +theorem mul_neg_eq (h : c < 0 ∧ a = b) : c * a = c * b := by + rw [h.2] + +theorem mul_tangent_mp_lower (h : x * y ≤ b * x + a * y - a * b) + : x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b := by + match lt_trichotomy (x - a) 0, lt_trichotomy (y - b) 0 with + | Or.inl xaNeg, Or.inl ybNeg => + nlinarith + | Or.inl xaNeg, Or.inr (Or.inl ybZero) => + have xaNeg' := le_of_lt xaNeg + simp at xaNeg' + have ybZero' := ge_of_eq ybZero + simp at ybZero' + exact Or.inl (And.intro xaNeg' ybZero') + | Or.inl xaNeg, Or.inr (Or.inr ybPos) => + have xaNeg' := le_of_lt xaNeg + simp at xaNeg' + have ybPos' := le_of_lt ybPos + simp at ybPos' + exact Or.inl (And.intro xaNeg' ybPos') + | Or.inr (Or.inl xaZero), Or.inl ybNeg => + have xaZero' := ge_of_eq xaZero + simp at xaZero' + have ybNeg' := le_of_lt ybNeg + simp at ybNeg' + exact Or.inr (And.intro xaZero' ybNeg') + | Or.inr (Or.inl xaZero), Or.inr (Or.inl ybZero) => + have xaZero' := le_of_eq xaZero + simp at xaZero' + have ybZero' := ge_of_eq ybZero + simp at ybZero' + exact Or.inl (And.intro xaZero' ybZero') + | Or.inr (Or.inl xaZero), Or.inr (Or.inr ybPos) => + have xaZero' := le_of_eq xaZero + simp at xaZero' + have ybPos' := le_of_lt ybPos + simp at ybPos' + exact Or.inl (And.intro xaZero' ybPos') + | Or.inr (Or.inr xaPos), Or.inl ybNeg => + have xaPos' := le_of_lt xaPos + simp at xaPos' + have ybNeg' := le_of_lt ybNeg + simp at ybNeg' + exact Or.inr (And.intro xaPos' ybNeg') + | Or.inr (Or.inr xaPos), Or.inr (Or.inl ybZero) => + have xaPos' := le_of_lt xaPos + simp at xaPos' + have ybZero' := le_of_eq ybZero + simp at ybZero' + exact Or.inr (And.intro xaPos' ybZero') + | Or.inr (Or.inr xaPos), Or.inr (Or.inr ybPos) => + nlinarith + +theorem mul_tangent_mpr_lower (h : x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b) + : x * y ≤ b * x + a * y - a * b := by + match h with + | Or.inl (And.intro h₁ h₂) => nlinarith + | Or.inr (And.intro h₁ h₂) => nlinarith + +theorem mul_tangent_lower : + x * y ≤ b * x + a * y - a * b ↔ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b := + ⟨mul_tangent_mp_lower, mul_tangent_mpr_lower⟩ + +theorem mul_tangent_lower_eq + : (x * y ≤ b * x + a * y - a * b) = (x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b) := + propext (mul_tangent_lower) + +theorem mul_tangent_mp_upper (h : x * y ≥ b * x + a * y - a * b) + : x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b := by + match lt_trichotomy (x - a) 0, lt_trichotomy (y - b) 0 with + | Or.inl xaNeg, Or.inl ybNeg => + have xaNeg' := le_of_lt xaNeg + simp at xaNeg' + have ybNeg' := le_of_lt ybNeg + simp at ybNeg' + exact Or.inl (And.intro xaNeg' ybNeg') + | Or.inl xaNeg, Or.inr (Or.inl ybZero) => + have xaNeg' := le_of_lt xaNeg + simp at xaNeg' + have ybZero' := le_of_eq ybZero + simp at ybZero' + exact Or.inl (And.intro xaNeg' ybZero') + | Or.inl xaNeg, Or.inr (Or.inr ybPos) => + nlinarith + | Or.inr (Or.inl xaZero), Or.inl ybNeg => + have xaZero' := le_of_eq xaZero + simp at xaZero' + have ybNeg' := le_of_lt ybNeg + simp at ybNeg' + exact Or.inl (And.intro xaZero' ybNeg') + | Or.inr (Or.inl xaZero), Or.inr (Or.inl ybZero) => + have xaZero' := le_of_eq xaZero + simp at xaZero' + have ybZero' := le_of_eq ybZero + simp at ybZero' + exact Or.inl (And.intro xaZero' ybZero') + | Or.inr (Or.inl xaZero), Or.inr (Or.inr ybPos) => + have xaZero' := ge_of_eq xaZero + simp at xaZero' + have ybPos' := le_of_lt ybPos + simp at ybPos' + exact Or.inr (And.intro xaZero' ybPos') + | Or.inr (Or.inr xaPos), Or.inl ybNeg => + nlinarith + | Or.inr (Or.inr xaPos), Or.inr (Or.inl ybZero) => + have xaPos' := le_of_lt xaPos + simp at xaPos' + have ybZero' := ge_of_eq ybZero + simp at ybZero' + exact Or.inr (And.intro xaPos' ybZero') + | Or.inr (Or.inr xaPos), Or.inr (Or.inr ybPos) => + have xaPos' := le_of_lt xaPos + simp at xaPos' + have ybPos' := le_of_lt ybPos + simp at ybPos' + exact Or.inr (And.intro xaPos' ybPos') + +theorem mul_tangent_mpr_upper (h : x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b) + : x * y ≥ b * x + a * y - a * b := by + match h with + | Or.inl (And.intro h₁ h₂) => nlinarith + | Or.inr (And.intro h₁ h₂) => nlinarith + +theorem mul_tangent_upper + : x * y ≥ b * x + a * y - a * b ↔ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b := + ⟨mul_tangent_mp_upper, mul_tangent_mpr_upper⟩ + +theorem mul_tangent_upper_eq + : (x * y ≥ b * x + a * y - a * b) = (x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b) := + propext (mul_tangent_upper) + +end Smt.Reconstruct.Real diff --git a/Smt/Reconstruct/Real/Polynorm.lean b/Smt/Reconstruct/Real/Polynorm.lean new file mode 100644 index 00000000..53624d9a --- /dev/null +++ b/Smt/Reconstruct/Real/Polynorm.lean @@ -0,0 +1,79 @@ +/- +Copyright (c) 2021-2024 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abdalrhman Mohamed +-/ + +import Mathlib.Data.Real.Basic + +namespace Smt.Reconstruct.Real + +open Lean + +open Lean Mathlib.Tactic.RingNF in +/-- Use `arithPolyNormCore` to rewrite the main goal. -/ +def polyNormCore (mv : MVarId) : MetaM (Option MVarId) := mv.withContext do + let tgt ← instantiateMVars (← mv.getType) + let s ← IO.mkRef {} + let r ← M.run s {} <| rewrite tgt + if r.expr.consumeMData.isConstOf ``True then + mv.assign (← Meta.mkOfEqTrue (← r.getProof)) + return none + else + Meta.applySimpResultToTarget mv tgt r + +def traceArithPolyNorm (r : Except Exception Unit) : MetaM MessageData := + return match r with + | .ok _ => m!"{checkEmoji}" + | _ => m!"{bombEmoji}" + +/-- Use `arithPolyNorm` to rewrite the main goal. -/ +def polyNorm (mv : MVarId) : MetaM Unit := withTraceNode `smt.reconstruct.arithPolyNorm traceArithPolyNorm do + mv.withContext do + if let .some mv ← polyNormCore mv then + throwError "[arithPolyNorm]: could not prove {← mv.getType}" + +def traceArithNormNum (r : Except Exception Unit) : MetaM MessageData := + return match r with + | .ok _ => m!"{checkEmoji}" + | _ => m!"{bombEmoji}" + +open Mathlib.Meta.NormNum in +def normNum (mv : MVarId) : MetaM Unit := withTraceNode `smt.reconstruct.normNum traceArithNormNum do + if let some (_, mv) ← normNumAt mv {} #[] true false then + throwError "[norm_num]: could not prove {← mv.getType}" + +open Qq in +partial def findConst (e : Q(Real)) : MetaM Q(Real) := do + match e with + | ~q($a * $b) => findConst b + | ~q($a + $b) => findConst b + | ~q($a - $b) => findConst b + | ~q(-$a) => findConst a + | _ => + if e.hasFVar || e.hasLooseBVars then + return q(1) + else if e.getUsedConstants.contains ``Neg.neg then + let e : Q(Real) := e + match e with + | ~q((-$a) / $b) => return q($a / $b) + | _ => return e + else + return e + +namespace Tactic + +syntax (name := polyNorm) "poly_norm" : tactic + +open Lean.Elab Tactic in +@[tactic polyNorm] def evalPolyNorm : Tactic := fun _ => + withMainContext do + let mv ← Tactic.getMainGoal + Real.polyNorm mv + replaceMainGoal [] + +end Smt.Reconstruct.Real.Tactic + +example (x y z : Real) : 1 * (x + y) * z / 4 = 1/(2 * 2) * (z * y + x * z) := by + poly_norm diff --git a/Smt/Reconstruct/Real/Rewrites.lean b/Smt/Reconstruct/Real/Rewrites.lean new file mode 100644 index 00000000..102b8674 --- /dev/null +++ b/Smt/Reconstruct/Real/Rewrites.lean @@ -0,0 +1,95 @@ +/- +Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their +institutional affiliations. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abdalrhman Mohamed +-/ + +import Mathlib.Data.Real.Basic + +namespace Smt.Reconstruct.Real.Rewrite + +open Function + +theorem div_by_const_elim_1_pos {t : Real} : t / 1 = t * 1 := + div_eq_mul_one_div t 1 ▸ Eq.symm (@one_div_one Real _) ▸ rfl +theorem div_by_const_elim_1_neg {t : Real} : t / -1 = t * -1 := + div_eq_mul_one_div t (-1) ▸ div_neg (1 : Real) ▸ Eq.symm (@one_div_one Real _) ▸ rfl +theorem div_by_const_elim_num_pos {t c : Real} : t / c = t * (1 / c) := + div_eq_mul_one_div t c +theorem div_by_const_elim_num_neg {t c : Real} : t / -c = t * (-1 / c) := + div_eq_mul_one_div t (-c) ▸ div_neg (1 : Real) ▸ neg_div c 1 ▸ rfl +theorem div_by_const_elim_real_pos {t c₁ c₂ : Real} : t / (c₁ / c₂) = t * (c₂ / c₁) := + div_eq_mul_one_div t (c₁ / c₂) ▸ one_div_div c₁ c₂ ▸ rfl +theorem div_by_const_elim_real_neg {t c₁ c₂ : Real} : t / (-c₁ / c₂) = t * (-c₂ / c₁) := + div_eq_mul_one_div t (-c₁ / c₂) ▸ one_div_div (-c₁) c₂ ▸ div_neg c₂ ▸ neg_div c₁ c₂ ▸ rfl + +-- https://github.com/cvc5/cvc5/blob/proof-new/src/theory/arith/rewrites + +variable {t ts x xs : Real} + +theorem plus_zero : ts + 0 + ss = ts + ss := + (add_zero ts).symm ▸ rfl + +theorem mul_one : ts * 1 * ss = ts * ss := + (_root_.mul_one ts).symm ▸ rfl +theorem mul_zero : ts * 0 * ss = 0 := + (MulZeroClass.mul_zero ts).symm ▸ (zero_mul ss).symm ▸ rfl + +theorem div_total : s ≠ 0 → t / s = t / s := + const _ rfl + +theorem neg_neg_one : -1 * (-1 * t) = t := + neg_mul _ t ▸ (one_mul t).symm ▸ neg_mul_neg _ t ▸ (one_mul t).symm ▸ rfl + +-- Eliminations + +theorem elim_uminus : -t = -1 * t := + neg_eq_neg_one_mul t ▸ rfl +theorem elim_minus : t - s = t + -1 * s := + neg_eq_neg_one_mul s ▸ sub_eq_add_neg _ s ▸ rfl +theorem elim_gt : (t > s) = ¬(t ≤ s) := + propext not_le.symm +theorem elim_lt : (t < s) = ¬(t ≥ s) := + propext not_le.symm +theorem elim_leq : (t ≤ s) = (s ≥ t) := + propext ge_iff_le + +theorem geq_norm1 : (t ≥ s) = (t - s ≥ 0) := + propext ⟨sub_nonneg_of_le, le_of_sub_nonneg⟩ + +theorem geq_norm2 : (t ≥ s) = (-t ≤ -s) := + propext (Iff.symm neg_le_neg_iff) + +theorem refl_leq : (t ≤ t) = True := + propext ⟨const _ trivial, const _ (le_refl t)⟩ +theorem refl_lt : (t < t) = False := + propext ⟨(lt_irrefl t), False.elim⟩ +theorem refl_geq : (t ≥ t) = True := + propext ⟨const _ trivial, const _ (le_refl t)⟩ +theorem refl_gt : (t > t) = False := + propext ⟨(lt_irrefl t), False.elim⟩ + +theorem eq_elim : (t = s) = (t ≥ s ∧ t ≤ s) := + propext (Iff.symm antisymm_iff) + +theorem plus_flatten : xs + (w + ys) + zs = xs + w + ys + zs := + add_assoc xs w ys ▸ rfl + +theorem mult_flatten : xs * (w * ys) * zs = xs * w * ys * zs := + mul_assoc xs w ys ▸ rfl + +theorem mult_dist : x * (y + z + ws) = x * y + x * (z + ws) := + add_assoc y z ws ▸ mul_add x y (z + ws) ▸ rfl + +theorem plus_cancel1 : ts + x + ss + (-1 * x) + rs = ts + ss + rs := + neg_eq_neg_one_mul x ▸ add_assoc ts x ss ▸ add_assoc ts (x + ss) (-x) ▸ + add_comm x ss ▸ (add_neg_cancel_right ss x).symm ▸ rfl +theorem plus_cancel2 : ts + (-1 * x) + ss + x + rs = ts + ss + rs := + neg_eq_neg_one_mul x ▸ add_assoc ts (-x) ss ▸ add_assoc ts (-x + ss) x ▸ + add_comm (-x) ss ▸ (neg_add_cancel_right ss x).symm ▸ rfl + +theorem abs_elim : (if x < 0 then -x else x) = if x < 0 then -x else x := + rfl + +end Smt.Reconstruct.Real.Rewrite diff --git a/Test/BitVec/Shift.expected b/Test/BitVec/Shift.expected index e73ada1d..9d781ffb 100644 --- a/Test/BitVec/Shift.expected +++ b/Test/BitVec/Shift.expected @@ -1,8 +1,8 @@ goal: x ++ y = zeroExtend 4 x <<< 2#2 ||| zeroExtend 4 y query: -(declare-const x (_ BitVec 2)) (declare-const y (_ BitVec 2)) +(declare-const x (_ BitVec 2)) (assert (distinct (concat x y) (bvor (bvshl ((_ zero_extend 2) x) #b10) ((_ zero_extend 2) y)))) (check-sat) Test/BitVec/Shift.lean:5:8: warning: declaration uses 'sorry' diff --git a/Test/BitVec/XorComm.expected b/Test/BitVec/XorComm.expected index 9d49feaf..bb102ca6 100644 --- a/Test/BitVec/XorComm.expected +++ b/Test/BitVec/XorComm.expected @@ -1,16 +1,16 @@ goal: x ^^^ y = y ^^^ x query: -(declare-const x (_ BitVec 2)) (declare-const y (_ BitVec 2)) +(declare-const x (_ BitVec 2)) (assert (distinct (bvxor x y) (bvxor y x))) (check-sat) Test/BitVec/XorComm.lean:3:8: warning: declaration uses 'sorry' goal: x ^^^ y = y ^^^ x query: -(declare-const y (_ BitVec 8)) (declare-const x (_ BitVec 8)) +(declare-const y (_ BitVec 8)) (assert (distinct (bvxor x y) (bvxor y x))) (check-sat) Test/BitVec/XorComm.lean:7:8: warning: declaration uses 'sorry' diff --git a/Test/Bool/Assoc.expected b/Test/Bool/Assoc.expected index 977c0696..1934db2a 100644 --- a/Test/Bool/Assoc.expected +++ b/Test/Bool/Assoc.expected @@ -1,10 +1,10 @@ goal: (f p (f q r) == f (f p q) r) = true query: -(declare-fun f (Bool Bool) Bool) (declare-const p Bool) -(declare-const r Bool) (declare-const q Bool) +(declare-fun f (Bool Bool) Bool) +(declare-const r Bool) (assert (distinct (= (f p (f q r)) (f (f p q) r)) true)) (check-sat) Test/Bool/Assoc.lean:3:8: warning: declaration uses 'sorry' diff --git a/Test/Bool/Comm.expected b/Test/Bool/Comm.expected index 3260a0a6..368f1f85 100644 --- a/Test/Bool/Comm.expected +++ b/Test/Bool/Comm.expected @@ -1,9 +1,9 @@ goal: (f p q == f q p) = true query: +(declare-const p Bool) (declare-const q Bool) (declare-fun f (Bool Bool) Bool) -(declare-const p Bool) (assert (distinct (= (f p q) (f q p)) true)) (check-sat) Test/Bool/Comm.lean:3:0: warning: declaration uses 'sorry' diff --git a/Test/Bool/Cong.expected b/Test/Bool/Cong.expected index fa6550a3..f97fc612 100644 --- a/Test/Bool/Cong.expected +++ b/Test/Bool/Cong.expected @@ -1,8 +1,8 @@ goal: (p == q) = true → (f p == f q) = true query: -(declare-fun f (Bool) Bool) (declare-const p Bool) +(declare-fun f (Bool) Bool) (declare-const q Bool) (assert (not (=> (= (= p q) true) (= (= (f p) (f q)) true)))) (check-sat) diff --git a/Test/Bool/Conjunction.expected b/Test/Bool/Conjunction.expected index 5ec6f87c..319cf0e0 100644 --- a/Test/Bool/Conjunction.expected +++ b/Test/Bool/Conjunction.expected @@ -1,7 +1,7 @@ goal: p = true → q = true → (p && q) = true query: -(declare-const q Bool) (declare-const p Bool) +(declare-const q Bool) (assert (not (=> (= p true) (=> (= q true) (= (and p q) true))))) (check-sat) diff --git a/Test/Bool/DisjunctiveSyllogism.expected b/Test/Bool/DisjunctiveSyllogism.expected index c0b891a9..7044302b 100644 --- a/Test/Bool/DisjunctiveSyllogism.expected +++ b/Test/Bool/DisjunctiveSyllogism.expected @@ -1,7 +1,7 @@ goal: (p || q) = true → (!p) = true → q = true query: -(declare-const q Bool) (declare-const p Bool) +(declare-const q Bool) (assert (not (=> (= (or p q) true) (=> (= (not p) true) (= q true))))) (check-sat) diff --git a/Test/Bool/PropExt.expected b/Test/Bool/PropExt.expected index 0869af7c..1b077583 100644 --- a/Test/Bool/PropExt.expected +++ b/Test/Bool/PropExt.expected @@ -1,7 +1,7 @@ goal: (p = true) = (q = true) → (p == q) = true query: -(declare-const q Bool) (declare-const p Bool) +(declare-const q Bool) (assert (not (=> (= (= p true) (= q true)) (= (= p q) true)))) (check-sat) diff --git a/Test/Bool/Resolution.expected b/Test/Bool/Resolution.expected index c1604be8..9efcedae 100644 --- a/Test/Bool/Resolution.expected +++ b/Test/Bool/Resolution.expected @@ -2,7 +2,7 @@ goal: (p || q) = true → (!p || r) = true → (q || r) = true query: (declare-const p Bool) -(declare-const r Bool) (declare-const q Bool) +(declare-const r Bool) (assert (not (=> (= (or p q) true) (=> (= (or (not p) r) true) (= (or q r) true))))) (check-sat) diff --git a/Test/Bool/Trans.expected b/Test/Bool/Trans.expected index 10ceea0a..07da80d1 100644 --- a/Test/Bool/Trans.expected +++ b/Test/Bool/Trans.expected @@ -1,8 +1,8 @@ goal: (p == q) = true → (q == r) = true → (p == r) = true query: +(declare-const q Bool) (declare-const p Bool) (declare-const r Bool) -(declare-const q Bool) (assert (not (=> (= (= p q) true) (=> (= (= q r) true) (= (= p r) true))))) (check-sat) diff --git a/Test/Int/Arith.expected b/Test/Int/Arith.expected index b4f36eb3..6788251b 100644 --- a/Test/Int/Arith.expected +++ b/Test/Int/Arith.expected @@ -1 +1,82 @@ -Test/Int/Arith.lean:4:2: error: [norm_num]: could not prove False +Test/Int/Arith.lean:3:47: error: unsolved goals +n m : Int +h : 0 < m +⊢ 0 < m → + ¬n % m < m → + ¬(m + -1 * if m = 0 then (fun x => x % 0) n else n % m) ≥ 1 → + n = (if m = 0 then (fun x => x % 0) n else n % m) + m * (n / m) → + m + -1 * n + m * (n / m) ≥ 1 → n % m = if m = 0 then (fun x => x % 0) n else n % m + +n m : Int +h : 0 < m +⊢ 0 < m → + ¬n % m < m → + n = (if m = 0 then (fun x => x % 0) n else n % m) + m * (n / m) → + ¬(m + -1 * if m = 0 then (fun x => x % 0) n else n % m) ≥ 1 → + m + -1 * n + m * (n / m) ≥ 1 → + m + -1 * n + m * (n / m) ≥ 1 → n % m = if m = 0 then (fun x => x % 0) n else n % m + +n m : Int +h : 0 < m +⊢ 0 < m → ¬n % m < m → n % m = n - m * (n / m) + +n m : Int +h : 0 < m +⊢ 0 < m → + ¬n % m < m → (m > 0 → m * (n / m) ≤ n ∧ n < m * (n / m + 1)) ∧ (m < 0 → m * (n / m) ≤ n ∧ n < m * (n / m + -1)) + +n m : Int +h : 0 < m +⊢ 0 < m → ¬n % m < m → n % m = if m = 0 then (fun x => x % 0) n else n % m +Test/Int/Arith.lean:3:0: error: application type mismatch + Smt.Reconstruct.Int.PolyNorm.Expr.denote_eq_from_toPolynomial_eq + (Eq.refl + ((Smt.Reconstruct.Int.PolyNorm.Expr.val (OfNat.ofNat 1)).mul + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 0).sub + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 1).add + ((Smt.Reconstruct.Int.PolyNorm.Expr.val 1).neg.mul + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 2).mul + (Smt.Reconstruct.Int.PolyNorm.Expr.var 3)))))).toPolynomial) +argument has type + ((Smt.Reconstruct.Int.PolyNorm.Expr.val (OfNat.ofNat 1)).mul + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 0).sub + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 1).add + ((Smt.Reconstruct.Int.PolyNorm.Expr.val 1).neg.mul + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 2).mul + (Smt.Reconstruct.Int.PolyNorm.Expr.var 3)))))).toPolynomial = + ((Smt.Reconstruct.Int.PolyNorm.Expr.val (OfNat.ofNat 1)).mul + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 0).sub + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 1).add + ((Smt.Reconstruct.Int.PolyNorm.Expr.val 1).neg.mul + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 2).mul (Smt.Reconstruct.Int.PolyNorm.Expr.var 3)))))).toPolynomial +but function has type + ((Smt.Reconstruct.Int.PolyNorm.Expr.val (OfNat.ofNat 1)).mul + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 0).sub + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 1).add + ((Smt.Reconstruct.Int.PolyNorm.Expr.val 1).neg.mul + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 2).mul + (Smt.Reconstruct.Int.PolyNorm.Expr.var 3)))))).toPolynomial = + ((Smt.Reconstruct.Int.PolyNorm.Expr.val (OfNat.ofNat 1)).mul + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 1).sub + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 0).add + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 2).mul + (Smt.Reconstruct.Int.PolyNorm.Expr.var 3))))).toPolynomial → + Smt.Reconstruct.Int.PolyNorm.Expr.denote + (fun v => + if h : v < ((((#[].push (if m = 0 then (fun x => x % 0) n else n % m)).push n).push m).push (n / m)).size then + ((((#[].push (if m = 0 then (fun x => x % 0) n else n % m)).push n).push m).push (n / m))[v] + else 0) + ((Smt.Reconstruct.Int.PolyNorm.Expr.val (OfNat.ofNat 1)).mul + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 0).sub + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 1).add + ((Smt.Reconstruct.Int.PolyNorm.Expr.val 1).neg.mul + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 2).mul (Smt.Reconstruct.Int.PolyNorm.Expr.var 3)))))) = + Smt.Reconstruct.Int.PolyNorm.Expr.denote + (fun v => + if h : v < ((((#[].push (if m = 0 then (fun x => x % 0) n else n % m)).push n).push m).push (n / m)).size then + ((((#[].push (if m = 0 then (fun x => x % 0) n else n % m)).push n).push m).push (n / m))[v] + else 0) + ((Smt.Reconstruct.Int.PolyNorm.Expr.val (OfNat.ofNat 1)).mul + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 1).sub + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 0).add + ((Smt.Reconstruct.Int.PolyNorm.Expr.var 2).mul (Smt.Reconstruct.Int.PolyNorm.Expr.var 3))))) diff --git a/Test/Int/Binders.expected b/Test/Int/Binders.expected index 7f2fd0ed..4169c399 100644 --- a/Test/Int/Binders.expected +++ b/Test/Int/Binders.expected @@ -2,8 +2,8 @@ goal: curryAdd a b = curryAdd b a query: (define-fun curryAdd ((a._@.Test.Int.Binders._hyg.3 Int) (a._@.Test.Int.Binders._hyg.5 Int)) Int (+ a._@.Test.Int.Binders._hyg.3 a._@.Test.Int.Binders._hyg.5)) -(declare-const a Int) (declare-const b Int) +(declare-const a Int) (assert (distinct (curryAdd a b) (curryAdd b a))) (check-sat) Test/Int/Binders.lean:5:0: warning: declaration uses 'sorry' @@ -11,8 +11,8 @@ goal: partCurryAdd a b = partCurryAdd b a query: (define-fun partCurryAdd ((a Int) (a._@.Test.Int.Binders._hyg.33 Int)) Int (+ a a._@.Test.Int.Binders._hyg.33)) -(declare-const a Int) (declare-const b Int) +(declare-const a Int) (assert (distinct (partCurryAdd a b) (partCurryAdd b a))) (check-sat) Test/Int/Binders.lean:11:0: warning: declaration uses 'sorry' @@ -20,8 +20,8 @@ goal: partCurryAdd' a b = partCurryAdd' b a query: (define-fun |partCurryAdd'| ((a Int) (a._@.Init.Prelude._hyg.2347 Int)) Int (+ a a._@.Init.Prelude._hyg.2347)) -(declare-const a Int) (declare-const b Int) +(declare-const a Int) (assert (distinct (+ a b) (+ b a))) (check-sat) Test/Int/Binders.lean:15:0: warning: declaration uses 'sorry' @@ -29,8 +29,8 @@ goal: mismatchNamesAdd a b = mismatchNamesAdd b a query: (define-fun mismatchNamesAdd ((a Int) (b Int)) Int (+ a b)) -(declare-const b Int) (declare-const a Int) +(declare-const b Int) (assert (distinct (mismatchNamesAdd a b) (mismatchNamesAdd b a))) (check-sat) Test/Int/Binders.lean:25:0: warning: declaration uses 'sorry' diff --git a/Test/Int/Cong.expected b/Test/Int/Cong.expected index e472e520..e69de29b 100644 --- a/Test/Int/Cong.expected +++ b/Test/Int/Cong.expected @@ -1,8 +0,0 @@ -goal: x = y → f x = f y - -query: -(declare-fun f (Int) Int) -(declare-const x Int) -(declare-const y Int) -(assert (not (=> (= x y) (= (f x) (f y))))) -(check-sat) diff --git a/Test/Int/Cong.lean b/Test/Int/Cong.lean index 6c7108c7..cccdbcde 100644 --- a/Test/Int/Cong.lean +++ b/Test/Int/Cong.lean @@ -1,5 +1,4 @@ import Smt theorem cong (x y : Int) (f : Int → Int) : x = y → f x = f y := by - smt_show - simp_all + smt diff --git a/Test/Int/DefineSort.expected b/Test/Int/DefineSort.expected index 9c64cdd6..15e6649e 100644 --- a/Test/Int/DefineSort.expected +++ b/Test/Int/DefineSort.expected @@ -3,8 +3,8 @@ goal: a.add b = b.add a query: (define-sort MyInt () Int) (define-fun MyInt.add ((a MyInt) (b MyInt)) MyInt (+ a b)) -(declare-const b MyInt) (declare-const a MyInt) +(declare-const b MyInt) (assert (distinct (MyInt.add a b) (MyInt.add b a))) (check-sat) Test/Int/DefineSort.lean:6:0: warning: declaration uses 'sorry' diff --git a/Test/Int/Dvd.expected b/Test/Int/Dvd.expected index 4311b71b..3eee65e4 100644 --- a/Test/Int/Dvd.expected +++ b/Test/Int/Dvd.expected @@ -3,8 +3,8 @@ goal: dvd a c = true query: (declare-fun dvd (Int Int) Bool) (assert (forall ((x Int)) (forall ((y Int)) (forall ((z Int)) (=> (= (dvd x y) true) (=> (= (dvd y z) true) (= (dvd x z) true))))))) -(declare-const c Int) (declare-const b Int) +(declare-const c Int) (assert (= (dvd b c) true)) (declare-const a Int) (assert (= (dvd a b) true)) @@ -15,8 +15,8 @@ goal: dvd c e = true query: (declare-fun dvd (Int Int) Bool) (assert (forall ((x Int)) (forall ((y Int)) (forall ((z Int)) (=> (= (dvd x y) true) (=> (= (dvd y z) true) (= (dvd x z) true))))))) -(declare-const e Int) (declare-const d Int) +(declare-const e Int) (assert (= (dvd d e) true)) (declare-const c Int) (assert (= (dvd c d) true)) diff --git a/Test/Int/DvdTimeout.expected b/Test/Int/DvdTimeout.expected index 6987110f..a78b96be 100644 --- a/Test/Int/DvdTimeout.expected +++ b/Test/Int/DvdTimeout.expected @@ -1,9 +1,9 @@ goal: dvd a (b + c + d) = true query: -(declare-const d Int) (declare-fun dvd (Int Int) Bool) (declare-const a Int) +(declare-const d Int) (assert (= (dvd a d) true)) (declare-const c Int) (assert (= (dvd a c) true)) @@ -13,8 +13,8 @@ query: (assert (distinct (dvd a (+ (+ b c) d)) true)) (check-sat) Test/Int/DvdTimeout.lean:12:25: error: unsolved goals -a b c d : ℤ -dvdax : ∀ (x y z : ℤ), dvd x y = true → dvd x z = true → dvd x (y + z) = true +a b c d : Int +dvdax : ∀ (x y z : Int), dvd x y = true → dvd x z = true → dvd x (y + z) = true h1 : dvd a b = true h2 : dvd a c = true h3 : dvd a d = true diff --git a/Test/Int/Let.expected b/Test/Int/Let.expected index 41d47ec4..e945919e 100644 --- a/Test/Int/Let.expected +++ b/Test/Int/Let.expected @@ -1,29 +1,3 @@ -goal: let y := 10; -f y = 10 - -query: -(declare-fun f (Int) Int) -(assert (= (f 10) 10)) -(assert (distinct (f 10) 10)) -(check-sat) -Test/Int/Let.lean:5:51: error: unsolved goals -f : ℤ → ℤ -h : f 10 = 10 -⊢ let y := 10; - f y = 10 -goal: f 10 = 10 - -query: -(declare-fun f (Int) Int) -(assert (= (f 10) 10)) -(assert (distinct (f 10) 10)) -(check-sat) -Test/Int/Let.lean:8:51: error: unsolved goals -f : ℤ → ℤ -h : - let y := 10; - f y = 10 -⊢ f 10 = 10 goal: f z = z query: @@ -45,7 +19,7 @@ goal: z 3 = 10 query: (declare-fun f (Int) Int) -(define-fun z ((x._@.Test.Int.Let._hyg.293 Int)) Int (f 10)) +(define-fun z ((x._@.Test.Int.Let._hyg.295 Int)) Int (f 10)) (assert (= (f 10) 10)) (assert (distinct (z 3) 10)) (check-sat) diff --git a/Test/Int/Let.lean b/Test/Int/Let.lean index ffc32dda..24a6d802 100644 --- a/Test/Int/Let.lean +++ b/Test/Int/Let.lean @@ -3,10 +3,10 @@ import Smt variable (f : Int → Int) example (h : f 10 = 10) : let y := 10; f y = 10 := by - smt_show [h] + smt [h] example (h : let y := 10; f y = 10) : f 10 = 10 := by - smt_show [h] + smt [h] example (h : f 10 = 10) : f 10 = 10 := by let z : Int := 10 diff --git a/Test/Int/Neg.expected b/Test/Int/Neg.expected index a21133d4..e69de29b 100644 --- a/Test/Int/Neg.expected +++ b/Test/Int/Neg.expected @@ -1,9 +0,0 @@ -goal: - -x = x - -query: -(declare-const x Int) -(assert (distinct (- (- x)) x)) -(check-sat) -Test/Int/Neg.lean:3:8: warning: declaration uses 'sorry' -Test/Int/Neg.lean:4:11: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice -note: this linter can be disabled with `set_option linter.unnecessarySeqFocus false` diff --git a/Test/Int/Neg.lean b/Test/Int/Neg.lean index 26a0429a..0a421b65 100644 --- a/Test/Int/Neg.lean +++ b/Test/Int/Neg.lean @@ -1,4 +1,4 @@ import Smt theorem neg (x : Int) : - -x = x := by - smt_show <;> sorry + smt diff --git a/Test/Nat/Cong.expected b/Test/Nat/Cong.expected index 7fe03f72..e3c5499f 100644 --- a/Test/Nat/Cong.expected +++ b/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.1827 Nat)) (=> (>= _uniq.1827 0) (>= (f _uniq.1827) 0)))) +(assert (forall ((_uniq.1521 Nat)) (=> (>= _uniq.1521 0) (>= (f _uniq.1521) 0)))) (declare-const x Nat) (assert (>= x 0)) (declare-const y Nat) diff --git a/Test/Nat/Forall'.expected b/Test/Nat/Forall'.expected index 5e96a978..85ab0c11 100644 --- a/Test/Nat/Forall'.expected +++ b/Test/Nat/Forall'.expected @@ -1,4 +1,4 @@ -goal: ∀ (x : ℕ), x ≥ 0 +goal: ∀ (x : Nat), x ≥ 0 query: (assert (not (forall ((x Int)) (=> (>= x 0) (<= 0 x))))) diff --git a/Test/Nat/Max.expected b/Test/Nat/Max.expected index c0cab591..266ef325 100644 --- a/Test/Nat/Max.expected +++ b/Test/Nat/Max.expected @@ -2,12 +2,12 @@ goal: x ≤ x.max' y ∧ y ≤ x.max' y query: (define-sort Nat () Int) +(declare-const x Nat) +(assert (>= x 0)) (declare-fun |Nat.max'| (Nat Nat) Nat) -(assert (forall ((_uniq.2660 Nat)) (=> (>= _uniq.2660 0) (forall ((_uniq.2661 Nat)) (=> (>= _uniq.2661 0) (>= (|Nat.max'| _uniq.2660 _uniq.2661) 0)))))) +(assert (forall ((_uniq.2212 Nat)) (=> (>= _uniq.2212 0) (forall ((_uniq.2213 Nat)) (=> (>= _uniq.2213 0) (>= (|Nat.max'| _uniq.2212 _uniq.2213) 0)))))) (declare-const y Nat) (assert (>= y 0)) -(declare-const x Nat) -(assert (>= x 0)) (assert (not (and (<= x (|Nat.max'| x y)) (<= y (|Nat.max'| x y))))) (check-sat) goal: x ≤ x.max' y ∧ y ≤ x.max' y @@ -15,10 +15,10 @@ goal: x ≤ x.max' y ∧ y ≤ x.max' y query: (define-sort Nat () Int) (define-fun |Nat.max'| ((x Nat) (y Nat)) Nat (ite (<= x y) y x)) -(assert (forall ((_uniq.6194 Nat)) (=> (>= _uniq.6194 0) (forall ((_uniq.6195 Nat)) (=> (>= _uniq.6195 0) (>= (|Nat.max'| _uniq.6194 _uniq.6195) 0)))))) -(declare-const y Nat) -(assert (>= y 0)) +(assert (forall ((_uniq.4701 Nat)) (=> (>= _uniq.4701 0) (forall ((_uniq.4702 Nat)) (=> (>= _uniq.4702 0) (>= (|Nat.max'| _uniq.4701 _uniq.4702) 0)))))) (declare-const x Nat) (assert (>= x 0)) +(declare-const y Nat) +(assert (>= y 0)) (assert (not (and (<= x (|Nat.max'| x y)) (<= y (|Nat.max'| x y))))) (check-sat) diff --git a/Test/Nat/NeqZero.expected b/Test/Nat/NeqZero.expected index f1a1e32e..7b40c2ff 100644 --- a/Test/Nat/NeqZero.expected +++ b/Test/Nat/NeqZero.expected @@ -1,10 +1,10 @@ -goal: ∀ (x : ℕ), x ≠ 0 +goal: ∀ (x : Nat), x ≠ 0 query: (assert (not (forall ((x Int)) (=> (>= x 0) (distinct x 0))))) (check-sat) Test/Nat/NeqZero.lean:3:8: warning: declaration uses 'sorry' -goal: ∀ (x : ℕ), x + 1 ≠ 0 +goal: ∀ (x : Nat), x + 1 ≠ 0 query: (assert (not (forall ((x Int)) (=> (>= x 0) (distinct (+ x 1) 0))))) diff --git a/Test/Nat/Sum'.expected b/Test/Nat/Sum'.expected index 9e1da1db..c52d77fa 100644 --- a/Test/Nat/Sum'.expected +++ b/Test/Nat/Sum'.expected @@ -1,4 +1,9 @@ -Test/Nat/Sum'.lean:7:12: error: [arithPolyNorm]: could not prove 0 + sum 0 = sum 0 +Test/Nat/Sum'.lean:7:12: error: tactic 'assumption' failed +case zero.a +_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 goal: sum (n + 1) = (n + 1) * (n + 1 + 1) / 2 query: @@ -6,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.16982 Nat)) (=> (>= _uniq.16982 0) (>= (sum _uniq.16982) 0)))) +(assert (forall ((_uniq.13678 Nat)) (=> (>= _uniq.13678 0) (>= (sum _uniq.13678) 0)))) (assert (= (sum n) (div (* n (+ n 1)) 2))) (assert (distinct (sum (+ n 1)) (div (* (+ n 1) (+ (+ n 1) 1)) 2))) (check-sat) diff --git a/Test/Nat/ZeroSub'.expected b/Test/Nat/ZeroSub'.expected index 7484093c..51848119 100644 --- a/Test/Nat/ZeroSub'.expected +++ b/Test/Nat/ZeroSub'.expected @@ -1,12 +1,12 @@ Test/Nat/ZeroSub'.lean:6:12: error: tactic 'assumption' failed case zero -_uniq✝⁵⁵³⁻⁰ : ¬Smt.Reconstruct.Builtin.distinct [0, 0] +_uniq✝⁴⁷⁸⁻⁰ : ¬Smt.Reconstruct.Builtin.distinct [0, 0] ⊢ ¬Smt.Reconstruct.andN' [] ¬0 - 0 = 0 Test/Nat/ZeroSub'.lean:7:17: error: application type mismatch HAdd.hAdd x argument x has type - ℕ : Type + Nat : Type but is expected to have type - ℤ : Type + Int : Type diff --git a/Test/Nat/ZeroSub.lean b/Test/Nat/ZeroSub.lean index e28a5cfe..95d1a95a 100644 --- a/Test/Nat/ZeroSub.lean +++ b/Test/Nat/ZeroSub.lean @@ -2,4 +2,4 @@ import Smt example : 0 - x = 0 := by smt_show - induction x <;> simp_all [Nat.sub_succ] + induction x <;> simp_all [← Nat.sub_succ] diff --git a/Test/Real/Density.expected b/Test/Real/Density.expected index 97460c0a..5b62cbfd 100644 --- a/Test/Real/Density.expected +++ b/Test/Real/Density.expected @@ -5,4 +5,4 @@ query: (declare-const z Real) (assert (not (=> (< x z) (exists ((y Real)) (and (< x y) (< y z)))))) (check-sat) -Test/Real/Density.lean:3:8: warning: declaration uses 'sorry' +Test/Real/Density.lean:4:8: warning: declaration uses 'sorry' diff --git a/Test/Real/Density.lean b/Test/Real/Density.lean index 4346dfe7..8445cd30 100644 --- a/Test/Real/Density.lean +++ b/Test/Real/Density.lean @@ -1,4 +1,5 @@ import Smt +import Smt.Real theorem density (x z : Real) : x < z → ∃ y, x < y ∧ y < z := by smt_show diff --git a/Test/Real/Inverse.expected b/Test/Real/Inverse.expected index 07203aa8..3de7d30f 100644 --- a/Test/Real/Inverse.expected +++ b/Test/Real/Inverse.expected @@ -4,4 +4,4 @@ query: (declare-const x Real) (assert (not (=> (distinct x 0.0) (exists ((y Real)) (= (* x y) 1.0))))) (check-sat) -Test/Real/Inverse.lean:3:8: warning: declaration uses 'sorry' +Test/Real/Inverse.lean:4:8: warning: declaration uses 'sorry' diff --git a/Test/Real/Inverse.lean b/Test/Real/Inverse.lean index d2971ffd..d54450d5 100644 --- a/Test/Real/Inverse.lean +++ b/Test/Real/Inverse.lean @@ -1,4 +1,5 @@ import Smt +import Smt.Real theorem inverse (x : Real) : x ≠ 0 → ∃ y, x * y = 1 := by smt_show diff --git a/Test/String/Length.expected b/Test/String/Length.expected index ea163afe..065a74fd 100644 --- a/Test/String/Length.expected +++ b/Test/String/Length.expected @@ -3,6 +3,6 @@ goal: "a".length = 1 query: (define-sort Nat () Int) (declare-fun String.length (String) Nat) -(assert (forall ((_uniq.922 String)) (>= (String.length _uniq.922) 0))) +(assert (forall ((_uniq.769 String)) (>= (String.length _uniq.769) 0))) (assert (distinct (String.length "a") 1)) (check-sat) diff --git a/Test/linarith.expected b/Test/linarith.expected index 76436fc4..45481b77 100644 --- a/Test/linarith.expected +++ b/Test/linarith.expected @@ -1,21 +1,21 @@ -Test/linarith.lean:33:9: warning: unused variable `e` +Test/linarith.lean:34:9: warning: unused variable `e` note: this linter can be disabled with `set_option linter.unusedVariables false` -Test/linarith.lean:52:0: warning: declaration uses 'sorry' -Test/linarith.lean:100:9: warning: unused variable `a` +Test/linarith.lean:53:0: warning: declaration uses 'sorry' +Test/linarith.lean:101:9: warning: unused variable `a` note: this linter can be disabled with `set_option linter.unusedVariables false` -Test/linarith.lean:100:13: warning: unused variable `c` +Test/linarith.lean:101:13: warning: unused variable `c` note: this linter can be disabled with `set_option linter.unusedVariables false` -Test/linarith.lean:105:9: warning: unused variable `a` +Test/linarith.lean:106:9: warning: unused variable `a` note: this linter can be disabled with `set_option linter.unusedVariables false` -Test/linarith.lean:105:13: warning: unused variable `c` +Test/linarith.lean:106:13: warning: unused variable `c` note: this linter can be disabled with `set_option linter.unusedVariables false` -Test/linarith.lean:117:60: warning: unused variable `h3` +Test/linarith.lean:118:60: warning: unused variable `h3` note: this linter can be disabled with `set_option linter.unusedVariables false` -Test/linarith.lean:124:9: warning: unused variable `a` +Test/linarith.lean:125:9: warning: unused variable `a` note: this linter can be disabled with `set_option linter.unusedVariables false` -Test/linarith.lean:124:13: warning: unused variable `c` +Test/linarith.lean:125:13: warning: unused variable `c` note: this linter can be disabled with `set_option linter.unusedVariables false` -Test/linarith.lean:167:34: warning: unused variable `z` +Test/linarith.lean:168:34: warning: unused variable `z` note: this linter can be disabled with `set_option linter.unusedVariables false` -Test/linarith.lean:168:5: warning: unused variable `h5` +Test/linarith.lean:169:5: warning: unused variable `h5` note: this linter can be disabled with `set_option linter.unusedVariables false` diff --git a/Test/linarith.lean b/Test/linarith.lean index bdd5dc17..68f25e7d 100644 --- a/Test/linarith.lean +++ b/Test/linarith.lean @@ -1,4 +1,5 @@ import Smt +import Smt.Real example {x y : Real} {f : Real → Real} : ¬(((1/2 : Real) = 1/2) ∧ x ≤ y ∧ y ≤ x ∧ ¬f x = f y) := by smt diff --git a/lakefile.lean b/lakefile.lean index 79fe60e9..bd8d2606 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -72,13 +72,11 @@ script test do where runTest (test : FilePath) (expected : FilePath) : ScriptM UInt32 := do IO.println s!"Start : {test}" - -- Note: this only works on Unix since it needs the shared library `libSmt` - -- to also loads its transitive dependencies. - let some dynlib := (← findModule? `Smt).map (·.dynlibFile) - | do IO.println s!"Error: Could not find `{nameToSharedLib "Smt"}`"; return 2 + let imports ← Lean.parseImports' (← IO.FS.readFile test) test.fileName.get! + let modules ← imports.filterMapM (findModule? ·.module) let out ← IO.Process.output { cmd := (← getLean).toString - args := #[s!"--load-dynlib={libcpp}", s!"--load-dynlib={dynlib}", test.toString] + args := #[s!"--load-dynlib={libcpp}"] ++ modules.map (s!"--load-dynlib={·.dynlibFile}") ++ #[test.toString] env := ← getAugmentedEnv } let expected ← IO.FS.readFile expected @@ -118,11 +116,11 @@ where updateTest (test : FilePath) : ScriptM UInt32 := do let expected := test.withExtension "expected" IO.println s!"Start : {test}" - let some dynlib := (← findModule? `Smt).map (·.dynlibFile) - | do IO.println s!"Error: Could not find `{nameToSharedLib "Smt"}`"; return 2 + let imports ← Lean.parseImports' (← IO.FS.readFile test) test.fileName.get! + let modules ← imports.filterMapM (findModule? ·.module) let out ← IO.Process.output { cmd := (← getLean).toString - args := #[s!"--load-dynlib={libcpp}", s!"--load-dynlib={dynlib}", test.toString] + args := #[s!"--load-dynlib={libcpp}"] ++ modules.map (s!"--load-dynlib={·.dynlibFile}") ++ #[test.toString] env := ← getAugmentedEnv } IO.FS.writeFile expected out.stdout From 91ac7f46c83137327715874d27851b7421a40725 Mon Sep 17 00:00:00 2001 From: joewatt95 Date: Mon, 8 Jul 2024 08:23:44 +0800 Subject: [PATCH 4/4] 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 | 4 ++-- Smt/Reconstruct/Real/Polynorm.lean | 1 + Test/BitVec/Shift.expected | 2 +- Test/Int/Binders.expected | 8 ++++---- Test/Int/Let.expected | 2 +- Test/Nat/Cong.expected | 2 +- Test/Nat/Sum'.expected | 4 ++-- Test/Real/Density.expected | 2 ++ Test/Real/Inverse.expected | 2 ++ Test/linarith.expected | 1 + lake-manifest.json | 18 +++++++++--------- lakefile.lean | 2 +- lean-toolchain | 2 +- 13 files changed, 28 insertions(+), 22 deletions(-) diff --git a/Smt/Data/Sexp.lean b/Smt/Data/Sexp.lean index e4b67302..b536d9dd 100644 --- a/Smt/Data/Sexp.lean +++ b/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 diff --git a/Smt/Reconstruct/Real/Polynorm.lean b/Smt/Reconstruct/Real/Polynorm.lean index 53624d9a..1cc389ab 100644 --- a/Smt/Reconstruct/Real/Polynorm.lean +++ b/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 diff --git a/Test/BitVec/Shift.expected b/Test/BitVec/Shift.expected index 9d781ffb..f7f9bcd5 100644 --- a/Test/BitVec/Shift.expected +++ b/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' diff --git a/Test/Int/Binders.expected b/Test/Int/Binders.expected index 4169c399..83c0b301 100644 --- a/Test/Int/Binders.expected +++ b/Test/Int/Binders.expected @@ -1,7 +1,7 @@ goal: curryAdd a b = curryAdd b a query: -(define-fun curryAdd ((a._@.Test.Int.Binders._hyg.3 Int) (a._@.Test.Int.Binders._hyg.5 Int)) Int (+ a._@.Test.Int.Binders._hyg.3 a._@.Test.Int.Binders._hyg.5)) +(define-fun curryAdd ((a._@.Test.Int.Binders._hyg.4 Int) (a._@.Test.Int.Binders._hyg.6 Int)) Int (+ a._@.Test.Int.Binders._hyg.4 a._@.Test.Int.Binders._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) (a._@.Test.Int.Binders._hyg.33 Int)) Int (+ a a._@.Test.Int.Binders._hyg.33)) +(define-fun partCurryAdd ((a Int) (a._@.Test.Int.Binders._hyg.36 Int)) Int (+ a a._@.Test.Int.Binders._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) (a._@.Init.Prelude._hyg.2347 Int)) Int (+ a a._@.Init.Prelude._hyg.2347)) +(define-fun |partCurryAdd'| ((a Int) (a._@.Init.Prelude._hyg.2495 Int)) Int (+ a a._@.Init.Prelude._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' diff --git a/Test/Int/Let.expected b/Test/Int/Let.expected index e945919e..cd2a1eac 100644 --- a/Test/Int/Let.expected +++ b/Test/Int/Let.expected @@ -19,7 +19,7 @@ goal: z 3 = 10 query: (declare-fun f (Int) Int) -(define-fun z ((x._@.Test.Int.Let._hyg.295 Int)) Int (f 10)) +(define-fun z ((x._@.Test.Int.Let._hyg.300 Int)) Int (f 10)) (assert (= (f 10) 10)) (assert (distinct (z 3) 10)) (check-sat) diff --git a/Test/Nat/Cong.expected b/Test/Nat/Cong.expected index e3c5499f..768e190e 100644 --- a/Test/Nat/Cong.expected +++ b/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) diff --git a/Test/Nat/Sum'.expected b/Test/Nat/Sum'.expected index c52d77fa..c934fc3b 100644 --- a/Test/Nat/Sum'.expected +++ b/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) diff --git a/Test/Real/Density.expected b/Test/Real/Density.expected index 5b62cbfd..0ec01b0f 100644 --- a/Test/Real/Density.expected +++ b/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` diff --git a/Test/Real/Inverse.expected b/Test/Real/Inverse.expected index 3de7d30f..1409551a 100644 --- a/Test/Real/Inverse.expected +++ b/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` diff --git a/Test/linarith.expected b/Test/linarith.expected index 45481b77..3200e752 100644 --- a/Test/linarith.expected +++ b/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` diff --git a/lake-manifest.json b/lake-manifest.json index 0283d11e..38c71683 100644 --- a/lake-manifest.json +++ b/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", diff --git a/lakefile.lean b/lakefile.lean index bd8d2606..5d333342 100644 --- a/lakefile.lean +++ b/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" diff --git a/lean-toolchain b/lean-toolchain index ef1f67e9..4ef27c47 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.8.0 +leanprover/lean4:v4.9.0