From 754bab442ae5d64a62a5ff062d9e9a15903f5397 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 10 Mar 2025 13:39:30 +0100
Subject: [PATCH] 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                  |  1 +
 src/Lean/Elab/Tactic/Omega/Frontend.lean | 11 ++++++++++-
 src/Lean/Elab/Term.lean                  |  2 +-
 tests/lean/run/auxinvariable.lean        | 18 ++++++++++++++++++
 4 files changed, 30 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/auxinvariable.lean

diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean
index 8e7bed47e4..f748cbf685 100644
--- a/src/Lean/Data/Name.lean
+++ b/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
diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean
index ce08b338ab..1eb742eec1 100644
--- a/src/Lean/Elab/Tactic/Omega/Frontend.lean
+++ b/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
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 41668d3994..d45e4ff610 100644
--- a/src/Lean/Elab/Term.lean
+++ b/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
diff --git a/tests/lean/run/auxinvariable.lean b/tests/lean/run/auxinvariable.lean
new file mode 100644
index 0000000000..2c01b168ee
--- /dev/null
+++ b/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