feat: omega to abstract its own proofs (#5998)

This PR lets `omega` always abstract its own proofs into an auxiliary
definition. The size of the olean of Vector.Extract goes down from 20MB
to 5MB with this, overall stdlib olean size and build instruction count
go down 5%.

Needs #7362.

src/Lean/Data/Name.lean

@@ -132,6 +132,7 @@ def isInternalDetail : Name → Bool
       || matchPrefix s "eq_"
       || matchPrefix s "match_"
       || matchPrefix s "proof_"
+      || matchPrefix s "omega_"
       || p.isInternalOrNum
   | .num _ _     => true
   | p            => p.isInternalOrNum

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

@@ -7,6 +7,8 @@ prelude
 import Lean.Elab.Tactic.Omega.Core
 import Lean.Elab.Tactic.FalseOrByContra
 import Lean.Elab.Tactic.Config
+import Lean.Elab.MutualDef
+import Lean.Meta.Closure
 
 /-!
 # Frontend to the `omega` tactic.
@@ -670,12 +672,19 @@ open Lean Elab Tactic Parser.Tactic
 
 /-- The `omega` tactic, for resolving integer and natural linear arithmetic problems. -/
 def omegaTactic (cfg : OmegaConfig) : TacticM Unit := do
+  let auxName ← Term.mkAuxName `omega
   liftMetaFinishingTactic fun g => do
     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 cfg
+      omega hyps g'.mvarId! cfg
+      -- Omega proofs are typically rather large, so hide them in a separate definition
+      let e ← mkAuxTheorem auxName type (← instantiateMVarsProfiling g') (zetaDelta := true)
+      g.assign e
+
 
 /-- The `omega` tactic, for resolving integer and natural linear arithmetic problems. This
 `TacticM Unit` frontend with default configuration can be used as an Aesop rule, for example via

src/Lean/Elab/Term.lean

@@ -1892,7 +1892,7 @@ def addAutoBoundImplicits' (xs : Array Expr) (type : Expr) (k : Array Expr → E
 
 def mkAuxName (suffix : Name) : TermElabM Name := do
   match (← read).declName? with
-  | none          => throwError "auxiliary declaration cannot be created when declaration name is not available"
+  | none          => Lean.mkAuxName (mkPrivateName (← getEnv) `aux) 1
   | some declName => Lean.mkAuxName (declName ++ suffix) 1
 
 builtin_initialize registerTraceClass `Elab.letrec

tests/lean/run/auxinvariable.lean

@@ -0,0 +1,18 @@
+/-!
+It used to be that aux theorems could only be created within declarations. But with `omega` wanting
+to create an aux theorem, and `omega` being used in, say, `variable` commands, this is not tenable.
+-/
+
+structure Foo (n : Nat) (h : n > 1 := by omega) : Type
+
+set_option pp.proofs true
+
+/-- info: Foo 3 (Decidable.byContradiction fun a => _check.omega_1 a) : Type -/
+#guard_msgs in
+#check Foo 3
+
+variable (x : Foo 2)
+
+/-- info: x : Foo 2 (Decidable.byContradiction fun a => aux_2 a) -/
+#guard_msgs in
+#check x