Update Lean toolchain.

Smt/Preprocess/Iff.lean

@@ -28,7 +28,7 @@ def elimIff (mv : MVarId) (hs : List Expr) : MetaM (List Expr × MVarId) := mv.w
   let simpTheorems ← #[``eq_self, ``iff_eq_eq].foldlM (·.addConst ·) ({} : Meta.SimpTheorems)
   let simpTheorems := #[simpTheorems]
   let congrTheorems ← Meta.getSimpCongrTheorems
-  let ctx := { simpTheorems, congrTheorems }
+  let ctx ← Meta.Simp.mkContext {} simpTheorems congrTheorems
   let (hs, mv) ← elimIffLocalDecls mv hs ctx
   let mv ← elimIffTarget mv ctx
   return (hs, mv)

Smt/Reconstruct/BitVec.lean

@@ -262,7 +262,8 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
       let ps := [``Nat.reduceAdd, ``Nat.reduceLT, ``reduceDIte]
       let simpTheorems ← ds.foldrM (fun n a => a.addDeclToUnfold n) {}
       let simpProcs ← ps.foldrM (fun n a => a.add n false) {}
-      let (some mv, _) ← Meta.simpTarget mv { simpTheorems := #[simpTheorems] } simpProcs | throwError "simp failed"
+      let ctx ← Meta.Simp.mkContext {} #[simpTheorems]
+      let (some mv, _) ← Meta.simpTarget mv ctx simpProcs | throwError "simp failed"
       mv.refl
       addThm q($x = $x') q(Eq.trans (BitVec.self_eq_bb $x) $h)
     | .EQUAL =>
@@ -278,8 +279,9 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
       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 ctx ← Meta.Simp.mkContext {} #[simpTheorems]
       let simpProcs ← ps.foldrM (fun n a => a.add n false) {}
-      let (some mv, _) ← Meta.simpTarget mv { simpTheorems := #[simpTheorems] } simpProcs | throwError "simp failed"
+      let (some mv, _) ← Meta.simpTarget mv ctx simpProcs | throwError "simp failed"
       mv.refl
       addThm q(($x = $y) = $p) q(Eq.trans (BitVec.eq_eq_beq $x $y) (Bool.eq_of_decide_eq $h))
     | .BITVECTOR_ADD =>
@@ -294,8 +296,9 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
       let ps := [``Nat.reduceAdd, ``Nat.reduceLT, ``reduceDIte, ``reduceIte]
       let simpTheorems ← ds.foldrM (fun n a => a.addDeclToUnfold n) {}
       let simpTheorems ← ts.foldrM (fun n a => a.addConst n) simpTheorems
+      let ctx ← Meta.Simp.mkContext {} #[simpTheorems]
       let simpProcs ← ps.foldrM (fun n a => a.add n false) {}
-      let (some mv, _) ← Meta.simpTarget mv { simpTheorems := #[simpTheorems] } simpProcs | throwError "simp failed"
+      let (some mv, _) ← Meta.simpTarget mv ctx simpProcs | throwError "simp failed"
       mv.refl
       addThm q($x + $y = $z) q(Eq.trans (BitVec.add_eq_adc' $x $y) $h)
     | _ => return none

Smt/Reconstruct/Bool/Tactic.lean

@@ -21,7 +21,8 @@ def traceBoolify (r : Except Exception MVarId) : MetaM MessageData :=
 def boolify (mv : MVarId) : MetaM MVarId := withTraceNode `smt.reconstruct.boolify traceBoolify do
   let ns := [``Bool.decide_eq_true, ``decide_true_eq, ``decide_false_eq, ``decide_not_eq, ``decide_and_eq, ``decide_or_eq, ``decide_eq_eq, ``decide_xor_eq]
   let simpTheorems ← ns.foldrM (fun n a => a.addTheorem (.decl n) (.const n [])) {}
-  let (some mv, _) ← Meta.simpTarget mv { simpTheorems } | throwError "failed to boolify goal:{mv}"
+  let ctx ← Meta.Simp.mkContext {} simpTheorems
+  let (some mv, _) ← Meta.simpTarget mv ctx | throwError "failed to boolify goal:{mv}"
   return mv
 
 namespace Tactic

Smt/Reconstruct/Rat.lean

@@ -15,8 +15,7 @@ import Smt.Reconstruct.Rewrite
 
 namespace Smt.Reconstruct.Rat
 
-open Lean hiding Rat
-open Qq
+open Lean Qq
 
 @[smt_sort_reconstruct] def reconstructRatSort : SortReconstructor := fun s => do match s.getKind with
   | .REAL_SORT => return q(Rat)
@@ -27,7 +26,7 @@ open Qq
     | .DIV_BY_ZERO => return q(fun (x : Rat) => x / 0)
     | _ => return none
   | .CONST_RATIONAL =>
-    let c : Lean.Rat := t.getRationalValue!
+    let c : Std.Internal.Rat := t.getRationalValue!
     let num : Q(Rat) := mkRatLit c.num.natAbs
     if c.den == 1 then
       if c.num ≥ 0 then
@@ -311,7 +310,7 @@ where
       return ha
 
 def reconstructArithPolyNormRel (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
-  let lcx : Lean.Rat := pf.getChildren[0]!.getResult[0]![0]!.getRationalValue!
+  let lcx : Std.Internal.Rat := pf.getChildren[0]!.getResult[0]![0]!.getRationalValue!
   let cx : Q(Rat) ← reconstructTerm pf.getChildren[0]!.getResult[0]![0]!
   let cy : Q(Rat) ← reconstructTerm pf.getChildren[0]!.getResult[1]![0]!
   let x₁ : Q(Rat) ← reconstructTerm pf.getResult[0]![0]!

Smt/Reconstruct/Rat/Polynorm.lean

@@ -283,8 +283,7 @@ theorem denote_eq_from_toPolynomial_eq {e₁ e₂ : RatExpr} (h : e₁.toPolynom
 
 end PolyNorm.RatExpr
 
-open Lean hiding Rat
-open Qq
+open Lean Qq
 
 abbrev PolyM := StateT (Array Q(Int) × Array Q(Rat)) MetaM
 

Smt/Reconstruct/Real.lean

@@ -25,7 +25,7 @@ open Lean Qq
     | .DIV_BY_ZERO => return q(fun (x : Real) => x / 0)
     | _ => return none
   | .CONST_RATIONAL =>
-    let c : Lean.Rat := t.getRationalValue!
+    let c : Std.Internal.Rat := t.getRationalValue!
     let num : Q(Real) := mkRealLit c.num.natAbs
     if c.den == 1 then
       if c.num ≥ 0 then
@@ -318,7 +318,7 @@ where
       return ha
 
 def reconstructArithPolyNormRel (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
-  let lcx : Lean.Rat := pf.getChildren[0]!.getResult[0]![0]!.getRationalValue!
+  let lcx : Std.Internal.Rat := pf.getChildren[0]!.getResult[0]![0]!.getRationalValue!
   let cx : Q(Real) ← reconstructTerm pf.getChildren[0]!.getResult[0]![0]!
   let cy : Q(Real) ← reconstructTerm pf.getChildren[0]!.getResult[1]![0]!
   let x₁ : Q(Real) ← reconstructTerm pf.getResult[0]![0]!

Smt/Reconstruct/Real/Polynorm.lean

@@ -290,8 +290,7 @@ theorem denote_eq_from_toPolynomial_eq {e₁ e₂ : RealExpr} (h : e₁.toPolyno
 
 end PolyNorm.RealExpr
 
-open Lean hiding Rat
-open Qq
+open Lean Qq
 
 abbrev PolyM := StateT (Array Q(Int) × Array Q(Real)) MetaM
 
@@ -397,7 +396,7 @@ def traceArithNormNum (r : Except Exception Unit) : MetaM MessageData :=
 
 open Mathlib.Meta.NormNum in
 def normNum (mv : MVarId) : MetaM Unit := withTraceNode `smt.reconstruct.normNum traceArithNormNum do
-  if let some (_, mv) ← normNumAt mv {} #[] true false then
+  if let some (_, mv) ← normNumAt mv (← Meta.Simp.mkContext) #[] true false then
     throwError "[norm_num]: could not prove {← mv.getType}"
 
 namespace Tactic

Smt/Tactic/EqnDef.lean

@@ -172,7 +172,7 @@ def specializeEqnDef (x : FVarId) (args : Array Expr) (opaqueConsts : Std.HashSe
         let (fvEq, mvarId) ← (← mvarId.assert (nm ++ `specialization) eqnRw pfRw).intro1P
         return (fvEq, [mvarId])
 
-syntax blockingConsts := "blocking [" term,* "]"
+syntax blockingConsts := "blocking" "[" term,* "]"
 
 /-- `specialize_def foo [arg₁, ⋯, argₙ]` introduces a new equational definition `foo.arg₁.⋯.argₙ`
 whose body is the partial evaluation of `foo arg₁ ⋯ argₙ`. During reduction, all SMT-LIB builtins

Smt/Tactic/Smt.lean

@@ -82,7 +82,7 @@ def smt (mv : MVarId) (hs : List Expr) (timeout : Option Nat := none) : MetaM (L
 namespace Tactic
 
 syntax smtHints := ("[" term,* "]")?
-syntax smtTimeout := ("(timeout := " num ")")?
+syntax smtTimeout := ("(" "timeout" " := " num ")")?
 
 /-- `smt` converts the current goal into an SMT query and checks if it is
 satisfiable. By default, `smt` generates the minimum valid SMT query needed to

Smt/Tactic/WHNFConfigurable.lean

@@ -223,7 +223,7 @@ private def reduceRec (recVal : RecursorVal) (recLvls : List Level) (recArgs : A
         trace[Smt.reduce.rec] "failed."
         failK ()
 
-    let major ← whnf <| recArgs.get ⟨majorIdx, h⟩
+    let major ← whnf <| recArgs[majorIdx]'h
     if (← read).letPushElim then
       letTelescopeAbstracting major fun _ major abs => do
         let e' ← cont major
@@ -244,7 +244,7 @@ private def reduceQuotRec (recVal  : QuotVal) (recArgs : Array Expr)
     : ReductionM α :=
   let process (majorPos argPos : Nat) : ReductionM α :=
     if h : majorPos < recArgs.size then do
-      let major := recArgs.get ⟨majorPos, h⟩
+      let major := recArgs[majorPos]'h
       let major ← whnf major
       match major with
       | Expr.app (Expr.app (Expr.app (Expr.const majorFn _) _) _) majorArg => do
@@ -273,7 +273,7 @@ mutual
     else do
       let majorIdx := recVal.getMajorIdx
       if h : majorIdx < recArgs.size then do
-        let major := recArgs.get ⟨majorIdx, h⟩
+        let major := recArgs[majorIdx]'h
         let major ← whnf major
         getStuckMVar? major
       else
@@ -282,7 +282,7 @@ mutual
   private partial def isQuotRecStuck? (recVal : QuotVal) (recArgs : Array Expr) : ReductionM (Option MVarId) :=
     let process? (majorPos : Nat) : ReductionM (Option MVarId) :=
       if h : majorPos < recArgs.size then do
-        let major := recArgs.get ⟨majorPos, h⟩
+        let major := recArgs[majorPos]'h
         let major ← whnf major
         getStuckMVar? major
       else
@@ -440,9 +440,9 @@ private def whnfMatcher (e : Expr) : ReductionM Expr := do
   let mut transparency ← getTransparency
   if transparency == TransparencyMode.reducible then
     transparency := TransparencyMode.instances
-  withTransparency transparency <|
-    withTheReader Meta.Context (fun ctx => { ctx with canUnfold? := canUnfoldAtMatcher ctx.canUnfold? }) do
-      whnf e
+  withTransparency transparency do
+    let ctx ← readThe Meta.Context
+    withCanUnfoldPred (canUnfoldAtMatcher ctx.canUnfold?) (whnf e)
 
 def reduceMatcher? (e : Expr) : ReductionM ReduceMatcherResult := do
   trace[Smt.reduce.matcher] "{e}"
@@ -702,7 +702,7 @@ where
 
 def shouldUnfold (ci : ConstantInfo) : ReductionM Bool := do
   let some canUnfold := (← readThe Meta.Context).canUnfold? | return true
-  let cfg := (← readThe Meta.Context).config
+  let cfg ← getConfig (← readThe Meta.Context)
   canUnfold cfg ci
 
 mutual
@@ -930,17 +930,18 @@ def reduceNat? (e : Expr) : ReductionM (Option Expr) :=
 @[inline] private def cached? (useCache : Bool) (e : Expr) : MetaM (Option Expr) := do
   if useCache then
     match (← getConfig).transparency with
-    | TransparencyMode.default => return (← get).cache.whnfDefault.find? e
-    | TransparencyMode.all     => return (← get).cache.whnfAll.find? e
+    | TransparencyMode.default => return (← get).cache.whnf.find? (← mkExprConfigCacheKey e)
+    | TransparencyMode.all     => return (← get).cache.whnf.find? (← mkExprConfigCacheKey e)
     | _                        => unreachable!
   else
     return none
 
 private def cache (useCache : Bool) (e r : Expr) : MetaM Expr := do
   if useCache then
+    let ecck ← mkExprConfigCacheKey e
     match (← getConfig).transparency with
-    | TransparencyMode.default => modify fun s => { s with cache.whnfDefault := s.cache.whnfDefault.insert e r }
-    | TransparencyMode.all     => modify fun s => { s with cache.whnfAll     := s.cache.whnfAll.insert e r }
+    | TransparencyMode.default => modify fun s => { s with cache.whnf := s.cache.whnf.insert ecck r }
+    | TransparencyMode.all     => modify fun s => { s with cache.whnf := s.cache.whnf.insert ecck r }
     | _                        => unreachable!
   return r
 

Smt/Tactic/WHNFSmt.lean

@@ -104,9 +104,8 @@ to let-lift `let-opaque` bindings. This can produce linearly-sized terms in cert
 
 Constants with names in `opaqueConsts` are also not unfolded. -/
 def smtOpaqueReduce (e : Expr) (opaqueConsts : Std.HashSet Name := {}) : MetaM Expr :=
-  withTheReader Meta.Context (fun ctx => { ctx with
-    canUnfold? := some (opaquePred opaqueConsts)
-  }) do Smt.reduce (skipTypes := false) e |>.run {
+  Meta.withCanUnfoldPred (opaquePred opaqueConsts) <|
+  Smt.reduce (skipTypes := false) e |>.run {
     letPushElim := true
   }
 

Smt/Translate/Commands.lean

@@ -29,15 +29,16 @@ inductive Command where
 
 namespace Command
 
-open Lean
-open Term
-open scoped Term.Notation
+open Lean Term
 
-def defNat : Command := .defineSort "Nat" [] (`"Int")
+def defNat : Command := .defineSort "Nat" [] (symbolT "Int")
 
 def defNatSub : Command :=
-  .defineFun "Nat.sub" [("x", `"Nat"), ("y", `"Nat")] (`"Nat")
-    (`"ite" • (`"<" • `"x" • `"y") • ``"0" • (`"-" • `"x" • `"y"))
+  .defineFun "Nat.sub" [("x", symbolT "Nat"), ("y", symbolT "Nat")] (symbolT "Nat")
+    (Term.mkApp3 (symbolT "ite")
+                 (Term.mkApp2 (symbolT "<") (symbolT "x") (symbolT "y"))
+                 (literalT "0")
+                 (Term.mkApp2 (symbolT "-") (symbolT "x") (symbolT "y")))
     false
 
 open ToSexp in

Smt/Translate/Term.lean

@@ -31,24 +31,15 @@ inductive Term where
   deriving Inhabited
 
 namespace Term
-namespace Notation
-
-scoped infixl:20 " • "  => appT
-scoped prefix:21 " ` "  => symbolT
-scoped prefix:21 " `` " => literalT
-
-end Notation
-
-open scoped Notation
 
 def mkApp2 (f a b : Term) : Term :=
-  f • a • b
+  appT (appT f a) b
 
 def mkApp3 (f a b c : Term) : Term :=
-  f • a • b • c
+  appT (appT (appT f a) b) c
 
 def mkApp4 (f a b c d : Term) : Term :=
-  f • a • b • c • d
+  appT (appT (appT (appT f a) b) c) d
 
 /-- SMT-LIBv2 quoting for symbols. -/
 def quoteSymbol (s : String) : String :=

Test/Auto.expected

@@ -0,0 +1,4 @@
+Test/Auto.lean:38:2: error: Auto.LamReif.reifTermCheckType :: LamTerm ((!9 (!13 (!1 !2)) !3) = (!0 (!1 !2) !3)) is not type correct
+Test/Auto.lean:41:2: error: Auto.LamReif.reifTermCheckType :: LamTerm ((!6 (!11 (!1 (!2 !3))) !3) = (!0 (!1 (!2 !3)) !3)) is not type correct
+Test/Auto.lean:44:2: error: Auto.LamReif.reifTermCheckType :: LamTerm ((!6 (!10 (!1 (!2 !3))) !3) = (!0 (!1 (!2 !3)) !3)) is not type correct
+Test/Auto.lean:48:2: error: Auto.LamReif.reifTermCheckType :: LamTerm ((!6 (!10 !1) (!2 (!3 !1))) = (!0 !1 (!2 (!3 !1)))) is not type correct

Test/BitVec/Shift.expected

@@ -1,16 +1,16 @@
 goal: x ++ y = zeroExtend 4 x <<< 2#2 ||| zeroExtend 4 y
 
 query:
-(declare-const x (_ BitVec 2))
 (declare-const y (_ BitVec 2))
+(declare-const x (_ BitVec 2))
 (assert (distinct (concat x y) (bvor (bvshl ((_ zero_extend 2) x) #b10) ((_ zero_extend 2) y))))
 (check-sat)
 Test/BitVec/Shift.lean:5:8: warning: declaration uses 'sorry'
 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'

Test/BitVec/XorComm.expected

@@ -1,8 +1,8 @@
 goal: x ^^^ y = y ^^^ x
 
 query:
-(declare-const x (_ BitVec 2))
 (declare-const y (_ BitVec 2))
+(declare-const x (_ BitVec 2))
 (assert (distinct (bvxor x y) (bvxor y x)))
 (check-sat)
 Test/BitVec/XorComm.lean:3:8: warning: declaration uses 'sorry'

Test/Int/Binders.expected

@@ -2,24 +2,24 @@ goal: curryAdd a b = curryAdd b a
 
 query:
 (define-fun curryAdd (([email protected]._hyg.4 Int) ([email protected]._hyg.6 Int)) Int (+ [email protected]._hyg.4 [email protected]._hyg.6))
-(declare-const b Int)
 (declare-const a Int)
+(declare-const b Int)
 (assert (distinct (curryAdd a b) (curryAdd b a)))
 (check-sat)
 Test/Int/Binders.lean:5:0: warning: declaration uses 'sorry'
 goal: partCurryAdd a b = partCurryAdd b a
 
 query:
 (define-fun partCurryAdd ((a Int) ([email protected]._hyg.36 Int)) Int (+ a [email protected]._hyg.36))
-(declare-const b Int)
 (declare-const a Int)
+(declare-const b Int)
 (assert (distinct (partCurryAdd a b) (partCurryAdd b a)))
 (check-sat)
 Test/Int/Binders.lean:11:0: warning: declaration uses 'sorry'
 goal: partCurryAdd' a b = partCurryAdd' b a
 
 query:
-(define-fun |partCurryAdd'| ((a Int) ([email protected]._hyg.2519 Int)) Int (+ a [email protected]._hyg.2519))
+(define-fun |partCurryAdd'| ((a Int) ([email protected]._hyg.2531 Int)) Int (+ a [email protected]._hyg.2531))
 (declare-const a Int)
 (declare-const b Int)
 (assert (distinct (+ a b) (+ b a)))

Test/Int/DefineSort.expected

@@ -3,8 +3,8 @@ goal: a.add b = b.add a
 query:
 (define-sort MyInt () Int)
 (define-fun MyInt.add ((a MyInt) (b MyInt)) MyInt (+ a b))
-(declare-const b MyInt)
 (declare-const a MyInt)
+(declare-const b MyInt)
 (assert (distinct (MyInt.add a b) (MyInt.add b a)))
 (check-sat)
 Test/Int/DefineSort.lean:6:0: warning: declaration uses 'sorry'

Test/Int/DvdTimeout.expected

@@ -1,9 +1,9 @@
 goal: dvd a (b + c + d) = true
 
 query:
-(declare-const a Int)
-(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)
 (assert (= (dvd a c) true))
@@ -19,4 +19,4 @@ h1 : dvd a b = true
 h2 : dvd a c = true
 h3 : dvd a d = true
 ⊢ dvd a (b + c + d) = true
-Test/Int/DvdTimeout.lean:13:33: error: unexpected token '(timeout :='; expected command
+Test/Int/DvdTimeout.lean:13:33: error: unexpected token '('; expected command

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.965 Nat)) (=> (>= _uniq.965 0) (>= (f _uniq.965) 0))))
+(assert (forall ((_uniq.970 Nat)) (=> (>= _uniq.970 0) (>= (f _uniq.970) 0))))
 (declare-const y Nat)
 (assert (>= y 0))
 (declare-const x Nat)