Subgroups are empty

Stream: mathlib4

[Yaël Dillies]

Trust Lean!

import Mathlib.Algebra.Group.Submonoid.Operations

variable {G : Type*} [Monoid G] (H : Submonoid G)

#synth One G -- `Monoid.toOne`
#synth One H -- `H.one`
#synth Nonempty G -- `One.instNonempty`
#synth Nonempty H
/-
failed to synthesize
  Nonempty ↥H
-/

[Sébastien Gouëzel]

Works fine on Lean 4.9.0.

[Michael Stoll]

The trace is

[Meta.synthInstance] ❌ Nonempty ↥H ▼
  [] new goal Nonempty ↥H ▼
    [instances] #[@Zero.instNonempty, @One.instNonempty, infSet_to_nonempty, supSet_to_nonempty, top_nonempty, bot_nonempty, @Nontrivial.to_nonempty, @instNonemptyOfInhabited, @instNonemptyOfMonad, @nonempty_lt, @Set.univ.nonempty, @Set.instNonemptyElemInsert, @Set.instNonemptyElemImage, @Set.instNonemptyRange, @Set.nonempty_Ici_subtype, @Set.nonempty_Iic_subtype, @Set.nonempty_Ioi_subtype, @Set.nonempty_Iio_subtype]
  [] ❌ apply @Set.nonempty_Iio_subtype to Nonempty ↥H ▶
  [] ❌ apply @Set.nonempty_Ioi_subtype to Nonempty ↥H ▶
  [] ❌ apply @Set.nonempty_Iic_subtype to Nonempty ↥H ▶
  [] ❌ apply @Set.nonempty_Ici_subtype to Nonempty ↥H ▶
  [] ❌ apply @Set.instNonemptyRange to Nonempty ↥H ▶
  [] ❌ apply @Set.instNonemptyElemImage to Nonempty ↥H ▶
  [] ❌ apply @Set.instNonemptyElemInsert to Nonempty ↥H ▶
  [] ❌ apply @Set.univ.nonempty to Nonempty ↥H ▶
  [] ❌ apply @nonempty_lt to Nonempty ↥H ▶
  [] ❌ apply @instNonemptyOfMonad to Nonempty ↥H ▶
  [] ✅ apply @instNonemptyOfInhabited to Nonempty ↥H ▼
    [tryResolve] ✅ Nonempty ↥H ≟ Nonempty ↥H
    [] new goal Inhabited ↥H ▼
      [instances] #[@Unique.instInhabited, @instInhabitedOfMonad, @Subtype.instInhabited]
  [] ✅ apply @Subtype.instInhabited to Inhabited ↥H ▼
    [tryResolve] ✅ Inhabited ↥H ≟ Inhabited ↥H
  [resume] propagating (x_0 : G) → x_0 ∈ H → Inhabited ↥H to subgoal Inhabited ↥H of Nonempty ↥H ▼
    [] size: 1
    [] skip answer containing metavariables instNonemptyOfInhabited

I don't really know what the last message means, but it seems to lead to a failure even though there are several :check:s and no :cross_mark:s in the last part of the trace, (EDIT:) even though there are further instances that can be tried. I would think that "skipping" instNonemptyOfInhabited should cause it to consider the next available instance in the list and not to give up altogether.

[Michael Stoll]

In the case of G, the trace is fairly long (going via boolean algebras and biheyting algebras among other stuff; the usual order detours...), but finally reaches the One.instNonempty instance and then eventually finds a One for G. (The relevant instance Monoid.toOne is only the sixth that is tried.)

[Michael Stoll]

BTW, Zero.instNonempty and One.instNonemtpy have very low priority (20) and so are tried last. Is there a reason behind that?

[Yaël Dillies]

I assume that's exactly the same reason as to why you tried to decouple the algebraic order hierarchy from the algebraic hierarchy: One is algebraic while Nonempty is not

[Matthew Ballard]

lean#4055 is sufficient to fix this right? #mathlib4 > Nonempty regression

[Yaël Dillies]

Oh right, it's the same issue

[Michael Stoll]

Still, I wonder why instance sythesis fails when trying Subtype.instInhabited rather than backtracking.

[Matthew Ballard]

You can make it work without removing the instance by inserting

      if answer.result.numMVars != 0 then
        return ()
      else

into docs#Lean.Meta.SynthInstance.resume at L598.

[Michael Stoll]

Should this be turned into an issue?

[Matthew Ballard]

Someone can ask about it in office hours but I imagine that the answer will be: "You put poorly formed instances into the machine at your own risk."

[Matthew Ballard]

Mathlib seems to be building fine as-is with the change but seems slower to my eye

[Matthew Ballard]

Just as I said that

error: ././././Mathlib/Topology/UniformSpace/Pi.lean:145:9-145:45: failed to synthesize instance
  UniformSpace (ι → X)

[Matthew Ballard]

Here is the list of all times this code branch is hit: https://gist.github.com/mattrobball/374f5c2951fbb92e129d59b7e92fa9f1

[Matthew Ballard]

After lean#4055, https://gist.github.com/mattrobball/df5a9fa5d1b3130c0892d5d0f1753086

[Matthew Ballard]

Actually I think at least the message should be modified to reflect that you skip the whole branch instead of just that node.

[Sébastien Gouëzel]

This is very interesting. What do you think for example of the first instance that is flagged by this, of the form:

instance Finset.decidableForallOfDecidableSSubsets {α : Type u_1} [DecidableEq α] {s : Finset α}
    {p : (t : Finset α) → t ⊂ s → Prop} [(t : Finset α) → (h : t ⊂ s) → Decidable (p t h)] :
    Decidable (∀ (t : Finset α) (h : t ⊂ s), p t h)

It has a very unusual form, and I am not sure it can ever fire. Should we just remove the instance?

[Matthew Ballard]

I think that is a good experiment

[Yaël Dillies]

Is it that unusual? Or do you mean the fact that it's a dependent function in h : t ⊂ s is unusual?

[Sébastien Gouëzel]

Yes, the fact that it's a dependent function is unusual -- how would typeclass inference check this assumption?

[Yaël Dillies]

Oh actually you're right. I found out that instances about Prop-dependent functions never apply

[Yaël Dillies]

I don't really understand why though. (∀ i : ι, Group (G i)) → Group (∀ i, G i) works fine if ι : Type* even though TC inference can't "find" i

[Sébastien Gouëzel]

I confirm that mathlib builds fine without this instance. #12987.

[Matthew Ballard]

I am happy to send this off but will wait a bit for anyone to comment

[Matthew Ballard]

Yaël Dillies said:

Oh actually you're right. I found out that instances about Prop-dependent functions never apply

Sounds like some un-intended consequences of proof irrelevance casing

[Matthew Ballard]

Sébastien Gouëzel said:

This is very interesting. What do you think for example of the first instance that is flagged by this, of the form:

instance Finset.decidableForallOfDecidableSSubsets {α : Type u_1} [DecidableEq α] {s : Finset α}
    {p : (t : Finset α) → t ⊂ s → Prop} [(t : Finset α) → (h : t ⊂ s) → Decidable (p t h)] :
    Decidable (∀ (t : Finset α) (h : t ⊂ s), p t h)

It has a very unusual form, and I am not sure it can ever fire. Should we just remove the instance?

Actually, the problems from this instance seem to come from using refine' in place of refine

[Matthew Ballard]

Quite a few of the remaining ones do

[Matthew Ballard]

Either that or convert

[Matthew Ballard]

Matthew Ballard said:

After lean#4055, https://gist.github.com/mattrobball/df5a9fa5d1b3130c0892d5d0f1753086

#12997 replaces some refine''s with refine's guided by this list

[Johan Commelin]

Should we forbid refine' in new contributions?

[Johan Commelin]

There is only ~11192 occurrences left in mathlib master :oops: :rofl:

[Matthew Ballard]

I like the more declarative syntax by default

[Matthew Ballard]

I did encounter one instance where the straightforward refine replacement failed but refine' was ok.

[Matthew Ballard]

I expect that is bad sign (for that instance)

[Yaël Dillies]

I was very much against refine originally because it was less convenient to use than refine'. Looking back, it seems that my issue with it was mostly with the highlighting being janky. Now that the ununifyable holes get properly highlighted, it's actually very nice to use.

[Matthew Ballard]

I think there are certainly some use case for refine' (really refine!?) but it is very much overused right now

[Damiano Testa]

Johan Commelin said:

Should we forbid refine' in new contributions?

If you've been following my recent posts, you might think that I would propose a linter for this (btw, there is already one for flagging refine', suggesting to use refine). However, for this usage, maybe there could be a CI action that looks at the diff and greps refine', adding a label if it finds any.

[Matthew Ballard]

I have! Completely separate question: are there any proto-autoformaters out there?

Here:

• swap refine' for refine
• capture errors and if the syntax is _ replace with ?_
• if this fails, leave it changed and keep going

[Damiano Testa]

I think that you might even have the linter (with more work) output the positions of the _ that require a ? and then feed that to something like sed for the final replacement.

[Damiano Testa]

The final catching of errors would be a little more brittle...

[Matthew Ballard]

Oh. That’s a good point. I was thinking of something written in Lean

[Damiano Testa]

Though, with the MetaTesting experiment, there was a way to try out new syntax replacing the old one, so maybe that too can be automated on top of that PR...

[Damiano Testa]

You may not even need to do the flagging first: you could get a CI cycle to try, for each refine', a replacement of it by the correct ?_ and, only when it works, output the change.

[Damiano Testa]

I am not sure how to handle at once a chain of several refine's in the same tacticSeq -- it might be quite expensive to make it try all subsets...

[Matthew Ballard]

The errors seem to have the correct reference from the language server after doing the swap

[Damiano Testa]

So, here is a proposal: the linter detects refine' and the locations of the _ that should become ?_, produces the syntax using ?_ and runs elabCommand on that. If successful, report success.

[Damiano Testa]

I think that Try this: cannot be used by linters, but once you know what to change, sed can finish up for you.

[Damiano Testa]

In fact, maybe as a first attempt you could even just replace all "full" _s in refine' by ?_ and think about cleaning up the unnecessary one later.

[Damiano Testa]

I remember that the very first refine' that the linter flagged was a refine' that did not have any _...

[Matthew Ballard]

I imagine that capture error + auto-rewrite using pure Lean will come up again in the future. Is there no existing mechanism to approach this?

[Damiano Testa]

capture error -- ok, obviously.

[Damiano Testa]

auto-rewrite, you can probably do it by rewriting the whole file, looking at positions and doing surgical replacements.

[Damiano Testa]

Using the output of logInfos is a no-go, in my experience, for essentially anything: it changes too much of the entering syntaxformatting.

[Matthew Ballard]

Yeah. Without stepping outside the current process would be nice

[Matthew Ballard]

Can we change the elaboration of refine' itself?

[Damiano Testa]

The slight problem with rewriting the file is that you then have to wait for .oleans.

[Damiano Testa]

The linters go sequentially, so I think that you would need a CI cycle for the flagging and then one for the rewriting (at least).

[Damiano Testa]

I tried (quite successfully) this for the theorem --> lemma substitution.

[Damiano Testa]

Matthew Ballard said:

Can we change the elaboration of refine' itself?

Very likely! It was implemented for the port, right? So it should be in Mathlib even, which would make it easy to change.

[Matthew Ballard]

I’m mainly thinking about the clearing the existing 11000+ uses in bulk as much as possible

[Damiano Testa]

How frequent is it that, in a proof, there is a refine' downstream an earlier refine'?

[Matthew Ballard]

Too frequent but not that frequent overall (pure feelings here)

[Damiano Testa]

Anyway, refine flags _ that it cannot solve, so getting that information should be relatively easy.

[Damiano Testa]

After that, you can have a CI cycle to prep for bulk replacement of the first layer of refine's.

[Damiano Testa]

There may even be a temporary refine'' for the refine's that cannot be directly converted to refine's and that should be skipped by iterations of the previous steps.

[Matthew Ballard]

I think 66-75% are just one _ => ?_

[Damiano Testa]

Oh, with the multigoal linter you would know if there are more than 1!

[Matthew Ballard]

And 95%+ should be amenable to the naive fix

[Damiano Testa]

So, actually, if you have `^ *refine' [^_]*_[^_]*$ you could try replacing and maybe it works a lot...

[Damiano Testa]

Out of curiosity, I am trying out this simple "refine' with one _" replacement: #13059.

[Damiano Testa]

I am benching it, but it builds!