Zulip Chat Archive

Stream: general

Topic: mono in data.set.lattice


Patrick Massot (Jun 12 2020 at 09:51):

Is there any objection to have import tactic.monotonicity at top of data.set.lattice? I'm asking because this is a fairly foundational file.

Patrick Massot (Jun 12 2020 at 09:52):

The monotonicity tactics are currently very under-employed in mathlib, but many lemmas from that file could be tagged. Like norm_cast, these tactics become useful only if lemmas are tagged appropriately.

Rob Lewis (Jun 12 2020 at 09:54):

tactic.monotonicity doesn't look so foundational itself. Does this import even work?

Rob Lewis (Jun 12 2020 at 09:54):

You can always tag the lemmas in tactic.monotonicity instead of at the moment of definition.

Patrick Massot (Jun 12 2020 at 09:54):

Yes, that's why I ask, and yes it works.

Rob Lewis (Jun 12 2020 at 09:57):

Without looking at an import graph it's hard to judge the cost here. Do we have a quick way to generate one of those yet?

Patrick Massot (Jun 12 2020 at 10:02):

Sure.

Patrick Massot (Jun 12 2020 at 10:02):

Which part do you want to see?

Patrick Massot (Jun 12 2020 at 10:02):

Everything below tactic.monotonicity?

Patrick Massot (Jun 12 2020 at 10:07):

Actually I was wrong, it's not easy. It seems that the recent fix that allows to use open_locale right after imports was not propagated to lean --deps, so import graph generation is currently broken @Gabriel Ebner

$ lean --deps src/algebra/pi_instances.lean
/tmp/mathlib/src/algebra/module.olean
/tmp/mathlib/src/ring_theory/subring.olean
/tmp/mathlib/src/ring_theory/prod.olean
error: file 'open_locale' not found in the LEAN_PATH
error: file 'big_operators' not found in the LEAN_PATH
/home/pmassot/.elan/toolchains/leanprover-community-lean-3.16.1/lib/lean/library/init/default.olean

Gabriel Ebner (Jun 12 2020 at 10:17):

Oops, lean#323.


Last updated: Dec 20 2023 at 11:08 UTC