Any ideas on how to debug this?

Stream: general

[Gabriel Ebner]

import all -- current mathlib master

-- simplify tactic failed to simplify
example (z : ℂ) : (complex.conj z).im = -z.im := by simp [complex.conj_im]
example (x : ℝ) : real.sin (-x) = -real.sin x := by simp [real.sin_neg]

-- works just fine
example (z : ℂ) : (complex.conj z).im = -z.im := by simp only [complex.conj_im]
example (x : ℝ) : real.sin (-x) = -real.sin x := by simp only [real.sin_neg]

[Sebastien Gouezel]

Ask squeeze_simp, it will give you the offending lemma.

[Gabriel Ebner]

Unfortunately, simp fails in the first two calls. So I don't think squeeze simp can do anything.

[Reid Barton]

Try set_option trace.simplify.rewrite true

[Sebastien Gouezel]

If you do

begin
  squeeze_simp,
  sorry,
end

you will see the simp lemmas that simp uses on your expression (the ones that prevent complex.conj_im from firing).

[Gabriel Ebner]

If it was only that easy. squeeze_simp also fails with "simplify tactic failed to simplify". (Internally, squeeze_simp looks at the proof produced by simp to determine the used lemmas; if simp doesn't simplify, then there's no proof.)

[Reid Barton]

Oh, that is weird. That error is supposed to mean that simp made no progress, right?

[Gabriel Ebner]

Reid Barton said:

Try set_option trace.simplify.rewrite true

That's my go-to option these days, but I don't see anything suspicious. In fact, complex.conj_im even seems to be used:

2. [simplify.rewrite] [complex.conj_im]: (complex.conj z).im ==> -z.im

[Reid Barton]

Another option is set_option trace.simplify true and search the log for complex.conj_im

[Gabriel Ebner]

It occurs twice in the log, once for z.conj.im and once for z.im. It even seems to rewrite the first term.

[Reid Barton]

Seems like simp is just being grumpy then

[Gabriel Ebner]

OMG, complex.im seems to disable simp entirely:

example (z : ℂ) : z.conj.im = z.conj.im + 0 := by simp -- fails

[Sebastien Gouezel]

A small dichotomy gives a failure with

import algebra.lie_algebra
       data.complex.basic

example (z : ℂ) : (complex.conj z).im = -z.im := by simp [complex.conj_im]

[Sebastien Gouezel]

The culprit for me was a memory problem. I increased the maximum memory in my Vscode, and the problem disappeared.

[Gabriel Ebner]

I get the error on the command-line as well, even with the imports reduced to algebra.lie_algebra and data.complex.basic.

[Gabriel Ebner]

Mmmh, import algebra.lie_algebra seems to be the culprit.

[Gabriel Ebner]

Oh wow, it's an instance issue, again.

[Reid Barton]

I've had a number of instances in the category theory library in which simp would refuse to apply a lemma for apparently no reason. Some cases were related to simp's handling of syntactic equality of implicit parameters but in other cases there seemed to be no explanation.

[Gabriel Ebner]

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_32 : @lie_ring ℝ real.add_comm_group := @lie_algebra.to_lie_ring ?x_33 ?x_34 ?x_35 ?x_36 ?x_37
[class_instances] (1) ?x_35 : comm_ring ?x_33 := @subalgebra.comm_ring ?x_38 ?x_39 ?x_40 ?x_41 ?x_42 ?x_43
[class_instances] (2) ?x_41 : comm_ring ?x_39 := @subalgebra.comm_ring ?x_44 ?x_45 ?x_46 ?x_47 ?x_48 ?x_49
[class_instances] (3) ?x_47 : comm_ring ?x_45 := @subalgebra.comm_ring ?x_50 ?x_51 ?x_52 ?x_53 ?x_54 ?x_55
[class_instances] (4) ?x_53 : comm_ring ?x_51 := @subalgebra.comm_ring ?x_56 ?x_57 ?x_58 ?x_59 ?x_60 ?x_61
[class_instances] (5) ?x_59 : comm_ring ?x_57 := @subalgebra.comm_ring ?x_62 ?x_63 ?x_64 ?x_65 ?x_66 ?x_67
[class_instances] (6) ?x_65 : comm_ring ?x_63 := @subalgebra.comm_ring ?x_68 ?x_69 ?x_70 ?x_71 ?x_72 ?x_73
[class_instances] (7) ?x_71 : comm_ring ?x_69 := @subalgebra.comm_ring ?x_74 ?x_75 ?x_76 ?x_77 ?x_78 ?x_79
[class_instances] (8) ?x_77 : comm_ring ?x_75 := @subalgebra.comm_ring ?x_80 ?x_81 ?x_82 ?x_83 ?x_84 ?x_85
[class_instances] (9) ?x_83 : comm_ring ?x_81 := @subalgebra.comm_ring ?x_86 ?x_87 ?x_88 ?x_89 ?x_90 ?x_91
[class_instances] (10) ?x_89 : comm_ring ?x_87 := @subalgebra.comm_ring ?x_92 ?x_93 ?x_94 ?x_95 ?x_96 ?x_97

[Reid Barton]

In some cases it also seems to get worse over time, that is, with new mathlib the simp stops working and there is no clear reason.

[Sebastien Gouezel]

It's really funny. In

example (z : ℂ) : (complex.conj z).im = -z.im := by simp [complex.conj_im]

class lie_algebra (R : Type u) (L : Type v)
  [comm_ring R] [add_comm_group L] extends module R L, lie_ring L :=
(lie_smul : ∀ (t : R) (x y : L), ⁅x, t • y⁆ = t • ⁅x, y⁆)

example (z : ℂ) : (complex.conj z).im = -z.im := by simp [complex.conj_im]

the first example works, and the second one fails. And yes, they are absolutely identical, but just adding a class inbetween has messed up typeclass search.

[Reid Barton]

aha! Well this lie_algebra R L extends lie_ring L is a known anti-pattern

[Sebastien Gouezel]

We need a linter for this!

[Gabriel Ebner]

This works:

example (z : ℂ) : (complex.conj z).im = -z.im := by simp [-lie_skew]

The lie_skew lemma has a [lie_ring L] argument which triggers this ugly search.

[Gabriel Ebner]

Thanks @Sebastien Gouezel and @Reid Barton for debugging this!

[Gabriel Ebner]

@Reid Barton Is there a standard replacement for this anti-pattern?

[Reid Barton]

move [lie_ring L] to before extends, and then add it as another argument in 100 places

[Reid Barton]

Although perhaps lie_ring could extend add_comm_group, which would help a bit

[Reid Barton]

I also have to say I don't understand why simp gets as far as trying to synthesize this instance

[Reid Barton]

So concretely, change

class lie_ring (L : Type v) [add_comm_group L] extends has_bracket L :=

to

class lie_ring (L : Type v) extends has_bracket L, add_comm_group L :=

and

class lie_algebra (R : Type u) (L : Type v)
  [comm_ring R] [add_comm_group L] extends module R L, lie_ring L :=

to

class lie_algebra (R : Type u) (L : Type v)
  [comm_ring R] [lie_ring L] extends module R L :=

[Reid Barton]

then delete [add_comm_group L] elsewhere or replace it by [lie_ring L] as appropriate

[Gabriel Ebner]

Is there a canonical Lie structure on a ring? Lots of lie_ring definitions are not instances.

[Reid Barton]

Yes, there is lie_ring.of_associative_ring ($[X, Y] = XY - YX$). I'm not sure why it is not an instance, but it seems reasonable to have it be opt-in.

[Reid Barton]

Is it causing a problem?

[Gabriel Ebner]

You have to write more instances by hand now. And the errors that you get when you have an extra add_comm_group instance lying around are not pretty.

[Gabriel Ebner]

#2084

[Floris van Doorn]

We need a linter for this!

The linter dangerous_instanceshould find this. I will investigate why it doesn't.

[Reid Barton]

I see. There seem to be two changes going on here.

• Since lie_algebra no longer extends lie_ring but is indexed on it you have to write two instances instead of one.
• In the lie_algebra instance the lie_ring part can't be inferred from the definition, and also can't be inferred from instance search because what I've been calling instances are not actually instances at all.

[Reid Barton]

For the second one maybe we can just make lie_ring.of_associative_ring an instance after all. @Oliver Nash @Johan Commelin was there a strong reason to not have it be an instance? I assume it was discussed at some point on the github issue but there are way too many collapsed comments to go looking for it...

[Reid Barton]

Gabriel, do you need this to bump the mathlib version or something?

[Floris van Doorn]

The linter dangerous_instanceshould find this. I will investigate why it doesn't.

Oh, dangerous_instance does catch this problem:

The following arguments become metavariables. argument 1: (R : Type u)

The problem is that currently linters are disabled for automatically generated definitions. This is necessary for many linters, but linters that check the library more globally (like the instance checking and simp-lemma checking) should be enabled for automatically generated declarations. This in on my to-do list.

[Gabriel Ebner]

Kind of, in the lean36 branch the simp_nf linter produces lots of timeouts. This is one of the timeouts.

[Reid Barton]

I think https://github.com/leanprover-community/mathlib/pull/1644#discussion_r343902029 is about this lie ring of ring instance/def

[Reid Barton]

Yes, I remember now. Another concern is if you have an instance saying a product of Lie algebras is a Lie algebra, then a product of rings becomes a Lie algebra in two ways. In this case I believe the resulting definitions will work out to be defeq, but in general there could be a problem.

[Johan Commelin]

Sorry for (partially) causing this mess.

[Johan Commelin]

I think we didn't make it an instance because we thought it was better to be conservative for now.

[Reid Barton]

Gabriel I think your change looks fine. Actually the ones for matrix n n R really should be instances, I think, because this is the "by definition" instance. (Unless we wanted to make a synonym gl n R := matrix n n R and attach the instance to that instead.) That would save one occurrence of @lie_algebra.

[Reid Barton]

Johan I think I even also argued that it should not be an instance.

[Johan Commelin]

@Gabriel Ebner What is the best way forward? Should this be fixed in a separate PR?

[Johan Commelin]

Because I guess that we are running the risk that the bump PR is going to be a huge mess of little changes, and if multiple people contribute, then there will be nobody who has an overview of whether the PR is still doing only harmless changes...

[Reid Barton]

Do you mean other than #2084?

[Reid Barton]

or is that already a "separate PR"?

[Johan Commelin]

Ooh, I hadn't seen that one yet...

[Johan Commelin]

I think this is fine as is. I wouldn't be surprised if we want the gl synonym/abbreviation. We can always turn that def into an instance later.

[Johan Commelin]

@Floris van Doorn If you can make the linter catch these errors that would be great. It would prevent future me from messing up again.

[Johan Commelin]

@Gabriel Ebner I've put #2084 on the merge queue

[Scott Morrison]

The linter is upset with #2084 because of

-- algebra/ordered_group.lean
#print add_neg_le_iff_le_add /- Left-hand side simplifies from
  a + -c ≤ b
to
  a ≤ c + b
using
  [add_neg_le_iff_le_add']
Try to change the left-hand side to the simplified term!
 -/

[Scott Morrison]

How was this not a problem previously?

[Gabriel Ebner]

Do you remember my original complaint in this thread? Apparently simp refuses to rewrite anything if the type class resolution fails (takes too long? not sure) for a single simp lemma. (This looks like a bug.) The lie_skew seems to apply to some (all?) negations and causes a loop in type class resolution. Hence there were a lot of terms that simp did not rewrite, even though they could be simplified with some by simp only [only simp lemmas here]. Now that the lie_algebra issue is fixed, simp is effectively more powerful and the linter can now detect more problems.

[Reid Barton]

What I think is the most surprising thing about this is that these simp failures are indistinguishable from "simp couldn't make any progress", right?

[Reid Barton]

So when simp fails to apply the lemma you expect, the reason could be that some other lemma is timing out?

[Reid Barton]

while one might naively expect that that would instead result in a timeout?

[Gabriel Ebner]

Reid Barton said:

So when simp fails to apply the lemma you expect, the reason could be that some other lemma is timing out?

Yes, this is very counterintuitive. But it's the best explanation I have before looking into the C++ code.

[Scott Morrison]

Ah, thanks. Sorry for the noise, I was jumping in halfway through.

[Gabriel Ebner]

https://github.com/leanprover-community/lean/issues/137

[Gabriel Ebner]

The linter actually ignored all errors from simp on purpose. There is a <|> pure none line in the linter. That's because I was getting lots of errors from type class resolution.

[Gabriel Ebner]

I've removed the line from the linter that ignores the errors. Let's say what it says now: https://github.com/leanprover-community/mathlib/runs/485926769

[Reid Barton]

okay, but in general interactive use... I will just try the example, thanks

[Reid Barton]

"neat"

[Oliver Nash]

Argh many apologies for mostly causing this mess, and many thanks for the PR which has fixed it.

[Patrick Massot]

As you can see from this discussion, these are very subtle issues, and nobody as a good rule book here.

[Oliver Nash]

Thanks @Patrick Massot I have just read through the thread and I still feel guilty, but I am too late to have anything to offer.

[Rob Lewis]

This is exactly what the linters are for: hard to know you're doing something dangerous, hard for any reviewer to notice, but the computer can notice easily. Finding this kind of situation is good because we can improve the linters.

[Kevin Buzzard]

So I am assuming that G_module_hom G M N should not extend add_monoid_hom M N for the same reason?

[Kevin Buzzard]

But I can still add a coercion manually, right?

[Reid Barton]

are these structures? The issue described here is only relevant to classes

[Kevin Buzzard]

Aah! Great!