Zulip Chat Archive

Stream: general

Topic: map_map


view this post on Zulip 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.

view this post on Zulip Simon Hudon (Apr 07 2019 at 16:08):

How about is_lawful_functor?

view this post on Zulip Patrick Massot (Apr 07 2019 at 16:11):

I don't understand your question

view this post on Zulip Kevin Buzzard (Apr 07 2019 at 16:14):

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

view this post on Zulip Patrick Massot (Apr 07 2019 at 16:15):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Jul 07 2020 at 18:11):

I'm all for :+1:

view this post on Zulip Patrick Massot (Jul 07 2020 at 18:12):

functor.map_map then?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Jul 07 2020 at 18:34):

Can you show me comap_mono?

view this post on Zulip Simon Hudon (Jul 07 2020 at 18:35):

Also the error message

view this post on Zulip Patrick Massot (Jul 07 2020 at 19:04):

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

view this post on Zulip Patrick Massot (Jul 07 2020 at 19:05):

The error message is "failed".

view this post on Zulip Simon Hudon (Jul 07 2020 at 19:05):

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

view this post on Zulip Simon Hudon (Jul 07 2020 at 19:05):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 07 2020 at 19:16):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 07 2020 at 19:21):

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

view this post on Zulip Simon Hudon (Jul 07 2020 at 19:25):

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

view this post on Zulip Patrick Massot (Jul 07 2020 at 19:29):

I never use it, period.

view this post on Zulip Simon Hudon (Jul 07 2020 at 19:30):

I don't think it needs to be protected

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Jul 07 2020 at 19:35):

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

view this post on Zulip Simon Hudon (Jul 07 2020 at 19:36):

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

view this post on Zulip Patrick Massot (Jul 07 2020 at 19:37):

order/basic

view this post on Zulip Patrick Massot (Jul 07 2020 at 19:39):

which import only data.set.basic

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 07 2020 at 19:42):

gr.pdf

view this post on Zulip Patrick Massot (Jul 07 2020 at 19:43):

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

view this post on Zulip Simon Hudon (Jul 07 2020 at 19:45):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Simon Hudon (Jul 07 2020 at 20:31):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 07 2020 at 20:40):

I'm struggling to minimize the map_mono issue

view this post on Zulip Patrick Massot (Jul 07 2020 at 20:40):

I get a different error message.

view this post on Zulip 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} α))

view this post on Zulip Simon Hudon (Jul 07 2020 at 20:44):

before line 100, trace xs and h

view this post on Zulip Patrick Massot (Jul 07 2020 at 20:45):

Nothing

view this post on Zulip Patrick Massot (Jul 07 2020 at 20:45):

wait

view this post on Zulip Patrick Massot (Jul 07 2020 at 20:46):

I didn't have my cursor right

view this post on Zulip Patrick Massot (Jul 07 2020 at 20:46):

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

view this post on Zulip Simon Hudon (Jul 07 2020 at 20:49):

I see

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 07 2020 at 20:54):

dsimp at what? lm_n?

view this post on Zulip 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)

view this post on Zulip Patrick Massot (Jul 07 2020 at 20:57):

That seems to work!

view this post on Zulip Patrick Massot (Jul 07 2020 at 20:58):

I mean for the identity is monotone lemma.

view this post on Zulip Simon Hudon (Jul 07 2020 at 20:58):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Simon Hudon (Jul 07 2020 at 21:03):

Ok

view this post on Zulip Simon Hudon (Jul 07 2020 at 21:04):

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

view this post on Zulip Simon Hudon (Jul 07 2020 at 21:04):

The function is called get_monotonicity_lemmas

view this post on Zulip Patrick Massot (Jul 07 2020 at 21:04):

yes, I see it

view this post on Zulip Simon Hudon (Jul 07 2020 at 21:05):

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

view this post on Zulip 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)

view this post on Zulip Patrick Massot (Jul 07 2020 at 21:06):

It's in the list

view this post on Zulip Patrick Massot (Jul 07 2020 at 21:06):

but no good match

view this post on Zulip Simon Hudon (Jul 07 2020 at 21:06):

What about the contents of ns'?

view this post on Zulip Patrick Massot (Jul 07 2020 at 21:07):

same list with only one element

view this post on Zulip 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

view this post on Zulip Simon Hudon (Jul 07 2020 at 21:13):

First, print rs

view this post on Zulip Patrick Massot (Jul 07 2020 at 21:14):

It's thinking about it

view this post on Zulip Simon Hudon (Jul 07 2020 at 21:14):

Time to make some tea

view this post on Zulip Patrick Massot (Jul 07 2020 at 21:14):

It's in ns but not rs

view this post on Zulip Simon Hudon (Jul 07 2020 at 21:18):

Ok so it probably happens in find_lemma

view this post on Zulip Simon Hudon (Jul 07 2020 at 21:19):

And looking at find_lemma, match_rule and match_rule_head are probably relevant

view this post on Zulip Patrick Massot (Jul 07 2020 at 21:19):

Yes, this I was able to tell

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 07 2020 at 21:20):

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

view this post on Zulip Simon Hudon (Jul 07 2020 at 21:20):

with a small adjustment

view this post on Zulip Simon Hudon (Jul 07 2020 at 21:20):

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

view this post on Zulip Patrick Massot (Jul 07 2020 at 21:20):

Yes

view this post on Zulip Patrick Massot (Jul 07 2020 at 21:50):

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

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Jul 08 2020 at 20:55):

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

view this post on Zulip Patrick Massot (Jul 08 2020 at 20:56):

Yes, please.

view this post on Zulip 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!

view this post on Zulip Patrick Massot (Jul 08 2020 at 20:56):

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

view this post on Zulip Patrick Massot (Jul 08 2020 at 20:56):

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

view this post on Zulip 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

view this post on Zulip Simon Hudon (Jul 08 2020 at 20:57):

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

view this post on Zulip Patrick Massot (Jul 08 2020 at 20:57):

I think they are opposite moves.


Last updated: May 13 2021 at 04:21 UTC