Update toolchain to 4.13.

.github/workflows/ci.yml

@@ -23,9 +23,6 @@ jobs:
     - name: Build lean-smt
       run: |
         lake update
-        lake build
-        lake build +Smt:dynlib
-        lake build +Smt.Rat:dynlib
-        lake build +Smt.Real:dynlib
+        lake build Smt Smt.Rat Smt.Real
     - name: Test lean-smt
       run: lake run test

Smt/Attribute.lean

@@ -14,12 +14,12 @@ open Lean
 /-- An extension to Lean's runtime environment to support SMT attributes.
     Maintains a set of function declarations for the `smt` tactic to utilize
     while generating the SMT query. -/
-abbrev SmtExtension := SimpleScopedEnvExtension (Name × Name) (HashMap Name (HashSet Name))
+abbrev SmtExtension := SimpleScopedEnvExtension (Name × Name) (Std.HashMap Name (Std.HashSet Name))
 
 /-- Adds a declaration to the set of function declarations maintained by the SMT
     environment extension. -/
-def addSmtEntry (d : HashMap Name (HashSet Name)) (e : (Name × Name)) :=
-  d.insert e.fst ((d.findD e.fst {}).insert e.snd)
+def addSmtEntry (d : Std.HashMap Name (Std.HashSet Name)) (e : (Name × Name)) :=
+  d.insert e.fst ((d.getD e.fst {}).insert e.snd)
 
 initialize smtExt : SmtExtension ← registerSimpleScopedEnvExtension {
   name     := `SmtExt

Smt/Data/Graph.lean

@@ -9,37 +9,37 @@ import Lean.Data.HashMap
 import Lean.Data.HashSet
 import Lean.Message
 
-open Lean Std
+open Lean
 
-def Graph (α) (β) [BEq α] [Hashable α] := Lean.HashMap α (Lean.HashMap α β)
+abbrev Graph (α) (β) [BEq α] [Hashable α] := Std.HashMap α (Std.HashMap α β)
 
 namespace Graph
 
 variable {α} {β} [BEq α] [Hashable α] (g : Graph α β) (v u : α) (e : β)
 
-def empty : Graph α β := HashMap.empty
+def empty : Graph α β := {}
 
 def vertices : List α := g.fold (fun a v _ => v :: a) []
 
 def neighbors? : Option (List α) :=
-  g.find? v >>= fun es => some (es.fold (fun a v _ => v :: a) [])
+  g[v]? >>= fun es => some (es.fold (fun a v _ => v :: a) [])
 
 def neighbors! : List α := match (g.neighbors? v) with
   | some ns => ns
   | none    => panic! "vertex is not in the graph"
 
-def addVertex : Graph α β := g.insert v HashMap.empty
+def addVertex : Graph α β := g.insert v {}
 
-def addEdge : Graph α β := g.insert v ((g.find! v).insert u e)
+def addEdge : Graph α β := g.insert v ((g[v]!).insert u e)
 
-def weight? : Option β := g.find? v >>= fun es => es.find? u
+def weight? : Option β := g[v]? >>= fun es => es[u]?
 
 partial def dfs [Monad m] (f : α → m Unit) : m Unit :=
-  StateT.run' (s := HashSet.empty) do
+  StateT.run' (s := {}) do
     for v in g.vertices do
       visitVertex v
 where
-  visitVertex (v : α) : StateT (Lean.HashSet α) m Unit := do
+  visitVertex (v : α) : StateT (Std.HashSet α) m Unit := do
     let vs ← get
     if vs.contains v then
       return
@@ -49,11 +49,11 @@ where
     f v
 
 partial def orderedDfs [Monad m] (vs : List α) (f : α → m Unit) : m Unit :=
-  StateT.run' (s := HashSet.empty) do
+  StateT.run' (s := {}) do
     for v in vs do
       visitVertex v
 where
-  visitVertex (v : α) : StateT (Lean.HashSet α) m Unit := do
+  visitVertex (v : α) : StateT (Std.HashSet α) m Unit := do
     let vs ← get
     if vs.contains v then
       return
@@ -62,7 +62,7 @@ where
       visitVertex u
     f v
 
-open Format in
+open Std.Format in
 protected def format [ToFormat α] [ToFormat β] : Format :=
   bracket "{" (joinSep (g.vertices.map formatVertex) ("," ++ line)) "}"
 where

Smt/Dsl/Sexp.lean

@@ -4,7 +4,9 @@ institutional affiliations. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Wojciech Nawrocki
 -/
-import Lean.Parser
+
+import Lean.PrettyPrinter.Formatter
+import Lean.PrettyPrinter.Parenthesizer
 
 import Smt.Data.Sexp
 

Smt/Reconstruct.lean

@@ -16,9 +16,9 @@ open Lean
 open Attribute
 
 structure Reconstruct.state where
-  userNames : HashMap String FVarId
-  termCache : HashMap cvc5.Term Expr
-  proofCache : HashMap cvc5.Proof Expr
+  userNames : Std.HashMap String FVarId
+  termCache : Std.HashMap cvc5.Term Expr
+  proofCache : Std.HashMap cvc5.Proof Expr
   count : Nat
   currAssums : Array Expr
   skippedGoals : Array MVarId
@@ -35,7 +35,7 @@ namespace Reconstruct
 
 private unsafe def getReconstructorsUnsafe (n : Name) (rcons : Type) : MetaM (List (rcons × Name)) := do
   let env ← getEnv
-  let names := ((smtExt.getState env).findD n {}).toList
+  let names := ((smtExt.getState env).getD n {}).toList
   let mut reconstructors := []
   for name in names do
     let fn ← IO.ofExcept <| Id.run <| ExceptT.run <|
@@ -75,7 +75,7 @@ def reconstructTerm : cvc5.Term → ReconstructM Expr := withTermCache fun t =>
     go rs t
 where
   withTermCache (r : cvc5.Term → ReconstructM Expr) (t : cvc5.Term) : ReconstructM Expr := do
-    match (← get).termCache.find? t with
+    match (← get).termCache[t]? with
     -- TODO: cvc5's global bound variables mess up the cache. Find a better fix.
     | some e => return e
     | none   => reconstruct r t
@@ -98,7 +98,7 @@ def withNewProofCache (k : ReconstructM α) : ReconstructM α := do
   return r
 
 def withProofCache (r : cvc5.Proof → ReconstructM Expr) (pf : cvc5.Proof) : ReconstructM Expr := do
-  match (← get).proofCache.find? pf with
+  match (← get).proofCache[pf]? with
   | some e => return e
   | none   => reconstruct r pf
 where
@@ -181,11 +181,15 @@ def traceReconstructProof (r : Except Exception (Expr × Expr × List MVarId)) :
   | _     => m!"{bombEmoji}"
 
 open Qq in
-partial def reconstructProof (pf : cvc5.Proof) (fvNames : HashMap String FVarId) : MetaM (Expr × Expr × List MVarId) := do
+partial def reconstructProof (pf : cvc5.Proof) (fvNames : Std.HashMap String FVarId) : MetaM (Expr × Expr × List MVarId) := do
   withTraceNode `smt.reconstruct.proof traceReconstructProof do
   let Prod.mk (p : Q(Prop)) state ← (Reconstruct.reconstructTerm (pf.getResult)).run ⟨fvNames, {}, {}, 0, #[], #[]⟩
-  let Prod.mk (h : Q(True → $p)) (.mk _ _ _ _ _ mvs) ← (Reconstruct.reconstructProof pf).run state
-  return (p, q($h trivial), mvs.toList)
+  let (h, .mk _ _ _ _ _ mvs) ← (Reconstruct.reconstructProof pf).run state
+  if pf.getArguments.isEmpty then
+    let h : Q(True → $p) ← pure h
+    return (p, q($h trivial), mvs.toList)
+  else
+    return (p, h, mvs.toList)
 
 open cvc5 in
 def traceSolve (r : Except Exception (Except SolverError Proof)) : MetaM MessageData :=
@@ -233,7 +237,7 @@ open Lean.Elab Tactic in
         let (_, mv) ← mv.intro1
         replaceMainGoal (mv :: mvs)
 where
-  getFVarNames : MetaM (HashMap String FVarId) := do
+  getFVarNames : MetaM (Std.HashMap String FVarId) := do
     let lCtx ← getLCtx
     return lCtx.getFVarIds.foldl (init := {}) fun m fvarId =>
       m.insert (lCtx.getRoundtrippingUserName? fvarId).get!.toString fvarId

Smt/Reconstruct/BitVec.lean

@@ -51,7 +51,7 @@ partial def synthDecidableInst (t : cvc5.Term) : ReconstructM Expr := do match t
       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(instDecidableEqBool («$x».getLsb $i) true)
+      return q(instDecidableEqBool («$x».getLsbD $i) true)
     | _ =>
       let p : Q(Prop) ← reconstructTerm t
       Meta.synthInstance q(Decidable $p)
@@ -229,7 +229,7 @@ where
     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 q(«$x».getLsbD $i = true)
   | _ => return none
 where
   leftAssocOp (op : Expr) (t : cvc5.Term) : ReconstructM Expr := do

Smt/Reconstruct/BitVec/Bitblast.lean

@@ -7,12 +7,10 @@ Authors: Abdalrhman Mohamed
 
 import Lean
 
-import Smt.Reconstruct.Prop.Core
-
 namespace BitVec
 
 def bb (x : BitVec w) : BitVec w :=
-  (iunfoldr (fun i _ => ((), x.getLsb i)) ()).snd
+  (iunfoldr (fun i _ => ((), x.getLsbD i)) ()).snd
 
 def self_eq_bb (x : BitVec w) : x = x.bb :=
   sorry
@@ -29,8 +27,8 @@ def beq (x : BitVec w) (y : BitVec w) : Bool :=
   go (w - 1)
 where
   go : Nat → Bool
-    | 0     => x.getLsb (w - 1) == y.getLsb (w - 1)
-    | i + 1 => x.getLsb ((w - 1) - (i + 1)) == y.getLsb ((w - 1) - (i + 1)) && go i
+    | 0     => x.getLsbD (w - 1) == y.getLsbD (w - 1)
+    | i + 1 => x.getLsbD ((w - 1) - (i + 1)) == y.getLsbD ((w - 1) - (i + 1)) && go i
 
 def eq_eq_beq (x : BitVec w) (y : BitVec w) : (x = y) = x.beq y :=
   sorry
@@ -44,12 +42,11 @@ theorem adcb_eq_adcb' : adcb = adcb' := by
 
 /-- Bitwise addition implemented via a ripple carry adder. -/
 def adc' (x y : BitVec w) : Bool → Bool × BitVec w :=
-  iunfoldr fun (i : Fin w) c => adcb' (x.getLsb i) (y.getLsb i) c
+  iunfoldr fun (i : Fin w) c => adcb' (x.getLsbD i) (y.getLsbD i) c
 
 theorem adc_eq_adc' : @adc = @adc' := by
   funext x y c
   rw [adc, adc', adcb_eq_adcb']
-  rfl
 
 theorem add_eq_adc' (x y : BitVec w) : x + y = (adc' x y false).snd := by
   rw [add_eq_adc, adc_eq_adc']

Smt/Reconstruct/Builtin.lean

@@ -30,7 +30,7 @@ def getFVarExpr! (n : Name) : MetaM Expr := do
   | none   => throwError "unknown free variable '{n}'"
 
 def getFVarOrConstExpr! (n : String) : ReconstructM Expr := do
-  match (← get).userNames.find? n with
+  match (← get).userNames[n]? with
   | some fv => return .fvar fv
   | none   => match (← getLCtx).findFromUserName? n.toName with
     | some d => return d.toExpr

Smt/Reconstruct/Int.lean

@@ -289,7 +289,7 @@ def reconstructSumUB (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
 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 := {}
+  let mut map : Std.HashMap cvc5.Term Nat := {}
   for h : i in [0:ts.size] do
     let t := ts[i]'(h.right)
     let p : Q(Prop) ← reconstructTerm t
@@ -303,43 +303,43 @@ def reconstructMulSign (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
   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 h : Q($q) ← if ts[map[vs[0]!]!]!.getKind == .NOT then
         let a : Q(Int) ← reconstructTerm vs[0]!
-        let ha : Q($a ≠ 0) := hs[map.find! vs[0]!]!
+        let ha : Q($a ≠ 0) := hs[map[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
+        go vs ts hs map ts[map[vs[0]!]!]!.getKind a hs[map[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
+      let k := ts[map[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]]!
+        let hb : Q($b < 0) := hs[map[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]]!
+        let hb : Q($b ≠ 0) := hs[map[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]]!
+        let hb : Q($b > 0) := hs[map[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]]!
+        let hb : Q($b < 0) := hs[map[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]]!
+        let hb : Q($b ≠ 0) := hs[map[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]]!
+        let hb : Q($b > 0) := hs[map[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}"
@@ -400,7 +400,7 @@ where
     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
+    addTac q($a = $b) Int.nativePolyNorm
   | .ARITH_POLY_NORM_REL =>
     if !pf.getResult[0]![0]!.getSort.isInteger then return none
     let cx : Int := pf.getChildren[0]!.getResult[0]![0]!.getIntegerValue

Smt/Reconstruct/Int/Polynorm.lean

@@ -303,12 +303,12 @@ end PolyNorm.Expr
 
 open Lean Qq
 
-partial def genCtx (e : Q(Int)) : StateT (Array Q(Int) × HashSet Q(Int)) MetaM Unit := do
+partial def genCtx (e : Q(Int)) : StateT (Array Q(Int) × Std.HashSet Q(Int)) MetaM Unit := do
   if !(← get).snd.contains e then
     go
     modify fun (es, cache) => (es, cache.insert e)
 where
-  go : StateT (Array Q(Int) × HashSet Q(Int)) MetaM Unit := do
+  go : StateT (Array Q(Int) × Std.HashSet Q(Int)) MetaM Unit := do
   match e with
   | ~q(OfNat.ofNat $x) => pure ()
   | ~q(-$x)            => genCtx x
@@ -317,15 +317,15 @@ where
   | ~q($x * $y)        => genCtx x >>= fun _ => genCtx y
   | _                  => if !(← get).fst.contains e then modify fun (es, cache) => (es.push e, cache)
 
-partial def toQPolyNormExpr (ctx : Q(PolyNorm.Context)) (es : Array Q(Int)) (e : Q(Int)) (cache : HashMap Expr (Expr × Expr)) :
-  MetaM (HashMap Expr (Expr × Expr) × (o : Q(PolyNorm.Expr)) × Q(«$o».denote $ctx = $e)) := do
-  match cache.find? e with
+partial def toQPolyNormExpr (ctx : Q(PolyNorm.Context)) (es : Array Q(Int)) (e : Q(Int)) (cache : Std.HashMap Expr (Expr × Expr)) :
+  MetaM (Std.HashMap Expr (Expr × Expr) × (o : Q(PolyNorm.Expr)) × Q(«$o».denote $ctx = $e)) := do
+  match cache.get? e with
   | some (e, h) => return ⟨cache, e, h⟩
   | none   =>
     let ⟨cache, o, h⟩ ← go
     return ⟨cache.insert e (o, h), o, h⟩
 where
-  go : MetaM (HashMap Expr (Expr × Expr) × (o : Q(PolyNorm.Expr)) × Q(«$o».denote $ctx = $e)) := do match e with
+  go : MetaM (Std.HashMap Expr (Expr × Expr) × (o : Q(PolyNorm.Expr)) × Q(«$o».denote $ctx = $e)) := do match e with
     | ~q(OfNat.ofNat $x) =>
       pure ⟨cache, q(.val (@OfNat.ofNat Int $x _)), q(rfl)⟩
     | ~q(-$x) =>

Smt/Reconstruct/Int/Rewrites.lean

@@ -49,9 +49,9 @@ theorem elim_gt : (t > s) = ¬(t ≤ s) :=
 theorem elim_lt : (t < s) = ¬(t ≥ s) :=
   propext Int.not_le.symm
 theorem elim_int_gt {t s : Int} : (t > s) = (t ≥ s + 1) :=
-  propext (Int.lt_iff_add_one_le s t)
+  propext Int.lt_iff_add_one_le
 theorem elim_int_lt {t s : Int} : (t < s) = (s ≥ t + 1) :=
-  propext (Int.lt_iff_add_one_le t s)
+  propext Int.lt_iff_add_one_le
 theorem elim_leq : (t ≤ s) = (s ≥ t) :=
   propext ge_iff_le