Zulip Chat Archive

Stream: general

Topic: monotonocity attribute

Patrick Massot (Dec 26 2019 at 19:56):

I don't really know the status of @Simon Hudon 's monotonicity tactic. It is not used much in mathlib, probably mostly because lemmas are not properly tagged @[mono]. But I hesitate to add annotations on the spot because it requires importing tactic.monotonicity.basic which is not listed among "basic" tactics in https://github.com/leanprover-community/mathlib/blob/master/src/tactic/basic.lean. For instance, set.prod_mono is not tagged, and belongs to a very low-level file data.set.basic. Should I import tactic.monotonicity there? Or should I add a line attribute [mono] set.prod_mono to https://github.com/leanprover-community/mathlib/blob/master/src/tactic/monotonicity/lemmas.lean?

Patrick Massot (Dec 26 2019 at 19:57):

By the way, I suspect https://github.com/leanprover-community/mathlib/blob/master/src/tactic/monotonicity/basic.lean should be searched for lemmas to move to tactic/core.lean.

Simon Hudon (Dec 26 2019 at 21:33):

By the way, I suspect https://github.com/leanprover-community/mathlib/blob/master/src/tactic/monotonicity/basic.lean should be searched for lemmas to move to tactic/core.lean.

I don't understand that sentence

Simon Hudon (Dec 26 2019 at 21:33):

But I think we should add monotonicity.basic in tactic.core

Patrick Massot (Dec 26 2019 at 21:34):

That sentence means lots of functions in that file look like they could be useful for other tactics, hence could move to https://github.com/leanprover-community/mathlib/blob/master/src/tactic/core.lean

Simon Hudon (Dec 26 2019 at 21:35):

Ah! Thanks!

Simon Hudon (Dec 26 2019 at 21:35):

Yes, I could move a bunch of that stuff

Patrick Massot (Dec 26 2019 at 21:35):

You mean "add monotonicity.basic in tactic.basic"?

Simon Hudon (Dec 26 2019 at 21:35):

Yes, that's what I meant, thank you

Simon Hudon (Dec 26 2019 at 21:38):

Is this a refactoring that you need for your projects?

Patrick Massot (Dec 26 2019 at 21:39):

No, I cheated in https://github.com/leanprover-community/mathlib/pull/1826/files#diff-7f1a53849cc74eb3182011a1cb3fc1a9R31.

Patrick Massot (Dec 26 2019 at 21:41):

But I'll probably try to add monotonicity.basic in tactic.basic and see whether something breaks, unless someone complains here.

Simon Hudon (Dec 26 2019 at 21:49):

That sounds good to me. Please let me know if it gets hairy

Last updated: Dec 20 2023 at 11:08 UTC