How do I invoke `native_decide` programmatically?

Stream: metaprogramming / tactics

[Geoffrey Irving]

I'm not sure how to call native_decide from tactic code. The following does not work:

import Lean.Elab.Tactic.Meta

open Lean
open Lean.Elab.Tactic

elab "call_native_decide" : tactic => do
  let (gs, _) ←  Lean.Elab.runTactic (← getMainGoal) (← `(tactic| native_decide))
  setGoals gs

example : 2 = 2 := by native_decide  -- Fine
example : 2 = 2 := by call_native_decide  -- auxiliary declaration cannot be created when declaration name is not available

[Damiano Testa]

There have been recent posts showing that native_decide is not that different from sorry: why do you want to use it?

[Geoffrey Irving]

Because decide and rfl hit stack overflows, and I am experimenting with what things might be like once the faster interpreter is a thing or native_decide is fixed in the future.

[Geoffrey Irving]

If native_decide = sorry it seems like that is a bug and should be fixed, but I don’t see why that should block my experimentation. :)

[Damiano Testa]

No, as long as you are aware that whatever code you produce will not be safe, go right ahead! sorry is an incredibly useful tactic, after all!

[Kyle Miller]

Saying native_decide is not different from sorry is an unfair characterization. If you trust the compiler, etc., then it only succeeds if the proposition is true.

[Geoffrey Irving]

Trust concerns aside, anyone know how to invoke it from tactic code?

[Damiano Testa]

I'm on mobile now, but I thought that there was a recent discussion about a proof of false using native_decide, no?

[Geoffrey Irving]

Which is already fixed I believe.

[Geoffrey Irving]

https://github.com/leanprover/lean4/issues/4306

[Geoffrey Irving]

In general I expect the compiler folk to (1) be very motivated to fix native_decide bugs and (2) have little difficulty doing so in each case. Certainly there is a greater probability of these than bugs in the kernel, but I am aware of that risk.

[Kyle Miller]

docs#Lean.Elab.runTactic doesn't pass in all the context you need.

Here:

elab "call_native_decide" : tactic => do
  let gs ← Lean.Elab.Tactic.run (← getMainGoal) do
    evalTactic (← `(tactic| native_decide))
  guard gs.isEmpty

[Damiano Testa]

Ah, thanks for digging this up! It was the discussion I had in mind and I had missed that it was resolved!

[Geoffrey Irving]

Wonderful, thank you!

[Kyle Miller]

You don't actually need to use Tactic.run here. It's just to make sure it only works on a single goal.

[Geoffrey Irving]

In my original code I have several different mvars in scope.

[Geoffrey Irving]

Here's the final interval tactic: https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/An.20interval.20tactic.20for.20constant.20real.20inequalities/near/445456796