Possible cause: occurs check failed

Stream: metaprogramming / tactics

[Pedro Minicz]

Why exact doesn't work in the following example (even though, infer_type `(nat.lt_irrefl %%n %%h) >>= trace prints false)?

import tactic

open tactic

setup_tactic_parser

meta def tactic.interactive.test (nm : parse ident) : tactic unit :=
do `(%%n > 0) ← get_local nm >>= infer_type,
   cases n,
   exfalso,
   h ← get_local nm,
   infer_type `(nat.lt_irrefl %%n %%h) >>= trace
   exact `(nat.lt_irrefl %%n %%h),
   get_local nm >>= clear

example {n : ℕ} (h : n > 0) : n ≠ 0 :=
begin
  test h,
  try { show n + 1 ≠ 0, from nat.succ_ne_zero n },
  all_goals { sorry }
end

[Pedro Minicz]

I also tried to instantiate_mvars on n and h to no success. In fact, tracing expr.to_raw_fmt showed the same thing before and after instantiation.

[Pedro Minicz]

The following example is even more intriguing. Why can't the metavariable be unified?

meta def tactic.interactive.test' (nm : parse ident) : tactic unit :=
do `(%%n > 0) ← get_local nm >>= infer_type,
   cases n,
   exfalso,
   g :: _ ← get_goals,
   h ← get_local nm,
   unify g `(nat.lt_irrefl %%n %%h),
   get_local nm >>= clear

example {n : ℕ} (h : n > 0) : n ≠ 0 :=
begin
  test h,
  -- unify tactic failed, failed to unify
  --   ?m_1 : false
  -- and
  --   nat.lt_irrefl n h : false
  try { show n + 1 ≠ 0, from nat.succ_ne_zero n },
  all_goals { sorry }
end

[Pedro Minicz]

Never mind, I was using an "old version" of n. The metavariable probably turned invalid after cases, thus the error. Although this is only a guess. I'd love to know a proper explanation.

meta def tactic.interactive.test (nm : parse ident) : tactic unit :=
do `(%%n > 0) ← get_local nm >>= infer_type,
   cases n,
   exfalso,
   `(%%n > 0) ← get_local nm >>= infer_type,
   h ← get_local nm,
   exact `(nat.lt_irrefl %%n %%h),
   get_local nm >>= clear

[Simon Hudon]

That's right. Think of cases as revert-ing variables and then intro-ing them again. They have the same names (most of the time) but they are not technically the same variables.

[Simon Hudon]

In the API, cases_core actually returns a list of substitutions so that you can transport your expressions from one context to the other.

[Simon Hudon]

You can see this in action if you print ls <- local_context, trace $ ls.map expr.local_uniq_name. You'll see the ugly names of the variables and that they change when you call cases