revert to v4.25.0

Author: PratherConid

Auto/Embedding/LCtx.lean

@@ -494,7 +494,7 @@ section push
   theorem pushLCtxs_cons (xs : List α) (lctx : Nat → α) :
     pushLCtxs (x :: xs) lctx = pushLCtx x (pushLCtxs xs lctx) := by
     apply funext; intros n; cases n <;>
-      simp [pushLCtxs, pushLCtx, Nat.blt, Nat.ble]
+      simp [pushLCtxs, pushLCtx, Nat.blt, Nat.ble, Nat.zero_ble]
 
   theorem pushLCtxs_append (xs ys : List α) (lctx : Nat → α) :
     pushLCtxs (xs ++ ys) lctx = pushLCtxs xs (pushLCtxs ys lctx) := by
@@ -512,7 +512,7 @@ section push
 
   theorem pushLCtxs_cons_zero (xs : List α) (lctx : Nat → α) :
     pushLCtxs (x :: xs) lctx 0 = x := by
-    dsimp [pushLCtxs, Nat.blt, Nat.ble, Nat.zero_ble]
+    simp [pushLCtxs, Nat.blt, Nat.ble, Nat.zero_ble]
 
   theorem pushLCtxs_cons_succ (xs : List α) (lctx : Nat → α) (n : Nat) :
     pushLCtxs (x :: xs) lctx (.succ n) = pushLCtxs xs lctx n := by
@@ -608,7 +608,11 @@ section push
     HEq (pushLCtxsDep (.cons x xs) lctx) (pushLCtxDep x (pushLCtxsDep xs lctx)) := by
     apply HEq.funext; intros n; cases n
     case zero =>
-      simp [pushLCtxs, pushLCtx, Nat.blt, Nat.ble, HList.getD]
+      simp only [
+        pushLCtxs, List.length_cons, Nat.blt, Nat.succ_eq_add_one,
+        Nat.reduceAdd, Nat.ble, List.getD_cons_zero, id_eq, HList.getD, pushLCtx
+      ]
+      rw [Nat.zero_ble]
     case succ n =>
       dsimp [pushLCtxs, pushLCtx, Nat.blt, Nat.ble]
       rw [Nat.succ_sub_succ]; rfl
@@ -617,7 +621,11 @@ section push
     {lctxty : α → Sort u} {ty : α} (x : lctxty ty) {tys : List α}
     (xs : HList lctxty tys) {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) :
     HEq (pushLCtxsDep (.cons x xs) lctx 0) x := by
-    simp [pushLCtxs, Nat.blt, Nat.ble, HList.getD]
+    simp only [
+      pushLCtxs, List.length_cons, Nat.blt, Nat.succ_eq_add_one,
+      Nat.reduceAdd, Nat.ble, List.getD_cons_zero, id_eq, HList.getD
+    ]
+    rw [Nat.zero_ble]
 
   theorem pushLCtxsDep_cons_succ
     {lctxty : α → Sort u} {ty : α} (x : lctxty ty) {tys : List α}
@@ -764,9 +772,17 @@ section push
       dsimp at heq; rw [← heq]
       rw [HList.ofFun_succ];
       congr
+      case e_3.h =>
+        simp [pushLCtxs, Nat.blt, Nat.ble, Nat.zero_ble]
       case e_4.h =>
         dsimp; rw [pushLCtxs_cons_succ_Fn]
         apply List.ofFun_ofPushLCtx; rfl
+      case e_5 =>
+        simp only [
+          pushLCtxs, List.length_cons, Nat.blt, Nat.succ_eq_add_one,
+          Nat.reduceAdd, Nat.ble, List.getD_cons_zero, id_eq, HList.getD
+        ]
+        rw [Nat.zero_ble]
       case e_6 =>
         apply HEq.trans _ (ofFun_ofPushLCtxDep rfl xs lctx)
         congr

Auto/Embedding/LamConv.lean

@@ -964,6 +964,8 @@ theorem LamWF.interp_instantiate1.{u}
   case eqBody => rw [pushLCtxAt_zero]
   case eqLarge =>
     apply eq_of_heq; apply LamWF.interp_heq <;> try rfl
+    case h.HLCtxTyEq =>
+      rw [pushLCtxAt_zero]
     case h.HLCtxTermEq =>
       apply HEq.trans (HEq.symm (pushLCtxAtDep_zero _ _)) _
       apply pushLCtxAtDep_heq <;> try rfl

Auto/EvaluateAuto/NameArr.lean

@@ -40,7 +40,7 @@ def Name.parseUniqRepr (n : String) : Name :=
     if s[0]? == '\\' then
       if let .some c := s[1]? then
         if c.isDigit then
-          return .inr ((String.toNat? (String.ofList (s.drop 1))).getD 0)
+          return .inr ((String.toNat? (String.mk (s.drop 1))).getD 0)
     let mut ret := ""
     let mut escape := false
     for c in s do

Auto/EvaluateAuto/OS.lean

@@ -19,7 +19,7 @@ where
   | '`' => "\\`"
   | '\"' => "\\\""
   | '\\' => "\\\\"
-  | c => String.ofList [c]
+  | c => String.mk [c]
 
 def runLeanFileUsingNewLeanProcess
   (leanFile : String) (memoryLimitKb : Nat) (timeLimitS : Nat) :

Auto/IR/SMT.lean

@@ -99,7 +99,7 @@ def SpecConst.toString : SpecConst → String
 | .binary bs => bs.foldl (fun acc b => acc.push (if b then '1' else '0')) "#b"
 | .num n     => ToString.toString (repr n)
 where specCharRepr (c : Char) : String :=
-  "\\u{" ++ String.ofList (Nat.toDigits 16 c.toNat) ++ "}"
+  "\\u{" ++ String.mk (Nat.toDigits 16 c.toNat) ++ "}"
 
 mutual
 

Auto/Lib/HList.lean

@@ -88,7 +88,7 @@ theorem HList.getD_append_left (xs : HList β as) (ys : HList β bs) (h : i < as
     dsimp [append]; cases i
     case zero => apply HEq.rfl
     case succ i =>
-      dsimp [getD]; apply IH; apply Nat.le_of_succ_le_succ h
+      simp only [getD]; apply IH; apply Nat.le_of_succ_le_succ h
 
 theorem HList.getD_append_right (xs : HList β as) (ys : HList β bs) (h : i ≥ as.length) :
   HEq ((append xs ys).getD df i) (ys.getD df (i - as.length)) := by
@@ -98,7 +98,7 @@ theorem HList.getD_append_right (xs : HList β as) (ys : HList β bs) (h : i ≥
     dsimp [append]; cases i
     case zero => contradiction
     case succ i =>
-      dsimp [getD]; rw [Nat.succ_sub_succ];
+      simp only [getD]; rw [Nat.succ_sub_succ];
       apply IH; apply Nat.le_of_succ_le_succ h
 
 def HList.append_get_left (xs : HList β (as ++ bs)) : HList β as :=

Auto/MathlibEmulator/ToExpr.lean

@@ -57,7 +57,7 @@ instance [ToLevel.{u}] : ToExpr PUnit.{u+1} where
   toTypeExpr := mkConst ``PUnit [toLevel.{u+1}]
 
 deriving instance ToExpr for String.Pos.Raw
-deriving instance ToExpr for Substring.Raw
+deriving instance ToExpr for Substring
 deriving instance ToExpr for SourceInfo
 deriving instance ToExpr for Syntax.Preresolved
 deriving instance ToExpr for Syntax

Auto/Parser/LeanLex.lean

@@ -15,7 +15,7 @@ private def sort : List Nat → List Nat :=
 -- Character class
 namespace CC
 
-private def alls    := String.ofList ((List.range 128).map Char.ofNat)
+private def alls    := String.mk ((List.range 128).map Char.ofNat)
 private def uppers  := "ABCDEFGHIJKLMNOPQRSTUVWXYZ"
 private def lowers  := "abcdefghijklmnopqrstuvwxyz"
 private def alphas  := "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz"
@@ -25,9 +25,9 @@ private def xdigits := "0123456789ABCDEFabcdef"
 private def puncts  := ".,!?:…"
 private def blanks  := " \t"
 private def spaces  := " \t\n\r\x0c\x0b"
-private def cntrls  := String.ofList ((List.range 32).map Char.ofNat)
-private def graphs  := String.ofList (alls.toList.filter (fun x => !" \t\n\r\x0c\x0b".toList.contains x))
-private def prints  := String.ofList (alls.toList.filter (fun x => !"\t\n\r\x0c\x0b".toList.contains x))
+private def cntrls  := String.mk ((List.range 32).map Char.ofNat)
+private def graphs  := String.mk (alls.toList.filter (fun x => !" \t\n\r\x0c\x0b".toList.contains x))
+private def prints  := String.mk (alls.toList.filter (fun x => !"\t\n\r\x0c\x0b".toList.contains x))
 
 inductive Ty where
   | all
@@ -95,7 +95,7 @@ where
     | [] => Std.HashSet.emptyWithCapacity
     | b :: bl => (go bl).insertMany (toHashSet b)
 
-def EREBracket.toString (e : EREBracket) := String.ofList e.toHashSet.toList
+def EREBracket.toString (e : EREBracket) := String.mk e.toHashSet.toList
 
 instance : ToString EREBracket where
   toString := EREBracket.toString
@@ -133,7 +133,7 @@ deriving BEq, Hashable, Inhabited
 def ERE.inStr (s : String) := ERE.bracket (.inStr s)
 
 /-- Match the given string -/
-def ERE.ofStr (s : String) := ERE.comp ⟨s.toList.map (fun c => .inStr (String.ofList [c]))⟩
+def ERE.ofStr (s : String) := ERE.comp ⟨s.toList.map (fun c => .inStr (String.mk [c]))⟩
 
 def ERE.ofCC (c : CC.Ty) := ERE.bracket (.cc c)
 
@@ -299,7 +299,7 @@ end
 def CharGrouping.toStringForChar (cg : CharGrouping Char) : String :=
   CharGrouping.toStringAux cg (fun l =>
     let sorted := sort (l.toList.map Char.toNat)
-    let str := String.ofList (sorted.map Char.ofNat)
+    let str := String.mk (sorted.map Char.ofNat)
     ToString.toString (repr str))
 
 instance : ToString (CharGrouping Char) where
@@ -308,7 +308,7 @@ instance : ToString (CharGrouping Char) where
 def ADFA.toStringForChar (a : ADFA Char) : String :=
   ADFA.toStringAux a (fun l =>
     let sorted := sort (l.toList.map Char.toNat)
-    let str := String.ofList (sorted.map Char.ofNat)
+    let str := String.mk (sorted.map Char.ofNat)
     ToString.toString (repr str))
 
 instance : ToString (ADFA Char) where
@@ -418,7 +418,7 @@ instance : ToString LexResultTy where
 structure LexResult where
   type       : LexResultTy
   -- Matched part
-  matched    : Substring.Raw
+  matched    : Substring
   -- Whether the appended `end of string` group is matched
   endSMatched : Bool
   state      : Nat
@@ -452,7 +452,7 @@ instance : ToString LexResult where
   We prepend `s` with the "beginning of string" group
     and append to `s` the "end of string" group
 -/
-def ERE.ADFALexEagerL (a : ADFA Char) (s : Substring.Raw) (cfg : LexConfig) : LexResult := Id.run <| do
+def ERE.ADFALexEagerL (a : ADFA Char) (s : Substring) (cfg : LexConfig) : LexResult := Id.run <| do
   -- Current position in `s`
   let mut p : String.Pos.Raw := s.startPos
   -- The value of `b` will represent where the match begins

Auto/Parser/LexInit.lean

@@ -11,10 +11,10 @@ namespace SMTSexp
 
 open Regex
 
-def whitespace : String := (String.ofList
+def whitespace : String := (String.mk
   ([9, 10, 13, 32].map Char.ofNat))
 
-def unprintable : String := String.ofList
+def unprintable : String := String.mk
   ((127 :: List.range 32).map Char.ofNat)
 
 def comment : ERE :=

Auto/Parser/SMTSexp.lean

@@ -35,7 +35,7 @@ def LexVal.toString : LexVal → String
     let nfrac := n % m
     let nfracs := s!"{nfrac}"
     let nfracs :=
-      String.ofList ((List.range (pow - nfracs.length)).map (fun _ => '0')) ++
+      String.mk ((List.range (pow - nfracs.length)).map (fun _ => '0')) ++
       nfracs
     s!"{nint}." ++ nfracs
 | .str s   => "\"" ++ String.intercalate "\"\"" (s.splitOn "\"") ++ "\""
@@ -78,7 +78,7 @@ def LexVal.ofString (s : String) (attr : String) : LexVal :=
   | "quotedsymbol" => .symb ((s.drop 1).take (s.length - 2))
   | "keyword"      => .kw (s.drop 1)
   | "comment"      =>
-    let rn : Nat := if String.Pos.Raw.get s (String.Pos.Raw.prev s (String.Pos.Raw.prev s s.rawEndPos)) == '\r' then 1 else 0
+    let rn : Nat := if String.Pos.Raw.get s (String.Pos.Raw.prev s (String.Pos.Raw.prev s s.endPos)) == '\r' then 1 else 0
     .comment ((s.drop 1).take (s.length - 2 - rn))
   | _              => panic! s!"LexVal.ofString :: {repr attr} is not a valid attribute"
 
@@ -139,16 +139,16 @@ local instance : Hashable Char := ⟨fun c => hash c.val⟩
      by `ERE.ADFALexEagerL SMTSexp.lexiconADFA`, and never as `done`.
 -/
 def parseSexp (s : String) (p : String.Pos.Raw) (partialResult : PartialResult) : ParseResult := Id.run <| do
-  if p == s.rawEndPos then
+  if p == s.endPos then
     return .incomplete partialResult p
   let nextLexicon (p : String.Pos.Raw) (lst : Nat) :=
-    Regex.ERE.ADFALexEagerL SMTSexp.lexiconADFA ⟨s, p, s.rawEndPos⟩
+    Regex.ERE.ADFALexEagerL SMTSexp.lexiconADFA ⟨s, p, s.endPos⟩
       {strict := true, initS := lst, prependBeginS := false, appendEndS := false}
   let mut lst := partialResult.lst
   let mut lexpart := partialResult.lexpart
   let mut pstk := partialResult.pstk
   let mut p := p
-  let endPos := s.rawEndPos
+  let endPos := s.endPos
   while true do
     -- If we're not resuming from an incomplete
     --   match of lexicon, skip white space