data.set.function

Stream: mathlib4

[Jireh Loreaux]

The PR for Data.Set.Function is almost ready, but I have to stop working on it for several hours, in case anyone wants to have a go at finishing it up: mathlib4#1035

[Jireh Loreaux]

There are just 3 declarations that need their proofs fixed and I think a few long lines and then it will be done.

[Thomas Murrills]

@Moritz Doll, does your reaction mean you’re working on it? I’ll give it a go rn if you’re not.

[Moritz Doll]

yes, I am having a look at it now. I don't mind if you look at it as well

[Eric Wieser]

cc @Yaël Dillies who has some open PRs against the mathlib3 file

[Thomas Murrills]

Ok! I saw your reaction after I did the easy bit: fixing the formatting. We just delete mathport warnings (which are above declarations that are good to go), right?

[Thomas Murrills]

(Pushed the format-fixing commit assuming so. If not I’ll undo it.)

[Moritz Doll]

partial progress for the first sorry:

lemma restrict_extend_range (f : α → β) (g : α → γ) (g' : β → γ) :
  (range f).restrict (extend f g g') = λ x, g x.coe_prop.some :=
begin
  classical,
  exact restrict_dite _ _,
end

works in mathlib3

[Moritz Doll]

and also in mathlib4 :tada:

[Moritz Doll]

sorries have been fixed - @Thomas Murrills I leave the formatting things to you

[Moritz Doll]

Maybe we should consider a terminal convert as evil

[Thomas Murrills]

Nice! :big_smile: my formatting commit apparently got in right before your commits, so with your merge I think we should be good!

[Moritz Doll]

I missed two errors, but now it the branch builds without errors on my machine and also the linter is happy

[Thomas Murrills]

Great! (I was finding and fixing the long lines manually—I've been struggling with some error building mathlib4 for the past hour or so, and couldn't access #lint 😅)

[Gabriel Ebner]

Maybe we should consider a terminal convert as evil

I find non-terminal converts to be much more evil.

[Moritz Doll]

but these are actually useful and not a hack

[Gabriel Ebner]

How are terminal converts not useful? They allow you to plug in a proof "up to subsingletons".

[Gabriel Ebner]

On the other hand non-terminal converts are pretty fragile in my experience. If you change the reducibility of a definition, or add subsingleton instances, the tactic suddenly returns a whole different set of goals. And these goals might not even be provable anymore. Whenever I see a convert break during a refactoring, I try to remove it.

[Moritz Doll]

I've used terminal convert once or twice in mathlib3 and the reason was that exact had really weird errors, but I was convinced that it should be just exact :sweat_smile:
I agree that convert is very fragile, but sometimes it is very close to how the informal proof goes and it is more tedious to work around with rather artificial haves.

[Scott Morrison]

@Moritz Doll, @Jireh Loreaux, I fixed quite a few names in https://github.com/leanprover-community/mathlib4/pull/1035/commits/8fc6e42ae6ea6e1283c81b05e7f7c9420751d0c8, for future reference.

I'll merge shortly.

[Jireh Loreaux]

Thanks. But I'm confused why, for example, Monotone.rangeFactorization has that spelling. It's a theorem, so it should be snake_case, right?

[Jireh Loreaux]

Oh wait, I get it. It's a lemma about rangeFactorization. Sorry, that's why I missed this and codRestrict. I'll check for this better next time.

[Jireh Loreaux]

The mapsTo was just one that slipped by.

[Moritz Doll]

On the other hand non-terminal converts are pretty fragile in my experience. If you change the reducibility of a definition, or add subsingleton instances, the tactic suddenly returns a whole different set of goals. And these goals might not even be provable anymore. Whenever I see a convert break during a refactoring, I try to remove it.

only 7 hours later I have three broken converts..

[Kevin Buzzard]

convert using 1 is a bit less fragile