surjective is not funprop!

Stream: Is there code for X?

[Kenny Lau]

import Mathlib

lemma foo : Function.Surjective (id : ℕ → ℕ) := by fun_prop
/-
`Function.Surjective id` is not a `fun_prop` goal!
Maybe you forgot marking `Function.Surjective` with `@[fun_prop]`.
-/

attribute [fun_prop] Function.Surjective
attribute [fun_prop] Function.surjective_id

lemma foo' : Function.Surjective (id : ℕ → ℕ) := by fun_prop

[Kenny Lau]

Why is Function.Surjective not marked as fun_prop?

[Floris van Doorn]

Nobody has done it yet.
I think it would be good to mark Surjective and friends as fun_prop, I think this was recently suggested elsewhere on Zulip.

[Kenny Lau]

@Floris van Doorn I want to do it. Which file should I do this in? I see that Mathlib.Tactic.FunProp is imported by:

Mathlib.Tactic.FunProp.Differentiable
Mathlib.Topology.Defs.Basic
Mathlib.MeasureTheory.MeasurableSpace.Embedding
Mathlib.Tactic.FunProp.ContDiff
Mathlib.Tactic.ContinuousFunctionalCalculus
Mathlib
Mathlib.Tactic

which all seem to be quite late in the import hierarchy compared to Mathlib/Logic/Function/Defs.lean which contains the definitions of injective, surjective, and bijective.

[Ruben Van de Velde]

Yeah, somewhere under Mathlib.Tactic.FunProp

[Kenny Lau]

@Ruben Van de Velde are you referring to the file itself, or a new file? If it's a new file, where should I put the new file?

[Aaron Liu]

Is docs#Function.Injective a fun_prop property? Can you put it together with that if it is?

[Jireh Loreaux]

@Kenny Lau you should only need to import Mathlib.Tactic.FunProp.Attr in order to mark them as @[fun_prop], and this file has very lightweight imports.

[Kenny Lau]

@Jireh Loreaux Are you saying I should import M.T.FunProp.Attr from M.Logic.Function.Defs?

[Michael Rothgang]

I'm not Jireh, but that's how I read the message.

[Jireh Loreaux]

Yes. The imports for Mathlib.Logic.Function.Defs are so minimal that the large-import tag might get placed on it anyway, but if so and someone complains we can have a discussion.

[Kenny Lau]

(#mathlib4 > `fun_prop` for Injective/Surjective/Bijective? @ 💬 )

[Robert Maxton]

Indeed, the only reason I haven't done it myself is that I've been waiting til I have the attention to write a script to find all the lemmas that prove injective/etc

[Robert Maxton]

and automatically fun_prop them, as I expect there to be hundreds if not thousands of them ^.^;

[Kenny Lau]

ah, I should add that I have made a very small start at #28191

[Kenny Lau]

@Robert Maxton Loogle already exists

[Robert Maxton]

Loogle exists, but I don't see an amazing way of tying it into a script, and for that matter I don't even see a way to get more than the first 200 results ^.^;

[Kenny Lau]

I think #loogle exists as a command if you do the right things

[Jovan Gerbscheid]

Would it also make sense to have fun_prop for Monotone/Antitone?

Btw I was recently running into the annoyance that the Monotone/Antitone lemmas are also useful in their unfolded form, since gcongr currently only takes that form. Any advice on what to do here? State them only in one form, or have some automation to get both forms?

[Kenny Lau]

yes

[Kenny Lau]

Jovan Gerbscheid said:

since gcongr currently only takes that form

change gcongr?

[Jovan Gerbscheid]

There is another reason to prefer the expanded form, at least when dealing with a lambda function (Monotone fun x => ...), namely that the lambda may not get beta-reduced:

import Mathlib

example (a b : ℝ) (h : a ≤ b) : False := by
  have := monotone_mul_left_of_nonneg zero_le_two h
  -- this : (fun x => 2 * x) a ≤ (fun x => 2 * x) b

But yes it would make sense to prove only the Monotone version for non-lambda functions.

[Alex Meiburg]

I also today ran into wanting StrictMono and StrictAnti as well.
On that note,

theorem Real.sqrt_mono : Monotone Real.sqrt :=
  fun _ _ ↦ Real.sqrt_le_sqrt

was missing too...

[Jovan Gerbscheid]

Note that the naming convention is to call it sqrt_monotone, as we are referring to the definition Monotone. I have a PR somewhere to fix this, which I'll get back to after the fix to gcongr gets merged in #28339

[Jireh Loreaux]

or rather monotone_sqrt.

[Jovan Gerbscheid]

No, the naming convention specifically says to use monotone and friends as suffixes. Similarly for surjective and friends

[Jireh Loreaux]

I always forget that one. I really dislike that convention.

[Alex Meiburg]

Well, #28550 should be an easy review at least