Zulip Chat Archive

Stream: general

Topic: unify fails in the presence of binders


view this post on Zulip Cyril Cohen (Aug 20 2019 at 06:18):

I encountered the following problem: nat.pred and nat.pred._main unify well, but if I eta-expand them, unification fails! Does someone have an explanation?

run_cmd do
  let trace_unify (e1 e2 : expr) : tactic unit := (do
    trace $ "try to unify " ++ to_string e1 ++ " with " ++ to_string e2,
    unify e1 e2 transparency.all,
    trace $ "unify successful between " ++ to_string e1 ++ " with " ++ to_string e2),
  let c1 : expr tt := const `nat.pred [],
  let c2 : expr tt := const `nat.pred._main [],
  trace_unify c1 c2, -- success
  trace "",
  let eta_nat t := lam `n bid (const `nat []) $ mk_app t [var 0],
  trace_unify (eta_nat c1) (eta_nat c2) -- failure!

view this post on Zulip Rob Lewis (Aug 20 2019 at 08:40):

I had no idea the syntax let eta_nat t := ... is allowed, heh.

view this post on Zulip Rob Lewis (Aug 20 2019 at 08:41):

I'll look into this when I have a minute.

view this post on Zulip Rob Lewis (Aug 20 2019 at 11:40):

I'm not sure what's going on. Does the elaborator use a special method for constants defined using the equation compiler? What's the relevant difference between n_id and n_id2 here?

def n_id :   
| 0 := 0
| (k+1) := k+1

set_option pp.all true

#print n_id -- n_id._main

def n_id2 := n_id._main

example : n_id = n_id2 := rfl -- succeeds

example : n_id = λ n, n_id n := rfl -- fails

example : n_id = λ n, n_id n := by {dsimp, refl} -- succeeds
-- proof term:
-- @id.{0} (@eq.{1} (nat → nat) n_id (λ (n : nat), n_id n)) (@eq.refl.{1} (nat → nat) n_id)

example : n_id = λ n, n_id n := -- fails
@id.{0} (@eq.{1} (nat  nat) n_id (λ (n : nat), n_id n)) (@eq.refl.{1} (nat  nat) n_id)

example : n_id2 = λ n, n_id2 n := rfl -- succeeds

example : n_id = λ n, n_id2 n := rfl -- succeeds

view this post on Zulip Cyril Cohen (Aug 20 2019 at 12:08):

that's really weird, do you know who would know what's happening?

view this post on Zulip Rob Lewis (Aug 20 2019 at 13:02):

This is bizarre. The declarations n_id and n_id2 are completely identical, unless there are attributes that aren't being printed. I'm not familiar with the elaborator code base, but it looks plausible that it's handling constants from the equation compiler differently.

view this post on Zulip Rob Lewis (Aug 20 2019 at 13:03):

I can't say for sure without stepping through it.

view this post on Zulip Rob Lewis (Aug 20 2019 at 13:03):

Maybe @Mario Carneiro or @Sebastian Ullrich know? But Mario's reaction doesn't seem promising.

view this post on Zulip Wojciech Nawrocki (Aug 20 2019 at 13:05):

Does Lean have a special case for typechecking via eta in the kernel? Since eta is derivable but iirc not part of the core algorithmic defeq rules

view this post on Zulip Mario Carneiro (Aug 20 2019 at 13:05):

I would guess it is some elaborator thing. It certainly wouldn't be the first time the elaborator shows weird edge case behaviors when you mess with reducibility settings and auxiliaries

view this post on Zulip Mario Carneiro (Aug 20 2019 at 13:05):

I'm 99% sure the kernel has no problem accepting this proof

view this post on Zulip Chris Hughes (Aug 20 2019 at 13:07):

works

run_cmd tactic.add_decl $ declaration.thm `nat.pred_eq_pred_main []
  `((λ n, nat.pred n) = λ n, nat.pred._main n) (pure `(@rfl _ nat.pred))

view this post on Zulip Mario Carneiro (Aug 20 2019 at 13:07):

eta is part of the core rules. It's not a reduction but it is handled in the preprocessing stage in a way that should be complete

view this post on Zulip Cyril Cohen (Aug 20 2019 at 13:12):

I guess the weirdest part is that n_id = λ n, n_id2 n := rfl succeeds while n_id = λ n, n_id n := rfl fails

view this post on Zulip Rob Lewis (Aug 20 2019 at 13:18):

@Cyril Cohen For your original issue: if you really need to check if things are defeq instead of unifying them, you could follow Chris' example -- if you can add a declaration proving they're equal by rfl, then they're defeq, and this skips the elaborator. Otherwise, maybe you could dsimp with an empty simp set before unifying:

run_cmd do
  let trace_unify (e1 e2 : expr) : tactic unit := (do
    let s := simp_lemmas.mk,
    e1  s.dsimplify [] e1 <|> return e1, e2  s.dsimplify [] e2 <|> return e2,
    trace $ "try to unify " ++ to_string e1 ++ " with " ++ to_string e2,
    unify e1 e2 transparency.all,
    trace $ "unify successful between " ++ to_string e1 ++ " with " ++ to_string e2),
  let c1 : expr tt := const `nat.pred [],
  let c2 : expr tt := const `nat.pred._main [],
  trace_unify c1 c2, -- success
  trace "",
  let eta_nat t := lam `n bid (const `nat []) $ mk_app t [var 0],
  trace_unify (eta_nat c1) (eta_nat c2)

view this post on Zulip Cyril Cohen (Aug 20 2019 at 13:22):

@Rob Lewis I really need to unify, my example was a reduced case originating from a real unification problem. I will try to dsimp, thanks for your advice.

view this post on Zulip Cyril Cohen (Aug 20 2019 at 13:43):

@Rob Lewis your solution seems to work for eta expansion, but eta expansion was sadly a special case of my problem. Here is another example of failure which I would like to work...

run_cmd do
  let trace_unify (e1 e2 : expr) : tactic unit := (do
    let s := simp_lemmas.mk,
    e1  s.dsimplify [] e1 <|> return e1, e2  s.dsimplify [] e2 <|> return e2,
    trace $ "try to unify " ++ to_string e1 ++ " with " ++ to_string e2,
    unify e1 e2 transparency.all,
    trace $ "unify successful between " ++ to_string e1 ++ " with " ++ to_string e2),
  t1  to_expr ``(λ (a0 : nat), n_id._main a0 = nat.zero), -- removing `= nat.zero` here
  t2  to_expr ``(λ (a0 : nat), n_id a0 = nat.zero), -- and here makes it work
  trace_unify t1 t2

view this post on Zulip Cyril Cohen (Aug 20 2019 at 13:45):

(and in my real example it is not a λ but a Π)

view this post on Zulip Floris van Doorn (Aug 20 2019 at 14:29):

This lemma is actually tricky to prove just using tactics:

def n_id : ℕ → ℕ
| 0 := 0
| (k+1) := k+1

example : (∀ n, n_id n = 0) = (∀ n, n_id._main n = 0) :=
sorry

refl, simp, dsimp, unfold, dunfold all fail, even when given arguments (unless you do something like by simp [show n_id = n_id._main, from rfl]). The only reasonable way I know how to do it is delta n_id, refl. Presumably that doesn't help Cyril's case...

view this post on Zulip Cyril Cohen (Aug 20 2019 at 14:49):

well, maybe I could use this and unfold every definition d such that a d._main exists... it sounds horribly unstable, but unless someone comes up with an API that does the job, or a better hack, I might as well try that

view this post on Zulip Floris van Doorn (Aug 20 2019 at 14:54):

That sounds like it could work...
And it's not like we have no other tactics that depends on hacks...

view this post on Zulip Rob Lewis (Aug 20 2019 at 15:06):

This is kind of a mess. I think this elaborator behavior explains some other weird failures I've seen, but they've been in proofs, not in metaprograms where they're hard to work around.

view this post on Zulip Cyril Cohen (Aug 20 2019 at 15:24):

well, maybe I could use this and unfold every definition d such that a d._main exists... it sounds horribly unstable, but unless someone comes up with an API that does the job, or a better hack, I might as well try that

This works in a some cases that used to fail... not sure yet what's wrong with the others (my bugs or lean bugs...)

meta def expr.delta_to_main (e : expr) : tactic expr := do
  env  get_env,
  let ns := e.collect_const,
  flip delta e $
  ns.foldr (λ n ns,
   if env.contains (n ++ `_main)  (env.is_projection n).is_some
   then n :: ns else ns) []

view this post on Zulip Sebastian Ullrich (Aug 22 2019 at 14:34):

Lean naively delta-reducing definitions defined using equations and leaving you with half-reduced recursor applications was one of the most common complaints with Lean 2. It's intended that Lean 3's reduction engine usually only reduces such definitions along the actual equations. The interaction with eta conversion probably isn't, but neither was users directly interacting with _main definitions.


Last updated: May 12 2021 at 04:19 UTC