feat: decide!

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -393,21 +393,25 @@ private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := do
               return ← blameDecideReductionFailure inst''
   return inst
 
-@[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun _ =>
+def evalDecideCore (bang : Bool) : TacticM Unit :=
   closeMainGoalUsing `decide fun expectedType => do
     let expectedType ← preprocessPropToDecide expectedType
     let d ← mkDecide expectedType
     let d ← instantiateMVars d
     -- Get instance from `d`
     let s := d.appArg!
+    let rflPrf ← mkEqRefl (toExpr true)
+    let prf := mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s rflPrf
+    if bang then
+      return prf
+
     -- Reduce the instance rather than `d` itself for diagnostics purposes.
     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.
-      let rflPrf ← mkEqRefl (toExpr true)
       return mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s rflPrf
     else
       -- Diagnose the failure, lazily so that there is no performance impact if `decide` isn't being used interactively.
@@ -462,6 +466,12 @@ private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := do
           did not reduce to '{MessageData.ofConstName ``isTrue}' or '{MessageData.ofConstName ``isFalse}'.\n\n\
           {stuckMsg}{hint}"
 
+@[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun _ =>
+  evalDecideCore false
+
+@[builtin_tactic Lean.Parser.Tactic.decideBang] def evalDecideBang : Tactic := fun _ =>
+  evalDecideCore true
+
 private def mkNativeAuxDecl (baseName : Name) (type value : Expr) : TermElabM Name := do
   let auxName ← Term.mkAuxName baseName
   let decl := Declaration.defnDecl {

src/Lean/Parser/Tactic.lean

@@ -125,6 +125,15 @@ example : 1 + 1 = 2 := by rfl
 @[builtin_tactic_parser] def decide := leading_parser
   nonReservedSymbol "decide"
 
+/--
+A variant of `decide` that does not check the proposition at the time of elaboration, and just
+assumes it is true. The proposition is of course still checked by the kernel.
+
+This is useful to speed up the processing of large proofs, by halfing the processing time.
+-/
+@[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.

tests/lean/run/decideBang.lean

@@ -0,0 +1,35 @@
+theorem foo1 : True := by decide
+
+theorem foo2 : True := by decide!
+
+/--
+error: tactic 'decide' proved that the proposition
+  False
+is false
+-/
+#guard_msgs in
+theorem foo3 : False := by decide
+
+-- NB: Below we see error messages as they come from the kernel
+
+/--
+error: application type mismatch
+  of_decide_eq_true (Eq.refl true)
+argument has type
+  true = true
+but function has type
+  decide False = true → False
+-/
+#guard_msgs in
+theorem foo4 : False := by decide!
+
+/--
+error: application type mismatch
+  Lean.ofReduceBool foo5._nativeDecide_1 true (Eq.refl true)
+argument has type
+  true = true
+but function has type
+  Lean.reduceBool foo5._nativeDecide_1 = true → foo5._nativeDecide_1 = true
+-/
+#guard_msgs in
+theorem foo5 : False := by native_decide