Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Possible cause: occurs check failed


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: May 09 2021 at 22:13 UTC