## Stream: general

### Topic: map_map

#### Patrick Massot (Apr 07 2019 at 16:05):

Could we get https://github.com/leanprover-community/mathlib/blob/master/src/category/basic.lean#L19 out of the root namespace? map_map is a really generic name, so it's real a pain.

#### Simon Hudon (Apr 07 2019 at 16:08):

How about is_lawful_functor?

#### Kevin Buzzard (Apr 07 2019 at 16:14):

What does protected even mean for a function in the root namespace?

#### Patrick Massot (Apr 07 2019 at 16:15):

I think there was a time when this line was indeed inside a name space

#### Scott Morrison (Apr 07 2019 at 21:34):

getting functor.map_id and functor.map_comp out of the root namespace would also be nice; these often get in the way of category_theory.functor.map_id and co.

#### Kevin Buzzard (Apr 07 2019 at 22:12):

getting functor.map_id and functor.map_comp out of the root namespace would also be nice; these often get in the way of category_theory.functor.map_id and co.

Could these just be protected?

#### Patrick Massot (Jul 07 2020 at 18:10):

@Simon Hudon , would you mind if we get map_mapout of the root namespace? It's a really generic name (and I always want filter.map_map instead, but that's a different topic). TBH, https://github.com/leanprover-community/mathlib/blob/master/src/control/basic.lean#L20 looks like it was meant to be name-spaced anyway.

I'm all for :+1:

#### Patrick Massot (Jul 07 2020 at 18:12):

functor.map_map then?

#### Patrick Massot (Jul 07 2020 at 18:14):

Anyone against taking the opportunity to rename filter.comap_comap_comp to filter.comap_comap for consistency?

#### Patrick Massot (Jul 07 2020 at 18:15):

And while Simon is here: any idea why the mono attribute doesn't like filter.map_mono and filter.comap_mono?

#### Patrick Massot (Jul 07 2020 at 18:18):

Note that

lemma comap_mono' {α β : Type*} {m : α → β} : ∀ {f g : filter β}, f ≤ g → comap m f ≤ comap m g :=
comap_mono

attribute [mono] comap_mono'


works.

#### Simon Hudon (Jul 07 2020 at 18:34):

Can you show me comap_mono?

#### Simon Hudon (Jul 07 2020 at 18:35):

Also the error message

#### Patrick Massot (Jul 07 2020 at 19:04):

comap_mono : ∀ {α : Type u_1} {β : Type u_2} {m : α → β}, monotone (comap m)

#### Patrick Massot (Jul 07 2020 at 19:05):

The error message is "failed".

#### Simon Hudon (Jul 07 2020 at 19:05):

I think it's just that it doesn't unfold monotone

#### Simon Hudon (Jul 07 2020 at 19:05):

That's pretty clear isn't it? Why do you need my help? :P

#### Simon Hudon (Jul 07 2020 at 19:08):

I think the reason for not unfolding definitions, is that subset is defined as a forall that mono would mistake for introducing relevant assumptions if we unfolded it. I just decided not to unfold anything. I could unfold specifically monotone. I wonder if there's a less intertwined mechanism that would work as well

#### Patrick Massot (Jul 07 2020 at 19:16):

Having a special case for monotone seems fair for a monotonicity tactic.

#### Simon Hudon (Jul 07 2020 at 19:21):

What I worry about is that there could be ways to have a different formulation (e.g. more adapted to category theory or more general) of monotone and we'd have to list all the variations in the tactic. Alternatively, we can just tag all the definitions with an attribute

#### Patrick Massot (Jul 07 2020 at 19:21):

Simon, do you actually want functor.map_map to be protected?

#### Simon Hudon (Jul 07 2020 at 19:25):

I'm not sure. Do you ever use it with filter.map_map?

#### Patrick Massot (Jul 07 2020 at 19:29):

I never use it, period.

#### Simon Hudon (Jul 07 2020 at 19:30):

I don't think it needs to be protected

#### Patrick Massot (Jul 07 2020 at 19:31):

About mono, I'd like to have something simple that unfold monotone and nothing else. Category people can complain later.

#### Simon Hudon (Jul 07 2020 at 19:35):

I can see you're not the one they come after with their sharp arrows

#### Simon Hudon (Jul 07 2020 at 19:36):

But seriously, what file is it defined in and does that file import fancy tactics?

order/basic

#### Patrick Massot (Jul 07 2020 at 19:39):

which import only data.set.basic

#### Simon Hudon (Jul 07 2020 at 19:42):

Cool, so that can be made to work. And it can be left as an exercise to the reader

gr.pdf

#### Patrick Massot (Jul 07 2020 at 19:43):

That's  leanproject import-graph --to order.basic gr.pdf

#### Simon Hudon (Jul 07 2020 at 19:45):

That is really a cool idea! I've never used it

#### Patrick Massot (Jul 07 2020 at 20:21):

Simon Hudon said:

Cool, so that can be made to work. And it can be left as an exercise to the reader

If this is serious then I'll need hints. For instance a docstring on each def of https://github.com/leanprover-community/mathlib/blob/master/src/tactic/monotonicity/basic.lean

#### Simon Hudon (Jul 07 2020 at 20:29):

Ok first step, I believe this is where the error message comes from:

https://github.com/leanprover-community/mathlib/blob/master/src/tactic/monotonicity/basic.lean#L84

Let's make a more helpful message

#### Simon Hudon (Jul 07 2020 at 20:31):

I think you could write fail!"Cannot find relation in {h}"

#### Simon Hudon (Jul 07 2020 at 20:35):

What you care about is mostly monotonicity.attr and monotonicity.check. monotonicity.check finds a relation in the type of the lemma and constructs a key to look it up in an index. That's where I would unfold monotone. Another reasonable approach would be to use an application of monotone as a way of determining what is the monotonic function and the relation it preserves

#### Patrick Massot (Jul 07 2020 at 20:40):

I'm struggling to minimize the map_mono issue

#### Patrick Massot (Jul 07 2020 at 20:40):

I get a different error message.

#### Patrick Massot (Jul 07 2020 at 20:41):

import order.basic
import tactic.monotonicity

@[mono]
lemma test {α : Type*} [preorder α] : ∀ x y : α, x ≤ y → id x ≤ id y :=
λ x y h, h

@[mono]
lemma test' {α : Type*} [preorder α] : monotone (id : α → α) :=
λ x y h, h


The first lemma works fine, the second one says:

oh? Pi {α : Type.{?_mlocal._fresh.1264.227}} [_inst_1 : preorder.{?_mlocal._fresh.1264.227} α], (monotone.{?_mlocal._fresh.1264.227 ?_mlocal._fresh.1264.227} α α _inst_1 _inst_1 (id.{succ ?_mlocal._fresh.1264.227} α))


#### Simon Hudon (Jul 07 2020 at 20:44):

before line 100, trace xs and h

Nothing

wait

#### Patrick Massot (Jul 07 2020 at 20:46):

I didn't have my cursor right

#### Patrick Massot (Jul 07 2020 at 20:46):

It says ([α, _inst_1], monotone id) twice

I see

#### Simon Hudon (Jul 07 2020 at 20:50):

mono_head_candidates 3 xs.reverse h is considering the head of the type (after all the -> and Pi) and at most three variables (in case we're considering the monotonicity of implication)

#### Simon Hudon (Jul 07 2020 at 20:52):

But monotone is not a relation. So before calling mono_head_candidates, you should use dsimp to unfold monotone on the type of the lemma

#### Patrick Massot (Jul 07 2020 at 20:54):

dsimp at what? lm_n?

#### Simon Hudon (Jul 07 2020 at 20:54):

you can call it as lm_t <- expr.dsimp lm_t { fail_if_unchanged := ff } tt [] [simp_arg_type.expr (monotone)],

(editted)

#### Patrick Massot (Jul 07 2020 at 20:57):

That seems to work!

#### Patrick Massot (Jul 07 2020 at 20:58):

I mean for the identity is monotone lemma.

#### Simon Hudon (Jul 07 2020 at 20:58):

And with the one that does not mention monotone, that works as well?

#### Patrick Massot (Jul 07 2020 at 21:01):

Yes, but it doesn't work with filters :sad: It accepts to add the attribute but doesn't use the lemma.

#### Patrick Massot (Jul 07 2020 at 21:02):

The trace for that lemma is ([α, β, m, a, b, a], filter.map m a ≤ filter.map m b)

Ok

#### Simon Hudon (Jul 07 2020 at 21:04):

Go to line 147. This is where we query the monotonicity cache.

#### Simon Hudon (Jul 07 2020 at 21:04):

The function is called get_monotonicity_lemmas

yes, I see it

#### Simon Hudon (Jul 07 2020 at 21:05):

A little lower, we search it and assign to ns a list of candidates. Print it

#### Simon Hudon (Jul 07 2020 at 21:06):

We're going to make sure that the lemma makes it to the list of candidates. After, we're going to see how it gets removed (if it does)

It's in the list

#### Patrick Massot (Jul 07 2020 at 21:06):

but no good match

#### Simon Hudon (Jul 07 2020 at 21:06):

What about the contents of ns'?

#### Patrick Massot (Jul 07 2020 at 21:07):

same list with only one element

#### Simon Hudon (Jul 07 2020 at 21:09):

In a different file https://github.com/leanprover-community/mathlib/blob/master/src/tactic/monotonicity/interactive.lean#L470 we have mono_aux that does more filtering and then makes several attempts at applying candidates

#### Simon Hudon (Jul 07 2020 at 21:13):

First, print rs

#### Simon Hudon (Jul 07 2020 at 21:14):

Time to make some tea

#### Patrick Massot (Jul 07 2020 at 21:14):

It's in ns but not rs

#### Simon Hudon (Jul 07 2020 at 21:18):

Ok so it probably happens in find_lemma

#### Simon Hudon (Jul 07 2020 at 21:19):

And looking at find_lemma, match_rule and match_rule_head are probably relevant

#### Patrick Massot (Jul 07 2020 at 21:19):

Yes, this I was able to tell

#### Simon Hudon (Jul 07 2020 at 21:20):

What I would try is put the same dsimp line here: https://github.com/leanprover-community/mathlib/blob/master/src/tactic/monotonicity/interactive.lean#L355

#### Patrick Massot (Jul 07 2020 at 21:20):

And clearly whatever unfolding was done when putting the attribute is now lost

#### Simon Hudon (Jul 07 2020 at 21:20):

Exactly because only the name of the lemma is put in the cache

Yes

#### Patrick Massot (Jul 07 2020 at 21:50):

https://github.com/leanprover-community/mathlib/pull/3310

#### Patrick Massot (Jul 08 2020 at 20:50):

@Simon Hudon Could you review the above PR? I think Scott, Rob and I sufficiently messed up with your work to ensure you can go from author to reviewer.

#### Simon Hudon (Jul 08 2020 at 20:55):

I approve. Should I post bors r+ to get it merged?

#### Rob Lewis (Jul 08 2020 at 20:56):

This is the only actual change, right? The rest is tracing or removing unused arguments. I think it should be uncontroversial!

#### Patrick Massot (Jul 08 2020 at 20:56):

Simon, do you understand how we ended up with all those unused argument?

#### Simon Hudon (Jul 08 2020 at 20:57):

I think I did some refactoring lazily and didn't bother making sure that the arguments were needed

#### Simon Hudon (Jul 08 2020 at 20:57):

Btw, what's the difference between bors r+ and bors r-?

#### Patrick Massot (Jul 08 2020 at 20:57):

I think they are opposite moves.

Last updated: May 13 2021 at 04:21 UTC