feat: decide +revert and improvements to native_decide

src/Init/Tactics.lean

@@ -1148,6 +1148,108 @@ macro "haveI" d:haveDecl : tactic => `(tactic| refine_lift haveI $d:haveDecl; ?_
 /-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/
 macro "letI" d:haveDecl : tactic => `(tactic| refine_lift letI $d:haveDecl; ?_)
 
+/--
+Configuration for the `decide` tactic family.
+-/
+structure DecideConfig where
+  /-- If true (default: false), then use only kernel reduction when reducing the `Decidable` instance.
+  This is more efficient, since the default mode reduces twice (once in the elaborator and again in the kernel),
+  however kernel reduction ignores transparency settings. The `decide!` tactic is a synonym for `decide +kernel`. -/
+  kernel : Bool := false
+  /-- If true (default: false), then uses the native code compiler to evaluate the `Decidable` instance,
+  admitting the result via the axiom `Lean.ofReduceBool`.  This can be significantly more efficient,
+  but it is at the cost of increasing the trusted code base, namely the Lean compiler
+  and all definitions with an `@[implemented_by]` attribute.
+  The instance is only evaluated once. The `native_decide` tactic is a synonym for `decide +native`. -/
+  native : Bool := false
+  /-- If true (default: true), then when preprocessing the goal, do zeta reduction to attempt to eliminate free variables. -/
+  zetaReduce : Bool := true
+  /-- If true (default: false), then when preprocessing reverts free variables. -/
+  revert : Bool := false
+
+/--
+`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`
+and then reducing that instance to evaluate the truth value of `p`.
+If it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.
+
+Limitations:
+- The target is not allowed to contain local variables or metavariables.
+  If there are local variables, you can try first using the `revert` tactic with these local variables
+  to move them into the target, which may allow `decide` to succeed.
+- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined
+  by well-founded recursion might not work, because evaluating them requires reducing proofs.
+  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.
+  These can appear for instances defined using tactics (such as `rw` and `simp`).
+  To avoid this, use definitions such as `decidable_of_iff` instead.
+
+## Examples
+
+Proving inequalities:
+```lean
+example : 2 + 2 ≠ 5 := by decide
+```
+
+Trying to prove a false proposition:
+```lean
+example : 1 ≠ 1 := by decide
+/-
+tactic 'decide' proved that the proposition
+  1 ≠ 1
+is false
+-/
+```
+
+Trying to prove a proposition whose `Decidable` instance fails to reduce
+```lean
+opaque unknownProp : Prop
+
+open scoped Classical in
+example : unknownProp := by decide
+/-
+tactic 'decide' failed for proposition
+  unknownProp
+since its 'Decidable' instance reduced to
+  Classical.choice ⋯
+rather than to the 'isTrue' constructor.
+-/
+```
+
+## Properties and relations
+
+For equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.
+```lean
+example : 1 + 1 = 2 := by decide
+example : 1 + 1 = 2 := by rfl
+```
+-/
+syntax (name := decide) "decide" optConfig : tactic
+
+/--
+`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.
+It has the following properties:
+- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.
+- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,
+  and once during kernel type checking), the `decide!` tactic reduces it exactly once.
+
+The `decide!` syntax is short for `decide +kernel`.
+-/
+syntax (name := decideBang) "decide!" optConfig : tactic
+
+/-- `native_decide` will attempt to prove a goal of type `p` by synthesizing an instance
+of `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this
+uses `#eval` to evaluate the decidability instance.
+
+This should be used with care because it adds the entire lean compiler to the trusted
+part, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using
+this method or anything that transitively depends on them. Nevertheless, because it is
+compiled, this can be significantly more efficient than using `decide`, and for very
+large computations this is one way to run external programs and trust the result.
+```
+example : (List.range 1000).length = 1000 := by native_decide
+```
+-/
+syntax (name := nativeDecide) "native_decide" optConfig : tactic
+
 /--
 The `omega` tactic, for resolving integer and natural linear arithmetic problems.
 

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -7,9 +7,11 @@ prelude
 import Lean.Meta.Tactic.Constructor
 import Lean.Meta.Tactic.Assert
 import Lean.Meta.Tactic.AuxLemma
+import Lean.Meta.Tactic.Cleanup
 import Lean.Meta.Tactic.Clear
 import Lean.Meta.Tactic.Rename
 import Lean.Elab.Tactic.Basic
+import Lean.Elab.Tactic.Config
 import Lean.Elab.SyntheticMVars
 
 namespace Lean.Elab.Tactic
@@ -347,6 +349,7 @@ def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId
       replaceMainGoal [← (← getMainGoal).rename fvarId h.getId]
   | _ => throwUnsupportedSyntax
 
+
 /--
 Make sure `expectedType` does not contain free and metavariables.
 It applies zeta and zetaDelta-reduction to eliminate let-free-vars.
@@ -355,8 +358,11 @@ private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
   let mut expectedType ← instantiateMVars expectedType
   if expectedType.hasFVar then
     expectedType ← zetaReduce expectedType
-  if expectedType.hasFVar || expectedType.hasMVar then
-    throwError "expected type must not contain free or meta variables{indentExpr expectedType}"
+  if expectedType.hasMVar then
+    throwError "expected type must not contain meta variables{indentExpr expectedType}"
+  if expectedType.hasFVar then
+    throwError "expected type must not contain free variables{indentExpr expectedType}\n\
+      Use the '+revert' option to automatically cleanup and revert free variables."
   return expectedType
 
 /--
@@ -381,36 +387,80 @@ private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := wi
               return ← blameDecideReductionFailure inst''
   return inst
 
-def evalDecideCore (tacticName : Name) (kernelOnly : Bool) : TacticM Unit :=
+def evalDecideCore (tacticName : Name) (cfg : Parser.Tactic.DecideConfig) : TacticM Unit := do
+  if cfg.revert then
+    -- In revert mode: clean up the local context and then revert everything that is left.
+    liftMetaTactic1 fun g => do
+      let g ← g.cleanup
+      let (_, g) ← g.revert (clearAuxDeclsInsteadOfRevert := true) (← g.getDecl).lctx.getFVarIds
+      return g
   closeMainGoalUsing tacticName fun expectedType _ => do
+    if cfg.kernel && cfg.native then
+      throwError "tactic '{tacticName}' failed, cannot simultaneously set both '+kernel' and '+native'"
     let expectedType ← preprocessPropToDecide expectedType
+    if cfg.native then
+      doNative expectedType
+    else if cfg.kernel then
+      doKernel expectedType
+    else
+      doElab expectedType
+where
+  doElab (expectedType : Expr) : TacticM Expr := do
     let pf ← mkDecideProof expectedType
     -- Get instance from `pf`
     let s := pf.appFn!.appArg!
-    if kernelOnly then
-      -- Reduce the decidable instance to (hopefully!) `isTrue` by passing `pf` to the kernel.
-      -- The `mkAuxLemma` function caches the result in two ways:
-      -- 1. First, the function makes use of a `type`-indexed cache per module.
-      -- 2. Second, once the proof is added to the environment, the kernel doesn't need to check the proof again.
-      let levelsInType := (collectLevelParams {} expectedType).params
-      -- Level variables occurring in `expectedType`, in ambient order
-      let lemmaLevels := (← Term.getLevelNames).reverse.filter levelsInType.contains
-      try
-        let lemmaName ← mkAuxLemma lemmaLevels expectedType pf
-        return mkConst lemmaName (lemmaLevels.map .param)
-      catch _ =>
-        diagnose expectedType s none
+    let r ← withAtLeastTransparency .default <| whnf s
+    if r.isAppOf ``isTrue then
+      -- Success!
+      -- While we have a proof from reduction, we do not embed it in the proof term,
+      -- and instead we let the kernel recompute it during type checking from the following more
+      -- efficient term. The kernel handles the unification `e =?= true` specially.
+      return pf
     else
-      let r ← withAtLeastTransparency .default <| whnf s
-      if r.isAppOf ``isTrue then
-        -- Success!
-        -- While we have a proof from reduction, we do not embed it in the proof term,
-        -- and instead we let the kernel recompute it during type checking from the following more
-        -- efficient term. The kernel handles the unification `e =?= true` specially.
-        return pf
-      else
-        diagnose expectedType s r
-where
+      diagnose expectedType s r
+  doKernel (expectedType : Expr) : TacticM Expr := do
+    let pf ← mkDecideProof expectedType
+    -- Get instance from `pf`
+    let s := pf.appFn!.appArg!
+    -- Reduce the decidable instance to (hopefully!) `isTrue` by passing `pf` to the kernel.
+    -- The `mkAuxLemma` function caches the result in two ways:
+    -- 1. First, the function makes use of a `type`-indexed cache per module.
+    -- 2. Second, once the proof is added to the environment, the kernel doesn't need to check the proof again.
+    let levelsInType := (collectLevelParams {} expectedType).params
+    -- Level variables occurring in `expectedType`, in ambient order
+    let lemmaLevels := (← Term.getLevelNames).reverse.filter levelsInType.contains
+    try
+      let lemmaName ← mkAuxLemma lemmaLevels expectedType pf
+      return mkConst lemmaName (lemmaLevels.map .param)
+    catch _ =>
+      diagnose expectedType s none
+  doNative (expectedType : Expr) : TacticM Expr := do
+    let d ← mkDecide expectedType
+    let levelsInType := (collectLevelParams {} expectedType).params
+    -- Level variables occurring in `expectedType`, in ambient order
+    let levels := (← Term.getLevelNames).reverse.filter levelsInType.contains
+    let auxDeclName ← Term.mkAuxName `_nativeDecide
+    let decl := Declaration.defnDecl {
+      name := auxDeclName
+      levelParams := levels
+      type := mkConst ``Bool
+      value := d
+      hints := .abbrev
+      safety := .safe
+    }
+    addAndCompile decl
+    -- get instance from `d`
+    let s := d.appArg!
+    let rflPrf ← mkEqRefl (toExpr true)
+    let pf := mkApp3 (mkConst ``of_decide_eq_true) expectedType s <| mkApp3 (mkConst ``Lean.ofReduceBool) (mkConst auxDeclName) (toExpr true) rflPrf
+    try
+      let lemmaName ← mkAuxLemma levels expectedType pf
+      return .const lemmaName (levels.map .param)
+    catch _ =>
+      throwError "\
+        tactic '{tacticName}' evaluated that the proposition\
+        {indentExpr expectedType}\n\
+        is false"
   diagnose {α : Type} (expectedType s : Expr) (r? : Option Expr) : TacticM α :=
     -- Diagnose the failure, lazily so that there is no performance impact if `decide` isn't being used interactively.
     throwError MessageData.ofLazyM (es := #[expectedType]) do
@@ -470,30 +520,20 @@ where
         did not reduce to '{.ofConstName ``isTrue}' or '{.ofConstName ``isFalse}'.\n\n\
         {stuckMsg}{hint}"
 
-@[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun _ =>
-  evalDecideCore `decide false
-
-@[builtin_tactic Lean.Parser.Tactic.decideBang] def evalDecideBang : Tactic := fun _ =>
-  evalDecideCore `decide! true
-
-private def mkNativeAuxDecl (baseName : Name) (type value : Expr) : TermElabM Name := do
-  let auxName ← Term.mkAuxName baseName
-  let decl := Declaration.defnDecl {
-    name := auxName, levelParams := [], type, value
-    hints := .abbrev
-    safety := .safe
-  }
-  addDecl decl
-  compileDecl decl
-  pure auxName
-
-@[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun _ =>
-  closeMainGoalUsing `nativeDecide fun expectedType _ => do
-    let expectedType ← preprocessPropToDecide expectedType
-    let d ← mkDecide expectedType
-    let auxDeclName ← mkNativeAuxDecl `_nativeDecide (Lean.mkConst `Bool) d
-    let rflPrf ← mkEqRefl (toExpr true)
-    let s := d.appArg! -- get instance from `d`
-    return mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s <| mkApp3 (Lean.mkConst ``Lean.ofReduceBool) (Lean.mkConst auxDeclName) (toExpr true) rflPrf
+declare_config_elab elabDecideConfig Parser.Tactic.DecideConfig
+
+@[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun stx => do
+  let cfg ← elabDecideConfig stx[1]
+  evalDecideCore `decide cfg
+
+@[builtin_tactic Lean.Parser.Tactic.decideBang] def evalDecideBang : Tactic := fun stx => do
+  let cfg ← elabDecideConfig stx[1]
+  let cfg := { cfg with kernel := true }
+  evalDecideCore `decide! cfg
+
+@[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun stx => do
+  let cfg ← elabDecideConfig stx[1]
+  let cfg := { cfg with native := true }
+  evalDecideCore `native_decide cfg
 
 end Lean.Elab.Tactic

src/Lean/Parser/Tactic.lean

@@ -67,90 +67,6 @@ doing a pattern match. This is equivalent to `fun` with match arms in term mode.
 @[builtin_tactic_parser] def introMatch := leading_parser
   nonReservedSymbol "intro" >> matchAlts
 
-/--
-`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`
-and then reducing that instance to evaluate the truth value of `p`.
-If it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.
-
-Limitations:
-- The target is not allowed to contain local variables or metavariables.
-  If there are local variables, you can try first using the `revert` tactic with these local variables
-  to move them into the target, which may allow `decide` to succeed.
-- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined
-  by well-founded recursion might not work, because evaluating them requires reducing proofs.
-  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.
-  These can appear for instances defined using tactics (such as `rw` and `simp`).
-  To avoid this, use definitions such as `decidable_of_iff` instead.
-
-## Examples
-
-Proving inequalities:
-```lean
-example : 2 + 2 ≠ 5 := by decide
-```
-
-Trying to prove a false proposition:
-```lean
-example : 1 ≠ 1 := by decide
-/-
-tactic 'decide' proved that the proposition
-  1 ≠ 1
-is false
--/
-```
-
-Trying to prove a proposition whose `Decidable` instance fails to reduce
-```lean
-opaque unknownProp : Prop
-
-open scoped Classical in
-example : unknownProp := by decide
-/-
-tactic 'decide' failed for proposition
-  unknownProp
-since its 'Decidable' instance reduced to
-  Classical.choice ⋯
-rather than to the 'isTrue' constructor.
--/
-```
-
-## Properties and relations
-
-For equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.
-```lean
-example : 1 + 1 = 2 := by decide
-example : 1 + 1 = 2 := by rfl
-```
--/
-@[builtin_tactic_parser] def decide := leading_parser
-  nonReservedSymbol "decide"
-
-/--
-`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.
-It has the following properties:
-- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.
-- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,
-  and once during kernel type checking), the `decide!` tactic reduces it exactly once.
--/
-@[builtin_tactic_parser] def decideBang := leading_parser
-  nonReservedSymbol "decide!"
-
-/-- `native_decide` will attempt to prove a goal of type `p` by synthesizing an instance
-of `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this
-uses `#eval` to evaluate the decidability instance.
-
-This should be used with care because it adds the entire lean compiler to the trusted
-part, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using
-this method or anything that transitively depends on them. Nevertheless, because it is
-compiled, this can be significantly more efficient than using `decide`, and for very
-large computations this is one way to run external programs and trust the result.
-```
-example : (List.range 1000).length = 1000 := by native_decide
-```
--/
-@[builtin_tactic_parser] def nativeDecide := leading_parser
-  nonReservedSymbol "native_decide"
-
 builtin_initialize
   register_parser_alias "matchRhsTacticSeq" matchRhs
 

tests/lean/1825.lean.expected.out

@@ -1,6 +1,3 @@
-1825.lean:2:8-2:13: error: application type mismatch
-  Lean.ofReduceBool boom'._nativeDecide_1 true (Eq.refl true)
-argument has type
-  true = true
-but function has type
-  Lean.reduceBool boom'._nativeDecide_1 = true → boom'._nativeDecide_1 = true
+1825.lean:2:71-2:84: error: tactic 'native_decide' evaluated that the proposition
+  -2147483648 + 2147483648 = -18446744069414584320
+is false