update to v4.13.0

Auto/Embedding/Lam2Base.lean

@@ -121,9 +121,9 @@ def Lam₂Type.check_iff_interp
     simp [check, interp]
     cases Nat.decLt n (List.length lctx)
     case isTrue h =>
-      simp [h]; simp [List.get?_eq_get h]
+      simp [h]
     case isFalse h =>
-      simp [h]; simp at h; simp [List.get?_len_le h]
+      simp [h, List.getElem?_eq]
   case func fn arg IHfn IHarg =>
     revert IHfn IHarg
     simp [check, interp]
@@ -134,9 +134,9 @@ def Lam₂Type.check_iff_interp
       simp;
       match cifn : interp val lctx fn, ciarg : interp val lctx arg with
       | .some ⟨0, _⟩, .some ⟨0, _⟩ => simp
-      | .some ⟨0, _⟩, .some ⟨n + 1, _⟩ => simp; simp_arith
+      | .some ⟨0, _⟩, .some ⟨n + 1, _⟩ => simp
       | .some ⟨0, _⟩, .none => simp
-      | .some ⟨n + 1, _⟩, _ => simp; simp_arith
+      | .some ⟨n + 1, _⟩, _ => simp
       | .none , _ => simp
     | .some 0, .some (n + 1) =>
       simp;
@@ -168,7 +168,7 @@ def Lam₂Type.check_iff_interp
       simp;
       match cifn : interp val lctx fn, ciarg : interp val lctx arg with
       | .some ⟨n + 1, _⟩, .some ⟨0, _⟩ => simp
-      | .some ⟨n + 1, _⟩, .some ⟨m + 1, _⟩ => simp; simp_arith
+      | .some ⟨n + 1, _⟩, .some ⟨m + 1, _⟩ => simp
       | .some ⟨n + 1, _⟩, .none => simp
       | .some ⟨0, _⟩, _ => simp
       | .none , _ => simp
@@ -185,7 +185,7 @@ def Lam₂Type.check_iff_interp
     | .some 0, _ =>
       simp;
       match cifn : interp val lctx fn with
-      | .some ⟨n + 1, _⟩ => simp; simp_arith
+      | .some ⟨n + 1, _⟩ => simp
       | .some ⟨0, _⟩ => simp
       | .none => simp
     | .none, _ =>

Auto/Embedding/LamBase.lean

@@ -3780,7 +3780,7 @@ def LamWF.bvarApps
           rw [List.length_reverse]; apply Nat.le_refl
         dsimp [lctxr]; rw [← List.reverseAux, List.reverseAux_eq]
         rw [pushLCtxs_lt (by rw [List.length_append]; apply Nat.le_trans exlt (Nat.le_add_right _ _))]
-        rw [List.getD_eq_getElem?_getD]; rw [List.getElem?_append exlt];
+        rw [List.getD_eq_getElem?_getD]; rw [List.getElem?_append_left exlt];
         rw [List.getElem?_reverse (by dsimp [List.length]; apply Nat.le_refl _)]
         dsimp [List.length]; simp
       conv => enter [2, 3]; rw [tyeq]

Auto/Embedding/LamBitVec.lean

@@ -55,10 +55,10 @@ 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_zeroExtend' {a : BitVec n} (le : n ≤ m) : (a.setWidth' le).toNat = a.toNat := rfl
 
   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 BitVec.setWidth; cases hdec : decide (n ≤ i)
     case false =>
       have hnle := of_decide_eq_false hdec
       rw [Bool.dite_eq_false (proof:=hnle)]; rfl
@@ -101,9 +101,9 @@ namespace BVLems
     apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_of_le_right (.step .refl) h)
 
   theorem msb_equiv_lt (a : BitVec n) : !a.msb ↔ a.toNat < 2 ^ (n - 1) := by
-    dsimp [BitVec.msb, BitVec.getMsb, BitVec.getLsb]
+    dsimp [BitVec.msb, BitVec.getMsbD, BitVec.getLsbD]
     cases n
-    case zero => simp
+    case zero => cases a <;> simp
     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 +112,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 => cases a <;> simp
     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
@@ -133,7 +133,7 @@ namespace BVLems
         rw [Nat.sub_one, Nat.pred_lt_iff_le (Nat.two_pow_pos _)]
         apply Nat.le_trans (Nat.sub_le _ _) (Nat.pow_le_pow_of_le_right (.step .refl) h)
       apply eq_of_val_eq; rw [toNat_ofNatLt, hzero]
-      rw [toNat_neg, Int.mod_def', Int.emod]; dsimp only;
+      rw [toNat_neg, Int.mod_def', Int.emod]
       rw [Nat.zero_mod, Int.natAbs_ofNat, Nat.succ_eq_add_one, Nat.zero_add]
       rw [Int.subNatNat_of_sub_eq_zero ((Nat.sub_eq_zero_iff_le).mpr (Nat.two_pow_pos _))]
       rw [Int.toNat_ofNat, BitVec.toNat_ofNat]

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/Embedding/LamInhReasoning.lean

@@ -10,18 +10,18 @@ namespace Auto.Embedding.Lam
 def Inhabitation.subsumeQuick (s₁ s₂ : LamSort) : Bool :=
   let s₁args := s₁.getArgTys
   let s₁res := s₁.getResTy
-  let s₂args := HashSet.empty.insertMany s₂.getArgTys
+  let s₂args := Std.HashSet.empty.insertMany s₂.getArgTys
   let s₂res := s₂.getResTy
   s₂args.contains s₂res || (s₁res == s₂res && (
     s₁args.all (fun arg => s₂args.contains arg)
   ))
 
 /-- Run a quick test on whether the inhabitation of `s` is trivial -/
-def Inhabitation.trivialQuick := go HashSet.empty
-where go (argTys : HashSet LamSort) (s : LamSort) : Bool :=
+def Inhabitation.trivialQuick := go Std.HashSet.empty
+where go (argTys : Std.HashSet LamSort) (s : LamSort) : Bool :=
   match s with
   | .func argTy resTy =>
     argTys.contains s || go (argTys.insert argTy) resTy
   | _ => argTys.contains s
 
-end Auto.Embedding.Lam
+end Auto.Embedding.Lam

Auto/Embedding/LamSystem.lean

@@ -209,7 +209,7 @@ theorem LamTerm.rwGenAllWith_lam : rwGenAllWith conv rty (.lam s body) =
   | .none =>
     match rty with
     | .func _ resTy => (rwGenAllWith conv resTy body).bind (LamTerm.lam s ·)
-    | _ => .none := by simp [rwGenAllWith]
+    | _ => .none := by cases rty <;> simp [rwGenAllWith]
 
 theorem LamTerm.rwGenAllWith_app : rwGenAllWith conv rty (.app s fn arg) =
   match conv rty (.app s fn arg) with
@@ -1492,7 +1492,7 @@ theorem LamTerm.evarBounded_rwGenAllWith (H : ∀ s, evarBounded (conv s) bound)
     case none.refl => apply Nat.le_max_right
     case some.refl => apply H _ _ _ h
   case lam s' body IH =>
-    simp [LamTerm.rwGenAllWith]
+    rw [LamTerm.rwGenAllWith_lam]
     match h₁ : conv s (.lam s' body) with
     | .some t' => intro h₂; cases h₂; apply H _ _ _ h₁
     | .none =>
@@ -1547,7 +1547,7 @@ theorem LamTerm.evarEquiv_rwGenAllWith (H : ∀ s, evarEquiv (conv s)) :
     case none.refl => rfl
     case some.refl => apply H _ _ _ h
   case lam s' body IH =>
-    simp [LamTerm.rwGenAllWith]
+    rw [LamTerm.rwGenAllWith_lam]
     match h₁ : conv s (.lam s' body) with
     | .some t' => intro h₂; cases h₂; apply H _ _ _ h₁
     | .none =>
@@ -1592,7 +1592,7 @@ theorem LamGenConvWith.rwGenAllWith (H : LamGenConvWith lval conv) : LamGenConvW
     case none.refl => apply LamGenEquivWith.refl
     case some.refl => apply H _ _ _ h
   case lam s' body IH =>
-    simp [LamTerm.rwGenAllWith]
+    rw [LamTerm.rwGenAllWith_lam]
     match h₁ : conv s (.lam s' body) with
     | .some t' => intro h₂; cases h₂; apply H _ _ _ h₁
     | .none =>

Auto/Embedding/LamTermInterp.lean

@@ -164,7 +164,7 @@ theorem LamTerm.lamCheck?Eq'_bvar
   (h : lctx.get? n = .some ⟨s, val⟩) :
   LamTerm.lamCheck?Eq' lval lctx (.bvar n) s := by
   dsimp [lamCheck?Eq', lamCheck?]; have ⟨hlt, _⟩ := List.get?_eq_some.mp h
-  rw [pushLCtxs_lt hlt, List.getD_eq_get?, h]; rfl
+  rw [pushLCtxs_lt hlt, List.getD_eq_getElem?_getD, ← List.get?_eq_getElem?, h]; rfl
 
 theorem LamTerm.lamCheck?Eq'_lam
   (h : LamTerm.lamCheck?Eq' lval (⟨argTy, val⟩ :: lctx) body s) :
@@ -201,7 +201,7 @@ theorem LamTerm.interpEq_bvar
   (s : LamSort) (val : s.interp lval.tyVal) (h : lctx.get? n = .some ⟨s, val⟩) :
   LamTerm.interpEq lval lctx (.bvar n) val := by
   dsimp [interpEq, interp]; have ⟨hlt, _⟩ := List.get?_eq_some.mp h
-  rw [pushLCtxs_lt hlt, List.getD_eq_get?, h]; rfl
+  rw [pushLCtxs_lt hlt, List.getD_eq_getElem?_getD, ← List.get?_eq_getElem?, h]; rfl
 
 theorem LamTerm.interpEq_lam
   (lval : LamValuation) (lctx : List ((s : LamSort) × s.interp lval.tyVal))
@@ -243,7 +243,7 @@ namespace Interp
 
 structure State where
   sortFVars    : Array FVarId               := #[]
-  sortMap      : HashMap LamSort FVarId     := {}
+  sortMap      : Std.HashMap LamSort FVarId     := {}
   -- Let `n := lctxTyRev.size`
   -- Reversed
   lctxTyRev    : Array LamSort              := #[]
@@ -253,11 +253,11 @@ structure State where
   -- Required : `lctxTyDrop[i] ≝ lctxTyRev[:(i+1)].data ≝ lctxTerm[(n-i-1):]`
   lctxTyDrop   : Array FVarId               := #[]
   -- Required : `tyEqFact[i][j] : lctxTy[i:].drop j = lctxTy[i+j:]`
-  typeEqFact   : HashMap (Nat × Nat) FVarId := {}
+  typeEqFact   : Std.HashMap (Nat × Nat) FVarId := {}
   -- Required : `lctxTermDrop[i] ≝ lctxTermRev[:(i+1)].data ≝ lctxTerm[(n-i-1):]`
   lctxTermDrop : Array FVarId               := #[]
   -- Required : `termEqFact[i][j] : lctxTerm[i:].drop j = lctxTerm[i+j:]`
-  termEqFact   : HashMap (Nat × Nat) FVarId := {}
+  termEqFact   : Std.HashMap (Nat × Nat) FVarId := {}
   -- Required : `lctxCon[i] : lctxTerm[i].map Sigma.snd = lctxTy[i]`
   lctxCon      : Array FVarId               := #[]
 
@@ -282,7 +282,7 @@ def getLCtxTy! (idx : Nat) : InterpM LamSort := do
 def sort2FVarId (s : LamSort) : InterpM FVarId := do
   let sortMap ← getSortMap
   let userName := (`interpsf).appendIndexAfter (← getSortMap).size
-  match sortMap.find? s with
+  match sortMap.get? s with
   | .some id => return id
   | .none =>
     match s with
@@ -336,4 +336,4 @@ where withLCtxTy {α : Type} (s : LamSort) (k : InterpM α) : InterpM α := do
 
 end Interp
 
-end Auto.Embedding.Lam
+end Auto.Embedding.Lam

Auto/Embedding/Lift.lean

@@ -85,10 +85,10 @@ def imulLift.{u} (m n : GLift.{1, u} Int) :=
   GLift.up (Int.mul m.down n.down)
 
 def idivLift.{u} (m n : GLift.{1, u} Int) :=
-  GLift.up (Int.div m.down n.down)
+  GLift.up (Int.tdiv m.down n.down)
 
 def imodLift.{u} (m n : GLift.{1, u} Int) :=
-  GLift.up (Int.mod m.down n.down)
+  GLift.up (Int.tmod m.down n.down)
 
 def iedivLift.{u} (m n : GLift.{1, u} Int) :=
   GLift.up (Int.ediv m.down n.down)