Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Possible cause: occurs check failed


Pedro Minicz (Sep 09 2020 at 23:51):

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 (Sep 09 2020 at 23:52):

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 (Sep 09 2020 at 23:56):

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 (Sep 10 2020 at 00:00):

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 (Sep 10 2020 at 00:02):

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 (Sep 10 2020 at 00:04):

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 (Sep 10 2020 at 00:06):

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


Last updated: Dec 20 2023 at 11:08 UTC