delayed_abstraction meta-variables

Stream: metaprogramming / tactics

[Stanislas Polu]

Hi! As part of lean-gym the following proof fails to apply the linarith with there are no goals (but that proof is valid outside of lean-gym):

theorem mathd_numbertheory_136
  (n : ℕ)
  (h₀ : 123 * n + 17 = 39500) : n = 321 :=
begin
  linarith,
end

In an attempt to handle these situations when a tactic fail but the tactic state has no remaining goal, we tried catching that condition and inspect the proof term. It appears to contain meta-variables with delayed_abstraction macros such as (delayed_abstraction n h₀ ?_mlocal._fresh.13.1571). Here's the full proof term:

fun (n : nat) (h₀ : eq.{1} nat (has_add.add.{0} nat nat.has_add (has_mul.mul.{0} nat nat.has_mul (bit1.{0} nat nat.has_one nat.has_add (bit1.{0} nat nat.has_one nat.has_add (bit0.{0} nat nat.has_add (bit1.{0} nat nat.has_one nat.has_add (bit1.{0} nat nat.has_one nat.has_add (bit1.{0} nat nat.has_one nat.has_add (has_one.one.{0} nat nat.has_one)))))
)) n) (bit1.{0} nat nat.has_one nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (has_one.one.{0} nat nat.has_one)))))) (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit1.{0} nat nat.has_one nat.has_add (bit1.{0} nat nat.has_one nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit1.{0} nat na
t.has_one nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit1.{0} nat nat.has_one nat.has_add (bit0.{0} nat nat.has_add (bit1.{0} nat nat.has_one nat.has_add (bit1.{0} nat nat.has_one nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (has_one.one.{0} nat nat.has_one))))))))))))))))), (linarith.eq_of_not_lt_of_not_gt.{0} nat
 nat.linear_order n (bit1.{0} nat nat.has_one nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit1.{0} nat nat.has_one nat.has_add (bit0.{0} nat nat.has_add (has_one.one.{0} nat nat.has_one))))))))) (not.intro (has_lt.lt.{0} nat (preorder.to_has_lt.{0} nat (dire
cted_order.to_preorder.{0} nat (linear_order.to_directed_order.{0} nat nat.linear_order))) n (bit1.{0} nat nat.has_one nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit1.{0} nat nat.has_one nat.has_add (bit0.{0} nat nat.has_add (has_one.one.{0} nat nat.has_one
)))))))))) (fun (ᾰ : has_lt.lt.{0} nat (preorder.to_has_lt.{0} nat (directed_order.to_preorder.{0} nat (linear_order.to_directed_order.{0} nat nat.linear_order))) n (bit1.{0} nat nat.has_one nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit1.{0} nat nat.has_on
e nat.has_add (bit0.{0} nat nat.has_add (has_one.one.{0} nat nat.has_one)))))))))), (delayed_abstraction n h₀ ᾰ ?_mlocal._fresh.13.4519))) (delayed_abstraction n h₀ ?_mlocal._fresh.13.1571))

pretty-printed:

λ (n : ℕ) (h₀ : 123 * n + 17 = 39500),
  linarith.eq_of_not_lt_of_not_gt n 321 (not.intro (λ (ᾰ : n < 321), ?m_1[n, h₀, ᾰ])) ?m_2[n, h₀]

@Jesse Michael Han may have a path towards requesting their evaluation but it may involve a diff in core lean. Wanted to quickly check in case people had an idea on how to force the evaluation of these meta-variables to recover a meta-variable free proof expression and possibly handle these failures as successes.

(I'm also curious to understand what happens in "normal" Lean to prevent what we're seeing here)

Thanks!

[Jesse Michael Han]

1) the normal interactive solution involves uses recover, and indeed that works here;

2) i think there's something like environment.unfold_all_macros already in core Lean

[Stanislas Polu]

I might have missed something but recover didn't replace the meta-variables in the resulting proof term in my attempts to use it?

[Jesse Michael Han]

update: recover only recovers the dummy goal |- true in this case and doesn't seem to get at the delayed_abstraction metavariables, and
env <- tactic.get_env, environment.unfold_all_macros env pf ... fails, similar to the error encountered in this thread: https://leanprover-community.github.io/archive/stream/113488-general/topic/expanding.20and.20serializing.20expressions.html

[Jason Rute]

What fails about linarith in lean-gym? Does the tactic fail? Or does it just fail the checks that it is a valid proof? If the latter, what checks fail?

[Jason Rute]

I don't know what this means: "tactic fail but the tactic state has no remaining goal"

[Jesse Michael Han]

here's an MWE (h/t @Gabriel Ebner), the problem seems to boil down to linarith failing when called from io.run_tactic versus being just executed as a tactic :thinking:

import tactic.basic
import data.real.basic

section mwe

namespace io

section run_tactic''
open interaction_monad.result
/-- verion of io.run_tactic which does not suppress the exception msg -/
meta def run_tactic'' {α} (tac :tactic α) : io α := do {
  io.run_tactic $ do {
    result ← tactic.capture tac,
    match result with
    | (success val _) := pure val
    | (exception m_fmt _ _) := do {
      let fmt_msg := (m_fmt.get_or_else (λ _, format!"n/a")) (),
      let msg := format!"[fatal] {fmt_msg}",
      tactic.trace msg,
      tactic.fail msg
    }
    end
  }
}
end run_tactic''
end io

theorem mathd_numbertheory_136
  (n : ℕ)
  (h₀ : 123 * n + 17 = 39500) : n = 321 :=
begin
  linarith,
end

meta def load_thm_and_replay_proof (nm : name) : tactic unit := do {
  env ← tactic.get_env,
  decl ← env.get nm,
  guard $ decl.is_theorem,
  let tgt := decl.type,
  m ← tactic.mk_meta_var tgt,
  tactic.set_goals [m],
  ts₀ ← tactic.read,
  tactic.read >>= λ x, tactic.trace $ format! "STATE: {x}",
  `[intros], -- succeeds
  tactic.read >>= λ x, tactic.trace $ format! "STATE: {x}",
  `[linarith] *> tactic.trace "LINARITH PASSED",
  tactic.read >>= λ x, tactic.trace $ format! "STATE: {x}",
  ts ← tactic.read,
  tactic.write ts₀,
  [g] ← tactic.get_goals,
  tactic.write ts,
  pf ← tactic.get_assignment g >>= tactic.instantiate_mvars,
  tactic.pp pf >>= λ pf, tactic.trace format! "PROOF TERM AFTER INSTANTIATION: {pf}",
  (guard $ bnot pf.has_meta_var) *> tactic.trace "PASSED" <|> tactic.trace "shouldn't contain metavariables >:("
}

#eval io.run_tactic'' $ load_thm_and_replay_proof `mathd_numbertheory_136 -- fails
#eval load_thm_and_replay_proof `mathd_numbertheory_136 -- passes

end mwe

[Jesse Michael Han]

i think the delayed abstraction stuff is a red herring, instantiate_mvars should take care of it when upstream bugs are fixed

[Jesse Michael Han]

there was something strange going on with the simplify call inside zify_proof inside the nat_to_int preprocessor for linarith --- capturing the result of zify_proof while backtracking the state seems to fix the bug, see #7901

[Eric Wieser]

I think I ran into something similar when messing with tactic state in conv mode - I think the core c++ simplification routine doesn't always manage its state properly, and has some hidden state outside of the monadic state.