unify fails in the presence of binders

Stream: general

[Cyril Cohen]

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!

[Rob Lewis]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Cyril Cohen]

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

[Rob Lewis]

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.

[Rob Lewis]

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

[Rob Lewis]

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

[Wojciech Nawrocki]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Chris Hughes]

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))

[Mario Carneiro]

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

[Cyril Cohen]

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

[Rob Lewis]

@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)

[Cyril Cohen]

@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.

[Cyril Cohen]

@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

[Cyril Cohen]

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

[Floris van Doorn]

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...

[Cyril Cohen]

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

[Floris van Doorn]

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

[Rob Lewis]

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.

[Cyril Cohen]

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) []

[Sebastian Ullrich]

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.