I love the linter

Stream: general

[Kevin Buzzard]

I've seen people going on about the linters, but I didn't ever realise it was as simple as just going to the bottom of your file and typing #lint. This should be better known! I've already learnt something new about simp by looking at my first linter output.

: -/
#print polynomial_derivation.map_C_mul /- Left-hand side simplifies from
  ⇑d (C k * f)
to
  C k * ⇑d f + f * ⇑d (C k)
using
  [polynomial_derivation.map_mul]
Try to change the left-hand side to the simplified term!
 -/

I particularly love the emoji in the top line. Here's the set-up:

import tactic
import data.polynomial

structure polynomial_derivation (R : Type) [comm_ring R] :=
(to_fun : polynomial R → polynomial R) -- Delta
(map_add' : ∀ (f g : polynomial R), to_fun (f + g) = to_fun f + to_fun g) --Delta2
(map_C_mul' : ∀ (k : R) (f : polynomial R), to_fun (polynomial.C k * f) = polynomial.C k * to_fun f) --Delta3
(map_mul' : ∀ (f g : polynomial R), to_fun (f * g) = f * to_fun g + g * to_fun f)

open polynomial

namespace polynomial_derivation

variables {R : Type} [comm_ring R]

/-- think of a polynomial derivation as a function from R[X] to R[X] -/
instance : has_coe_to_fun (polynomial_derivation R) :=
{ F := λ _, polynomial R → polynomial R,
  coe := to_fun -- should say `to_fun` once the derivation is defined
}

@[simp]
theorem map_add (d : polynomial_derivation R) : ∀ {f g : polynomial R}, d (f + g) = d f + d g := d.map_add'

@[simp]
def map_C_mul (d : polynomial_derivation R): ∀ (k : R) (f : polynomial R), d (C k * f) = C k * d f := d.map_C_mul'

@[simp]
def map_mul (d : polynomial_derivation R): ∀ (f g : polynomial R), d (f * g) = f * d g + g * d f := d.map_mul'

[Kevin Buzzard]

What did I do wrong?

[Mario Carneiro]

map_C_mul is a special case of map_mul

[Mario Carneiro]

You could set the priority higher, or you could prove that d (C k) = 0 and then you will get the same result without it

[Johan Commelin]

Prove map_C, tag that one as simp and remove simp from map_C_mul.

[Mario Carneiro]

also, shouldn't you be getting a lint for marking those theorems as def?

[Kevin Buzzard]

This is something Shing and I are working on. It's still a WIP but nearly done.

[Kevin Buzzard]

Mario Carneiro said:

map_C_mul is a special case of map_mul

Only in the presence of map_C

[Kevin Buzzard]

So have we got the definition of the structure wrong?

[Mario Carneiro]

no, the lhs of map_C_mul is an instantiation of the lhs of map_mul

[Mario Carneiro]

that means that given input d (C k * f) they will race to see which will rewrite first

[Kevin Buzzard]

Yes I understand that, but the right hand side isn't, right?

[Mario Carneiro]

in the absence of map_C, that means it's not confluent

[Kevin Buzzard]

I know who wants to win that race though

[Mario Carneiro]

then set the priority of the winner higher

[Kevin Buzzard]

I have no real idea what the word confluent means.

[Kevin Buzzard]

Should I be changing priorities of winners, or should be aiming for full confluence compliance?

[Mario Carneiro]

confluent means that if A rewrites to B and A also rewrites to C, then B and C will eventually reach some common point D

[Kevin Buzzard]

right -- so that was exactly what didn't happen when we made all the structure fields simp lemmas

[Mario Carneiro]

You can make it confluent by adding map_C as a simp lemma

[Kevin Buzzard]

and removing simp from map_C_mul I guess

[Mario Carneiro]

not even

[Kevin Buzzard]

Do I or not?

[Mario Carneiro]

confluence means that they can diverge but they come back together

[Mario Carneiro]

if you have "shortcut" simp lemmas this can cause a confluent rewrite system even though there is not a unique path

[Kevin Buzzard]

Do they come back together? This will be a 50-50 chance depending on whether it's add_zero or zero_add which is definitions, right?

[Kevin Buzzard]

Oh no, who cares about defeq here

[Mario Carneiro]

d (C k * f) = C k * d f + f * d (C k) = C k * d f + f * 0 = C k * d f + 0 = C k * d f

[Kevin Buzzard]

There is some other relation -- simp_rel, which is I guess related to defeq

[Kevin Buzzard]

Right -- I don't care whether it's add_zero or zero_add which is the definitional one, I just need to make sure they are both tagged with @[simp]

[Mario Carneiro]

right, this is not a defeq thing

[Mario Carneiro]

note also that simp_rel is not symmetric like defeq

[Kevin Buzzard]

But I want to encourage simp to go the short way and not do the calculation you posted.

[Mario Carneiro]

that's what priority is for

[Mario Carneiro]

or you can just throw them in a bag and let them duke it out

[Kevin Buzzard]

So where is the AI that analyses my confluent rewriting system and says "I suggest you put the following priorities on these simp lemmas: ..."?

[Mario Carneiro]

hey, at least we detected the split

[Kevin Buzzard]

so is this hard? I thought that would be exactly the sort of thing you were good at

[Mario Carneiro]

figuring out that it's confluent is hard enough (undecidable?)

[Kevin Buzzard]

I know but the system here is tiny

[Mario Carneiro]

the simp set is massive

[Kevin Buzzard]

I know I will not be rewriting lists here, polynomials are atoms

[Kevin Buzzard]

I know to ignore all $\le$ simp lemmas

[Mario Carneiro]

if you analyze the simplified problem, in some cases, you can prove confluence

[Kevin Buzzard]

I just want them off. I want to say "look, this is about polynomial rings, so you can have all polynomial ring simp lemmas and that's it, no junk about filters"

[Mario Carneiro]

You can also nolint it and move on with your life

[Kevin Buzzard]

"I don't care if someone accidentally imported topological spaces"

[Johan Commelin]

This is the moment where Kenny posts his remark about simpsets.

[Kevin Buzzard]

I'm all ears. I really felt like I learnt something new about simp today.

[Mario Carneiro]

the topological spaces lemmas don't apply, but it can be hard to determine that in advance

[Kevin Buzzard]

Thanks @Shing Tak Lam . He wrote the proofs but I did the simp labelling.

[Mario Carneiro]

What if your polynomial ring also happens to be a topological space?

[Mario Carneiro]

Simp is pretty smart about looking only at the relevant lemmas to apply, but it has the simple job, it has a term already and is rewriting it. Analyzing the simp set as a whole is much harder

[Mario Carneiro]

and yes, this is an active area of CS research

[Mario Carneiro]

if you want to read a wikipedia article, try https://en.wikipedia.org/wiki/Knuth%E2%80%93Bendix_completion_algorithm

[Kevin Buzzard]

Where are the docs for #lint? I want to switch all but one of them off.

[Rob Lewis]

https://leanprover-community.github.io/mathlib_docs/commands.html#linting%20commands

[Rob Lewis]

#lint only doc_blame

[Kevin Buzzard]

I :heart: the docs

[Mario Carneiro]

where's doc_thank?

[Kevin Buzzard]

Yeah I could just link to that

[Kevin Buzzard]

rofl I couldn't find it in the docs because I didn't know #lint was a command :-)

[Mario Carneiro]

I see a feature request: go to definition for user commands

[Mario Carneiro]

also hover with doc string

[Kevin Buzzard]

Yeah, these were the exact two things I tried before I asked here.

[Gabriel Ebner]

Mario Carneiro said:

figuring out that it's confluent is hard enough (undecidable?)

By Newman's lemma, confluence follows from local confluence and termination. Checking termination is undecidable (in general), but if we assume termination then we only need to check for local confluence, which is straightforward.
I've implemented this linter, but it didn't make it into the maintenance paper. You can look at the results here: https://gist.github.com/gebner/6f72773b22b18f6e1d4e4f8532aedfe8

The big issues are:

1. The implementation is really slow. It takes 3 hours to run.
2. In some cases, it takes even longer. There is a timeout implemented using try_for (shown as "timeout" in the output). But the linter framework doesn't work well with linters that fail non-deterministically (as is the case with try_for).
3. I'm not sure how useful the results are. Should all non-confluent pairs be fixed?

[Mario Carneiro]

Not all non-confluent pairs should be fixed. This probably gets even more dicey if we have nolint confluence lemmas and you somehow have to check confluence of everything else

[Mario Carneiro]

I have been working under the assumption that simp is only a best effort rewrite system with no pretensions to confluence, so I never made any serious attempt to keep the overall system confluent or nearly so

[Mario Carneiro]

and more to the point, as a #lint, fixing a confluence bug is not necessarily a thing you can just do. I would rather have more simplification at the cost of confluence

[Kevin Buzzard]

OK so here is a development of group theory in Lean. I always felt like at the beginning I was going uphill proving mul_one because the axiom was one_mul. Is this anything to do with confluent rewriting? And how do I figure out what lemmas to tag as simp? I just tried randomly -- as long as they passed the basic criteria (like being an equality rather than an implication, and the right hand side being a bit simpler than the left hand side, and everything being in canonical form) they were in.

[Mario Carneiro]

But the linter framework doesn't work well with linters that fail non-deterministically (as is the case with try_for).

But... but... what's all that business about (deterministic) timeout then?

[Gabriel Ebner]

Mario Carneiro said:

and more to the point, as a #lint, fixing a confluence bug is not necessarily a thing you can just do.

Most of the time the solution is to add more simp lemmas. It only becomes a problem if the new simp lemmas then introduce new confluence bugs. :slight_smile:

[Kevin Buzzard]

Hey linter

/- UNUSED ARGUMENTS: -/
#print mygroup.group.inv_eq_of_mul_eq_one /- argument 5: (h : a * b = 1) -/

what are you talking about?

[Mario Carneiro]

one example of a known non-confluence in simp is the rules around coercion. ↑x < ↑y <-> x < y, but also ↑(x + y) = ↑x + ↑y so ↑(a + b) < ↑c can simplify to either a + b < c or ↑a + ↑b < ↑c

[Kevin Buzzard]

Oh I see, a sorried proof and it complains that I didn't use the hypotheses.

[Gabriel Ebner]

Mario Carneiro said:

But... but... what's all that business about (deterministic) timeout then?

The deterministic part is unfortunately a bit optimistic in my experience. It just means that the timeout is not affected by how fast your machine is (or how many other programs you have running). But the timeout still depends on the state of the caches, the result of mk_fresh_name, etc.
So the linter would probably be deterministic if you run it twice on the same mathlib revision. But a tiny change could cause the linter to fail on unrelated declarations.

[Gabriel Ebner]

Mario Carneiro said:

one example of a known non-confluence in simp is the rules around coercion. ↑x < ↑y <-> x < y, but also ↑(x + y) = ↑x + ↑y so ↑(a + b) < ↑c can simplify to either a + b < c or ↑a + ↑b < ↑c

That's a good one. For completion, you'd need to add ↑a + ↑b < ↑c <-> a + b < c and ↑a + ↑b + ↑c < ↑d <-> a + b + c < d and so on.

[Kevin Buzzard]

let's get started!

[Kevin Buzzard]

how many do you think we'll need in practice?

[Sebastian Ullrich]

Obviously it's in parentheses because it's not always true. Uh.

[Gabriel Ebner]

Kevin Buzzard said:

OK so here is a development of group theory in Lean. [...] Is this anything to do with confluent rewriting?

Yes. In term rewriting systems, completion refers to the process of taking a set of equations (such as your group axioms) and producing a confluent and terminating set of rewrite rules (lemmas tagged as simp) with the property that every equation following from the group axioms is provable by simp. (For groups this works, and you can also do this automatically.)
There is a paper by Kaliszyk and Sternagel where they try to automatically derive a simp set in this way for all equations in the HOL light library: https://easychair.org/publications/paper/h6b

[Kevin Buzzard]

So simp-labelling is an art? No wonder I'm no good at it. I had assumed it was a science.

[Mario Carneiro]

there is a reasonably objective success metric, and an algorithm that will work in a large number of practical cases, but sometimes you have to be clever. In that sense it's like theorem proving

[Kevin Buzzard]

Why did I feel like I was going uphill until I'd proved mul_one and mul_right_inv, and then everything became trivial?

[Patrick Massot]

@Kevin Buzzard , I strongly suggests your should read this paper.

[Kevin Buzzard]

Thanks Patrick. Hey, they complain about list.length_singleton on p8. This feels a bit like the difference between {x} and {y | y = x}. @Mario Carneiro was talking about redefining {x} but perhaps [x] is a bit different because I can only think of cons x nil for the definition.