feat: adapt non-equality theorems in mkTheoremFromDecl (#13041)

This PR extends `mkTheoremFromDecl` and `mkTheoremFromExpr` to handle
theorems whose conclusion is not an equality, enabling `Sym.simp` to use
a broader class of lemmas as rewrite rules.

Adaptations:
- `¬ p` → `p = False` via `eq_false`
- `p ↔ q` → `p = q` via `propext`
- `p` (proposition) → `p = True` via `eq_true`

Conjunctions (`p ∧ q`) are not handled here since the `SymM` E-graph
aggressively splits them via case analysis.

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

src/Lean/Meta/Sym/Simp/Theorems.lean

@@ -8,6 +8,7 @@ prelude
 public import Lean.Meta.Sym.Pattern
 public import Lean.Meta.DiscrTree
 import Lean.Meta.Sym.Simp.DiscrTree
+import Lean.Meta.AppBuilder
 import Lean.ExtraModUses
 public section
 namespace Lean.Meta.Sym.Simp
@@ -44,9 +45,67 @@ def Theorems.getMatch (thms : Theorems) (e : Expr) : Array Theorem :=
 def Theorems.getMatchWithExtra (thms : Theorems) (e : Expr) : Array (Theorem × Nat) :=
   Sym.getMatchWithExtra thms.thms e
 
+/-- Describes how a theorem's conclusion was adapted to an equality for use in `Sym.simp`. -/
+private inductive EqAdaptation where
+  /-- Already an equality `lhs = rhs`. Proof is used as-is. -/
+  | eq
+  /-- Was `¬ p`. Proof `h` adapted to `eq_false h : p = False`. -/
+  | eqFalse
+  /-- Was `p ↔ q`. Proof `h` adapted to `propext h : p = q`. -/
+  | iff
+  /-- Was a proposition `p`. Proof `h` adapted to `eq_true h : p = True`. -/
+  | eqTrue
+
+/--
+Analyze the conclusion of a theorem type and extract `(lhs, rhs)` for use as a
+rewrite rule in `Sym.simp`. Handles:
+- `lhs = rhs` — used as-is
+- `¬ p` — adapted to `p = False`
+- `p ↔ q` — adapted to `p = q`
+- `p` (proposition) — adapted to `p = True`
+-/
+private def selectEqKey (type : Expr) : MetaM (Expr × Expr × EqAdaptation) := do
+  match_expr type with
+  | Eq _ lhs rhs => return (lhs, rhs, .eq)
+  | Not p => return (p, mkConst ``False, .eqFalse)
+  | Iff lhs rhs => return (lhs, rhs, .iff)
+  | _ =>
+    unless (← isProp type) do
+      throwError "cannot use as a simp theorem, conclusion is not a proposition{indentExpr type}"
+    return (type, mkConst ``True, .eqTrue)
+
+/--
+Wrap a proof expression according to the adaptation applied to its type.
+Given a proof `h : <original type>`, returns a proof of the adapted equality.
+This wrapping must be applied AFTER the proof has been applied to its quantified arguments.
+-/
+private def wrapProof (numVars : Nat) (expr : Expr) (adaptation : EqAdaptation) : MetaM Expr :=
+  match adaptation with
+  | .eq => return expr
+  | .eqFalse =>
+    wrapInner numVars expr fun h => mkAppM ``eq_false #[h]
+  | .iff =>
+    wrapInner numVars expr fun h => mkAppM ``propext #[h]
+  | .eqTrue =>
+    wrapInner numVars expr fun h => mkAppM ``eq_true #[h]
+where
+  /-- Wraps the innermost application of `expr` (after `numVars` arguments) with `wrap`. -/
+  wrapInner (numVars : Nat) (expr : Expr) (wrap : Expr → MetaM Expr) : MetaM Expr := do
+    let type ← inferType expr
+    forallBoundedTelescope type numVars fun xs _ => do
+      let h := mkAppN expr xs
+      mkLambdaFVars xs (← wrap h)
+
 def mkTheoremFromDecl (declName : Name) : MetaM Theorem := do
-  let (pattern, rhs) ← mkEqPatternFromDecl declName
-  return { expr := mkConst declName, pattern, rhs }
+  let (pattern, (rhs, adaptation)) ← mkPatternFromDeclWithKey declName selectEqKey
+  let expr ← wrapProof pattern.varTypes.size (mkConst declName) adaptation
+  return { expr, pattern, rhs }
+
+/-- Create a `Theorem` from a proof expression. Handles equalities, `¬`, `↔`, and propositions. -/
+def mkTheoremFromExpr (e : Expr) : MetaM Theorem := do
+  let (pattern, (rhs, adaptation)) ← mkPatternFromExprWithKey e [] selectEqKey
+  let expr ← wrapProof pattern.varTypes.size e adaptation
+  return { expr, pattern, rhs }
 
 /--
 Environment extension storing a set of `Sym.Simp` theorems.

tests/elab/sym_simp_adapt1.lean

@@ -0,0 +1,72 @@
+import Lean
+set_option linter.unusedVariables false
+set_option warn.sorry false
+/-! Tests for `mkTheoremFromDecl` adaptation of non-equality theorems -/
+
+opaque p : Nat → Prop
+opaque q : Nat → Prop
+
+-- Equality theorem (no adaptation needed)
+theorem eq_thm : p x = q x := sorry
+
+-- Negation theorem: `¬ p x` adapted to `p x = False`
+theorem neg_thm : ¬ p x := sorry
+
+-- Iff theorem: `p x ↔ q x` adapted to `p x = q x`
+theorem iff_thm : p x ↔ q x := sorry
+
+-- Proposition theorem: `p x` adapted to `p x = True`
+theorem prop_thm : p x := sorry
+
+-- Quantified negation: `∀ x, ¬ p x` adapted to `∀ x, p x = False`
+theorem quant_neg : ∀ x, ¬ p x := sorry
+
+-- Quantified prop: `∀ x, p x` adapted to `∀ x, p x = True`
+theorem quant_prop : ∀ x, p x := sorry
+
+-- Test: `simp` with a proposition theorem (`h : p x`) rewrites `p x` to `True`
+register_sym_simp propSimp where
+  post := ground >> rewrite [prop_thm]
+
+example : p x = True := by
+  sym => simp propSimp
+
+-- Test: `simp` with a negation theorem (`h : ¬ p x`) rewrites `p x` to `False`
+register_sym_simp negSimp where
+  post := ground >> rewrite [neg_thm]
+
+example : p x = False := by
+  sym => simp negSimp
+
+-- Test: `simp` with an iff theorem (`h : p x ↔ q x`) rewrites `p x` to `q x`
+register_sym_simp iffSimp where
+  post := ground >> rewrite [iff_thm]
+
+example : p x = q x := by
+  sym => simp iffSimp
+
+-- Test: quantified prop still works
+register_sym_simp quantPropSimp where
+  post := ground >> rewrite [quant_prop]
+
+example (y : Nat) : p y = True := by
+  sym => simp quantPropSimp
+
+-- Test: quantified negation still works
+register_sym_simp quantNegSimp where
+  post := ground >> rewrite [quant_neg]
+
+example (y : Nat) : p y = False := by
+  sym => simp quantNegSimp
+
+register_sym_simp simple where
+  post := ground
+
+example (x : Nat) : p x := by
+  sym => simp simple [quant_prop]
+
+example (x : Nat) : ¬ p x := by
+  sym => simp simple [quant_neg]
+
+example (x : Nat) : p x = q x := by
+  sym => simp simple [iff_thm]