From bd2d8b6dc75551145b24c00df3705ae347b27368 Mon Sep 17 00:00:00 2001 From: Adrien Champion Date: Mon, 10 Jun 2024 16:45:47 +0200 Subject: [PATCH 01/11] bump to v4.8.0 --- Smt/Reconstruct.lean | 2 +- Smt/Reconstruct/Arith.lean | 10 +- .../Arith/ArithMulSign/Lemmas.lean | 13 +-- .../Arith/ArithMulSign/Tactic.lean | 6 +- Smt/Reconstruct/Arith/MulPosNeg/Lemmas.lean | 2 +- Smt/Reconstruct/Arith/SumBounds/Tactic.lean | 2 +- Smt/Reconstruct/BitVec.lean | 6 +- Smt/Reconstruct/Builtin.lean | 4 +- Smt/Reconstruct/Prop/Lemmas.lean | 93 ++++++++++--------- Smt/Reconstruct/Quant.lean | 2 +- Smt/Reconstruct/UF.lean | 6 +- Smt/Tactic/EqnDef.lean | 4 +- Smt/Tactic/WHNFConfigurable.lean | 4 +- Smt/Translate/Int.lean | 2 +- Smt/Translate/Nat.lean | 2 +- Smt/Translate/Real.lean | 2 +- lake-manifest.json | 32 +++---- lakefile.lean | 6 +- lean-toolchain | 2 +- 19 files changed, 106 insertions(+), 94 deletions(-) diff --git a/Smt/Reconstruct.lean b/Smt/Reconstruct.lean index 7e6b149e..5ed1e440 100644 --- a/Smt/Reconstruct.lean +++ b/Smt/Reconstruct.lean @@ -204,7 +204,7 @@ def solve (query : String) (timeout : Option Nat) : MetaM (Except Error cvc5.Pro let ps ← Solver.getProof if h : 0 < ps.size then return ps[0] - throw (self := instMonadExcept _ _) (Error.user_error "something went wrong") + throw (self := instMonadExceptOfMonadExceptOf _ _) (Error.user_error "something went wrong") syntax (name := reconstruct) "reconstruct" str : tactic diff --git a/Smt/Reconstruct/Arith.lean b/Smt/Reconstruct/Arith.lean index d47a6a5a..4af252ec 100644 --- a/Smt/Reconstruct/Arith.lean +++ b/Smt/Reconstruct/Arith.lean @@ -28,12 +28,12 @@ open Qq | _ => return none def getTypeAndInst (s : cvc5.Sort) : Σ α : Q(Type), Q(LinearOrderedRing $α) := match s.isInteger with - | false => ⟨q(Real), q(Real.instLinearOrderedRingReal)⟩ - | true => ⟨q(Int), q(Int.linearOrderedCommRing.toLinearOrderedRing)⟩ + | false => ⟨q(Real), q(Real.instLinearOrderedRing)⟩ + | true => ⟨q(Int), q(Int.instLinearOrderedCommRing.toLinearOrderedRing)⟩ def getTypeAndInst' (s : cvc5.Sort) : Σ (α : Q(Type)) (_ : Q(LinearOrderedRing $α)), Q(FloorRing $α) := match s.isInteger with - | false => ⟨q(Real), q(Real.instLinearOrderedRingReal), q(Real.instFloorRingRealInstLinearOrderedRingReal)⟩ - | true => ⟨q(Int), q(Int.linearOrderedCommRing.toLinearOrderedRing), q(instFloorRingIntToLinearOrderedRingLinearOrderedCommRing)⟩ + | false => ⟨q(Real), q(Real.instLinearOrderedRing), q(Real.instFloorRing)⟩ + | true => ⟨q(Int), q(Int.instLinearOrderedCommRing.toLinearOrderedRing), q(instFloorRingInt)⟩ @[smt_term_reconstruct] def reconstructArith : TermReconstructor := fun t => do match t.getKind with | .SKOLEM => match t.getSkolemId with @@ -130,7 +130,7 @@ where | 1 => q(1 : Real) | _ + 2 => let h : Q(Nat.AtLeastTwo $n) := h ▸ q(instNatAtLeastTwo) - let h := mkApp3 q(@instOfNatAtLeastTwo Real) (mkRawNatLit n) q(Real.natCast) h + 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]! diff --git a/Smt/Reconstruct/Arith/ArithMulSign/Lemmas.lean b/Smt/Reconstruct/Arith/ArithMulSign/Lemmas.lean index 4d84a183..e29f3eed 100644 --- a/Smt/Reconstruct/Arith/ArithMulSign/Lemmas.lean +++ b/Smt/Reconstruct/Arith/ArithMulSign/Lemmas.lean @@ -5,8 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Tomaz Gomes Mascarenhas -/ -import Mathlib.Algebra.Parity -import Mathlib.Data.Nat.Parity +import Mathlib.Algebra.Order.Ring.Defs +-- import Mathlib.Algebra.Order.Ring.Nat +-- import Mathlib.Data.Nat.Parity import Mathlib.Data.Real.Basic import Smt.Reconstruct.Arith.MulPosNeg.Lemmas @@ -95,18 +96,18 @@ theorem combineSigns₄ : a < 0 → b < 0 → b * a > 0 := by simp at h exact h -theorem castPos : ∀ (a : Int), a > 0 → Real.intCast.intCast a > 0 := by +theorem castPos : ∀ (a : Int), a > 0 → ↑a > 0 := by intros a h simp [h] -theorem castNeg : ∀ (a : Int), a < 0 → Real.intCast.intCast a < 0 := by +theorem castNeg : ∀ (a : Int), a < 0 → ↑a < 0 := by intros a h simp [h] instance : HMul ℤ ℝ ℝ where - hMul z r := Real.intCast.intCast z * r + hMul z r := ↑z * r instance : HMul ℝ ℤ ℝ where - hMul r z := r * Real.intCast.intCast z + hMul r z := r * ↑z end Smt.Reconstruct.Arith diff --git a/Smt/Reconstruct/Arith/ArithMulSign/Tactic.lean b/Smt/Reconstruct/Arith/ArithMulSign/Tactic.lean index 23ffb76d..075f697a 100644 --- a/Smt/Reconstruct/Arith/ArithMulSign/Tactic.lean +++ b/Smt/Reconstruct/Arith/ArithMulSign/Tactic.lean @@ -7,7 +7,7 @@ Authors: Tomaz Gomes Mascarenhas import Lean -import Mathlib.Data.Nat.Parity +import Mathlib.Algebra.Order.Ring.Nat import Mathlib.Data.Real.Basic import Smt.Reconstruct.Arith.ArithMulSign.Lemmas @@ -24,9 +24,9 @@ inductive Pol where deriving BEq def intLOR := mkApp2 (.const ``LinearOrderedCommRing.toLinearOrderedRing [.zero]) - (.const ``Int []) (.const ``Int.linearOrderedCommRing []) + (.const ``Int []) (.const ``Int.instLinearOrderedCommRing []) -def RealLOR := Expr.const ``Real.instLinearOrderedRingReal [] +def RealLOR := Expr.const ``Real.instLinearOrderedRing [] def traceMulSign (r : Except Exception Unit) : MetaM MessageData := diff --git a/Smt/Reconstruct/Arith/MulPosNeg/Lemmas.lean b/Smt/Reconstruct/Arith/MulPosNeg/Lemmas.lean index 5bac7eb3..10d55003 100644 --- a/Smt/Reconstruct/Arith/MulPosNeg/Lemmas.lean +++ b/Smt/Reconstruct/Arith/MulPosNeg/Lemmas.lean @@ -15,7 +15,7 @@ variable [LinearOrderedRing α] variable {a b c : α} -@[simp] def zToR : Int → Real := Real.intCast.intCast +@[simp] def zToR (i : Int) : Real := ↑i def uncurry {p₁ p₂ p₃ : Prop} : (p₁ → p₂ → p₃) → (p₁ ∧ p₂) → p₃ := by intros h₁ h₂ diff --git a/Smt/Reconstruct/Arith/SumBounds/Tactic.lean b/Smt/Reconstruct/Arith/SumBounds/Tactic.lean index 8c56660b..43415cec 100644 --- a/Smt/Reconstruct/Arith/SumBounds/Tactic.lean +++ b/Smt/Reconstruct/Arith/SumBounds/Tactic.lean @@ -17,7 +17,7 @@ namespace Smt.Reconstruct.Arith open Lean open Meta Elab.Tactic Expr -theorem castEQ : ∀ {a b : Int}, a = b → Real.intCast.intCast a = Real.intCast.intCast b := by +theorem castEQ : ∀ {a b : Int}, a = b → (↑a : Real) = (↑b : Real) := by intros a b h rw [h] diff --git a/Smt/Reconstruct/BitVec.lean b/Smt/Reconstruct/BitVec.lean index dca202d8..fec2dd77 100644 --- a/Smt/Reconstruct/BitVec.lean +++ b/Smt/Reconstruct/BitVec.lean @@ -34,14 +34,14 @@ partial def synthDecidableInst (t : cvc5.Term) : ReconstructM Expr := do match t return q(@instDecidableNot $p $hp) | .AND => rightAssocOpDecidableInst q(And) q(@instDecidableAnd) t | .OR => rightAssocOpDecidableInst q(Or) q(@instDecidableOr) t - | .XOR => rightAssocOpDecidableInst q(XOr) q(@XOr.instDecidableXOr) t + | .XOR => rightAssocOpDecidableInst q(XOr) q(@XOr.instDecidable) t | .EQUAL => if t[0]!.getSort.getKind == .BOOLEAN_SORT then let p : Q(Prop) ← reconstructTerm t[0]! let q : Q(Prop) ← reconstructTerm t[1]! let hp : Q(Decidable $p) ← synthDecidableInst t[0]! let hq : Q(Decidable $q) ← synthDecidableInst t[1]! - return q(@instDecidableEqProp $p $q (@instDecidableIff $p $q $hp $hq)) + return q(@instDecidableEqOfIff $p $q (@instDecidableIff $p $q $hp $hq)) if t[0]!.getSort.getKind == .BITVECTOR_SORT then let w : Nat := t[0]!.getSort.getBitVectorSize.val return q(@instDecidableEqBitVec $w) @@ -275,7 +275,7 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do let mv ← Bool.boolify h.mvarId! let ds := [``BitVec.beq, ``BitVec.beq.go] let ts := [``BitVec.getLsb_cons, ``Nat.succ.injEq] - let ps := [``Nat.reduceAdd, ``Nat.reduceSub, ``Nat.reduceEq, ``reduceIte] + let ps := [``Nat.reduceAdd, ``Nat.reduceSub, ``Nat.reduceEqDiff, ``reduceIte] let simpTheorems ← ds.foldrM (fun n a => a.addDeclToUnfold n) {} let simpTheorems ← ts.foldrM (fun n a => a.addConst n) simpTheorems let simpProcs ← ps.foldrM (fun n a => a.add n false) {} diff --git a/Smt/Reconstruct/Builtin.lean b/Smt/Reconstruct/Builtin.lean index 98cb7744..acc5689c 100644 --- a/Smt/Reconstruct/Builtin.lean +++ b/Smt/Reconstruct/Builtin.lean @@ -38,7 +38,7 @@ def getFVarOrConstExpr! (n : Name) : MetaM Expr := do @[smt_term_reconstruct] def reconstructBuiltin : TermReconstructor := fun t => do match t.getKind with | .VARIABLE => getFVarExpr! (getVariableName t) - | .CONSTANT => getFVarOrConstExpr! t.getSymbol + | .CONSTANT => getFVarOrConstExpr! <| Name.mkSimple t.getSymbol | .EQUAL => let α : Q(Type) ← reconstructSort t[0]!.getSort let x : Q($α) ← reconstructTerm t[0]! @@ -65,7 +65,7 @@ def getFVarOrConstExpr! (n : Name) : MetaM Expr := do | _ => return none where getVariableName (t : cvc5.Term) : Name := - if t.hasSymbol then t.getSymbol else Name.num `x t.getId + if t.hasSymbol then Name.mkSimple t.getSymbol else Name.num `x t.getId def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do match pf.getRewriteRule with diff --git a/Smt/Reconstruct/Prop/Lemmas.lean b/Smt/Reconstruct/Prop/Lemmas.lean index bef550c3..a5d40c5e 100644 --- a/Smt/Reconstruct/Prop/Lemmas.lean +++ b/Smt/Reconstruct/Prop/Lemmas.lean @@ -182,47 +182,56 @@ theorem notNotElim : ∀ {p : Prop}, ¬ ¬ p → p := theorem notNotIntro : ∀ {p : Prop}, p → ¬ ¬ p := λ p np => np p -theorem deMorgan : ∀ {l : List Prop}, ¬ orN (notList l) → andN l := - by intros l h - exact match l with - | [] => True.intro - | [t] => by simp only [andN] - simp only [notList, orN, map] at h - cases Classical.em t with - | inl tt => exact tt - | inr ntt => exact False.elim (h ntt) - | h₁::h₂::t => by simp [orN, notList, map] at h - have ⟨ t₁, t₂ ⟩ := deMorganSmall h - have ih := @deMorgan (h₂::t) t₂ - simp [andN] - have t₁' := notNotElim t₁ - exact ⟨ t₁', ih ⟩ - -theorem deMorgan₂ : ∀ {l : List Prop}, andN l → ¬ orN (notList l) := - by intros l h - exact match l with - | [] => by simp [orN, notList] - | [t] => by simp only [orN, notList]; simp [andN] at h; exact notNotIntro h - | h₁::h₂::t => by simp [orN, notList, map] - simp [andN] at h - apply deMorganSmall₂ - have nnh₁ := notNotIntro (And.left h) - have ih := @deMorgan₂ (h₂::t) (And.right h) - exact ⟨nnh₁, ih⟩ - -theorem deMorgan₃ : ∀ {l : List Prop}, ¬ orN l → andN (notList l) := - by intros l h - exact match l with - | [] => True.intro - | [t] => by simp [andN, notList, map] - simp [orN, Not] at h - exact h - | h₁::h₂::t => by simp [orN, Not] at h - have ⟨t₁, t₂⟩ := deMorganSmall h - simp [orN, Not] at t₂ - simp [andN, notList, map] - have ih := @deMorgan₃ (h₂::t) t₂ - exact ⟨t₁, ih⟩ +theorem deMorgan : ∀ {l : List Prop}, ¬ orN (notList l) → andN l := by + intros l h + exact match l with + | [] => True.intro + | [t] => by + simp only [andN] + simp only [notList, orN, map] at h + cases Classical.em t with + | inl tt => exact tt + | inr ntt => exact False.elim (h ntt) + | h₁::h₂::t => by + simp only [orN, notList, map] at h + have ⟨ t₁, t₂ ⟩ := deMorganSmall h + have ih := @deMorgan (h₂::t) t₂ + simp [andN] + have t₁' := notNotElim t₁ + exact ⟨ t₁', ih ⟩ + +theorem deMorgan₂ : ∀ {l : List Prop}, andN l → ¬ orN (notList l) := by + intros l h + exact match l with + | [] => by + simp [orN, notList] + | [t] => by + simp only [orN, notList] + simp [andN] at h + exact notNotIntro h + | h₁::h₂::t => by + simp only [orN, notList, map] + simp [andN] at h + apply deMorganSmall₂ + have nnh₁ := notNotIntro (And.left h) + have ih := @deMorgan₂ (h₂::t) (And.right h) + exact ⟨nnh₁, ih⟩ + +theorem deMorgan₃ : ∀ {l : List Prop}, ¬ orN l → andN (notList l) := by + intros l h + exact match l with + | [] => True.intro + | [t] => by + simp only [andN, notList, map] + simp only [orN, Not] at h + exact h + | h₁::h₂::t => by + simp only [orN, Not] at h + have ⟨t₁, t₂⟩ := deMorganSmall h + simp only [orN, Not] at t₂ + simp [andN, notList, map] + have ih := @deMorgan₃ (h₂::t) t₂ + exact ⟨t₁, ih⟩ theorem cnfAndNeg' : ∀ (l : List Prop), andN l ∨ orN (notList l) := by intro l @@ -652,7 +661,7 @@ theorem length_eraseIdx (h : i < l.length) : (eraseIdx l i).length = l.length -1 | succ i => simp rw [length_cons, succ_lt_succ_iff] at hi - rw [ih hi, Nat.succ_eq_add_one, Nat.sub_add_cancel (zero_lt_of_lt hi)] + rw [ih hi, Nat.sub_add_cancel (zero_lt_of_lt hi)] theorem take_append (a b : List α) : take a.length (a ++ b) = a := by have H3:= take_append_drop a.length (a ++ b) diff --git a/Smt/Reconstruct/Quant.lean b/Smt/Reconstruct/Quant.lean index bf33318a..8f43297c 100644 --- a/Smt/Reconstruct/Quant.lean +++ b/Smt/Reconstruct/Quant.lean @@ -28,7 +28,7 @@ namespace Smt.Reconstruct.Quant open Lean Qq def getVariableName (t : cvc5.Term) : Name := - if t.hasSymbol then t.getSymbol else Name.num `x t.getId + if t.hasSymbol then Name.mkSimple t.getSymbol else Name.num `x t.getId @[smt_term_reconstruct] def reconstructQuant : TermReconstructor := fun t => do match t.getKind with | .FORALL => diff --git a/Smt/Reconstruct/UF.lean b/Smt/Reconstruct/UF.lean index 8dd07db4..a39bf65f 100644 --- a/Smt/Reconstruct/UF.lean +++ b/Smt/Reconstruct/UF.lean @@ -22,8 +22,10 @@ def getFVarOrConstExpr! (n : Name) : MetaM Expr := do @[smt_sort_reconstruct] def reconstructUS : SortReconstructor := fun s => do match s.getKind with | .INTERNAL_SORT_KIND - | .UNINTERPRETED_SORT => getFVarOrConstExpr! s.getSymbol - | _ => return none + | .UNINTERPRETED_SORT => + Name.mkSimple s.getSymbol + |> getFVarOrConstExpr! + | _ => return none @[smt_term_reconstruct] def reconstructUF : TermReconstructor := fun t => do match t.getKind with | .APPLY_UF => diff --git a/Smt/Tactic/EqnDef.lean b/Smt/Tactic/EqnDef.lean index f7456a6b..07464a1a 100644 --- a/Smt/Tactic/EqnDef.lean +++ b/Smt/Tactic/EqnDef.lean @@ -109,7 +109,7 @@ def addEqnDefWithBody (nm : Name) (e : Expr) : TacticM (FVarId × FVarId) := do -- in the equational definition. let (fvVar, mvarId) ← (← mvarId.define nm tp e).intro1P return (fvVar, [mvarId]) - + let (eqn, pf) ← withMainContext <| lambdaTelescope e fun args body => do let lhs ← mkAppOptM' (mkFVar fvVar) (args.map some) let eqn ← mkEq lhs body @@ -127,7 +127,7 @@ def addEqnDefWithBody (nm : Name) (e : Expr) : TacticM (FVarId × FVarId) := do open Lean Meta Elab Tactic in /-- Place an equational definition for a constant in the local context. -/ elab "extract_def" i:ident : tactic => do - let nm ← resolveGlobalConstNoOverloadWithInfo i + let nm ← Elab.realizeGlobalConstNoOverloadWithInfo i let _ ← addEqnDefForConst nm /-- Specialize an equational definition via partial evaluation. See `specialize_def`. -/ diff --git a/Smt/Tactic/WHNFConfigurable.lean b/Smt/Tactic/WHNFConfigurable.lean index 46d83f74..072dbeb0 100644 --- a/Smt/Tactic/WHNFConfigurable.lean +++ b/Smt/Tactic/WHNFConfigurable.lean @@ -980,7 +980,7 @@ def reduceProjOf? (e : Expr) (p : Name → Bool) : MetaM (Option Expr) := do | _ => pure none private instance [MonadAlwaysExcept ε m] [STWorld ω m] [BEq α] [Hashable α] : MonadAlwaysExcept ε (MonadCacheT α β m) := - instMonadAlwaysExceptStateRefT' ε + instMonadAlwaysExceptStateRefT' partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : ReductionM Expr := let rec visit (e : Expr) : MonadCacheT Expr Expr ReductionM Expr := @@ -1007,7 +1007,7 @@ partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : Redu else args ← args.modifyM i visit if f.isConstOf ``Nat.succ && args.size == 1 && args[0]!.isRawNatLit then - pure <| mkRawNatLit (args[0]!.natLit?.get! + 1) + pure <| mkRawNatLit (args[0]!.nat?.get! + 1) else pure <| mkAppN f args -- `let`-bindings are normally substituted by WHNF, but they are left alone when `zeta` is off, diff --git a/Smt/Translate/Int.lean b/Smt/Translate/Int.lean index 456beb8e..b8d8bc95 100644 --- a/Smt/Translate/Int.lean +++ b/Smt/Translate/Int.lean @@ -19,7 +19,7 @@ open Translator Term | _ => return none @[smt_translate] def translateInt : Translator := fun (e : Q(Int)) => match e with - | ~q(OfNat.ofNat $n) => return if let some n := n.natLit? then literalT (toString n) else none + | ~q(OfNat.ofNat $n) => return if let some n := n.nat? then literalT (toString n) 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) diff --git a/Smt/Translate/Nat.lean b/Smt/Translate/Nat.lean index aab304f6..3a3d767f 100644 --- a/Smt/Translate/Nat.lean +++ b/Smt/Translate/Nat.lean @@ -16,7 +16,7 @@ open Lean Expr open Translator Term @[smt_translate] def translateNat : Translator := fun (e : Q(Nat)) => match e with - | ~q(OfNat.ofNat $n) => return if let some n := n.natLit? then literalT (toString n) else none + | ~q(OfNat.ofNat $n) => return if let some n := n.nat? then literalT (toString n) else none | ~q(.zero) => return literalT "0" | ~q(.succ $n) => return mkApp2 (symbolT "+") (← applyTranslators! n) (literalT "1") | ~q($n + $m) => return mkApp2 (symbolT "+") (← applyTranslators! n) (← applyTranslators! m) diff --git a/Smt/Translate/Real.lean b/Smt/Translate/Real.lean index 77412aab..763748f9 100644 --- a/Smt/Translate/Real.lean +++ b/Smt/Translate/Real.lean @@ -27,7 +27,7 @@ open Translator Term @[smt_translate] def translateReal : Translator := fun (e : Q(Real)) => match e with | ~q((($x : Int) : Real)) => return appT (symbolT "to_real") (← applyTranslators! x) | ~q(@OfNat.ofNat _ _ (@instOfNatAtLeastTwo _ _ _ instNatAtLeastTwo)) => - return if let some n := (e.getArg! 1).natLit? then literalT s!"{n}.0" else none + return if let some n := (e.getArg! 1).nat? then literalT s!"{n}.0" else none | ~q(0) => return (literalT "0.0") | ~q(1) => return (literalT "1.0") | ~q(-$x) => return appT (symbolT "-") (← applyTranslators! x) diff --git a/lake-manifest.json b/lake-manifest.json index 0c1fe6bc..d9029a9f 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,20 +1,20 @@ {"version": 7, "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/abdoo8080/lean-cvc5.git", + [{"url": "https://github.com/anzenlang/lean-cvc5.git", "type": "git", "subDir": null, - "rev": "00acb97db0bb56c3e8b5fedf2d564e3be444a65e", + "rev": "5c18f7fe381143b62ef9d809b52214405cdc7c9e", "name": "cvc5", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.8.0", "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/std4", + {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a", - "name": "std", + "rev": "551ff2d7dffd7af914cdbd01abbd449fe3e3d428", + "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "64365c656d5e1bffa127d2a1795f471529ee0178", + "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -31,25 +31,25 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79", + "rev": "53ba96ad7666d4a2515292974631629b5ea5dfee", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8", + "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.30", + "inputRev": "v0.0.36", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5", + "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,19 +58,19 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662", + "rev": "77e081815b30b0d30707e1c5b0c6a6761f7a2404", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "a45ae63747140c1b2cbad9d46f518015c047047a", + "rev": "b5eba595428809e96f3ed113bc7ba776c5f801ac", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.7.0", + "inputRev": "v4.8.0", "inherited": false, "configFile": "lakefile.lean"}], "name": "smt", diff --git a/lakefile.lean b/lakefile.lean index 87d80634..575fad46 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,11 +2,11 @@ import Lake open Lake DSL -require cvc5 from git - "https://github.com/abdoo8080/lean-cvc5.git" @ "main" +require cvc5 from + git "https://github.com/anzenlang/lean-cvc5.git" @ "v4.8.0" require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" @ "v4.7.0" + "https://github.com/leanprover-community/mathlib4.git" @ "v4.8.0" def libcpp : String := if System.Platform.isWindows then "libstdc++-6.dll" diff --git a/lean-toolchain b/lean-toolchain index 9ad30404..ef1f67e9 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.7.0 +leanprover/lean4:v4.8.0 From 6cd626ec05b457159e1e7ccf476c17d6809fd228 Mon Sep 17 00:00:00 2001 From: Adrien Champion Date: Tue, 11 Jun 2024 12:00:33 +0200 Subject: [PATCH 02/11] chore: revert `lean-cvc5` dependency --- lakefile.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lakefile.lean b/lakefile.lean index 575fad46..9a3ffbeb 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -3,7 +3,7 @@ import Lake open Lake DSL require cvc5 from - git "https://github.com/anzenlang/lean-cvc5.git" @ "v4.8.0" + git "https://github.com/abdoo8080/lean-cvc5.git" require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.8.0" From 73cbf0b9864bcbc03e4cea261f82f6b76eb0f30e Mon Sep 17 00:00:00 2001 From: Adrien Champion Date: Tue, 11 Jun 2024 14:55:02 +0200 Subject: [PATCH 03/11] chore: apply PR review Co-authored-by: Abdalrhman Mohamed --- Smt/Reconstruct/Builtin.lean | 2 +- Smt/Reconstruct/UF.lean | 4 +--- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/Smt/Reconstruct/Builtin.lean b/Smt/Reconstruct/Builtin.lean index acc5689c..a1a19ed1 100644 --- a/Smt/Reconstruct/Builtin.lean +++ b/Smt/Reconstruct/Builtin.lean @@ -38,7 +38,7 @@ def getFVarOrConstExpr! (n : Name) : MetaM Expr := do @[smt_term_reconstruct] def reconstructBuiltin : TermReconstructor := fun t => do match t.getKind with | .VARIABLE => getFVarExpr! (getVariableName t) - | .CONSTANT => getFVarOrConstExpr! <| Name.mkSimple t.getSymbol + | .CONSTANT => getFVarOrConstExpr! (Name.mkSimple t.getSymbol) | .EQUAL => let α : Q(Type) ← reconstructSort t[0]!.getSort let x : Q($α) ← reconstructTerm t[0]! diff --git a/Smt/Reconstruct/UF.lean b/Smt/Reconstruct/UF.lean index a39bf65f..f5b5f9be 100644 --- a/Smt/Reconstruct/UF.lean +++ b/Smt/Reconstruct/UF.lean @@ -22,9 +22,7 @@ def getFVarOrConstExpr! (n : Name) : MetaM Expr := do @[smt_sort_reconstruct] def reconstructUS : SortReconstructor := fun s => do match s.getKind with | .INTERNAL_SORT_KIND - | .UNINTERPRETED_SORT => - Name.mkSimple s.getSymbol - |> getFVarOrConstExpr! + | .UNINTERPRETED_SORT => getFVarOrConstExpr! (Name.mkSimple s.getSymbol) | _ => return none @[smt_term_reconstruct] def reconstructUF : TermReconstructor := fun t => do match t.getKind with From d0f2daec77ef04e46ccff16b74d9719a3fa45c23 Mon Sep 17 00:00:00 2001 From: Adrien Champion Date: Tue, 11 Jun 2024 16:50:01 +0200 Subject: [PATCH 04/11] chore: ignore macos trash files --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 34f949aa..fd4fa84b 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ /.vscode /.lake +.DS_Store From f94d4f7347de0b557b6c7ac5664ea88e98c75f63 Mon Sep 17 00:00:00 2001 From: Adrien Champion Date: Tue, 11 Jun 2024 16:52:40 +0200 Subject: [PATCH 05/11] chore: homogeneous lakefile requires --- lakefile.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 9a3ffbeb..0eb638fd 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -5,8 +5,8 @@ open Lake DSL require cvc5 from git "https://github.com/abdoo8080/lean-cvc5.git" -require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" @ "v4.8.0" +require mathlib from + git "https://github.com/leanprover-community/mathlib4.git" @ "v4.8.0" def libcpp : String := if System.Platform.isWindows then "libstdc++-6.dll" From 6cb1c513501cb276ddcfc32b7cc452cf81726034 Mon Sep 17 00:00:00 2001 From: Adrien Champion Date: Tue, 11 Jun 2024 16:56:19 +0200 Subject: [PATCH 06/11] chore: bump tests to 4.8 --- Test/EqnDef/Extract.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/EqnDef/Extract.lean b/Test/EqnDef/Extract.lean index acf1ad44..3a16e882 100644 --- a/Test/EqnDef/Extract.lean +++ b/Test/EqnDef/Extract.lean @@ -2,7 +2,7 @@ import Smt open Lean Meta Elab Tactic in elab "extract_def" i:ident : tactic => do - let nm ← resolveGlobalConstNoOverloadWithInfo i + let nm ← Elab.realizeGlobalConstNoOverloadWithInfo i let _ ← Smt.addEqnDefForConst nm def foo : Int := 10 From bef4fe37ad5e8be8b18423d81d66cc92e17557cd Mon Sep 17 00:00:00 2001 From: Adrien Champion Date: Tue, 11 Jun 2024 17:01:33 +0200 Subject: [PATCH 07/11] chore: cvc5 dependency --- lake-manifest.json | 6 +++--- lakefile.lean | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index d9029a9f..0bf1bf8d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,13 +1,13 @@ {"version": 7, "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/anzenlang/lean-cvc5.git", + [{"url": "https://github.com/abdoo8080/lean-cvc5.git", "type": "git", "subDir": null, - "rev": "5c18f7fe381143b62ef9d809b52214405cdc7c9e", + "rev": "1088ef5027ca324c83b13bee1d5eb5e3d27e8ce4", "name": "cvc5", "manifestFile": "lake-manifest.json", - "inputRev": "v4.8.0", + "inputRev": "main", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/batteries", diff --git a/lakefile.lean b/lakefile.lean index 0eb638fd..79fe60e9 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" + git "https://github.com/abdoo8080/lean-cvc5.git" @ "main" require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.8.0" From dd1d818cf580ea543cf08bb0eb311ad250ddf52d Mon Sep 17 00:00:00 2001 From: Adrien Champion Date: Wed, 12 Jun 2024 08:31:40 +0200 Subject: [PATCH 08/11] fix: bumping more files to 4.8 --- Smt/Reconstruct/Arith/ArithMulSign/Tactic.lean | 2 +- Smt/Reconstruct/Arith/MulPosNeg/Tactic.lean | 3 ++- Smt/Reconstruct/Arith/TransFns/ArithTransPi.lean | 10 +++++++--- Smt/Tactic/Concretize.lean | 9 ++++++--- 4 files changed, 16 insertions(+), 8 deletions(-) diff --git a/Smt/Reconstruct/Arith/ArithMulSign/Tactic.lean b/Smt/Reconstruct/Arith/ArithMulSign/Tactic.lean index 075f697a..6b3448fc 100644 --- a/Smt/Reconstruct/Arith/ArithMulSign/Tactic.lean +++ b/Smt/Reconstruct/Arith/ArithMulSign/Tactic.lean @@ -181,7 +181,7 @@ where | _ => throwError "[arithMulSign]: unexpected type for expression" let lorInst := if exprIsInt then intLOR else RealLOR let zeroI := mkApp (mkConst ``Int.ofNat) (mkNatLit 0) - let zeroR ← mkAppOptM' (.const ``OfNat.ofNat [.zero]) #[mkConst ``Real, (mkNatLit 0), none] + let zeroR ← mkAppOptM ``OfNat.ofNat #[mkConst ``Real, (mkNatLit 0), none] -- zero with the same type as the current argument let currZero := if exprIsInt then zeroI else zeroR let bindedType: Expr ← diff --git a/Smt/Reconstruct/Arith/MulPosNeg/Tactic.lean b/Smt/Reconstruct/Arith/MulPosNeg/Tactic.lean index a6af2153..737cd6ee 100644 --- a/Smt/Reconstruct/Arith/MulPosNeg/Tactic.lean +++ b/Smt/Reconstruct/Arith/MulPosNeg/Tactic.lean @@ -63,7 +63,8 @@ def arithMulMeta (va vb vc : Expr) (pos : Bool) (compId : Nat) (thms : List Name else throwError "[arithMul]: index too large" let zeroI := mkApp (mkConst ``Int.ofNat) (mkNatLit 0) - let zeroR ← mkAppOptM' (.const ``OfNat.ofNat [.zero]) #[mkConst ``Real, (mkNatLit 0), none] + let zeroR ← + mkAppOptM ``OfNat.ofNat #[mkConst ``Real, (mkNatLit 0), none] let zeroC := if typeC == mkConst ``Int then zeroI else zeroR let premiseLeft ← if pos then mkAppM ``LT.lt #[zeroC, vc] diff --git a/Smt/Reconstruct/Arith/TransFns/ArithTransPi.lean b/Smt/Reconstruct/Arith/TransFns/ArithTransPi.lean index c7d0d16d..13027884 100644 --- a/Smt/Reconstruct/Arith/TransFns/ArithTransPi.lean +++ b/Smt/Reconstruct/Arith/TransFns/ArithTransPi.lean @@ -25,16 +25,20 @@ open Elab Tactic Meta open Real def expr_3141592 : Expr := - mkApp5 (Expr.const ``OfScientific.ofScientific [Level.zero]) (mkConst ``Rat) (Lean.Expr.const `Rat.instOfScientificRat []) (.lit (.natVal 3141592)) (mkConst ``Bool.true) (.lit (.natVal 6)) + mkApp5 (Expr.const ``OfScientific.ofScientific [Level.zero]) + (mkConst ``Rat) (Lean.Expr.const `Rat.instOfScientific []) + (.lit (.natVal 3141592)) (mkConst ``Bool.true) (.lit (.natVal 6)) def expr_3141593 : Expr := - mkApp5 (Expr.const ``OfScientific.ofScientific [Level.zero]) (mkConst ``Rat) (Lean.Expr.const `Rat.instOfScientificRat []) (.lit (.natVal 3141593)) (mkConst ``Bool.true) (.lit (.natVal 6)) + mkApp5 (Expr.const ``OfScientific.ofScientific [Level.zero]) + (mkConst ``Rat) (Lean.Expr.const `Rat.instOfScientific []) + (.lit (.natVal 3141593)) (mkConst ``Bool.true) (.lit (.natVal 6)) def ratCast_lt_mpr {x y : ℚ} : x < y → (x : ℝ) < (y : ℝ) := ratCast_lt.mpr def ratOfFloat : Expr → Expr | .app (.app (.app (.app (.app a _) _) d) e) f => - .app (.app (.app (.app (.app a (mkConst ``Rat)) (mkConst ``Rat.instOfScientificRat)) d) e) f + .app (.app (.app (.app (.app a (mkConst ``Rat)) (mkConst ``Rat.instOfScientific)) d) e) f | e => e def isOfNatNatLit : Expr → Bool diff --git a/Smt/Tactic/Concretize.lean b/Smt/Tactic/Concretize.lean index f6ffbb20..1a4b5222 100644 --- a/Smt/Tactic/Concretize.lean +++ b/Smt/Tactic/Concretize.lean @@ -77,7 +77,10 @@ def Location.simpRwAt (loc : Location) (pf : Expr) : TacticM Unit := do } _ ← Tactic.simpLocation ctx #[] (loc := loc.toTacticLocation) let { ctx, .. } ← mkSimpContext Syntax.missing (eraseLocal := false) (kind := .dsimp) - Tactic.dsimpLocation { ctx with config := { ctx.config with failIfUnchanged := false } } (loc := loc.toTacticLocation) + Tactic.dsimpLocation + { ctx with config := { ctx.config with failIfUnchanged := false } } + (loc := loc.toTacticLocation) + (simprocs := #[]) end Lean.Meta @@ -209,7 +212,7 @@ def concretizeApp (e : Expr) : ConcretizeM TransformStep := do for (pi, a) in info.paramInfo.zip args do let argTp ← inferType a -- TODO: This has good results but might be expensive. - let a' := if !pi.isInstImplicit then ← whnf a else a + let a' ← if !pi.isInstImplicit then whnf a else pure a let isConcretizable := !a'.hasLooseBVars ∧ !a'.hasFVar ∧ (argTp.isType ∨ pi.hasFwdDeps ∨ pi.isInstImplicit) if isConcretizable then @@ -347,7 +350,7 @@ The Coq variant is in `snipe`: - https://github.com/smtcoq/sniper/blob/af7b0d22f496f8e7a0ee6ca495314d80ea2aa881/theories/elimination_polymorphism.v -/ elab "concretize" "[" nms:ident,* "]" : tactic => do - let nms ← (nms : Array Syntax).mapM resolveGlobalConstNoOverloadWithInfo + let nms ← (nms : Array Syntax).mapM (liftM $ Elab.realizeGlobalConstNoOverloadWithInfo ·) let concretizeSet := nms.foldl (init := .empty) (NameSet.insert · ·) evalConcretize |>.run' { visitSet := #[.goal] } From 805fc23361d1650014e898829dc3ec989c37d5b9 Mon Sep 17 00:00:00 2001 From: Adrien Champion Date: Wed, 12 Jun 2024 10:13:59 +0200 Subject: [PATCH 09/11] fix: use `rawNatLit?` not `nat?` on `Lean.expr` --- Smt/Tactic/WHNFConfigurable.lean | 2 +- Smt/Translate/Int.lean | 2 +- Smt/Translate/Nat.lean | 2 +- Smt/Translate/Real.lean | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Smt/Tactic/WHNFConfigurable.lean b/Smt/Tactic/WHNFConfigurable.lean index 072dbeb0..e8a04728 100644 --- a/Smt/Tactic/WHNFConfigurable.lean +++ b/Smt/Tactic/WHNFConfigurable.lean @@ -1007,7 +1007,7 @@ partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : Redu else args ← args.modifyM i visit if f.isConstOf ``Nat.succ && args.size == 1 && args[0]!.isRawNatLit then - pure <| mkRawNatLit (args[0]!.nat?.get! + 1) + pure <| mkRawNatLit (args[0]!.rawNatLit?.get! + 1) else pure <| mkAppN f args -- `let`-bindings are normally substituted by WHNF, but they are left alone when `zeta` is off, diff --git a/Smt/Translate/Int.lean b/Smt/Translate/Int.lean index b8d8bc95..ee680b27 100644 --- a/Smt/Translate/Int.lean +++ b/Smt/Translate/Int.lean @@ -19,7 +19,7 @@ open Translator Term | _ => return none @[smt_translate] def translateInt : Translator := fun (e : Q(Int)) => match e with - | ~q(OfNat.ofNat $n) => return if let some n := n.nat? then literalT (toString n) else none + | ~q(OfNat.ofNat $n) => return if let some n := n.rawNatLit? then literalT (toString n) 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) diff --git a/Smt/Translate/Nat.lean b/Smt/Translate/Nat.lean index 3a3d767f..26d88dd3 100644 --- a/Smt/Translate/Nat.lean +++ b/Smt/Translate/Nat.lean @@ -16,7 +16,7 @@ open Lean Expr open Translator Term @[smt_translate] def translateNat : Translator := fun (e : Q(Nat)) => match e with - | ~q(OfNat.ofNat $n) => return if let some n := n.nat? then literalT (toString n) else none + | ~q(OfNat.ofNat $n) => return if let some n := n.rawNatLit? then literalT (toString n) else none | ~q(.zero) => return literalT "0" | ~q(.succ $n) => return mkApp2 (symbolT "+") (← applyTranslators! n) (literalT "1") | ~q($n + $m) => return mkApp2 (symbolT "+") (← applyTranslators! n) (← applyTranslators! m) diff --git a/Smt/Translate/Real.lean b/Smt/Translate/Real.lean index 763748f9..b1abaaee 100644 --- a/Smt/Translate/Real.lean +++ b/Smt/Translate/Real.lean @@ -27,7 +27,7 @@ open Translator Term @[smt_translate] def translateReal : Translator := fun (e : Q(Real)) => match e with | ~q((($x : Int) : Real)) => return appT (symbolT "to_real") (← applyTranslators! x) | ~q(@OfNat.ofNat _ _ (@instOfNatAtLeastTwo _ _ _ instNatAtLeastTwo)) => - return if let some n := (e.getArg! 1).nat? then literalT s!"{n}.0" else none + return if let some n := (e.getArg! 1).rawNatLit? then literalT s!"{n}.0" else none | ~q(0) => return (literalT "0.0") | ~q(1) => return (literalT "1.0") | ~q(-$x) => return appT (symbolT "-") (← applyTranslators! x) From f9c4fcbed7afb9ee67df4a1c998f1db629b7936c Mon Sep 17 00:00:00 2001 From: Adrien Champion Date: Wed, 12 Jun 2024 10:23:47 +0200 Subject: [PATCH 10/11] chore: update test expected outputs --- Test/BitVec/Shift.expected | 2 +- Test/BitVec/XorComm.expected | 2 +- Test/Bool/Assoc.expected | 2 +- Test/Bool/Comm.expected | 2 +- Test/Bool/Cong.expected | 4 +- Test/Bool/PropExt.expected | 2 +- Test/Bool/Symm.expected | 2 +- Test/Bool/Trans.expected | 4 +- Test/Int/Binders.expected | 2 +- Test/Int/DefineSort.expected | 2 +- Test/Int/Dvd.expected | 4 +- Test/Int/DvdTimeout.expected | 2 +- Test/Int/Let.expected | 2 +- Test/Int/Neg.expected | 3 +- Test/Nat/Cong.expected | 2 +- Test/Nat/Max.expected | 12 +++--- Test/Nat/Sum'.expected | 4 +- Test/Nat/Triv.expected | 2 +- Test/Nat/ZeroSub'.expected | 2 +- .../Arith/ArithMulSign.expected | 25 ++++++----- Test/Reconstruction/Arith/SumBounds.expected | 4 +- Test/Reconstruction/Arith/TightBounds.lean | 6 +-- Test/Reconstruction/Factor.expected | 40 ++++++++++++++++++ Test/Reconstruction/LiftOrNToNeg.expected | 10 +++++ Test/Reconstruction/Resolution.expected | 42 +++++++++++++++++++ Test/String/Contains.expected | 2 +- Test/String/Length.expected | 4 +- Test/String/Replace.expected | 2 +- Test/linarith.expected | 31 +++++++++----- 29 files changed, 165 insertions(+), 58 deletions(-) diff --git a/Test/BitVec/Shift.expected b/Test/BitVec/Shift.expected index 88005d8d..e73ada1d 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 x (_ BitVec 3)) (declare-const y (_ BitVec 3)) +(declare-const x (_ 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/BitVec/XorComm.expected b/Test/BitVec/XorComm.expected index 4a526c8e..9d49feaf 100644 --- a/Test/BitVec/XorComm.expected +++ b/Test/BitVec/XorComm.expected @@ -9,8 +9,8 @@ Test/BitVec/XorComm.lean:3:8: warning: declaration uses 'sorry' goal: x ^^^ y = y ^^^ x query: -(declare-const x (_ BitVec 8)) (declare-const y (_ BitVec 8)) +(declare-const x (_ 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 a3e3474f..977c0696 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-const q Bool) (declare-fun f (Bool Bool) Bool) (declare-const p Bool) (declare-const r Bool) +(declare-const q 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 368f1f85..3260a0a6 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 bfb05ad6..fa6550a3 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-const q Bool) -(declare-const p Bool) (declare-fun f (Bool) Bool) +(declare-const p Bool) +(declare-const q Bool) (assert (not (=> (= (= p q) true) (= (= (f p) (f q)) true)))) (check-sat) diff --git a/Test/Bool/PropExt.expected b/Test/Bool/PropExt.expected index 1b077583..0869af7c 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 p Bool) (declare-const q Bool) +(declare-const p Bool) (assert (not (=> (= (= p true) (= q true)) (= (= p q) true)))) (check-sat) diff --git a/Test/Bool/Symm.expected b/Test/Bool/Symm.expected index 63cedce5..11294ebf 100644 --- a/Test/Bool/Symm.expected +++ b/Test/Bool/Symm.expected @@ -1,7 +1,7 @@ goal: (p == q) = true → (q == p) = true query: -(declare-const p Bool) (declare-const q Bool) +(declare-const p Bool) (assert (not (=> (= (= p q) true) (= (= q p) true)))) (check-sat) diff --git a/Test/Bool/Trans.expected b/Test/Bool/Trans.expected index 3d07089c..10ceea0a 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 r 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/Binders.expected b/Test/Int/Binders.expected index b2777836..7f2fd0ed 100644 --- a/Test/Int/Binders.expected +++ b/Test/Int/Binders.expected @@ -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/DefineSort.expected b/Test/Int/DefineSort.expected index b9538500..9c64cdd6 100644 --- a/Test/Int/DefineSort.expected +++ b/Test/Int/DefineSort.expected @@ -1,4 +1,4 @@ -goal: MyInt.add a b = MyInt.add b a +goal: a.add b = b.add a query: (define-sort MyInt () Int) diff --git a/Test/Int/Dvd.expected b/Test/Int/Dvd.expected index 3eee65e4..4311b71b 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 b Int) (declare-const c Int) +(declare-const b 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 d Int) (declare-const e Int) +(declare-const d 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 377898d8..6987110f 100644 --- a/Test/Int/DvdTimeout.expected +++ b/Test/Int/DvdTimeout.expected @@ -1,8 +1,8 @@ goal: dvd a (b + c + d) = true query: -(declare-fun dvd (Int Int) Bool) (declare-const d Int) +(declare-fun dvd (Int Int) Bool) (declare-const a Int) (assert (= (dvd a d) true)) (declare-const c Int) diff --git a/Test/Int/Let.expected b/Test/Int/Let.expected index 707f7fd9..41d47ec4 100644 --- a/Test/Int/Let.expected +++ b/Test/Int/Let.expected @@ -45,7 +45,7 @@ goal: z 3 = 10 query: (declare-fun f (Int) Int) -(define-fun z ((x._@.Test.Int.Let._hyg.283 Int)) Int (f 10)) +(define-fun z ((x._@.Test.Int.Let._hyg.293 Int)) Int (f 10)) (assert (= (f 10) 10)) (assert (distinct (z 3) 10)) (check-sat) diff --git a/Test/Int/Neg.expected b/Test/Int/Neg.expected index 3c17196e..a21133d4 100644 --- a/Test/Int/Neg.expected +++ b/Test/Int/Neg.expected @@ -5,4 +5,5 @@ query: (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 [linter.unnecessarySeqFocus] +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/Nat/Cong.expected b/Test/Nat/Cong.expected index c8a2f20b..7fe03f72 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.1765 Nat)) (=> (>= _uniq.1765 0) (>= (f _uniq.1765) 0)))) +(assert (forall ((_uniq.1827 Nat)) (=> (>= _uniq.1827 0) (>= (f _uniq.1827) 0)))) (declare-const x Nat) (assert (>= x 0)) (declare-const y Nat) diff --git a/Test/Nat/Max.expected b/Test/Nat/Max.expected index ef131aec..c0cab591 100644 --- a/Test/Nat/Max.expected +++ b/Test/Nat/Max.expected @@ -1,24 +1,24 @@ -goal: x ≤ max' x y ∧ y ≤ max' x y +goal: x ≤ x.max' y ∧ y ≤ x.max' y query: (define-sort Nat () Int) (declare-fun |Nat.max'| (Nat Nat) Nat) -(assert (forall ((_uniq.2574 Nat)) (=> (>= _uniq.2574 0) (forall ((_uniq.2575 Nat)) (=> (>= _uniq.2575 0) (>= (|Nat.max'| _uniq.2574 _uniq.2575) 0)))))) +(assert (forall ((_uniq.2660 Nat)) (=> (>= _uniq.2660 0) (forall ((_uniq.2661 Nat)) (=> (>= _uniq.2661 0) (>= (|Nat.max'| _uniq.2660 _uniq.2661) 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 ≤ max' x y ∧ y ≤ max' x y +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.6062 Nat)) (=> (>= _uniq.6062 0) (forall ((_uniq.6063 Nat)) (=> (>= _uniq.6063 0) (>= (|Nat.max'| _uniq.6062 _uniq.6063) 0)))))) -(declare-const x Nat) -(assert (>= x 0)) +(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)) +(declare-const x Nat) +(assert (>= x 0)) (assert (not (and (<= x (|Nat.max'| x y)) (<= y (|Nat.max'| x y))))) (check-sat) diff --git a/Test/Nat/Sum'.expected b/Test/Nat/Sum'.expected index daa74b34..9e1da1db 100644 --- a/Test/Nat/Sum'.expected +++ b/Test/Nat/Sum'.expected @@ -1,12 +1,12 @@ Test/Nat/Sum'.lean:7:12: error: [arithPolyNorm]: could not prove 0 + sum 0 = sum 0 -goal: sum (Nat.succ n) = Nat.succ n * (Nat.succ n + 1) / 2 +goal: sum (n + 1) = (n + 1) * (n + 1 + 1) / 2 query: (define-sort Nat () Int) (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.23999 Nat)) (=> (>= _uniq.23999 0) (>= (sum _uniq.23999) 0)))) +(assert (forall ((_uniq.16982 Nat)) (=> (>= _uniq.16982 0) (>= (sum _uniq.16982) 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/Triv.expected b/Test/Nat/Triv.expected index 16bc0715..6e1275ca 100644 --- a/Test/Nat/Triv.expected +++ b/Test/Nat/Triv.expected @@ -1,4 +1,4 @@ -goal: Nat.zero + Nat.succ Nat.zero = Nat.succ Nat.zero +goal: Nat.zero + Nat.zero.succ = Nat.zero.succ query: (assert (distinct (+ 0 1) (+ 0 1))) diff --git a/Test/Nat/ZeroSub'.expected b/Test/Nat/ZeroSub'.expected index 77fd6f3c..7484093c 100644 --- a/Test/Nat/ZeroSub'.expected +++ b/Test/Nat/ZeroSub'.expected @@ -1,7 +1,7 @@ Test/Nat/ZeroSub'.lean:6:12: error: tactic 'assumption' failed case zero _uniq✝⁵⁵³⁻⁰ : ¬Smt.Reconstruct.Builtin.distinct [0, 0] -⊢ ¬Smt.Reconstruct.andN' [] ¬0 - Nat.zero = 0 +⊢ ¬Smt.Reconstruct.andN' [] ¬0 - 0 = 0 Test/Nat/ZeroSub'.lean:7:17: error: application type mismatch HAdd.hAdd x argument diff --git a/Test/Reconstruction/Arith/ArithMulSign.expected b/Test/Reconstruction/Arith/ArithMulSign.expected index 23d01cc5..e18aae01 100644 --- a/Test/Reconstruction/Arith/ArithMulSign.expected +++ b/Test/Reconstruction/Arith/ArithMulSign.expected @@ -1,35 +1,38 @@ Test/Reconstruction/Arith/ArithMulSign.lean:6:2: error: type mismatch - _uniq.410 + _uniq.436 has type a + 3 > Int.ofNat 0 → (a + 3) ^ 2 > 0 : Prop but is expected to have type a + 3 > 0 → (a + 3) ^ 2 > 0 : Prop Test/Reconstruction/Arith/ArithMulSign.lean:12:2: error: application type mismatch - combineSigns₃ (powNegOdd _uniq.1721 (Nat.odd_iff.mpr rfl)) (powPos _uniq.1693) + combineSigns₃ (powNegOdd _uniq.1842 (Nat.odd_iff.mpr rfl)) (powPos _uniq.1813) argument - powPos _uniq.1693 + powPos _uniq.1813 has type a ^ 2 > 0 : Prop but is expected to have type Pow.pow a 2 > 0 : Prop Test/Reconstruction/Arith/ArithMulSign.lean:21:2: error: application type mismatch - combineSigns₂ (powPos _uniq.3314) + combineSigns₂ (powPos _uniq.3537) argument - powPos _uniq.3314 + powPos _uniq.3537 has type b ^ 2 > 0 : Prop but is expected to have type Pow.pow b 2 > 0 : Prop -Test/Reconstruction/Arith/ArithMulSign.lean:24:2: error: type mismatch - _uniq.5807 +Test/Reconstruction/Arith/ArithMulSign.lean:24:2: error: application type mismatch + combineSigns₄ (powNegOdd _uniq.6270 (Nat.odd_iff.mpr rfl)) + (castNeg (Pow.pow a 3) (powNegOdd _uniq.6211 (Nat.odd_iff.mpr rfl))) +argument + castNeg (Pow.pow a 3) (powNegOdd _uniq.6211 (Nat.odd_iff.mpr rfl)) has type - a < Int.ofNat 0 → b < OfNat.ofNat 0 → zToR (Pow.pow a 3) * Pow.pow b 3 > 0 : Prop + Pow.pow a 3 < 0 : Prop but is expected to have type - a < 0 → b < 0 → ↑a ^ 3 * b ^ 3 > 0 : Prop + zToR (Pow.pow a 3) < 0 : Prop Test/Reconstruction/Arith/ArithMulSign.lean:33:2: error: application type mismatch - combineSigns₂ (powPos _uniq.8568) + combineSigns₂ (powPos _uniq.9015) argument - powPos _uniq.8568 + powPos _uniq.9015 has type b ^ 2 > 0 : Prop but is expected to have type diff --git a/Test/Reconstruction/Arith/SumBounds.expected b/Test/Reconstruction/Arith/SumBounds.expected index 997019b4..fe8df328 100644 --- a/Test/Reconstruction/Arith/SumBounds.expected +++ b/Test/Reconstruction/Arith/SumBounds.expected @@ -13,9 +13,9 @@ has type but is expected to have type a + (b + (c + w)) ≤ d + (e + (f + z)) : Prop Test/Reconstruction/Arith/SumBounds.lean:16:2: error: type mismatch - _uniq.1532 + _uniq.1647 has type - c + b + IntCast.intCast a < f + e + IntCast.intCast d : Prop + c + b + ↑a < f + e + ↑d : Prop but is expected to have type ↑a + (b + c) < ↑d + (e + f) : Prop Test/Reconstruction/Arith/SumBounds.lean:20:2: error: application type mismatch diff --git a/Test/Reconstruction/Arith/TightBounds.lean b/Test/Reconstruction/Arith/TightBounds.lean index cfc9d475..64893b39 100644 --- a/Test/Reconstruction/Arith/TightBounds.lean +++ b/Test/Reconstruction/Arith/TightBounds.lean @@ -2,14 +2,14 @@ import Smt.Reconstruct.Arith open Smt.Reconstruct.Arith -example {a b : Int} : a < b → (a : Int) ≤ Int.ceil (Real.intCast.intCast b) - 1 := by +example {a b : Int} : a < b → (a : Int) ≤ Int.ceil (Real.instIntCast.intCast b) - 1 := by intro h intTightUb h -example {a : Int} : Real.intCast.intCast a < (7.2 : Real) → a ≤ Int.ceil (7.2 : Real) - 1 := by +example {a : Int} : Real.instIntCast.intCast a < (7.2 : Real) → a ≤ Int.ceil (7.2 : Real) - 1 := by intro h intTightUb h -example {a b : Int} : a > b → (a : Int) ≥ Int.floor (Real.intCast.intCast b) + 1 := by +example {a b : Int} : a > b → (a : Int) ≥ Int.floor (Real.instIntCast.intCast b) + 1 := by intro h intTightLb h diff --git a/Test/Reconstruction/Factor.expected b/Test/Reconstruction/Factor.expected index e69de29b..3c7bcd62 100644 --- a/Test/Reconstruction/Factor.expected +++ b/Test/Reconstruction/Factor.expected @@ -0,0 +1,40 @@ +Test/Reconstruction/Factor.lean:7:3: error: unknown tactic +Test/Reconstruction/Factor.lean:5:39: error: unsolved goals +A B C : Prop +h : A ∨ B ∨ C ∨ B +⊢ A ∨ B ∨ C +Test/Reconstruction/Factor.lean:11:3: error: unknown tactic +Test/Reconstruction/Factor.lean:9:31: error: unsolved goals +A B : Prop +h : A ∨ B ∨ B +⊢ A ∨ B +Test/Reconstruction/Factor.lean:15:6: error: unknown tactic +Test/Reconstruction/Factor.lean:14:2: error: unsolved goals +A B C : Prop +h : A ∨ A ∨ A ∨ A ∨ B ∨ A ∨ B ∨ A ∨ C ∨ B ∨ C ∨ B ∨ A +⊢ A ∨ B ∨ C +Test/Reconstruction/Factor.lean:19:3: error: unknown tactic +Test/Reconstruction/Factor.lean:17:61: error: unsolved goals +A B C D : Prop +h : (A ∨ B) ∨ C ∨ D ∨ C ∨ A ∨ B +⊢ (A ∨ B) ∨ C ∨ D +Test/Reconstruction/Factor.lean:23:3: error: unknown tactic +Test/Reconstruction/Factor.lean:21:51: error: unsolved goals +A B C : Prop +h : (A ∨ B ∨ C) ∨ A ∨ B ∨ C +⊢ A ∨ B ∨ C +Test/Reconstruction/Factor.lean:28:6: error: unknown tactic +Test/Reconstruction/Factor.lean:27:2: error: unsolved goals +A B E F : Prop +h : A ∨ B ∨ (E ∨ F) ∨ A ∨ B ∨ E ∨ F +⊢ A ∨ B ∨ E ∨ F +Test/Reconstruction/Factor.lean:33:6: error: unknown tactic +Test/Reconstruction/Factor.lean:32:2: error: unsolved goals +A B C E F : Prop +h : (A ∨ B ∨ C) ∨ (E ∨ F) ∨ (A ∨ B ∨ C) ∨ E ∨ F +⊢ (A ∨ B ∨ C) ∨ E ∨ F +Test/Reconstruction/Factor.lean:37:3: error: unknown tactic +Test/Reconstruction/Factor.lean:35:61: error: unsolved goals +A B C D : Prop +h : (A ∨ B) ∨ C ∨ D ∨ C ∨ A ∨ B +⊢ (A ∨ B) ∨ C ∨ D diff --git a/Test/Reconstruction/LiftOrNToNeg.expected b/Test/Reconstruction/LiftOrNToNeg.expected index e69de29b..f7725502 100644 --- a/Test/Reconstruction/LiftOrNToNeg.expected +++ b/Test/Reconstruction/LiftOrNToNeg.expected @@ -0,0 +1,10 @@ +Test/Reconstruction/LiftOrNToNeg.lean:7:3: error: unknown tactic +Test/Reconstruction/LiftOrNToNeg.lean:5:51: error: unsolved goals +A B C : Prop +h : ¬A ∨ B ∨ ¬C ∨ False +⊢ ¬A ∨ B ∨ ¬C +Test/Reconstruction/LiftOrNToNeg.lean:11:3: error: unknown tactic +Test/Reconstruction/LiftOrNToNeg.lean:9:63: error: unsolved goals +A B C D : Prop +h : ¬A ∨ ¬B ∨ ¬C ∨ ¬D ∨ False +⊢ ¬(A ∧ B ∧ C ∧ D) diff --git a/Test/Reconstruction/Resolution.expected b/Test/Reconstruction/Resolution.expected index e69de29b..0b517800 100644 --- a/Test/Reconstruction/Resolution.expected +++ b/Test/Reconstruction/Resolution.expected @@ -0,0 +1,42 @@ +Test/Reconstruction/Resolution.lean:7:3: error: unknown tactic +Test/Reconstruction/Resolution.lean:5:69: error: unsolved goals +A B C D E F G : Prop +h₁ : A ∨ B ∨ C ∨ D +h₂ : E ∨ ¬C ∨ F ∨ G +⊢ A ∨ B ∨ D ∨ E ∨ F ∨ G +Test/Reconstruction/Resolution.lean:11:3: error: unknown tactic +Test/Reconstruction/Resolution.lean:9:55: error: unsolved goals +A B C D E : Prop +h₁ : A ∨ B ∨ C ∨ D +h₂ : E ∨ ¬B +⊢ A ∨ (C ∨ D) ∨ E +Test/Reconstruction/Resolution.lean:15:3: error: unknown tactic +Test/Reconstruction/Resolution.lean:13:37: error: unsolved goals +A B C : Prop +h₁ : ¬A +h₂ : B ∨ A ∨ C +⊢ B ∨ C +Test/Reconstruction/Resolution.lean:19:3: error: unknown tactic +Test/Reconstruction/Resolution.lean:17:89: error: unsolved goals +A B C D : Prop +h₁ : ¬(A ∧ B) ∨ C ∨ ¬D ∨ ¬A +h₂ : A ∨ ¬(A ∧ B) +⊢ ¬(A ∧ B) ∨ C ∨ ¬D ∨ ¬(A ∧ B) +Test/Reconstruction/Resolution.lean:23:3: error: unknown tactic +Test/Reconstruction/Resolution.lean:21:45: error: unsolved goals +A B C D : Prop +h₁ : A ∨ B ∨ C ∨ D +h₂ : ¬A +⊢ B ∨ C ∨ D +Test/Reconstruction/Resolution.lean:27:3: error: unknown tactic +Test/Reconstruction/Resolution.lean:25:82: error: unsolved goals +B A C D E F : Prop +h₁ : B ∨ A ∨ C ∨ A +h₂ : D ∨ ¬A ∨ E ∨ ¬A ∨ F +⊢ B ∨ C ∨ A ∨ D ∨ E ∨ ¬A ∨ F +Test/Reconstruction/Resolution.lean:31:3: error: unknown tactic +Test/Reconstruction/Resolution.lean:29:29: error: unsolved goals +A : Prop +h₁ : A +h₂ : ¬A +⊢ False diff --git a/Test/String/Contains.expected b/Test/String/Contains.expected index a982ab1f..c01ed4a5 100644 --- a/Test/String/Contains.expected +++ b/Test/String/Contains.expected @@ -1,4 +1,4 @@ -goal: String.contains "a" 'a' = true +goal: "a".contains 'a' = true query: (declare-sort Char 0) diff --git a/Test/String/Length.expected b/Test/String/Length.expected index 12f338a7..ea163afe 100644 --- a/Test/String/Length.expected +++ b/Test/String/Length.expected @@ -1,8 +1,8 @@ -goal: String.length "a" = 1 +goal: "a".length = 1 query: (define-sort Nat () Int) (declare-fun String.length (String) Nat) -(assert (forall ((_uniq.886 String)) (>= (String.length _uniq.886) 0))) +(assert (forall ((_uniq.922 String)) (>= (String.length _uniq.922) 0))) (assert (distinct (String.length "a") 1)) (check-sat) diff --git a/Test/String/Replace.expected b/Test/String/Replace.expected index 960a3c39..e4a934b6 100644 --- a/Test/String/Replace.expected +++ b/Test/String/Replace.expected @@ -1,4 +1,4 @@ -goal: String.replace "a" "a" "b" = "b" +goal: "a".replace "a" "b" = "b" query: (assert (distinct (str.replace_all "a" "a" "b") "b")) diff --git a/Test/linarith.expected b/Test/linarith.expected index 488416c6..e0eb6602 100644 --- a/Test/linarith.expected +++ b/Test/linarith.expected @@ -1,11 +1,22 @@ -Test/linarith.lean:33:9: warning: unused variable `e` [linter.unusedVariables] +Test/linarith.lean:33: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` [linter.unusedVariables] -Test/linarith.lean:100:13: warning: unused variable `c` [linter.unusedVariables] -Test/linarith.lean:105:9: warning: unused variable `a` [linter.unusedVariables] -Test/linarith.lean:105:13: warning: unused variable `c` [linter.unusedVariables] -Test/linarith.lean:117:60: warning: unused variable `h3` [linter.unusedVariables] -Test/linarith.lean:124:9: warning: unused variable `a` [linter.unusedVariables] -Test/linarith.lean:124:13: warning: unused variable `c` [linter.unusedVariables] -Test/linarith.lean:167:34: warning: unused variable `z` [linter.unusedVariables] -Test/linarith.lean:168:5: warning: unused variable `h5` [linter.unusedVariables] +Test/linarith.lean:100: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` +note: this linter can be disabled with `set_option linter.unusedVariables false` +Test/linarith.lean:105: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` +note: this linter can be disabled with `set_option linter.unusedVariables false` +Test/linarith.lean:117: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` +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` +note: this linter can be disabled with `set_option linter.unusedVariables false` From 9756df37a361576308a9d4461bfc67bd219032ee Mon Sep 17 00:00:00 2001 From: Adrien Champion Date: Wed, 12 Jun 2024 10:30:51 +0200 Subject: [PATCH 11/11] chore: gitignore --- .gitignore | 2 -- 1 file changed, 2 deletions(-) diff --git a/.gitignore b/.gitignore index fd4fa84b..bfb30ec8 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1 @@ -/.vscode /.lake -.DS_Store