chore: rename wrongly named backwards. options to backward. (#11303)

This PR renames rename wrongly named `backwards.` options to
`backward.`

Author: nomeata

src/Lean/Meta/Constructions/NoConfusion.lean

@@ -45,7 +45,7 @@ def mkNoConfusionCtorArg (ctorName : Name) (P : Expr) : MetaM Expr := do
       t := mkForall name .default eq t
     mkLambdaFVars (xs ++ fields1 ++ fields2) t
 
-register_builtin_option backwards.linearNoConfusionType : Bool := {
+register_builtin_option backward.linearNoConfusionType : Bool := {
   defValue := true
   descr    := "use the linear-size construction for the `noConfusionType` declaration of an inductive type. Set to false to use the previous, simpler but quadratic-size construction. "
 }
@@ -54,7 +54,7 @@ def mkNoConfusionTypeName (indName : Name) : Name :=
   Name.str indName "noConfusionType"
 
 def canUseLinear (indName : Name) : MetaM Bool := do
-  unless backwards.linearNoConfusionType.get (← getOptions) do return false
+  unless backward.linearNoConfusionType.get (← getOptions) do return false
   -- Check if the prelude is loaded
   unless (← hasConst ``Eq.propIntro) do return false
   -- Check if we have the constructor elim helpers
@@ -74,7 +74,7 @@ def mkNoConfusionType (indName : Name) : MetaM Unit := do
   let ConstantInfo.inductInfo info ← getConstInfo indName | unreachable!
   let useLinearConstruction :=
     (info.numCtors > 2) &&
-    backwards.linearNoConfusionType.get (← getOptions) &&
+    backward.linearNoConfusionType.get (← getOptions) &&
     (← hasConst (mkCtorElimName indName))
   let casesOnName := mkCasesOnName indName
   let casesOnInfo ← getConstVal casesOnName

src/Lean/Meta/Match/Match.lean

@@ -18,7 +18,7 @@ public section
 
 namespace Lean.Meta.Match
 
-register_builtin_option backwards.match.sparseCases : Bool := {
+register_builtin_option backward.match.sparseCases : Bool := {
   defValue := true
   descr := "if true (the default), generate and use sparse case constructs when splitting inductive
     types. In some cases this will prevent Lean from noticing that a match statement is complete
@@ -27,7 +27,7 @@ register_builtin_option backwards.match.sparseCases : Bool := {
      ,"
 }
 
-register_builtin_option backwards.match.rowMajor : Bool := {
+register_builtin_option backward.match.rowMajor : Bool := {
   defValue := true
   descr := "If true (the default), match compilation will split the discrimnants based \
     on position of the first constructor pattern in the first alternative. If false, \
@@ -580,7 +580,7 @@ private def processConstructor (p : Problem) : MetaM (Array Problem) := do
     -- We use a sparse case analysis only if there is at least one non-constructor pattern,
     -- but not just because there are constructors missing (in that case we benefit from
     -- the eager split in ruling out constructors by type or by a more explicit error message)
-    if backwards.match.sparseCases.get (← getOptions) && hasVarOrInaccessiblePattern p then
+    if backward.match.sparseCases.get (← getOptions) && hasVarOrInaccessiblePattern p then
       let ctors := collectCtors p
       trace[Meta.Match.match] "using sparse cases: {ctors}"
       pure (some ctors)
@@ -918,7 +918,7 @@ private partial def process (p : Problem) : StateRefT State MetaM Unit := do
     process p
     return
 
-  if backwards.match.rowMajor.get (← getOptions) then
+  if backward.match.rowMajor.get (← getOptions) then
     match firstRefutablePattern p with
     | some i =>
       if i > 0 then

tests/lean/run/issue10749.lean

@@ -121,7 +121,7 @@ fun motive x x_1 x_2 x_3 x_4 h_1 h_2 h_3 h_4 h_5 h_6 =>
 -- Just testing the backwards compatibility option
 
 set_option match.ignoreUnusedAlts true in
-set_option backwards.match.rowMajor false in
+set_option backward.match.rowMajor false in
 def testOld (a : List Nat) : Nat :=
   match a with
   | _ => 3

tests/lean/run/match1.lean

@@ -143,7 +143,7 @@ match n, parity n with
 | _, Parity.even j => false :: natToBin j
 | _, Parity.odd  j => true  :: natToBin j
 
-set_option backwards.match.sparseCases false in
+set_option backward.match.sparseCases false in
 /--
 error: Tactic `cases` failed with a nested error:
 Dependent elimination failed: Failed to solve equation