Update to lean v4.13.0

Auto/Embedding/LamBitVec.lean

@@ -55,16 +55,18 @@ namespace BVLems
     unfold BitVec.ushiftRight BitVec.toNat
     dsimp; rw [Nat.shiftRight_eq_div_pow]
 
-  theorem toNat_zeroExtend' {a : BitVec n} (le : n ≤ m) : (a.zeroExtend' le).toNat = a.toNat := rfl
+  theorem toNat_setWidth {a : BitVec n} (le : n ≤ m) : (a.setWidth m).toNat = a.toNat := by
+    unfold setWidth
+    simp only [le, ↓reduceDIte, toNat_setWidth']
 
   theorem toNat_zeroExtend {a : BitVec n} (i : Nat) : (a.zeroExtend i).toNat = a.toNat % (2 ^ i) := by
-    unfold BitVec.zeroExtend; cases hdec : decide (n ≤ i)
+    unfold BitVec.zeroExtend setWidth; cases hdec : decide (n ≤ i)
     case false =>
       have hnle := of_decide_eq_false hdec
       rw [Bool.dite_eq_false (proof:=hnle)]; rfl
     case true =>
       have hle := of_decide_eq_true hdec
-      rw [Bool.dite_eq_true (proof:=hle), toNat_zeroExtend']
+      rw [Bool.dite_eq_true (proof:=hle), toNat_setWidth']
       rw [Nat.mod_eq_of_lt]; rcases a with ⟨⟨a, isLt⟩⟩;
       apply Nat.le_trans isLt; apply Nat.pow_le_pow_of_le_right (Nat.le_step .refl) hle
 
@@ -103,7 +105,7 @@ namespace BVLems
   theorem msb_equiv_lt (a : BitVec n) : !a.msb ↔ a.toNat < 2 ^ (n - 1) := by
     dsimp [BitVec.msb, getMsbD, getLsbD]
     cases n
-    case zero => simp
+    case zero => simp [BitVec.toNat]
     case succ n =>
       have dtrue : decide (0 < n + 1) = true := by simp
       rw [dtrue, Bool.not_eq_true', Bool.true_and, Nat.succ_sub_one, Nat.testBit_false_iff]
@@ -112,7 +114,7 @@ namespace BVLems
   theorem msb_equiv_lt' (a : BitVec n) : !a.msb ↔ 2 * a.toNat < 2 ^ n := by
     rw [msb_equiv_lt]
     cases n
-    case zero => simp
+    case zero => simp [BitVec.toNat]
     case succ n =>
       rw [Nat.succ_sub_one, Nat.pow_succ, Nat.mul_comm (m:=2)]
       apply Iff.symm; apply Nat.mul_lt_mul_left

Auto/Embedding/LamChecker.lean

@@ -2460,17 +2460,17 @@ theorem Checker.getValidExport_indirectReduce_reflection
 structure RTableStatus where
   rTable        : Array REntry := #[]
   rTableTree    : BinTree REntry := BinTree.leaf
-  nonemptyMap   : HashMap LamSort Nat := {}
-  wfMap         : HashMap (List LamSort × LamSort × LamTerm) Nat := {}
-  validMap      : HashMap (List LamSort × LamTerm) Nat := {}
+  nonemptyMap   : Std.HashMap LamSort Nat := {}
+  wfMap         : Std.HashMap (List LamSort × LamSort × LamTerm) Nat := {}
+  validMap      : Std.HashMap (List LamSort × LamTerm) Nat := {}
   -- maxEVarSucc
   maxEVarSucc   : Nat := 0
   -- lamEVarTy
   lamEVarTy     : Array LamSort := #[]
   -- This works as a cache for `BinTree.ofListGet lamEVarTy.data`
   lamEVarTyTree : BinTree LamSort := BinTree.leaf
   -- `chkMap.find?[re]` returns the checkstep which proves `re`
-  chkMap        : HashMap REntry ChkStep := {}
+  chkMap        : Std.HashMap REntry ChkStep := {}
   deriving Inhabited
 
 def RTableStatus.push (rs : RTableStatus) (re : REntry) :=
@@ -2494,8 +2494,8 @@ def RTableStatus.newEtomWithValid (rs : RTableStatus) (c : ChkStep) (re : REntry
 
 def RTableStatus.findPos? (rs : RTableStatus) (re : REntry) :=
   match re with
-  | .nonempty s => rs.nonemptyMap.find? s
-  | .wf lctx s t => rs.wfMap.find? (lctx, s, t)
-  | .valid lctx t => rs.validMap.find? (lctx, t)
+  | .nonempty s => rs.nonemptyMap.get? s
+  | .wf lctx s t => rs.wfMap.get? (lctx, s, t)
+  | .valid lctx t => rs.validMap.get? (lctx, t)
 
 end Auto.Embedding.Lam

Auto/Embedding/LamConv.lean

@@ -1957,8 +1957,8 @@ section UnsafeOps
   /-- Turn `ts[i]` into `.bvar i` -/
   def LamTerm.abstractsImp (t : LamTerm) (ts : Array LamTerm) :=
     let ts := ts.mapIdx (fun i x => (x, LamTerm.bvar i.val))
-    let tmap := @Lean.HashMap.ofList _ _ inferInstance inferInstance ts.data
-    t.replace (fun x => tmap.find? x) 0
+    let tmap := @Std.HashMap.ofList _ _ inferInstance inferInstance ts.toList
+    t.replace (fun x => tmap.get? x) 0
 
   def LamTerm.abstractsRevImp (t : LamTerm) (ts : Array LamTerm) := t.abstractsImp ts.reverse
 

Auto/IR/SMT.lean

@@ -33,7 +33,7 @@ deriving BEq, Hashable, Inhabited
 def SIdent.toString : SIdent → String
 | .symb s => if isSimpleSymbol s then s else "|" ++ s ++ "|"
 | .indexed s idx =>
-  s!"(_ {s} " ++ String.intercalate " " (idx.data.map (fun idx =>
+  s!"(_ {s} " ++ String.intercalate " " (idx.toList.map (fun idx =>
     match idx with
     | .inl idx => s!"{idx}"
     | .inr idx => s!"{idx}")) ++ ")"
@@ -63,7 +63,7 @@ where go : List SSort → List SIdent →  List String
 | a :: as, binders => SSort.toStringAux a binders :: go as binders
 
 def SSort.toString (s : SSort) (binders : Array SIdent) : String :=
-  SSort.toStringAux s binders.data
+  SSort.toStringAux s binders.toList
 
 /-- Caution : Do not use this in define-sort, because sort there might contain bvars -/
 instance : ToString SSort where
@@ -181,7 +181,7 @@ private partial def STerm.toStringAux : STerm → List SIdent → String
     intro ++ body
   | .attr t attrs, binders =>
     let intro := "(! " ++ STerm.toStringAux t binders ++ " "
-    let sattrs := String.intercalate " " (attrs.data.map (attrToStringAux · binders))
+    let sattrs := String.intercalate " " (attrs.toList.map (attrToStringAux · binders))
     intro ++ sattrs ++ ")"
 where
   goQIdApp : List STerm → List SIdent → List String
@@ -194,9 +194,9 @@ where
         let pattern := "(" ++ (ToString.toString (SIdent.symb constr))
         pattern ++ body
       else
-        let binders := args.data.map .symb ++ binders
+        let binders := args.toList.map .symb ++ binders
         let body := " " ++ STerm.toStringAux body binders ++ ")"
-        let args := args.data.map (fun x => ToString.toString (SIdent.symb x))
+        let args := args.toList.map (fun x => ToString.toString (SIdent.symb x))
         let pattern := "((" ++ String.intercalate " " (ToString.toString (SIdent.symb constr) :: args) ++ ")"
         pattern ++ body
   goMatchBody : List (MatchCase STerm) → List SIdent → List String
@@ -206,16 +206,16 @@ where
     | .none s,     _ => ":" ++ s
     | .spec s sc,  _ => s!":{s} {sc.toString}"
     | .symb s s',  _ => s!":{s} {s'}"
-    | .sexpr s ts, binders => s!":{s} (" ++ String.intercalate " " (ts.data.map (STerm.toStringAux · binders)) ++ ")"
+    | .sexpr s ts, binders => s!":{s} (" ++ String.intercalate " " (ts.toList.map (STerm.toStringAux · binders)) ++ ")"
 
 def STerm.toString (t : STerm) (binders : Array SIdent) : String :=
-  STerm.toStringAux t binders.data
+  STerm.toStringAux t binders.toList
 
 instance : ToString STerm where
   toString t := STerm.toString t #[]
 
 def Attribute.toString (attr : Attribute) (binders : Array SIdent) : String :=
-  SMT.STerm.toStringAux.attrToStringAux attr binders.data
+  SMT.STerm.toStringAux.attrToStringAux attr binders.toList
 
 instance : ToString Attribute where
   toString attr := Attribute.toString attr #[]
@@ -232,7 +232,7 @@ private def ConstrDecl.toString : ConstrDecl → Array SIdent → String
 | ⟨name, selDecls⟩, binders =>
   let pre := s!"({SIdent.symb name}"
   let selDecls := selDecls.map (fun (name, sort) => s!"({SIdent.symb name} " ++ SSort.toString sort binders ++ ")")
-  String.intercalate " " (pre :: selDecls.data) ++ ")"
+  String.intercalate " " (pre :: selDecls.toList) ++ ")"
 
 /--
  〈datatype_dec〉 ::= ( 〈constructor_dec〉+ ) | ( par ( 〈symbol 〉+ ) ( 〈constructor_dec〉+ ) )
@@ -243,11 +243,11 @@ structure DatatypeDecl where
 
 private def DatatypeDecl.toString : DatatypeDecl → String := fun ⟨params, cstrDecls⟩ =>
   let scstrDecls := cstrDecls.map (fun d => ConstrDecl.toString d (params.map SIdent.symb))
-  let scstrDecls := "(" ++ String.intercalate " " scstrDecls.data ++ ")"
+  let scstrDecls := "(" ++ String.intercalate " " scstrDecls.toList ++ ")"
   if params.size == 0 then
     scstrDecls
   else
-    "(par ("  ++ String.intercalate " " params.data ++ ") " ++ scstrDecls ++ ")"
+    "(par ("  ++ String.intercalate " " params.toList ++ ") " ++ scstrDecls ++ ")"
 
 inductive SMTOption where
   | diagnosticOC            : String → SMTOption
@@ -345,26 +345,26 @@ def Command.toString : Command → String
 | .checkSat                            => "(check-sat)"
 | .declFun name argSorts resSort       =>
   let pre := s!"(declare-fun {SIdent.symb name} ("
-  let argSorts := String.intercalate " " (argSorts.map ToString.toString).data ++ ") "
+  let argSorts := String.intercalate " " (argSorts.map ToString.toString).toList ++ ") "
   let trail := s!"{resSort})"
   pre ++ argSorts ++ trail
 | .declSort name arity                 => s!"(declare-sort {SIdent.symb name} {arity})"
 | .defFun isRec name args resTy body =>
   let pre := if isRec then "(define-fun-rec " else "(define-fun "
   let pre := pre ++ ToString.toString (SIdent.symb name) ++ " "
-  let binders := "(" ++ String.intercalate " " (args.map (fun (name, sort) => s!"({SIdent.symb name} {sort})")).data ++ ") "
+  let binders := "(" ++ String.intercalate " " (args.map (fun (name, sort) => s!"({SIdent.symb name} {sort})")).toList ++ ") "
   let trail := s!"{resTy} " ++ STerm.toString body (args.map (fun (name, _) => SIdent.symb name)) ++ ")"
   pre ++ binders ++ trail
 | .defSort name args body              =>
   let pre := s!"(define-sort {SIdent.symb name} ("
-  let sargs := String.intercalate " " args.data ++ ") "
+  let sargs := String.intercalate " " args.toList ++ ") "
   let trail := SSort.toString body (args.map SIdent.symb) ++ ")"
   pre ++ sargs ++ trail
 | .declDtype name ddecl                =>
   s!"(declare-datatype {SIdent.symb name} {ddecl.toString})"
 | .declDtypes infos               =>
-  let sort_decs := String.intercalate " " (infos.data.map (fun (name, args, _) => s!"({SIdent.symb name} {args})"))
-  let datatype_decs := String.intercalate " " (infos.data.map (fun (_, _, ddecl) => ddecl.toString))
+  let sort_decs := String.intercalate " " (infos.toList.map (fun (name, args, _) => s!"({SIdent.symb name} {args})"))
+  let datatype_decs := String.intercalate " " (infos.toList.map (fun (_, _, ddecl) => ddecl.toString))
   s!"(declare-datatypes ({sort_decs}) ({datatype_decs}))"
 | .echo s                              => s!"(echo \"{s}\")"
 | .exit                                => "(exit)"
@@ -385,10 +385,10 @@ section
   -/
   structure State where
     -- Map from high-level construct to symbol
-    h2lMap    : HashMap ω String   := {}
+    h2lMap    : Std.HashMap ω String   := {}
     -- Inverse of `h2lMap`
     -- Map from symbol to high-level construct
-    l2hMap    : HashMap String ω   := {}
+    l2hMap    : Std.HashMap String ω   := {}
     -- We allow two types of names
     -- · `"_" ++ s`,
     -- · `"_" ++ s ++ "_" ++ <num>`
@@ -402,7 +402,7 @@ section
     --   been used, we return `n'` as the final name. If `n'` has
     --   been used for `k` times (`k > 0`), return `n' ++ s!"_{k - 1}"`.
     -- `usedNames` records the `k - 1` for each `n'`
-    usedNames : HashMap String Nat := {}
+    usedNames : Std.HashMap String Nat := {}
     -- List of commands
     commands  : Array Command      := #[]
 
@@ -443,7 +443,7 @@ section
       preName := "pl_" ++ preName
     if preName.back.isDigit then
       preName := preName ++ "_"
-    if let .some idx := (← getUsedNames).find? preName then
+    if let .some idx := (← getUsedNames).get? preName then
       -- Used
       setUsedNames ((← getUsedNames).insert preName (idx + 1))
       return "_" ++ preName ++ s!"_{idx}"
@@ -457,7 +457,7 @@ section
         "~!@$%^&*_-+=<>.?/" ++
         "ΑαΒβΓγΔδΕεΖζΗηΘθΙιΚκΛλΜμΝνΞξΟοΠπΡρΣσςΤτΥυΦφΧχΨψΩω" ++
         "₀₁₂₃₄₅₆₇₈₉"
-      let allowedSet : HashSet UInt32 := HashSet.insertMany HashSet.empty (List.map Char.val allowedStr.toList)
+      let allowedSet : Std.HashSet UInt32 := Std.HashSet.insertMany Std.HashSet.empty (List.map Char.val allowedStr.toList)
       c.isAlphanum || allowedSet.contains c.val
 
 
@@ -471,7 +471,7 @@ section
   partial def h2Symb (cstr : ω) (nameSuggestion : Option String) : TransM ω String := do
     let l2hMap ← getL2hMap
     let h2lMap ← getH2lMap
-    if let .some name := h2lMap.find? cstr then
+    if let .some name := h2lMap.get? cstr then
       return name
     let .some nameSuggestion := nameSuggestion
       | throwError "IR.SMT.h2Symb :: Fresh high-level constraint {cstr} without name suggestion"

Auto/Lib/Containers.lean

@@ -3,7 +3,7 @@ open Lean
 
 namespace Auto
 
-def mergeHashSet {α : Type u} [BEq α] [Hashable α] (a1 a2 : HashSet α) :=
+def mergeHashSet {α : Type u} [BEq α] [Hashable α] (a1 a2 : Std.HashSet α) :=
   if a1.size < a2.size then
     a2.insertMany a1.toArray
   else
@@ -22,4 +22,4 @@ class Container {α : Type u} (C : Type v → Type w) where
   insertCorrect₁ : ∀ (c : C β) (k : α) (v : β), get? (insert c k v) k = .some val
   insertCorrect₂ : ∀ (c : C β) (k₁ k₂ : α) (v : β), k₁ ≠ k₂ → get? (insert c k₁ v) k₂ = get? c k₂
 
-end Auto
+end Auto

Auto/Lib/DeCompile.lean

@@ -13,7 +13,7 @@ namespace ExprDeCompile
 --   as explicit
 
 structure Context where
-  usedNames : HashSet String
+  usedNames : Std.HashSet String
 
 structure State where
   binderNames : Array String := #[]
@@ -69,7 +69,7 @@ private partial def exprDeCompileAux (final : Bool) (e : Expr) : ExprDeCompM Str
       return ret
     let fs ← exprDeCompileAux final f
     let argss ← args.mapM (exprDeCompileAux final)
-    let argssC := String.intercalate " " argss.data
+    let argssC := String.intercalate " " argss.toList
     return s!"({fs} {argssC})"
   | Expr.proj _ idx b =>
     let bs ← exprDeCompileAux final b
@@ -94,7 +94,7 @@ private partial def exprDeCompileAux (final : Bool) (e : Expr) : ExprDeCompM Str
   | Expr.bvar n =>
     let bn := (← get).binderNames
     return bn[bn.size - n - 1]!
-where 
+where
   constFinalDeComp (name : Name) (us : List Level) :=
     if List.length us == 0 then
       "@" ++ name.toString
@@ -118,7 +118,7 @@ where
       e := .lam `_ (ty.instantiateLevelParams lparams cst.constLevels!) e .default
     return e
 
-def levelCollectNames (l : Level) : StateT (HashSet String) MetaM Unit := do
+def levelCollectNames (l : Level) : StateT (Std.HashSet String) MetaM Unit := do
   match l with
   | .zero => return
   | .succ l => levelCollectNames l
@@ -127,7 +127,7 @@ def levelCollectNames (l : Level) : StateT (HashSet String) MetaM Unit := do
   | .max l1 l2 => levelCollectNames l1; levelCollectNames l2
   | .imax l1 l2 => levelCollectNames l1; levelCollectNames l2
 
-def exprCollectNames (e : Expr) : StateT (HashSet String) MetaM Unit := do
+def exprCollectNames (e : Expr) : StateT (Std.HashSet String) MetaM Unit := do
   match e with
   | Expr.forallE _ d b _ => exprCollectNames d; exprCollectNames b
   | Expr.lam _ d b _ => exprCollectNames d; exprCollectNames b
@@ -143,7 +143,7 @@ def exprCollectNames (e : Expr) : StateT (HashSet String) MetaM Unit := do
   | Expr.lit _ => return
   | Expr.sort l => levelCollectNames l
   | Expr.mvar .. => return
-  | Expr.fvar f => 
+  | Expr.fvar f =>
     let some decl := (← getLCtx).find? f
       | throwError "Unknown free variable {e}"
     let name := decl.userName.toString
@@ -212,4 +212,4 @@ universe u
 
 --/
 
-end Auto
+end Auto

Auto/Lib/ExprExtra.lean

@@ -46,7 +46,7 @@ def Expr.forallBinders (e : Expr) : Array (Name × Expr × BinderInfo) :=
     | _ => []
   Array.mk (aux e)
 
-def Expr.collectRawM [Monad m] (p : Expr → m Bool) : Expr → m (HashSet Expr)
+def Expr.collectRawM [Monad m] (p : Expr → m Bool) : Expr → m (Std.HashSet Expr)
 | e@(.forallE _ d b _) => do
   let hd ← collectRawM p d
   let hb ← collectRawM p b
@@ -70,7 +70,7 @@ def Expr.collectRawM [Monad m] (p : Expr → m Bool) : Expr → m (HashSet Expr)
 | e@(.proj _ _ b) => do
   let hb ← collectRawM p b
   addp? p e hb
-| e => addp? p e HashSet.empty
+| e => addp? p e Std.HashSet.empty
 where addp? p e hs := do
   if ← p e then
     return hs.insert e

Auto/Lib/LevelExtra.lean

@@ -17,13 +17,13 @@ def Level.collectLevelMVars (l : Level) : MetaM (Array LMVarId) := do
   let hset := go l
   return hset.toArray
 where
-  go : Level → HashSet LMVarId
+  go : Level → Std.HashSet LMVarId
   | .zero => {}
   | .succ l => go l
   | .max l₁ l₂ => mergeHashSet (go l₁) (go l₂)
   | .imax l₁ l₂ => mergeHashSet (go l₁) (go l₂)
   | .param _ => {}
-  | .mvar id => HashSet.empty.insert id
+  | .mvar id => Std.HashSet.empty.insert id
 
 def Level.findParam? (p : Name → Bool) : Level → Option Name
 | .zero => .none
@@ -36,4 +36,4 @@ def Level.findParam? (p : Name → Bool) : Level → Option Name
   | false => .none
 | .mvar _ => .none
 
-end Auto
+end Auto

Auto/Lib/MessageData.lean

@@ -17,6 +17,6 @@ def MessageData.list (as : List α) (f : α → MessageData) : MessageData :=
   .compose m!"[" (.compose (MessageData.intercalate m!", " (as.map f)) m!"]")
 
 def MessageData.array (as : Array α) (f : α → MessageData) : MessageData :=
-  MessageData.list as.data f
+  MessageData.list as.toList f
 
-end Auto
+end Auto

Auto/Lib/MonadUtils.lean

@@ -62,9 +62,9 @@ def structureProjs (structTy : Expr) : CoreM (Name × Expr × Array (Name × Exp
     | throwError s!"structureProjs :: {structName} is not a structure"
   let structMkExpr := mkAppN (Expr.const structDotMk lvls) structTy.getAppArgs
   let tyArgs := structTy.getAppArgs
-  let nameMap : HashMap Name StructureFieldInfo := HashMap.ofList
-    (structInfo.fieldInfo.map (fun sfi => (sfi.fieldName, sfi))).data
-  let sorted := structInfo.fieldNames.map (fun name => nameMap.find! name)
+  let nameMap : Std.HashMap Name StructureFieldInfo := Std.HashMap.ofList
+    (structInfo.fieldInfo.map (fun sfi => (sfi.fieldName, sfi))).toList
+  let sorted := structInfo.fieldNames.map (fun name => nameMap.get! name)
   let fieldInfos := sorted.map (fun i =>
       -- Field name, Projection function
       (i.fieldName, mkAppN (Expr.const i.projFn lvls) tyArgs))