map_map

Stream: general

[Patrick Massot]

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]

How about is_lawful_functor?

[Patrick Massot]

I don't understand your question

[Kevin Buzzard]

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

[Patrick Massot]

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

[Scott Morrison]

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]

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]

@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.

[Simon Hudon]

I'm all for :+1:

[Patrick Massot]

functor.map_map then?

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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]

Can you show me comap_mono?

[Simon Hudon]

Also the error message

[Patrick Massot]

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

[Patrick Massot]

The error message is "failed".

[Simon Hudon]

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

[Simon Hudon]

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

[Simon Hudon]

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]

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

[Simon Hudon]

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]

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

[Simon Hudon]

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

[Patrick Massot]

I never use it, period.

[Simon Hudon]

I don't think it needs to be protected

[Patrick Massot]

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

[Simon Hudon]

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

[Simon Hudon]

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

[Patrick Massot]

order/basic

[Patrick Massot]

which import only data.set.basic

[Simon Hudon]

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

[Patrick Massot]

gr.pdf

[Patrick Massot]

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

[Simon Hudon]

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

[Patrick Massot]

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]

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]

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

[Simon Hudon]

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]

I'm struggling to minimize the map_mono issue

[Patrick Massot]

I get a different error message.

[Patrick Massot]

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]

before line 100, trace xs and h

[Patrick Massot]

Nothing

[Patrick Massot]

wait

[Patrick Massot]

I didn't have my cursor right

[Patrick Massot]

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

[Simon Hudon]

I see

[Simon Hudon]

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]

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]

dsimp at what? lm_n?

[Simon Hudon]

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

(editted)

[Patrick Massot]

That seems to work!

[Patrick Massot]

I mean for the identity is monotone lemma.

[Simon Hudon]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Simon Hudon]

Ok

[Simon Hudon]

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

[Simon Hudon]

The function is called get_monotonicity_lemmas

[Patrick Massot]

yes, I see it

[Simon Hudon]

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

[Simon Hudon]

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)

[Patrick Massot]

It's in the list

[Patrick Massot]

but no good match

[Simon Hudon]

What about the contents of ns'?

[Patrick Massot]

same list with only one element

[Simon Hudon]

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]

First, print rs

[Patrick Massot]

It's thinking about it

[Simon Hudon]

Time to make some tea

[Patrick Massot]

It's in ns but not rs

[Simon Hudon]

Ok so it probably happens in find_lemma

[Simon Hudon]

And looking at find_lemma, match_rule and match_rule_head are probably relevant

[Patrick Massot]

Yes, this I was able to tell

[Simon Hudon]

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]

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

[Simon Hudon]

with a small adjustment

[Simon Hudon]

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

[Patrick Massot]

Yes

[Patrick Massot]

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

[Patrick Massot]

@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]

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

[Patrick Massot]

Yes, please.

[Rob Lewis]

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

[Patrick Massot]

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

[Patrick Massot]

Rob, you missed https://github.com/leanprover-community/mathlib/pull/3310/files#diff-54c5eab6d816f396b485233519d628acR356

[Simon Hudon]

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

[Simon Hudon]

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

[Patrick Massot]

I think they are opposite moves.