From f0e6b5645664e746c360765dc16541c52ba78c99 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed Date: Tue, 22 Oct 2024 23:15:57 -0700 Subject: [PATCH] Optimize Rat's polynorm and fix bugs. (#138) * Optimize Rat's polynorm and fix bugs. * Fix lean-cvc5 version. * Compile Smt.Rat. * Fix lean-cvc5 version. * Fix Rat bug. --- .github/workflows/ci.yml | 1 + Smt/Reconstruct.lean | 3 +- Smt/Reconstruct/Int/Polynorm.lean | 4 +- Smt/Reconstruct/Prop.lean | 16 +-- Smt/Reconstruct/Rat.lean | 1 - Smt/Reconstruct/Rat/Polynorm.lean | 218 +++++++++++++++++++++++------- Smt/Reconstruct/Real.lean | 5 +- Smt/Reconstruct/UF.lean | 4 +- Test/Rat/linarith.expected | 4 + Test/Rat/linarith.lean | 135 ++++++++++++++++++ Test/linarith.lean | 6 + lake-manifest.json | 2 +- lakefile.lean | 2 +- 13 files changed, 333 insertions(+), 68 deletions(-) create mode 100644 Test/Rat/linarith.expected create mode 100644 Test/Rat/linarith.lean diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 63d200ae..a62910e4 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -25,6 +25,7 @@ jobs: lake update lake build lake build +Smt:dynlib + lake build +Smt.Rat:dynlib lake build +Smt.Real:dynlib - name: Test lean-smt run: lake run test diff --git a/Smt/Reconstruct.lean b/Smt/Reconstruct.lean index 0da72a8f..837bfbc5 100644 --- a/Smt/Reconstruct.lean +++ b/Smt/Reconstruct.lean @@ -136,7 +136,7 @@ def addThm (type : Expr) (val : Expr) : ReconstructM Expr := do let name := Name.num `s (← incCount) let mv ← Meta.mkFreshExprMVar type .natural name mv.mvarId!.assign val - trace[smt.reconstruct.proof] "have {name} : {type} := {mv}" + trace[smt.reconstruct.proof] "have {name} : {type} := {val}" return mv def addTac (type : Expr) (tac : MVarId → MetaM Unit) : ReconstructM Expr := do @@ -202,6 +202,7 @@ def solve (query : String) (timeout : Option Nat) : MetaM (Except Error cvc5.Pro Solver.setOption "dag-thresh" "0" Solver.setOption "simplification" "none" Solver.setOption "enum-inst" "true" + Solver.setOption "cegqi-midpoint" "true" Solver.setOption "produce-models" "true" Solver.setOption "produce-proofs" "true" Solver.setOption "proof-elim-subtypes" "true" diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean index fb524dd8..c44de280 100644 --- a/Smt/Reconstruct/Int/Polynorm.lean +++ b/Smt/Reconstruct/Int/Polynorm.lean @@ -256,8 +256,8 @@ inductive Expr where | var (v : Nat) | neg (a : Expr) | add (a b : Expr) - | mul (a b : Expr) | sub (a b : Expr) + | mul (a b : Expr) deriving Inhabited, Repr namespace Expr @@ -372,7 +372,7 @@ def nativePolyNorm (mv : MVarId) : MetaM Unit := do let ctx : Q(PolyNorm.Context) ← pure q((«$is».getD · 0)) let ⟨cache, el, _⟩ ← toQPolyNormExpr ctx es l {} let ⟨_, er, _⟩ ← toQPolyNormExpr ctx es r cache - let hp ← nativeDecide q(«$el».toPolynomial = «$er».toPolynomial) + let hp ← nativeDecide q(«$el».toPolynomial = «$er».toPolynomial) let he := q(@PolyNorm.Expr.denote_eq_from_toPolynomial_eq $ctx $el $er $hp) mv.assign he where diff --git a/Smt/Reconstruct/Prop.lean b/Smt/Reconstruct/Prop.lean index ce15a450..e364fd58 100644 --- a/Smt/Reconstruct/Prop.lean +++ b/Smt/Reconstruct/Prop.lean @@ -246,9 +246,9 @@ def reconstructResolution (c₁ c₂ : Array cvc5.Term) (pol l : cvc5.Term) (hps let hij : Q($ps[$i] = ¬$qs[$j]) := if pol.getBooleanValue then .app q(Prop.eq_not_not) q($ps[$i]) else .app q(@Eq.refl Prop) q($ps[$i]) - addThm (← rightAssocOp q(Or) (getResolutionResult c₁ c₂ pol l)) q(Prop.orN_resolution $hps $hqs $hi $hj $hij) + return q(Prop.orN_resolution $hps $hqs $hi $hj $hij) else - addThm (← rightAssocOp q(Or) (c₁ ++ c₂)) q(@Prop.orN_append_left $ps $qs $hps) + return q(@Prop.orN_append_left $ps $qs $hps) where rightAssocOp (op : Expr) (ts : Array cvc5.Term) : ReconstructM Expr := do if ts.isEmpty then @@ -285,12 +285,12 @@ def reconstructChainResolution (cs as : Array cvc5.Term) (ps : Array Expr) : Rec let c₂ := clausify pf.getChildren[1]!.getResult l let hps ← reconstructProof pf.getChildren[0]! let hqs ← reconstructProof pf.getChildren[1]! - reconstructResolution c₁ c₂ p l hps hqs + addThm (← reconstructTerm pf.getResult) (← reconstructResolution c₁ c₂ p l hps hqs) | .CHAIN_RESOLUTION => let cs := pf.getChildren.map (·.getResult) let as := pf.getArguments let ps ← pf.getChildren.mapM reconstructProof - reconstructChainResolution cs as ps + addThm (← reconstructTerm pf.getResult) (← reconstructChainResolution cs as ps) | .FACTORING => let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult let q : Q(Prop) ← reconstructTerm pf.getResult @@ -345,11 +345,9 @@ def reconstructChainResolution (cs as : Array cvc5.Term) (ps : Array Expr) : Rec let f := fun pf ⟨q, hq⟩ => do let p : Q(Prop) ← reconstructTerm pf.getResult let hp : Q($p) ← reconstructProof pf - let hq ← addThm q($p ∧ $q) q(And.intro $hp $hq) - let q := q($p ∧ $q) - return ⟨q, hq⟩ - let ⟨_, hq⟩ ← cpfs.pop.foldrM f (⟨q, hq⟩ : Σ q : Q(Prop), Q($q)) - return hq + return ⟨q($p ∧ $q), q(And.intro $hp $hq)⟩ + let ⟨q, hq⟩ ← cpfs.pop.foldrM f (⟨q, hq⟩ : Σ q : Q(Prop), Q($q)) + addThm q hq | .NOT_OR_ELIM => let f t ps := do let p : Q(Prop) ← reconstructTerm t diff --git a/Smt/Reconstruct/Rat.lean b/Smt/Reconstruct/Rat.lean index 9be8dab6..295c18e7 100644 --- a/Smt/Reconstruct/Rat.lean +++ b/Smt/Reconstruct/Rat.lean @@ -422,7 +422,6 @@ where | .GT => addThm q(($x₁ > $x₂) = ($y₁ > $y₂)) q(Rat.gt_of_sub_eq_neg $hcx $hcy $h) | _ => return none - return none | .ARITH_MULT_SIGN => if pf.getResult[1]![0]!.getSort.isInteger then return none reconstructMulSign pf diff --git a/Smt/Reconstruct/Rat/Polynorm.lean b/Smt/Reconstruct/Rat/Polynorm.lean index 93ff125e..1088a330 100644 --- a/Smt/Reconstruct/Rat/Polynorm.lean +++ b/Smt/Reconstruct/Rat/Polynorm.lean @@ -18,14 +18,32 @@ theorem Rat.neg_mul_eq_neg_mul (a b : Rat) : -(a * b) = -a * b := by namespace Smt.Reconstruct.Rat.PolyNorm -abbrev Var := Nat +structure Var where + type : Bool + val : Nat +deriving DecidableEq, Repr + +instance : LE Var where + le v₁ v₂ := v₁.type < v₂.type ∨ (v₁.type = v₂.type ∧ v₁.val ≤ v₂.val) + +instance : LT Var where + lt v₁ v₂ := v₁.type < v₂.type ∨ (v₁.type = v₂.type ∧ v₁.val < v₂.val) + +instance (v₁ v₂ : Var) : Decidable (v₁ ≤ v₂) := + if h : v₁.type < v₂.type ∨ (v₁.type = v₂.type ∧ v₁.val ≤ v₂.val) then isTrue h else isFalse h + +instance (v₁ v₂ : Var) : Decidable (v₁ < v₂) := + if h : v₁.type < v₂.type ∨ (v₁.type = v₂.type ∧ v₁.val < v₂.val) then isTrue h else isFalse h def Context := Var → Rat +def IntContext := Nat → Int +def RatContext := Nat → Rat + structure Monomial where coeff : Rat vars : List Var -deriving Inhabited, Repr +deriving Inhabited, Repr, DecidableEq namespace Monomial @@ -158,37 +176,87 @@ theorem denote_divConst {p : Polynomial} : (p.divConst c).denote ctx = p.denote end Polynomial -inductive Expr where - | val (v : Rat) +inductive IntExpr where + | val (v : Int) | var (v : Nat) - | neg (a : Expr) - | add (a b : Expr) - | sub (a b : Expr) - | mul (a b : Expr) - | divConst (a : Expr) (c : Rat) + | neg (a : IntExpr) + | add (a b : IntExpr) + | sub (a b : IntExpr) + | mul (a b : IntExpr) deriving Inhabited, Repr -namespace Expr +namespace IntExpr -def toPolynomial : Expr → Polynomial +def toPolynomial : IntExpr → Polynomial | val v => if v = 0 then [] else [{ coeff := v, vars := [] }] - | var v => [{ coeff := 1, vars := [v] }] + | var v => [{ coeff := 1, vars := [⟨false, 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 +def denote (ctx : IntContext) : IntExpr → 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 - | divConst a c => a.denote ctx / c -theorem denote_toPolynomial {e : Expr} : e.denote ctx = e.toPolynomial.denote ctx := by +theorem denote_toPolynomial {rctx : RatContext} {e : IntExpr} : e.denote ictx = e.toPolynomial.denote (fun ⟨b, n⟩ => if b then rctx n else ictx n) := 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, Rat.intCast_neg, ih] + | add a b ih₁ ih₂ => + simp only [denote, toPolynomial, Polynomial.denote_add, Rat.intCast_add, ih₁, ih₂] + | sub a b ih₁ ih₂ => + simp only [denote, toPolynomial, Polynomial.denote_sub, Rat.intCast_sub, ih₁, ih₂] + | mul a b ih₁ ih₂ => + simp only [denote, toPolynomial, Polynomial.denote_mul, Rat.intCast_mul, ih₁, ih₂] + +end IntExpr + +inductive RatExpr where + | val (v : Rat) + | var (v : Nat) + | neg (a : RatExpr) + | add (a b : RatExpr) + | sub (a b : RatExpr) + | mul (a b : RatExpr) + | divConst (a : RatExpr) (c : Rat) + | cast (a : IntExpr) +deriving Inhabited, Repr + +namespace RatExpr + +def toPolynomial : RatExpr → Polynomial + | val v => if v = 0 then [] else [{ coeff := v, vars := [] }] + | var v => [{ coeff := 1, vars := [⟨true, 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 + | cast a => a.toPolynomial + +def denote (ictx : IntContext) (rctx : RatContext) : RatExpr → Rat + | val v => v + | var v => rctx v + | neg a => -a.denote ictx rctx + | add a b => a.denote ictx rctx + b.denote ictx rctx + | sub a b => a.denote ictx rctx - b.denote ictx rctx + | mul a b => a.denote ictx rctx * b.denote ictx rctx + | divConst a c => a.denote ictx rctx / c + | cast a => a.denote ictx + +theorem denote_toPolynomial {e : RatExpr} : e.denote ictx rctx = e.toPolynomial.denote (fun ⟨b, n⟩ => if b then rctx n else ictx n) := by induction e with | val v => simp only [denote, toPolynomial] @@ -207,24 +275,35 @@ theorem denote_toPolynomial {e : Expr} : e.denote ctx = e.toPolynomial.denote ct simp only [denote, toPolynomial, Polynomial.denote_mul, ih₁, ih₂] | divConst a c ih => simp only [denote, toPolynomial, Polynomial.denote_divConst, ih] + | cast a => + simpa only [denote] using IntExpr.denote_toPolynomial -theorem denote_eq_from_toPolynomial_eq {e₁ e₂ : Expr} (h : e₁.toPolynomial = e₂.toPolynomial) : e₁.denote ctx = e₂.denote ctx := by +theorem denote_eq_from_toPolynomial_eq {e₁ e₂ : RatExpr} (h : e₁.toPolynomial = e₂.toPolynomial) : e₁.denote ictx rctx = e₂.denote ictx rctx := by rw [denote_toPolynomial, denote_toPolynomial, h] -end PolyNorm.Expr +end PolyNorm.RatExpr open Lean hiding Rat open Qq -abbrev PolyM := StateT (Array Q(Rat)) MetaM +abbrev PolyM := StateT (Array Q(Int) × Array Q(Rat)) MetaM + +def getRatIndex (e : Q(Rat)) : PolyM Nat := do + let ⟨is, rs⟩ ← get + if let some i := rs.findIdx? (· == e) then + return i + else + let size := rs.size + set (is, rs.push e) + return size -def getIndex (e : Q(Rat)) : PolyM Nat := do - let es ← get - if let some i := es.findIdx? (· == e) then +def getIntIndex (e : Q(Rat)) : PolyM Nat := do + let ⟨is, rs⟩ ← get + if let some i := is.findIdx? (· == e) then return i else - let size := es.size - set (es.push e) + let size := is.size + set (is.push e, rs) return size partial def toRatConst (e : Q(Rat)) : PolyM Rat := do @@ -237,40 +316,64 @@ partial def toRatConst (e : Q(Rat)) : PolyM Rat := do | ~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 +partial def toQPolyNormIntExpr (e : Q(Int)) : PolyM Q(PolyNorm.IntExpr) := 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 + | ~q(OfNat.ofNat $n) => pure q(.val (@OfNat.ofNat Int $n _)) + | ~q(-$x) => pure q(.neg $(← toQPolyNormIntExpr x)) + | ~q($x + $y) => pure q(.add $(← toQPolyNormIntExpr x) $(← toQPolyNormIntExpr y)) + | ~q($x - $y) => pure q(.sub $(← toQPolyNormIntExpr x) $(← toQPolyNormIntExpr y)) + | ~q($x * $y) => pure q(.mul $(← toQPolyNormIntExpr x) $(← toQPolyNormIntExpr y)) + | e => let v : Nat ← getIntIndex e; pure q(.var $v) + +partial def toQPolyNormRatExpr (e : Q(Rat)) : PolyM Q(PolyNorm.RatExpr) := 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) + | ~q(-$x) => pure q(.neg $(← toQPolyNormRatExpr x)) + | ~q($x + $y) => pure q(.add $(← toQPolyNormRatExpr x) $(← toQPolyNormRatExpr y)) + | ~q($x - $y) => pure q(.sub $(← toQPolyNormRatExpr x) $(← toQPolyNormRatExpr y)) + | ~q($x * $y) => pure q(.mul $(← toQPolyNormRatExpr x) $(← toQPolyNormRatExpr y)) + | ~q($x / $y) => pure q(.divConst $(← toQPolyNormRatExpr x) $(PolyNorm.Monomial.toExpr.toExprCoeff (← toRatConst y))) + | ~q(($x : Int)) => pure q(.cast $(← toQPolyNormIntExpr x)) + | e => let v : Nat ← getRatIndex 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 (l, (is, rs)) ← (toQPolyNormRatExpr l).run (#[], #[]) + let (r, (is, rs)) ← (toQPolyNormRatExpr r).run (is, rs) + let is : Q(Array Int) ← pure (is.foldl (fun acc e => q(«$acc».push $e)) q(#[])) + let rs : Q(Array Rat) ← pure (rs.foldl (fun acc e => q(«$acc».push $e)) q(#[])) + let ictx : Q(PolyNorm.IntContext) := q((«$is».getD · 0)) + let rctx : Q(PolyNorm.RatContext) := q((«$rs».getD · 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) + mv.assign q(@PolyNorm.RatExpr.denote_eq_from_toPolynomial_eq $ictx $rctx $l $r $h) + +def nativePolyNorm (mv : MVarId) : MetaM Unit := do + let some (_, l, r) := (← mv.getType).eq? + | throwError "[poly_norm] expected an equality, got {← mv.getType}" + let (l, (is, rs)) ← (toQPolyNormRatExpr l).run (#[], #[]) + let (r, (is, rs)) ← (toQPolyNormRatExpr r).run (is, rs) + let is : Q(Array Int) ← pure (is.foldl (fun acc e => q(«$acc».push $e)) q(#[])) + let rs : Q(Array Rat) ← pure (rs.foldl (fun acc e => q(«$acc».push $e)) q(#[])) + let ictx : Q(PolyNorm.IntContext) := q((«$is».getD · 0)) + let rctx : Q(PolyNorm.RatContext) := q((«$rs».getD · 0)) + let h ← nativeDecide q(«$l».toPolynomial = «$r».toPolynomial) + mv.assign q(@PolyNorm.RatExpr.denote_eq_from_toPolynomial_eq $ictx $rctx $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}" + nativeDecide (p : Q(Prop)) : MetaM Q($p) := do + let hp : Q(Decidable $p) ← Meta.synthInstance q(Decidable $p) + let auxDeclName ← mkNativeAuxDecl `_nativePolynorm q(Bool) q(decide $p) + let b : Q(Bool) := .const auxDeclName [] + return .app q(@of_decide_eq_true $p $hp) (.app q(Lean.ofReduceBool $b true) q(Eq.refl true)) + mkNativeAuxDecl (baseName : Name) (type value : Expr) : MetaM Name := do + let auxName ← Lean.mkAuxName baseName 1 + let decl := Declaration.defnDecl { + name := auxName, levelParams := [], type, value + hints := .abbrev + safety := .safe + } + addAndCompile decl + pure auxName namespace Tactic @@ -283,7 +386,24 @@ open Lean.Elab Tactic in Rat.polyNorm mv replaceMainGoal [] +syntax (name := nativePolyNorm) "native_poly_norm" : tactic + +open Lean.Elab Tactic in +@[tactic nativePolyNorm] def evalNativePolyNorm : Tactic := fun _ => + withMainContext do + let mv ← Tactic.getMainGoal + Rat.nativePolyNorm mv + replaceMainGoal [] + end Smt.Reconstruct.Rat.Tactic +open Smt.Reconstruct.Rat.PolyNorm.RatExpr + example (x y z : Rat) : 1 * (x + y) * z / 4 = 1/(2 * 2) * (z * y + x * z) := by poly_norm + +example (x y : Int) (z : Rat) : 1 * (x + y) * z / 4 = 1/(2 * 2) * (z * y + x * z) := by + poly_norm + +example (x y : Int) (z : Rat) : 1 * (x + y) * z / 4 = 1/(2 * 2) * (z * y + x * z) := by + native_poly_norm diff --git a/Smt/Reconstruct/Real.lean b/Smt/Reconstruct/Real.lean index 6675918b..ea499d44 100644 --- a/Smt/Reconstruct/Real.lean +++ b/Smt/Reconstruct/Real.lean @@ -411,6 +411,7 @@ where addTac q($a = $b) Real.polyNorm | .ARITH_POLY_NORM_REL => if pf.getResult[0]![0]!.getSort.isInteger then return none + let lcx : Lean.Rat := pf.getChildren[0]!.getResult[0]![0]!.getRationalValue let cx : Q(Real) ← reconstructTerm pf.getChildren[0]!.getResult[0]![0]! let x₁ : Q(Real) ← reconstructTerm pf.getResult[0]![0]! let x₂ : Q(Real) ← reconstructTerm pf.getResult[0]![1]! @@ -425,14 +426,14 @@ where Real.normNum hcx.mvarId! Real.normNum hcy.mvarId! addThm q(($x₁ = $x₂) = ($y₁ = $y₂)) q(Real.eq_of_sub_eq $hcx $hcy $h) - else if pf.getChildren[0]!.getResult[0]![0]!.getRationalValue > 0 then + else if lcx > 0 then let hcx : Q($cx > 0) ← Meta.mkFreshExprMVar q($cx > 0) let hcy : Q($cy > 0) ← Meta.mkFreshExprMVar q($cy > 0) Real.normNum hcx.mvarId! Real.normNum hcy.mvarId! match k with | .LT => - addThm q(($x₁ < $x₂) = ($y₁ < $y₂)) q(lt_of_sub_eq_pos $hcx $hcy $h) + addThm q(($x₁ < $x₂) = ($y₁ < $y₂)) q(Real.lt_of_sub_eq_pos $hcx $hcy $h) | .LEQ => addThm q(($x₁ ≤ $x₂) = ($y₁ ≤ $y₂)) q(Real.le_of_sub_eq_pos $hcx $hcy $h) | .GEQ => diff --git a/Smt/Reconstruct/UF.lean b/Smt/Reconstruct/UF.lean index 10f39253..e23fb4ee 100644 --- a/Smt/Reconstruct/UF.lean +++ b/Smt/Reconstruct/UF.lean @@ -82,8 +82,8 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do let c : Q($α) ← reconstructTerm cpfs[i]!.getResult[1]! let hab : Q($a = $b) := curr let hbc : Q($b = $c) ← reconstructProof cpfs[i]! - curr ← addThm q($a = $c) q(Eq.trans $hab $hbc) - return curr + curr := q(Eq.trans $hab $hbc) + addThm (← reconstructTerm pf.getResult) curr | .CONG => let k := pf.getResult[0]!.getKind if k == .FORALL || k == .EXISTS || k == .WITNESS || k == .LAMBDA || k == .SET_COMPREHENSION then diff --git a/Test/Rat/linarith.expected b/Test/Rat/linarith.expected new file mode 100644 index 00000000..85b845f3 --- /dev/null +++ b/Test/Rat/linarith.expected @@ -0,0 +1,4 @@ +Test/Rat/linarith.lean:91:9: warning: unused variable `a` +note: this linter can be disabled with `set_option linter.unusedVariables false` +Test/Rat/linarith.lean:91:13: warning: unused variable `c` +note: this linter can be disabled with `set_option linter.unusedVariables false` diff --git a/Test/Rat/linarith.lean b/Test/Rat/linarith.lean new file mode 100644 index 00000000..8510b7b7 --- /dev/null +++ b/Test/Rat/linarith.lean @@ -0,0 +1,135 @@ +import Smt +import Smt.Rat + +namespace Smt.Translate.Rat + +open Qq +open Translator Term + +@[smt_translate] def translateType : Translator := fun (e : Q(Type)) => match e with + | ~q(Rat) => return symbolT "Real" + | _ => return none + +@[smt_translate] def translateRat : Translator := fun (e : Q(Rat)) => match e with + | ~q(OfNat.ofNat $n) => return if let some n := n.rawNatLit? then literalT s!"{n}.0" else none + | ~q(-$x) => return appT (symbolT "-") (← applyTranslators! x) + | ~q($x + $y) => return mkApp2 (symbolT "+") (← applyTranslators! x) (← applyTranslators! y) + | ~q($x - $y) => return mkApp2 (symbolT "-") (← applyTranslators! x) (← applyTranslators! y) + | ~q($x * $y) => return mkApp2 (symbolT "*") (← applyTranslators! x) (← applyTranslators! y) + | ~q($x / $y) => return mkApp2 (symbolT "/") (← applyTranslators! x) (← applyTranslators! y) + | _ => return none + +@[smt_translate] def translateProp : Translator := fun (e : Q(Prop)) => match e with + | ~q(($x : Rat) < $y) => return mkApp2 (symbolT "<") (← applyTranslators! x) (← applyTranslators! y) + | ~q(($x : Rat) ≤ $y) => return mkApp2 (symbolT "<=") (← applyTranslators! x) (← applyTranslators! y) + | ~q(($x : Rat) ≥ $y) => return mkApp2 (symbolT ">=") (← applyTranslators! x) (← applyTranslators! y) + | ~q(($x : Rat) > $y) => return mkApp2 (symbolT ">") (← applyTranslators! x) (← applyTranslators! y) + | _ => return none + +end Smt.Translate.Rat + +example {x y : Rat} {f : Rat → Rat} : ¬(((1/2 : Rat) = 1/2) ∧ x ≤ y ∧ y ≤ x ∧ ¬f x = f y) := by + smt + +example {x y : Rat} {f : Rat → Rat} : ¬(((1/2 : Int) = 1/2) ∧ x ≤ y ∧ y ≤ x ∧ ¬f x = f y) := by + smt + +example (A B : Rat) (h : 0 < A * B) : 0 < A*B/8 := by + smt [h] + +example (A B : Rat) (h : 0 < A * B) : 0 < A/8*B := by + smt [h] + +example (ε : Rat) (h1 : ε > 0) : ε / 2 + ε / 3 + ε / 7 < ε := by + smt [h1] + +example (x y z : Rat) (h1 : 2*x < 3*y) (h2 : -4*x + z/2 < 0) + (h3 : 12*y - z < 0) : False := by + smt [h1, h2, h3] + +example (ε : Rat) (h1 : ε > 0) : ε / 2 < ε := by + smt [h1] + +example (ε : Rat) (h1 : ε > 0) : ε / 3 + ε / 3 + ε / 3 = ε := by + smt [h1] + +example (x : Rat) (h : 0 < x) : 0 < x/1 := by + smt [h] + +example (x : Rat) (h : x < 0) : 0 < x/(-1) := by + smt [h] + +example (x : Rat) (h : x < 0) : 0 < x/(-2) := by + smt [h] + +example (x : Rat) (h : x < 0) : 0 < x/(-4/5) := by + smt [h] + +example (x : Rat) (h : 0 < x) : 0 < x/2/3 := by + smt [h] + +example (x : Rat) (h : 0 < x) : 0 < x/(2/3) := by + smt [h] + +-- example (a b c : Rat) (h2 : b + 2 > 3 + b) : False := by +-- smt [h2] +-- all_goals (ring_nf; simp) +-- norm_num + +-- example (a b c : Rat) (h2 : b + 2 > 3 + b) : False := by +-- smt [h2] +-- all_goals (ring_nf; simp) +-- norm_num + +example (g v V c h : Rat) (h1 : h = 0) (h2 : v = V) (h3 : V > 0) (h4 : g > 0) + (h5 : 0 ≤ c) (h6 : c < 1) : v ≤ V := by + smt [h1, h2, h3, h4, h5, h6] + +example (a b c : Rat) (h1 : a > 0) (h2 : b > 5) (h3 : c < -10) (h4 : a + b - c < 3) : False := by + smt [h1, h2, h3, h4] + +example (a b c : Rat) (h2 : b > 0) (h3 : ¬ b ≥ 0) : False := by + smt [h2, h3] + +example (x y z : Rat) (hx : x ≤ 3*y) (h2 : y ≤ 2*z) (h3 : x ≥ 6*z) : x = 3*y := by + smt [hx, h2, h3] + +example (x y z : Rat) (hx : ¬ x > 3*y) (h2 : ¬ y > 2*z) (h3 : x ≥ 6*z) : x = 3*y := by + smt [hx, h2, h3] + +-- example (x y : Rat) (h : 6 + ((x + 4) * x + (6 + 3 * y) * y) = 3) (h' : (x + 4) * x ≥ 0) +-- (h'' : (6 + 3 * y) * y ≥ 0) : False := by +-- smt [h, h''] +-- all_goals sorry + +example (a : Rat) (ha : 0 ≤ a) : 0 * 0 ≤ 2 * a := by + smt [ha] + +example (x y : Rat) (h : x < y) : x ≠ y := by + smt [h] + +example (x y : Rat) (h : x < y) : ¬ x = y := by + smt [h] + +-- example (x : Rat) : id x ≥ x := by +-- let idℝ := fun (x : Rat) => x +-- let hidℝ : idℝ = fun x => x := rfl +-- have : @id Rat = idℝ := rfl +-- rewrite [this] +-- smt [idℝ] +-- all_goals (ring_nf; simp) +-- sorry + +example (prime : Int → Prop) (x y z : Rat) (h1 : 2*x + ((-3)*y) < 0) (h2 : (-4)*x + 2*z < 0) (h3 : 12*y + (-4)* z < 0) + (h4 : prime 7) : False := by + smt [h1, h2, h3, h4] + +example (prime : Int → Prop) (x y z : Rat) (h1 : 2*1*x + (3)*(y*(-1)) < 0) (h2 : (-2)*x*2 < -(z + z)) + (h3 : 12*y + (-4)* z < 0) (h4 : prime 7) : False := by + smt [h1, h2, h3, h4] + +example : ∃ (x : Rat), x > 2 ∧ x * x < 24 := by + smt + +example : ∃ (x : Rat), x > 2 ∧ x * 2 < 24 := by + smt diff --git a/Test/linarith.lean b/Test/linarith.lean index 68f25e7d..c6f54fc5 100644 --- a/Test/linarith.lean +++ b/Test/linarith.lean @@ -264,3 +264,9 @@ example (u v x y A B : Int) -> u * y + v * x + u * v < 3 * A * B := by smt [a, a_1, a_2, a_3, a_4, a_5, a_6, a_7, a_8] + +example : ∃ (x : Real), x > 2 ∧ x * x < 24 := by + smt + +example : ∃ (x : Real), x > 2 ∧ x * 2 < 24 := by + smt diff --git a/lake-manifest.json b/lake-manifest.json index c72f9d8d..3c14ec95 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -8,7 +8,7 @@ "rev": "c97ff4cfc218c11af8c1598b8225a6fcc094f5cd", "name": "cvc5", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "c97ff4cfc218c11af8c1598b8225a6fcc094f5cd", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/batteries", diff --git a/lakefile.lean b/lakefile.lean index e4f5e63a..fcf14b15 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -3,7 +3,7 @@ import Lake open Lake DSL require cvc5 from - git "https://github.com/abdoo8080/lean-cvc5.git" @ "main" + git "https://github.com/abdoo8080/lean-cvc5.git" @ "c97ff4cfc218c11af8c1598b8225a6fcc094f5cd" require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.11.0"