simp local confluence checker

Stream: general

[Kim Morrison]

@Joachim Breitner has a working implementation of something close to this. It remains high on my TODO list to actually try it out, and report on how useful it is re: List lemmas (which I've been working on). But it's been sitting on my TODO list for some time now. :-)

[Jared green]

link?

[Andrés Goens]

that sounds really interesting! looking forward to seeing more of that

[Joachim Breitner]

https://github.com/nomeata/lean-simplc/blob/master/Simplc.lean
Happy to explain what I am doing, or help anyone to use it who wants to check their simp API’s for local confluence.

[Kim Morrison]

I am finally trying this out. It's indeed very helpful. :-)

It would be really nice if the output for inspect could also show what simp does to each of the results, in the case that joining fails. I think this would make it easier to identify missing lemmas.

EDIT: oh, I was misread the output: the "Joining failed with" output essentially shows this.

[Kim Morrison]

Another thing that would be useful is for simp_lc inspect could show a warning if either of the named lemmas is not actually @[simp].

(Because I expect a typical workflow will be to remove some @[simp] statements, and then when returning to the simp_lc file there is an indication that that inspect line can now be removed.)

[Joachim Breitner]

I was assuming that simp_lc inspect is only used while investigating a specific pair, but only simp_lc whitelist, simp_lc ignore and simp_lc check are non-termporary.

[Kim Morrison]

Could whitelist show a warning if there isn't actually a problem with that pair?

[Kim Morrison]

Otherwise if the problem goes away independently I will never know to delete that line.

[Joachim Breitner]

That’s more plausible, at least until one starts using simp_lc check [domain_specific_simpset] or so. And then there could be variants, or an option to disable the warning.

[Joachim Breitner]

Warning implemented and pushed

[Kim Morrison]

Maybe you didn't push? I don't see it.

[Joachim Breitner]

Now pushed for real

[Kim Morrison]

Also -- i'm finding that try repeat simp_all is often needed, and gives better results than try simp_all

[Joachim Breitner]

Ever since I banned lake into a container that doesn’t have access to my ssh keys, I fall prey of git push–switch windows–missed the error message

[Joachim Breitner]

Kim Morrison said:

Also -- i'm finding that try repeat simp_all is often needed, and gives better results than try simp_all

Sounds like a bug in simp_all?

[Kim Morrison]

Yeah, I'm not certain. I think this has come up before and we decided it was not a bug, ...

[Kim Morrison]

open List

@[simp] theorem range'_head (n : Nat) (h) : (range' s n).head h = s := by
  sorry

example (s n : Nat) (h : range' s n ≠ []) : s ≤ (List.range' s n).head h ∧ (List.range' s n).head h < s + n := by
  simp_all
  simp_all
  omega

[Kim Morrison]

I agree that looks like simp_all's fault.

[Kim Morrison]

#5094

[Joachim Breitner]

More likely https://github.com/leanprover/lean4/issues/5094

[Kim Morrison]

Oh, after encountering another instance of needing simp_all; simp_all, I am back to believing that this is the correct behaviour of simp_all.

The point is that simp_all first tries to simp hypotheses, then the goal. The problem can be that if the goal depends on the hypotheses in interesting ways, this may block simplification of a hypothesis. When we then move to the goal, the dependency can be removed, but simp_all does not then go back to look at the hypotheses again.

[Kim Morrison]

Here's the other example that made it clear:

example (f : α → Option β) (h₁ : (f a).isSome = true) (h₂ : f a = none) : [(none.get (by rw [h₂] at h₁; simp at h₁) : α)] = [] := by
  simp_all
  simp_all

[Kim Morrison]

@Joachim Breitner, it would be helpful to be able to whitelist a lemma entirely. I'm finding some that I think I do want as @[simp] lemmas, but I just don't care about the non-confluence that it produces.

[Kim Morrison]

I guess

attribute [-simp] head_mem getLast_mem get_find?_mem in
simp_lc check in List

suffices for this

[Joachim Breitner]

Doesn't simp_lc ignore do what you want?

[Joachim Breitner]

Made it use try repeat simp_all. I hope that won’t run into too many loops.

[Kim Morrison]

Fantastic, thanks.

[Kim Morrison]

I would really like whitelist (or some other command) to still run the confluence check, and to give a warning if it is in fact confluent.

Having the warning if one of the lemmas is not a simp lemma is great, but the problem is that if I've whitelisted something, and then add a simp lemma that would resolve it, I never know to remove the whitelist.

[Kim Morrison]

I could achieve this with #guard_msgs, but it's very verbose!

[Kim Morrison]

Also, for my use case at least, the "Try this:" message from check would actually be more useful if it produced inspect rather than whitelist. I understand the reasoning for making it whitelist, but my first step is always to mass edit it back to inspect...

[Joachim Breitner]

I was worried about the cases where you whitelist something because it loops or crashes or so. But maybe that doesn't happen so often. And I can just make two commands.

[Joachim Breitner]

Both implemented. You even get a Try this action to remove the whitelist command. And an option to disable this check.

[Kim Morrison]

One more tiny request: can the message "Checking 671 simp lemmas for critical pairs" say how many confluent pairs it found?

[Kim Morrison]

Oh, yet another: can I write simp_lc check in Foo Bar to check lemmas in multiple namespaces.

[Kim Morrison]

In particular, two namespaces. Since we're doing pairwise checks on lemmas, in principle one could get complete coverage from doing pairwise checks on namespaces.

[Joachim Breitner]

Sounds like we need a general algebra of lemma restrictions, for use in loogle and in tools like this :-)

[Joachim Breitner]

Both implemented.

[Kim Morrison]

@Joachim Breitner, if you have a chance could you take a look at:

simp_lc inspect List.forall_mem_ne' Subtype.forall -- stuck at solving universe constraint

[Joachim Breitner]

Hmm, not sure if my tool can do much here: If you set this goal up manually you also get this:

example (p : α → Prop) (a : α) (l : List { a // p a }):
 (∀ (a' : { a // p a }), a' ∈ l → ¬a' = a) = (∀ (a' : { a // p a }), a' ∈ l → ¬a' = a) :=
 sorry

produces

stuck at solving universe constraint
  ?u.4466+1 =?= max 1 ?u.4059
while trying to unify
  Type ?u.4466 : Type (?u.4466 + 1)
with
  Sort (max 1 ?u.4059) : Type (max 1 ?u.4059)

It helps to constrain (α : Type u) .

[Joachim Breitner]

With that you can investigate the pair manually:

example (α : Type u) (p : α → Prop) (a : { a // p a }) (l : List { a // p a }):
 (∀ (a' : { a // p a }), a' ∈ l → ¬a' = a) = (∀ (a' : { a // p a }), a' ∈ l → ¬a' = a) := by
 conv => lhs; rw [List.forall_mem_ne']
 conv => rhs; rw [Subtype.forall]
 simp -- fails

[Kim Morrison]

That's fine. I can whitelist it with the option to disable whitelist checking.

[Joachim Breitner]

Actually, that universe equation at least uniquely sets the first variable to 0. Should lean recognize this or is this equation too arcane?

[Kim Morrison]

I don't think it does: if it were min on the right hand side it would?

[Joachim Breitner]

Ah, I keep making that mistake with min and max :-)

[Kim Morrison]

Could we make simp_lc check in _root_ work, to ignore everything in a namespace?

[Joachim Breitner]

It’s a bit odd since in List will include List.Perm.foo (should it?) but pragmatically: Sure.

[Kim Morrison]

Yeah, I agree it is weird, but I'm not really sure how else to partition up the work...

[Joachim Breitner]

Oh, the feature request is fine, merely the syntax is a bit non-uniform. As mentioned before, a more expensive and well designed lemma filtering syntax would be useful, but not worth for just this ad-hoc tool. Maybe eventually for Loogle, and reusable here.

[Joachim Breitner]

Added support for in _root_

[Kim Morrison]

Thanks!

[Kim Morrison]

Minor bug report: simp_lc ignore X silences simp_lc inspect A X, but not simp_lc inspect X A. Whatever the behaviour here, it should be the same in either order.

[Joachim Breitner]

Which behavior would you prefer? Ignore ignore when using inspect explicitly, or adhere to it?

[Joachim Breitner]

Ah, judging from the code I probably wanted to ignore only affect simp_lc check. Made that change (mostly untested). I think that’s the better choice.

[Kim Morrison]

simp_lc check
-- Checking 5753 simp lemmas for critical pairs
-- Investigated 6190 critical pairs

We're getting there. There are still a few whitelists that indicate problems about Nat/Int/List, but not many, and BitVec and Fin are really bad.

[Joachim Breitner]

Happy to hear that it's working as intended, and to see the long list of improvements hitting the standard library that you have been producing this week.

You have not looked at Array yet, I assume?

[Kim Morrison]

Array was apparently confluent to begin with.

[Joachim Breitner]

Now I wonder if my tool is buggy :cold_sweat: