refl won't prove J <= J for ideals

Stream: maths

[Kevin Buzzard]

import ring_theory.noetherian -- or anything to get ideals

example (n : ℕ) : n ≤ n :=
begin
  refl, -- works fine; in my mind this is because "≤ is tagged with @[refl] somewhere"
end

example (R : Type) [comm_ring R] (J : ideal R) : J ≤ J :=
begin
  refl, -- fails?
end

Is something missing here? This should work, right?

[Kevin Buzzard]

exact le_refl J, works fine

[Yaël Dillies]

This is a somewhat common issue. I'm not sure why exactly anymore but it's something obscure like computability...

[Kevin Buzzard]

example (R : Type) [comm_ring R] (J : ideal R) : J ≤ J :=
begin
  classical,
  refl, -- still fails ;-)
end

[Yaël Dillies]

There are definitely previous threads about it.

[Kevin Buzzard]

It wouldn't surprise me if I started at least one of them ;-)

[Yaël Dillies]

No but like computability of the instance, not decidability assumptions

[Kevin Buzzard]

I can't find another thread this year :-(

example (R : Type) [comm_ring R] (J : ideal R) : J ≤ J :=
begin
  letI : preorder (ideal R) := infer_instance, -- works fine
  refl,
  /-
  invalid apply tactic, failed to unify
    J ≤ J
  with
    ∀ [_inst_1 : preorder ?m_1] (a : ?m_1), a ≤ a
  -/
end

[Kevin Buzzard]

Is it the apply bug?

[Kevin Buzzard]

example (R : Type) [comm_ring R] (J : ideal R) : J ≤ J :=
begin
--  apply le_refl, -- fails
  refine le_refl _, -- works
end

OK so it's probably the apply bug (for me the apply bug is by definition anything when apply doesn't work, because I never understood it properly)

[Kyle Miller]

I haven't had a chance to check it within Lean to confirm whether it's the apply bug, but for reference here's where apply (well, docs#tactic.apply_core) occurs when you use refl: https://github.com/leanprover-community/lean/blob/283f6ed8083ab4dd7c36300f31816c5cb793f2f7/library/init/meta/relation_tactics.lean#L17

[Kevin Buzzard]

Now I know what I'm looking for I can indeed confirm I've asked this before: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/refl.20for.20.3C.3D.20on.20ennreal/near/281662943

[Damiano Testa]

In a similar situation, Floris taught me that this kind of error can be caused by a missing instantiate_mvars. However, if it is the apply-bug, likely this is not the issue!

[Kevin Buzzard]

and indeed refl' works fine here too.

[Kyle Miller]

Something to understand about @[refl] is that for a give head there can be at most one associated lemma -- this means that in Kevin's original two examples they must both be (trying to be) using le_refl, and in particular apply le_refl is a pretty good approximation for what both are doing. (The only difference might be that it passes the new_goals.non_dep_only option?)

[Kyle Miller]

This is a limitation I forgot about recently, and one hopes that there are no @[refl], @[trans], or @[symm] lemmas in mathlib that accidentally override the expected general one for a given notation!

[Kyle Miller]

Examples to illustrate the potential problem:

example (n : nat) : n ≤ n := by refl -- ok

example (n : int) : n ≤ n := by refl -- ok

@[refl] lemma new_refl (n : nat) : n ≤ n := le_refl n

example (n : int) : n ≤ n := by refl -- error! the le refl lemma is specialized to nat

[Damiano Testa]

Kyle, does refl' work in your example? (I'm not at a computer now.)

[Kyle Miller]

No, that doesn't solve the problem that there's a refl database inside Lean that is indexed by the head of the expression. The effect of the @[refl] line is to forget the old @[refl] lemma.

[Damiano Testa]

Ooh, that is very sad!

[Kyle Miller]

The refl' tactic is exactly the same as refl but it uses something more like apply'. Here's the relevant line for refl' that looks up the refl lemma (the refl tactic has the same line): https://github.com/leanprover-community/mathlib/blob/7f5bf383ec988aa0ea700583c6449332003722a7/src/tactic/apply.lean#L102

[Kyle Miller]

(and if you trace through the code, for reflexivity the op_for function is docs#environment.refl_for, which is what consults this refl database)

[Damiano Testa]

So, would it be possible to have a list of the "current" rfl-lemmas and check that each is proved by refl in all subsequent PRs?

[Damiano Testa]

Kind of a "no rfl-lemma was harmed in the making of this PR" linter.

[Kyle Miller]

I'm not sure what the right way to handle it is. One is your idea to make sure that any overriding is done in a strictly-more-general way, which is fairly robust. Another is to modify the @[refl]/@[symm]/@[trans] attributes to disallow overriding unless you do something like @[refl override] if you mean it (and disallow this in mathlib). Another is to have some output of all the mathlib refl/symm/trans lemmas in mathlib and make sure each head has at most one associated lemma.

[Kyle Miller]

Maybe this is not a good assumption, but I think mathlib probably doesn't need the ability to override lemmas associated to these tags.

[Kyle Miller]

Oh, right, and fourth option, just sit tight and be aware of this possible problem and wait until Lean 4, where I think they use a typeclass for the databases. (Correct me if I'm wrong here.)

[Damiano Testa]

Since the database is there already, the check might simply be to see if solve_aux <type_of_rfl_lemma> `[{ refl }] succeeds.

[Damiano Testa]

Anyway, it may not be worth it, with Lean4 so close...

[Mario Carneiro]

This is the apply bug. It was recently fixed in lean 4

[Mario Carneiro]

in lean 3 you should just use refl'