chore: fix tests

src/Init/Data/RArray.lean

@@ -26,11 +26,11 @@ See `RArray.ofFn` and `RArray.ofArray` in module `Lean.Data.RArray` for function
 It is not universe-polymorphic. ; smaller proof objects and no complication with the `ToExpr` type
 class.
 -/
-inductive RArray (α : Type u) : Type u where
+inductive RArray (α : Type) : Type where
   | leaf : α → RArray α
   | branch : Nat → RArray α → RArray α → RArray α
 
-variable {α : Type u}
+variable {α : Type}
 
 /-- The crucial operation, written with very little abstractional overhead -/
 noncomputable def RArray.get (a : RArray α) (n : Nat) : α :=

src/Init/Grind/CommRing/SOM.lean

@@ -35,10 +35,10 @@ def RArray.get (a : RArray α) (n : Nat) : α :=
 
 abbrev Context (α : Type u) := RArray α
 
-def Var.denote {α} (ctx : Context α) (v : Var) : α :=
+def Var.denote (ctx : Context α) (v : Var) : α :=
   ctx.get v
 
-def Expr.denote {α} [CommRing α] (ctx : Context α) : Expr → α
+def Expr.denote [CommRing α] (ctx : Context α) : Expr → α
   | .add a b  => denote ctx a + denote ctx b
   | .sub a b  => denote ctx a - denote ctx b
   | .mul a b  => denote ctx a * denote ctx b
@@ -55,7 +55,7 @@ structure Power where
 def Power.varLt (p₁ p₂ : Power) : Bool :=
   p₁.x.blt p₂.x
 
-def Power.denote {α} [CommRing α] (ctx : Context α) : Power → α
+def Power.denote [CommRing α] (ctx : Context α) : Power → α
   | {x, k} =>
     match k with
     | 0 => 1
@@ -67,11 +67,11 @@ inductive Mon where
   | cons (p : Power) (m : Mon)
   deriving BEq, Repr
 
-def Mon.denote {α} [CommRing α] (ctx : Context α) : Mon → α
+def Mon.denote [CommRing α] (ctx : Context α) : Mon → α
   | .leaf p => p.denote ctx
   | .cons p m => p.denote ctx * denote ctx m
 
-def Mon.denote' {α} [CommRing α] (ctx : Context α) : Mon → α
+def Mon.denote' [CommRing α] (ctx : Context α) : Mon → α
   | .leaf p => p.denote ctx
   | .cons p m => go (p.denote ctx) m
 where
@@ -222,23 +222,18 @@ def Poly.addConst (p : Poly) (k : Int) : Poly :=
   | .add k' m p => .add k' m (addConst p k)
 
 def Poly.insert (k : Int) (m : Mon) (p : Poly) : Poly :=
-  bif k == 0 then
-    p
-  else
-    go p
-where
-  go : Poly → Poly
-    | .num k' => .add k m (.num k')
-    | .add k' m' p =>
-      match m.grevlex m' with
-      | .eq =>
-        let k'' := k + k'
-        bif k'' == 0 then
-          p
-        else
-          .add k'' m p
-      | .lt => .add k m (.add k' m' p)
-      | .gt => .add k' m' (go p)
+  match p with
+  | .num k' => .add k m (.num k')
+  | .add k' m' p =>
+    match m.grevlex m' with
+    | .eq =>
+      let k'' := k + k'
+      bif k'' == 0 then
+        p
+      else
+        .add k'' m p
+    | .lt => .add k m (.add k' m' p)
+    | .gt => .add k' m' (insert k m p)
 
 def Poly.concat (p₁ p₂ : Poly) : Poly :=
   match p₁ with
@@ -248,8 +243,6 @@ def Poly.concat (p₁ p₂ : Poly) : Poly :=
 def Poly.mulConst (k : Int) (p : Poly) : Poly :=
   bif k == 0 then
     .num 0
-  else bif k == 1 then
-    p
   else
     go p
 where
@@ -296,6 +289,7 @@ where
     | .num k => acc.combine (p₂.mulConst k)
     | .add k m p₁ => go p₁ (acc.combine (p₂.mulMon k m))
 
+-- TODO: optimize
 def Poly.pow (p : Poly) (k : Nat) : Poly :=
   match k with
   | 0 => .num 1
@@ -315,153 +309,27 @@ def Expr.toPoly : Expr → Poly
     | .var x => Poly.ofMon (.leaf {x, k})
     | _ => a.toPoly.pow k
 
-/-!
-**Definitions for the `IsCharP` case**
-
-We considered using a single set of definitions parameterized by `Option c`, but decided against it to avoid
-unnecessary kernel‑reduction overhead. Once we can specialize definitions before they reach the kernel,
-we can merge the two versions. Until then, the `IsCharP` definitions will carry the `C` suffix.
--/
-def Poly.addConstC (p : Poly) (k : Int) (c : Nat) : Poly :=
-  match p with
-  | .num k' => .num ((k' + k) % c)
-  | .add k' m p => .add k' m (addConstC p k c)
-
-def Poly.insertC (k : Int) (m : Mon) (p : Poly) (c : Nat) : Poly :=
-  let k := k % c
-  bif k == 0 then
-    p
-  else
-    go k p
-where
-  go (k : Int) : Poly → Poly
-    | .num k' => .add k m (.num k')
-    | .add k' m' p =>
-      match m.grevlex m' with
-      | .eq =>
-        let k'' := (k + k') % c
-        bif k'' == 0 then
-          p
-        else
-          .add k'' m p
-      | .lt => .add k m (.add k' m' p)
-      | .gt => .add k' m' (go k p)
-
-def Poly.mulConstC (k : Int) (p : Poly) (c : Nat) : Poly :=
-  let k := k % c
-  bif k == 0 then
-    .num 0
-  else bif k == 1 then
-    p
-  else
-    go p
-where
-  go : Poly → Poly
-   | .num k' => .num ((k*k') % c)
-   | .add k' m p =>
-     let k := (k*k') % c
-     bif k == 0 then
-      go p
-    else
-      .add k m (go p)
-
-def Poly.mulMonC (k : Int) (m : Mon) (p : Poly) (c : Nat) : Poly :=
-  let k := k % c
-  bif k == 0 then
-    .num 0
-  else
-    go p
-where
-  go : Poly → Poly
-   | .num k' =>
-     let k := (k*k') % c
-     bif k == 0 then
-       .num 0
-     else
-       .add k m (.num 0)
-   | .add k' m' p =>
-     let k := (k*k') % c
-     bif k == 0 then
-       go p
-     else
-       .add k (m.mul m') (go p)
-
-def Poly.combineC (p₁ p₂ : Poly) (c : Nat) : Poly :=
-  go hugeFuel p₁ p₂
-where
-  go (fuel : Nat) (p₁ p₂ : Poly) : Poly :=
-    match fuel with
-    | 0 => p₁.concat p₂
-    | fuel + 1 => match p₁, p₂ with
-      | .num k₁, .num k₂ => .num ((k₁ + k₂) % c)
-      | .num k₁, .add k₂ m₂ p₂ => addConstC (.add k₂ m₂ p₂) k₁ c
-      | .add k₁ m₁ p₁, .num k₂ => addConstC (.add k₁ m₁ p₁) k₂ c
-      | .add k₁ m₁ p₁, .add k₂ m₂ p₂ =>
-        match m₁.grevlex m₂ with
-        | .eq =>
-          let k := (k₁ + k₂) % c
-          bif k == 0 then
-            go fuel p₁ p₂
-          else
-            .add k m₁ (go fuel p₁ p₂)
-        | .lt => .add k₁ m₁ (go fuel p₁ (.add k₂ m₂ p₂))
-        | .gt => .add k₂ m₂ (go fuel (.add k₁ m₁ p₁) p₂)
-
-def Poly.mulC (p₁ : Poly) (p₂ : Poly) (c : Nat) : Poly :=
-  go p₁ (.num 0)
-where
-  go (p₁ : Poly) (acc : Poly) : Poly :=
-    match p₁ with
-    | .num k => acc.combineC (p₂.mulConstC k c) c
-    | .add k m p₁ => go p₁ (acc.combineC (p₂.mulMonC k m c) c)
-
-def Poly.powC (p : Poly) (k : Nat) (c : Nat) : Poly :=
-  match k with
-  | 0 => .num 1
-  | 1 => p
-  | k+1 => p.mulC (powC p k c) c
-
-def Expr.toPolyC (e : Expr) (c : Nat) : Poly :=
-  go e
-where
-  go : Expr → Poly
-    | .num n   => .num (n % c)
-    | .var x   => Poly.ofVar x
-    | .add a b => (go a).combineC (go b) c
-    | .mul a b => (go a).mulC (go b) c
-    | .neg a   => (go a).mulConstC (-1) c
-    | .sub a b => (go a).combineC ((go b).mulConstC (-1) c) c
-    | .pow a k =>
-      match a with
-      | .num n => .num ((n^k) % c)
-      | .var x => Poly.ofMon (.leaf {x, k})
-      | _ => (go a).powC k c
-
-/-!
-Theorems for justifying the procedure for commutative rings in `grind`.
--/
-
-theorem Power.denote_eq {α} [CommRing α] (ctx : Context α) (p : Power)
+theorem Power.denote_eq [CommRing α] (ctx : Context α) (p : Power)
     : p.denote ctx = p.x.denote ctx ^ p.k := by
   cases p <;> simp [Power.denote] <;> split <;> simp [pow_zero, pow_succ, one_mul]
 
-theorem Mon.denote'_go_eq_denote {α} [CommRing α] (ctx : Context α) (a : α) (m : Mon)
+theorem Mon.denote'_go_eq_denote [CommRing α] (ctx : Context α) (a : α) (m : Mon)
     : denote'.go ctx a m = a * denote ctx m := by
   induction m generalizing a <;> simp [Mon.denote, Mon.denote'.go]
   next p' m ih =>
     simp [Mon.denote] at ih
     rw [ih, mul_assoc]
 
-theorem Mon.denote'_eq_denote {α} [CommRing α] (ctx : Context α) (m : Mon)
+theorem Mon.denote'_eq_denote [CommRing α] (ctx : Context α) (m : Mon)
     : denote' ctx m = denote ctx m := by
   cases m <;> simp [Mon.denote, Mon.denote']
   next p m => apply denote'_go_eq_denote
 
-theorem Mon.denote_ofVar {α} [CommRing α] (ctx : Context α) (x : Var)
+theorem Mon.denote_ofVar [CommRing α] (ctx : Context α) (x : Var)
     : denote ctx (ofVar x) = x.denote ctx := by
   simp [denote, ofVar, Power.denote_eq, pow_succ, pow_zero, one_mul]
 
-theorem Mon.denote_concat {α} [CommRing α] (ctx : Context α) (m₁ m₂ : Mon)
+theorem Mon.denote_concat [CommRing α] (ctx : Context α) (m₁ m₂ : Mon)
     : denote ctx (concat m₁ m₂) = m₁.denote ctx * m₂.denote ctx := by
   induction m₁ <;> simp [concat, denote, *]
   next p₁ m₁ ih => rw [mul_assoc]
@@ -476,7 +344,7 @@ private theorem eq_of_blt_false {a b : Nat} : a.blt b = false → b.blt a = fals
   replace h₂ := le_of_blt_false h₂
   exact Nat.le_antisymm h₂ h₁
 
-theorem Mon.denote_mulPow {α} [CommRing α] (ctx : Context α) (p : Power) (m : Mon)
+theorem Mon.denote_mulPow [CommRing α] (ctx : Context α) (p : Power) (m : Mon)
     : denote ctx (mulPow p m) = p.denote ctx * m.denote ctx := by
   fun_induction mulPow <;> simp [mulPow, *]
   next => simp [denote]
@@ -490,7 +358,7 @@ theorem Mon.denote_mulPow {α} [CommRing α] (ctx : Context α) (p : Power) (m :
     have := eq_of_blt_false h₁ h₂
     simp [denote, Power.denote_eq, pow_add, this, mul_assoc]
 
-theorem Mon.denote_mul {α} [CommRing α] (ctx : Context α) (m₁ m₂ : Mon)
+theorem Mon.denote_mul [CommRing α] (ctx : Context α) (m₁ m₂ : Mon)
     : denote ctx (mul m₁ m₂) = m₁.denote ctx * m₂.denote ctx := by
   unfold mul
   generalize hugeFuel = fuel
@@ -547,49 +415,45 @@ theorem Mon.eq_of_revlex {m₁ m₂ : Mon} : revlex m₁ m₂ = .eq → m₁ = m
 theorem Mon.eq_of_grevlex {m₁ m₂ : Mon} : grevlex m₁ m₂ = .eq → m₁ = m₂ := by
   simp [grevlex, then_eq]; intro; apply eq_of_revlex
 
-theorem Poly.denote_ofMon {α} [CommRing α] (ctx : Context α) (m : Mon)
+theorem Poly.denote_ofMon [CommRing α] (ctx : Context α) (m : Mon)
     : denote ctx (ofMon m) = m.denote ctx := by
   simp [ofMon, denote, intCast_one, intCast_zero, one_mul, add_zero]
 
-theorem Poly.denote_ofVar {α} [CommRing α] (ctx : Context α) (x : Var)
+theorem Poly.denote_ofVar [CommRing α] (ctx : Context α) (x : Var)
     : denote ctx (ofVar x) = x.denote ctx := by
   simp [ofVar, denote_ofMon, Mon.denote_ofVar]
 
-theorem Poly.denote_addConst {α} [CommRing α] (ctx : Context α) (p : Poly) (k : Int) : (addConst p k).denote ctx = p.denote ctx + k := by
+theorem Poly.denote_addConst [CommRing α] (ctx : Context α) (p : Poly) (k : Int) : (addConst p k).denote ctx = p.denote ctx + k := by
   fun_induction addConst <;> simp [addConst, denote, *]
   next => rw [intCast_add]
   next => simp [add_comm, add_left_comm, add_assoc]
 
-theorem Poly.denote_insert {α} [CommRing α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
+theorem Poly.denote_insert [CommRing α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
     : (insert k m p).denote ctx = k * m.denote ctx + p.denote ctx := by
-  simp [insert, cond_eq_if] <;> split
-  next => simp [*, intCast_zero, zero_mul, zero_add]
+  fun_induction insert <;> simp_all +zetaDelta [insert, denote, cond_eq_if]
+  next h₁ _ h₂ =>
+    rw [← add_assoc, Mon.eq_of_grevlex h₁, ← right_distrib, ← intCast_add, h₂, intCast_zero, zero_mul, zero_add]
+  next h₁ _ _ =>
+    rw [intCast_add, right_distrib, add_assoc, Mon.eq_of_grevlex h₁]
   next =>
-    fun_induction insert.go <;> simp_all +zetaDelta [insert.go, denote, cond_eq_if]
-    next h₁ _ h₂ =>
-      rw [← add_assoc, Mon.eq_of_grevlex h₁, ← right_distrib, ← intCast_add, h₂, intCast_zero, zero_mul, zero_add]
-    next h₁ _ _ =>
-      rw [intCast_add, right_distrib, add_assoc, Mon.eq_of_grevlex h₁]
-    next =>
-      rw [add_left_comm]
+    rw [add_left_comm]
 
-theorem Poly.denote_concat {α} [CommRing α] (ctx : Context α) (p₁ p₂ : Poly)
+theorem Poly.denote_concat [CommRing α] (ctx : Context α) (p₁ p₂ : Poly)
     : (concat p₁ p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
   fun_induction concat <;> simp [concat, *, denote_addConst, denote]
   next => rw [add_comm]
   next => rw [add_assoc]
 
-theorem Poly.denote_mulConst {α} [CommRing α] (ctx : Context α) (k : Int) (p : Poly)
+theorem Poly.denote_mulConst [CommRing α] (ctx : Context α) (k : Int) (p : Poly)
     : (mulConst k p).denote ctx = k * p.denote ctx := by
   simp [mulConst, cond_eq_if] <;> split
   next => simp [denote, *, intCast_zero, zero_mul]
   next =>
-    split <;> try simp [*, intCast_one, one_mul]
     fun_induction mulConst.go <;> simp [mulConst.go, denote, *]
     next => rw [intCast_mul]
     next => rw [intCast_mul, left_distrib, mul_assoc]
 
-theorem Poly.denote_mulMon {α} [CommRing α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
+theorem Poly.denote_mulMon [CommRing α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
     : (mulMon k m p).denote ctx = k * m.denote ctx * p.denote ctx := by
   simp [mulMon, cond_eq_if] <;> split
   next => simp [denote, *, intCast_zero, zero_mul]
@@ -598,7 +462,7 @@ theorem Poly.denote_mulMon {α} [CommRing α] (ctx : Context α) (k : Int) (m :
     next => simp [intCast_mul, intCast_zero, add_zero, mul_comm, mul_left_comm, mul_assoc]
     next => simp [Mon.denote_mul, intCast_mul, left_distrib, mul_comm, mul_left_comm, mul_assoc]
 
-theorem Poly.denote_combine {α} [CommRing α] (ctx : Context α) (p₁ p₂ : Poly)
+theorem Poly.denote_combine [CommRing α] (ctx : Context α) (p₁ p₂ : Poly)
     : (combine p₁ p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
   unfold combine; generalize hugeFuel = fuel
   fun_induction combine.go
@@ -610,22 +474,22 @@ theorem Poly.denote_combine {α} [CommRing α] (ctx : Context α) (p₁ p₂ : P
     simp +zetaDelta at h; simp [*, denote, intCast_add]
     rw [right_distrib, Mon.eq_of_grevlex hg, add_assoc]
 
-theorem Poly.denote_mul_go {α} [CommRing α] (ctx : Context α) (p₁ p₂ acc : Poly)
+theorem Poly.denote_mul_go [CommRing α] (ctx : Context α) (p₁ p₂ acc : Poly)
     : (mul.go p₂ p₁ acc).denote ctx = acc.denote ctx + p₁.denote ctx * p₂.denote ctx := by
   fun_induction mul.go
     <;> simp [mul.go, denote_combine, denote_mulConst, denote, *, right_distrib, denote_mulMon, add_assoc]
 
-theorem Poly.denote_mul {α} [CommRing α] (ctx : Context α) (p₁ p₂ : Poly)
+theorem Poly.denote_mul [CommRing α] (ctx : Context α) (p₁ p₂ : Poly)
     : (mul p₁ p₂).denote ctx = p₁.denote ctx * p₂.denote ctx := by
   simp [mul, denote_mul_go, denote, intCast_zero, zero_add]
 
-theorem Poly.denote_pow {α} [CommRing α] (ctx : Context α) (p : Poly) (k : Nat)
+theorem Poly.denote_pow [CommRing α] (ctx : Context α) (p : Poly) (k : Nat)
    : (pow p k).denote ctx = p.denote ctx ^ k := by
  fun_induction pow <;> simp [pow, denote, intCast_one, pow_zero]
  next => simp [pow_succ, pow_zero, one_mul]
  next => simp [denote_mul, *, pow_succ, mul_comm]
 
-theorem Expr.denote_toPoly {α} [CommRing α] (ctx : Context α) (e : Expr)
+theorem Expr.denote_toPoly [CommRing α] (ctx : Context α) (e : Expr)
    : e.toPoly.denote ctx = e.denote ctx := by
   fun_induction toPoly
     <;> simp [toPoly, denote, Poly.denote, Poly.denote_ofVar, Poly.denote_combine,
@@ -635,117 +499,5 @@ theorem Expr.denote_toPoly {α} [CommRing α] (ctx : Context α) (e : Expr)
   next => rw [intCast_pow]
   next => simp [Poly.denote_ofMon, Mon.denote, Power.denote_eq]
 
-theorem Poly.denote_addConstC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (p : Poly) (k : Int) : (addConstC p k c).denote ctx = p.denote ctx + k := by
-  fun_induction addConstC <;> simp [addConstC, denote, *]
-  next => rw [IsCharP.intCast_emod, intCast_add]
-  next => simp [add_comm, add_left_comm, add_assoc]
-
-theorem Poly.denote_insertC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
-    : (insertC k m p c).denote ctx = k * m.denote ctx + p.denote ctx := by
-  simp [insertC, cond_eq_if] <;> split
-  next =>
-    rw [← IsCharP.intCast_emod (p := c)]
-    simp +zetaDelta [*, intCast_zero, zero_mul, zero_add]
-  next =>
-    fun_induction insertC.go <;> simp_all +zetaDelta [insertC.go, denote, cond_eq_if]
-    next h₁ _ h₂ => rw [IsCharP.intCast_emod]
-    next h₁ _ h₂ =>
-      rw [← add_assoc, Mon.eq_of_grevlex h₁, ← right_distrib, ← intCast_add, ← IsCharP.intCast_emod (p := c), h₂,
-          intCast_zero, zero_mul, zero_add]
-    next h₁ _ _ =>
-      rw [IsCharP.intCast_emod, intCast_add, right_distrib, add_assoc, Mon.eq_of_grevlex h₁]
-    next => rw [IsCharP.intCast_emod]
-    next => rw [add_left_comm]
-
-theorem Poly.denote_mulConstC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (k : Int) (p : Poly)
-    : (mulConstC k p c).denote ctx = k * p.denote ctx := by
-  simp [mulConstC, cond_eq_if] <;> split
-  next =>
-    rw [← IsCharP.intCast_emod (p := c)]
-    simp [denote, *, intCast_zero, zero_mul]
-  next =>
-    split
-    next =>
-      rw [← IsCharP.intCast_emod (p := c)]
-      simp [*, intCast_one, one_mul]
-    next =>
-      fun_induction mulConstC.go <;> simp [mulConstC.go, denote, IsCharP.intCast_emod, cond_eq_if, *]
-      next => rw [intCast_mul]
-      next h _ =>
-        simp +zetaDelta at h; simp [*]
-        rw [left_distrib, ← mul_assoc, ← intCast_mul, ← IsCharP.intCast_emod (x := k * _) (p := c),
-            h, intCast_zero, zero_mul, zero_add]
-      next h _ =>
-        simp +zetaDelta at h
-        simp [*, denote, IsCharP.intCast_emod, intCast_mul, mul_assoc, left_distrib]
-
-theorem Poly.denote_mulMonC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
-    : (mulMonC k m p c).denote ctx = k * m.denote ctx * p.denote ctx := by
-  simp [mulMonC, cond_eq_if] <;> split
-  next =>
-    rw [← IsCharP.intCast_emod (p := c)]
-    simp [denote, *, intCast_zero, zero_mul]
-  next =>
-    fun_induction mulMonC.go <;> simp [mulMonC.go, denote, *, cond_eq_if]
-    next h =>
-      simp +zetaDelta at h; simp [*, denote]
-      rw [mul_assoc, mul_left_comm, ← intCast_mul, ← IsCharP.intCast_emod (x := k * _) (p := c), h]
-      simp [intCast_zero, mul_zero]
-    next h =>
-      simp +zetaDelta at h; simp [*, denote, IsCharP.intCast_emod]
-      simp [intCast_mul, intCast_zero, add_zero, mul_comm, mul_left_comm, mul_assoc]
-    next h _ =>
-      simp +zetaDelta at h; simp [*, denote, left_distrib]
-      rw [mul_left_comm]
-      conv => rhs; rw [← mul_assoc, ← mul_assoc, ← intCast_mul, ← IsCharP.intCast_emod (p := c)]
-      rw [Int.mul_comm] at h
-      simp [h, intCast_zero, zero_mul, zero_add]
-    next h _ =>
-      simp +zetaDelta at h
-      simp [*, denote, IsCharP.intCast_emod, Mon.denote_mul, intCast_mul, left_distrib,
-        mul_comm, mul_left_comm, mul_assoc]
-
-theorem Poly.denote_combineC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (p₁ p₂ : Poly)
-    : (combineC p₁ p₂ c).denote ctx = p₁.denote ctx + p₂.denote ctx := by
-  unfold combineC; generalize hugeFuel = fuel
-  fun_induction combineC.go
-    <;> simp [combineC.go, *, denote_concat, denote_addConstC, denote, intCast_add,
-          cond_eq_if, add_comm, add_left_comm, add_assoc, IsCharP.intCast_emod]
-  next hg _ h _ =>
-    simp +zetaDelta at h; simp [*]
-    rw [← add_assoc, Mon.eq_of_grevlex hg, ← right_distrib, ← intCast_add,
-      ← IsCharP.intCast_emod (p := c),
-      h, intCast_zero, zero_mul, zero_add]
-  next hg _ h _ =>
-    simp +zetaDelta at h; simp [*, denote, intCast_add, IsCharP.intCast_emod]
-    rw [right_distrib, Mon.eq_of_grevlex hg, add_assoc]
-
-theorem Poly.denote_mulC_go {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (p₁ p₂ acc : Poly)
-    : (mulC.go p₂ c p₁ acc).denote ctx = acc.denote ctx + p₁.denote ctx * p₂.denote ctx := by
-  fun_induction mulC.go
-    <;> simp [mulC.go, denote_combineC, denote_mulConstC, denote, *, right_distrib, denote_mulMonC, add_assoc]
-
-theorem Poly.denote_mulC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (p₁ p₂ : Poly)
-    : (mulC p₁ p₂ c).denote ctx = p₁.denote ctx * p₂.denote ctx := by
-  simp [mulC, denote_mulC_go, denote, intCast_zero, zero_add]
-
-theorem Poly.denote_powC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (p : Poly) (k : Nat)
-   : (powC p k c).denote ctx = p.denote ctx ^ k := by
- fun_induction powC <;> simp [powC, denote, intCast_one, pow_zero]
- next => simp [pow_succ, pow_zero, one_mul]
- next => simp [denote_mulC, *, pow_succ, mul_comm]
-
-theorem Expr.denote_toPolyC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (e : Expr)
-   : (e.toPolyC c).denote ctx = e.denote ctx := by
-  unfold toPolyC
-  fun_induction toPolyC.go
-    <;> simp [toPolyC.go, denote, Poly.denote, Poly.denote_ofVar, Poly.denote_combineC,
-          Poly.denote_mulC, Poly.denote_mulConstC, Poly.denote_powC, *]
-  next => rw [IsCharP.intCast_emod]
-  next => rw [intCast_neg, neg_mul, intCast_one, one_mul]
-  next => rw [intCast_neg, neg_mul, intCast_one, one_mul, sub_eq_add_neg]
-  next => rw [IsCharP.intCast_emod, intCast_pow]
-  next => simp [Poly.denote_ofMon, Mon.denote, Power.denote_eq]
-
 end CommRing
 end Lean.Grind

src/Lean/Data/RArray.lean

@@ -59,17 +59,22 @@ where
     case case1 => simp [ofFn.go, size]
     case case2 ih1 ih2 hiu => rw [ofFn.go]; simp +zetaDelta [size, *]; omega
 
-open Meta in
+open Meta
 def RArray.toExpr (ty : Expr) (f : α → Expr) (a : RArray α) : MetaM Expr := do
-  let u ← getDecLevel ty
-  let leaf := mkConst ``RArray.leaf [u]
-  let branch := mkConst ``RArray.branch [u]
-  let rec go (a : RArray α) : MetaM Expr := do
-    match a with
-    | .leaf x  =>
-      return mkApp2 leaf ty (f x)
-    | .branch p l r =>
-      return mkApp4 branch ty (mkRawNatLit p) (← go l) (← go r)
-  go a
+  let k (leaf branch : Expr) : MetaM Expr :=
+    let rec go (a : RArray α) : MetaM Expr := do
+      match a with
+      | .leaf x  =>
+        return mkApp2 leaf ty (f x)
+      | .branch p l r =>
+        return mkApp4 branch ty (mkRawNatLit p) (← go l) (← go r)
+    go a
+  let info ← getConstInfo ``RArray
+  -- TODO: remove after bootstrapping hell
+  if info.levelParams.isEmpty then
+    k (mkConst ``RArray.leaf) (mkConst ``RArray.branch)
+  else
+    let u ← getDecLevel ty
+    k (mkConst ``RArray.leaf [u]) (mkConst ``RArray.branch [u])
 
 end Lean

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -674,19 +674,16 @@ open Lean Elab Tactic Parser.Tactic
 def omegaTactic (cfg : OmegaConfig) : TacticM Unit := do
   let declName? ← Term.getDeclName?
   liftMetaFinishingTactic fun g => do
-    if debug.terminalTacticsAsSorry.get (← getOptions) then
-      g.admit
-    else
-      let some g ← g.falseOrByContra | return ()
-      g.withContext do
-        let type ← g.getType
-        let g' ← mkFreshExprSyntheticOpaqueMVar type
-        let hyps := (← getLocalHyps).toList
-        trace[omega] "analyzing {hyps.length} hypotheses:\n{← hyps.mapM inferType}"
-        omega hyps g'.mvarId! cfg
-        -- Omega proofs are typically rather large, so hide them in a separate definition
-        let e ← mkAuxTheorem (prefix? := declName?) type (← instantiateMVarsProfiling g') (zetaDelta := true)
-        g.assign e
+    let some g ← g.falseOrByContra | return ()
+    g.withContext do
+      let type ← g.getType
+      let g' ← mkFreshExprSyntheticOpaqueMVar type
+      let hyps := (← getLocalHyps).toList
+      trace[omega] "analyzing {hyps.length} hypotheses:\n{← hyps.mapM inferType}"
+      omega hyps g'.mvarId! cfg
+      -- Omega proofs are typically rather large, so hide them in a separate definition
+      let e ← mkAuxTheorem (prefix? := declName?) type (← instantiateMVarsProfiling g') (zetaDelta := true)
+      g.assign e
 
 
 /-- The `omega` tactic, for resolving integer and natural linear arithmetic problems. This

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean

@@ -100,7 +100,7 @@ where
     | (type, ctx) :: ctxs =>
       let typeExpr := type.denoteType
       let ctxExpr ← toContextExprCore ctx typeExpr
-      withLetDecl ((`ctx).appendIndexAfter i) (mkApp (mkConst ``RArray [levelZero]) typeExpr) ctxExpr fun ctx => do
+      withLetDecl ((`ctx).appendIndexAfter i) (mkApp (mkConst ``RArray) typeExpr) ctxExpr fun ctx => do
         go (i+1) ctxs (r.insert type ctx)
 
 private def getLetCtxVars : ProofM (Array Expr) := do
@@ -110,7 +110,7 @@ private def getLetCtxVars : ProofM (Array Expr) := do
   return r
 
 private abbrev withProofContext (x : ProofM Expr) : GoalM Expr := do
-  withLetDecl `ctx (mkApp (mkConst ``RArray [levelZero]) (mkConst ``Int)) (← toContextExpr) fun ctx =>
+  withLetDecl `ctx (mkApp (mkConst ``RArray) (mkConst ``Int)) (← toContextExpr) fun ctx =>
   withForeignContexts fun foreignCtxs =>
     go { ctx, foreignCtxs } |>.run' {}
 where

src/Lean/Meta/Tactic/Grind/Main.lean

@@ -161,26 +161,20 @@ def Result.toMessageData (result : Result) : MetaM MessageData := do
   return MessageData.joinSep msgs m!"\n"
 
 def main (mvarId : MVarId) (params : Params) (mainDeclName : Name) (fallback : Fallback) : MetaM Result := do profileitM Exception "grind" (← getOptions) do
-  if debug.terminalTacticsAsSorry.get (← getOptions) then
-    mvarId.admit
-    return {
-        failures := [], skipped := [], issues := [], config := params.config, trace := {}, counters := {}, simp := {}
-    }
-  else
-    let go : GrindM Result := withReducible do
-      let goals ← initCore mvarId params
-      let (failures, skipped) ← solve goals fallback
-      trace[grind.debug.final] "{← ppGoals goals}"
-      let issues   := (← get).issues
-      let trace    := (← get).trace
-      let counters := (← get).counters
-      let simp     := (← get).simpStats
-      if failures.isEmpty then
-        -- If there are no failures and diagnostics are enabled, we still report the performance counters.
-        if (← isDiagnosticsEnabled) then
-          if let some msg ← mkGlobalDiag counters simp then
-            logInfo msg
-      return { failures, skipped, issues, config := params.config, trace, counters, simp }
-    go.run mainDeclName params fallback
+  let go : GrindM Result := withReducible do
+    let goals ← initCore mvarId params
+    let (failures, skipped) ← solve goals fallback
+    trace[grind.debug.final] "{← ppGoals goals}"
+    let issues   := (← get).issues
+    let trace    := (← get).trace
+    let counters := (← get).counters
+    let simp     := (← get).simpStats
+    if failures.isEmpty then
+      -- If there are no failures and diagnostics are enabled, we still report the performance counters.
+      if (← isDiagnosticsEnabled) then
+        if let some msg ← mkGlobalDiag counters simp then
+          logInfo msg
+    return { failures, skipped, issues, config := params.config, trace, counters, simp }
+  go.run mainDeclName params fallback
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Util.lean

@@ -11,12 +11,6 @@ import Lean.Meta.PPGoal
 
 namespace Lean.Meta
 
-register_builtin_option debug.terminalTacticsAsSorry : Bool := {
-  defValue := false
-  group    := "debug"
-  descr    := "when enabled, terminal tactics such as `grind` and `omega` are replaced with `sorry`. Useful for debugging and fixing bootstrapping issues"
-}
-
 /-- Get the user name of the given metavariable. -/
 def _root_.Lean.MVarId.getTag (mvarId : MVarId) : MetaM Name :=
   return (← mvarId.getDecl).userName

src/stdlib_flags.h

@@ -7,8 +7,6 @@ options get_default_options() {
 #if LEAN_IS_STAGE0 == 1
     // set to true to generally avoid bootstrapping issues limited to proofs
     opts = opts.update({"debug", "proofAsSorry"}, false);
-    // set to true to generally avoid bootstrapping issues in `omega` and `grind`
-    opts = opts.update({"debug", "terminalTacticsAsSorry"}, false);
     // switch to `true` for ABI-breaking changes affecting meta code;
     // see also next option!
     opts = opts.update({"interpreter", "prefer_native"}, false);

stage0/src/stdlib_flags.h

@@ -7,8 +7,6 @@ options get_default_options() {
 #if LEAN_IS_STAGE0 == 1
     // set to true to generally avoid bootstrapping issues limited to proofs
     opts = opts.update({"debug", "proofAsSorry"}, false);
-    // set to true to generally avoid bootstrapping issues in `omega` and `grind`
-    opts = opts.update({"debug", "terminalTacticsAsSorry"}, false);
     // switch to `true` for ABI-breaking changes affecting meta code;
     // see also next option!
     opts = opts.update({"interpreter", "prefer_native"}, false);