Eq.refl fails when by rfl succeeds.

Stream: lean4

[Iurii Zamiatin]

The terms Lean4 equation compiler generates for these 2 definitions

def div2 (m : Nat) : Nat -> Nat
  | .succ (.succ n) => div2 (.succ m) n
  | _ => m

def div2' (m : Nat) : Nat -> Nat
  | .succ (.succ n) => div2' (.succ m) n
  | _ => m

are identical (both compile to eliminators). Naturally, I expected that the equality of those two could be proven with reflexivity. However,

def my_div2_is_div2' : Eq div2 div2' := Eq.refl div2

does not type-check:

type mismatch
  Eq.refl div2
has type
  div2 = div2 : Prop
but is expected to have type
  div2 = div2' : Prop

despite the fact that

def div2_is_div2' : Eq div2 div2' := by rfl

does, in fact, type-check. Actually, when printed out, we get the same exact term as earlier:

def div2_is_div2' : div2 = div2' := Eq.refl div2

What is going on here? I have tested this with the online playground, version "4.7.0-rc2".

[Kyle Miller]

One little-known feature of the rfl tactic is that if there are no free variables, it will essentially try rfl with no transparency constraints, using the way the kernel would check Eq.refl. Here, it looks like not even by with_unfolding_all exact rfl is as powerful as by rfl.

[Iurii Zamiatin]

Kyle Miller said:

One little-known feature of the rfl tactic is that if there are no free variables, it will essentially try rfl with no transparency constraints, using the way the kernel would check Eq.refl. Here, it looks like not even by with_unfolding_all exact rfl is as powerful as by rfl.

Sorry, I don’t quite understand what “no transparency constraints” means here. Could you expand on that? The issue here is that Eq.refl fails to prove equality of two identical terms, but by rfl manages to somehow (with #print suggesting it’s also done through Eq.refl).

I would expect any tactic to produce a term kernel can type check, but this doesn’t seem to hold here.

[Eric Rodriguez]

For performance, there's such a thing as "transparency" which allows some expressions not to be unfolded during defeq checks. The level of transparency you want to unfold to can be modified, depending on whether you want the evaluation of isDefEq to be fast and maybe give you a false negative, or slower with less false negatives. These reducibility settings in your particular example prevent most tactics from evaluating this equality to really truly be an equality, but this special feature of rfl, which uses the kernel's equality checker, allows this to go through.

[Iurii Zamiatin]

I see, thanks. In that case wouldn’t it make sense for the proof term generated with by rfl to indicate that higher evaluation depth is needed?

[Notification Bot]

Iurii Zamiatin has marked this topic as resolved.

[Robert Maxton]

I think @Kyle Miller's point here is that the the evaluation depth accessible by rfl (which is a very low level command/tactic apparently) is otherwise unaccessible.

[Notification Bot]

Iurii Zamiatin has marked this topic as unresolved.

[Iurii Zamiatin]

Are the rules for determining which definitions are considered to be transparent by the elaborator documented somewhere?

[Iurii Zamiatin]

Are the rules for determining which bindings are transparent documented somewhere?
EDIT: Sorry, I am not sure why the message got posted twice, I am new to Zulip.

[Notification Bot]

Iurii Zamiatin has marked this topic as resolved.

[Notification Bot]

Robert Maxton has marked this topic as unresolved.

[Robert Maxton]

When you resolve a topic, the thread title changes, which changes the link, and the same is true of unresolving it. (I believe this is the reason you need to be a mod to resolve/unresolve old topics -- people may have created links that they expected to be permanent in that time, and resolving/unresolving the topic will break their links.)

I infer from the above behavior that this is in fact implemented as a new topic; Zulip attempts to intelligently move all the messages in a given topic to the "new" topic, but if you unresolve and post twice in short succession, it can end up associating one of your messages to the "other"/"old" topic instead.

[Robert Maxton]

(I'm assuming you did intend to unresolve this topic, so I did it for you so as to avoid a repeat)

[Eric Rodriguez]

in general, in this zulip instance we avoid resolving topics for this sort of reason

[Kyle Miller]

Iurii Zamiatin said:

I see, thanks. In that case wouldn’t it make sense for the proof term generated with by rfl to indicate that higher evaluation depth is needed?

It's weird that Eq.refl is the proof generated by by rfl, right?

There are two type checkers in the Lean system: the elaborator's and the kernel's. The kernel typechecker is simpler (you might say it's "lean"), and the elaborator's typechecker is meant to help with everything that needs to be done during elaboration. The elaborator's typechecker tends to be more conservative than the kernel's, and it also has these different definition transparency levels to help control what gets unfolded and when.

Tactics do not need to create proof terms that would pass the elaborator's typechecker (so long as they pass the kernel's), and apparently rfl in this case is generating such a proof term.

It's possible that it's not a matter of transparency — that was just a guess — and it could be from some other difference between the elaborator and the kernel.

[Iurii Zamiatin]

Kyle Miller said:

Iurii Zamiatin said:

I see, thanks. In that case wouldn’t it make sense for the proof term generated with by rfl to indicate that higher evaluation depth is needed?

It's weird that Eq.refl is the proof generated by by rfl, right?

There are two type checkers in the Lean system: the elaborator's and the kernel's. The kernel typechecker is simpler (you might say it's "lean"), and the elaborator's typechecker is meant to help with everything that needs to be done during elaboration. The elaborator's typechecker tends to be more conservative than the kernel's, and it also has these different definition transparency levels to help control what gets unfolded and when.

Tactics do not need to create proof terms that would pass the elaborator's typechecker (so long as they pass the kernel's), and apparently rfl in this case is generating such a proof term.

It's possible that it's not a matter of transparency — that was just a guess — and it could be from some other difference between the elaborator and the kernel.

Thanks, I understand that now. I do wonder how elaborator chooses which terms to expand though. Originally I thought it didn’t look inside any top level definitions, but that doesn’t seem to be the case - simple definitions like

def two := 2
example : two = 2 := Eq.refl two 2

are accepted by the elaborator. What is the cutoff? Is it based on term size?

[Kevin Buzzard]

In Lean 3, definitions were semireducible by default, and maybe the same is true in Lean 4. semireducible is one of three transparency levels (the middle one).

[Kevin Buzzard]

@[irreducible] def two := 2
example : two = 2 := Eq.refl two -- fails -- but `by rfl` works

[Kyle Miller]

No, it's not based on term size, and it (usually) has to do with the reducibility of a definition: @[reducible], class projections of instances, semireducible, and @[irreducible], like what Kevin is saying.

In this case, it turns out to do with a feature called "smart unfolding". This causes recursive definitions to unfold in a nicer way that omits the internal details of recursors.

One way to avoid this is the delta tactic, which unfolds without doing smart unfolding:

def div2 (m : Nat) : Nat -> Nat
  | .succ (.succ n) => div2 (.succ m) n
  | _ => m

def div2' (m : Nat) : Nat -> Nat
  | .succ (.succ n) => div2' (.succ m) n
  | _ => m

example : Eq div2 div2' := by
  delta div2 div2'
  exact rfl

Another is to turn off smart unfolding:

set_option smartUnfolding false
example : Eq div2 div2' := rfl