kernel is_def_eq confusion

Stream: Type theory

[Leonard Wigman]

1) i was looking through lean's kernel code and was surprised to find that, apparently, is_def_eq (which is mostly just a wrapper for is_def_eq_core) doesn't seem to unfold definitions.
near the bottom of the function, a comment claims "At this point, t_n and s_n are in weak head normal form (modulo metavariables and proof irrelevance)", even though there are only calls to whnf_core, which doesn't unfold definitions.
(i don't quite understand that comment about proof irrelevance either, as is_def_eq_proof_irrel(t_n, s_n) was checked above.)
does the front-end unfold definitions before passing terms to the kernel, or am i missing something? (that would be odd, given that not all definitions need to be unfolded.)
it seems, without unfolding, is_def_eq("a.succ", "a + 1") would return false.

2) the code, that handles def-eq of constants, only returns true, if the terms are the same constant and the levels are def-eq. why can't this return false, if the terms are the same constants, but the levels are not def-eq (ie if same_constants(a, b) { return levels_eq(a.levels, b.levels) })?

(3: is this actually the right channel for this question? :D)

for context: i stumbled upon this, cause i was trying to figure out what @[reducible] meant. i remembered something like "that's used by the elaborator, the kernel can unfold all definitions".

[Mario Carneiro]

@Leonard Wigman
(1) although I'm not entirely sure by looking at the code, I am certain that is_def_eq_core does in fact unfold definitions, and actually unfold_definition it is reachable in several places from that function. I would have to test it with a basic example like a.succ =?= a + 1 to be sure.
(2) No that would not be correct, because you could have def Foo.{u} : Type := Unit and then Foo.{1} and Foo.{2} are defeq.
(3) I don't think it is, #lean4 or #lean4 dev seems like a better place to get authoritative answers about this from devs.

[Leonard Wigman]

@Mario Carneiro, thanks!
1) oh, i completely missed r = lazy_delta_reduction(t_n, s_n);, that would explain it :^)

2) i'm not sure i understand. for Foo.{1} and Foo.{2}, the const Foo would be the same. then returning is_def_eq(const_levels(t_n), const_levels(s_n)) would return false, because level 1 is not equivalent to 2 :thinking:
to be clear, i'm proposing:

// old
if (is_constant(t_n) && is_constant(s_n) && const_name(t_n) == const_name(s_n) &&
        is_def_eq(const_levels(t_n), const_levels(s_n)))
        return true;

// new
if (is_constant(t_n) && is_constant(s_n) && const_name(t_n) == const_name(s_n))
        return is_def_eq(const_levels(t_n), const_levels(s_n));

3) okay, i'll use #lean4 next time :ok:

[Mario Carneiro]

2) i'm not sure i understand. for Foo.{1} and Foo.{2}, the const Foo would be the same. then returning is_def_eq(const_levels(t_n), const_levels(s_n)) would return false, because level 1 is not equivalent to 2

Right, I'm saying that false is the wrong answer, because Foo.{1} and Foo.{2} are defeq

[Mario Carneiro]

we need to proceed to the rest of the function to do the unfolding work, because the answer could be true, and is in this case

[Leonard Wigman]

because Foo.{1} and Foo.{2} are defeq

oh interesting!
i just assumed definitions were injective, which they of course aren't.
which means, i also have a bug in my c1 args1 =?= c2 args2 code, whoops :D

i should probably go over the typing rules again. i think i assumed, if i fail to show the premises of a rule, the terms are not def-eq. but it's more like the rules "induce" the def-eq terms, so all rules have to fail.