refactor: put new eqns options into backward namespace (#5207)

in #4154 and #5129 the rules for equational lemmas have changed, and new
options were introduced that can be used to revert to the pre-4.12
behavior. Hopefully nobody really needs these options besides for
backwards compatibility, therefore we put these options in the
`backward` option name space.

So the previous behavior can be achieved by setting
```lean
set_option backward.eqns.nonrecursive false
set_option backward.eqns.deepRecursiveSplit false
```

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -91,7 +91,7 @@ private def findMatchToSplit? (deepRecursiveSplit : Bool) (env : Environment) (e
 partial def splitMatch? (mvarId : MVarId) (declNames : Array Name) : MetaM (Option (List MVarId)) := commitWhenSome? do
   let target ← mvarId.getType'
   let rec go (badCases : ExprSet) : MetaM (Option (List MVarId)) := do
-    if let some e := findMatchToSplit? (eqns.deepRecursiveSplit.get (← getOptions)) (← getEnv)
+    if let some e := findMatchToSplit? (backward.eqns.deepRecursiveSplit.get (← getOptions)) (← getEnv)
                                        target declNames badCases then
       try
         Meta.Split.splitMatch mvarId e

src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean

@@ -94,7 +94,7 @@ def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if (← isRecursiveDefinition declName) then
     return none
   if let some (.defnInfo info) := (← getEnv).find? declName then
-    if eqns.nonrecursive.get (← getOptions) then
+    if backward.eqns.nonrecursive.get (← getOptions) then
       mkEqns declName info
     else
       let o ← mkSimpleEqThm declName

src/Lean/Meta/Eqns.lean

@@ -12,12 +12,12 @@ import Lean.Meta.Match.MatcherInfo
 
 namespace Lean.Meta
 
-register_builtin_option eqns.nonrecursive : Bool := {
+register_builtin_option backward.eqns.nonrecursive : Bool := {
     defValue := true
     descr    := "Create fine-grained equational lemmas even for non-recursive definitions."
   }
 
-register_builtin_option eqns.deepRecursiveSplit : Bool := {
+register_builtin_option backward.eqns.deepRecursiveSplit : Bool := {
     defValue := true
     descr    := "Create equational lemmas for recursive functions like for non-recursive \
                 functions. If disabled, match statements in recursive function definitions \
@@ -35,7 +35,7 @@ This is implemented by
  * eagerly realizing the equations when they are set to a non-default vaule
  * when realizing them lazily, reset the options to their default
 -/
-def eqnAffectingOptions : Array (Lean.Option Bool) := #[eqns.nonrecursive, eqns.deepRecursiveSplit]
+def eqnAffectingOptions : Array (Lean.Option Bool) := #[backward.eqns.nonrecursive, backward.eqns.deepRecursiveSplit]
 
 /--
 Environment extension for storing which declarations are recursive.

tests/lean/run/eqnOptions.lean

@@ -17,7 +17,7 @@ end Test1
 
 namespace Test2
 
-set_option eqns.nonrecursive false in
+set_option backward.eqns.nonrecursive false in
 def nonrecfun : Bool → Nat
   | false => 0
   | true => 0
@@ -42,7 +42,7 @@ def nonrecfun : Bool → Nat
   | true => 0
 
 -- should have no effect
-set_option eqns.nonrecursive false
+set_option backward.eqns.nonrecursive false
 
 /--
 info: equations:

tests/lean/run/wfEqns5.lean

@@ -32,7 +32,7 @@ info: foo.eq_def :
 #check foo.eq_4
 
 
-set_option eqns.deepRecursiveSplit false in
+set_option backward.eqns.deepRecursiveSplit false in
 def bar : Nat → Nat → Nat
   | 0, m => match m with | 0 => 0 | m => m
   | n+1, m => bar n m
@@ -101,7 +101,7 @@ info: Structural.foo.eq_def :
 #check Structural.foo.eq_4
 
 
-set_option eqns.deepRecursiveSplit false in
+set_option backward.eqns.deepRecursiveSplit false in
 def bar : Nat → Nat → Nat
   | 0, m => match m with | 0 => 0 | m => m
   | n+1, m => bar n m