Zulip Chat Archive

Stream: general

Topic: linter for `fact`


view this post on Zulip Scott Morrison (Jul 25 2020 at 05:00):

I don't think this is an issue yet, but I noticed @Sebastien Gouezel introduced instance : fact ((0 : ℝ) < 1) := zero_lt_one in https://github.com/leanprover-community/mathlib/pull/3528/files#diff-7133d335dc07594a328658c93fc0e380R373

I suspect that other people will want that fact, perhaps outside the manifolds directories.

Perhaps at some point we should add a linter that checks for duplicated instances?

view this post on Zulip Mario Carneiro (Jul 25 2020 at 06:35):

I don't think there should be any global instances for fact

view this post on Zulip Jalex Stark (Jul 25 2020 at 06:40):

how does this instance get used right now? is it for getting to nonempty Icc (0:\R) 1?

view this post on Zulip Mario Carneiro (Jul 25 2020 at 06:49):

If so, I think that should be an instance of its own

view this post on Zulip Sebastien Gouezel (Jul 25 2020 at 07:14):

No, it is to get a manifold with boundary structure on Icc 0 1, which requires the fact. And this manifold with boundary structure will be used all over the place when we mention smooth homotopies.

view this post on Zulip Jalex Stark (Jul 25 2020 at 07:16):

shouldn't we need this fact only in the definition of the manifold with boundary structure?

view this post on Zulip Johan Commelin (Jul 25 2020 at 07:19):

Mario Carneiro said:

I don't think there should be any global instances for fact

I wouldn't mind having fact (nat.prime 2) as a global instance.

view this post on Zulip Mario Carneiro (Jul 25 2020 at 08:32):

It's not about what would be nice to have, it's about making fact performant. fact is the least efficient of all typeclasses, because it is an unstructured bag of theorems that must be linearly enumerated for any fact typeclass instance. I would prefer that the behavior of fact inference is under control of the user, meaning only local instances and hypotheses are allowed

view this post on Zulip Mario Carneiro (Jul 25 2020 at 08:33):

If you want a manifold with boundary structure on Icc 0 1, make that an instance

view this post on Zulip Sebastien Gouezel (Jul 25 2020 at 13:42):

Like in #3549?

view this post on Zulip Mario Carneiro (Jul 25 2020 at 16:47):

By the way, don't forget that you can use localized for instances too. It seems quite reasonable that things like fact (prime 2) can be put in a locale for a bunch of related files

view this post on Zulip Reid Barton (Jul 25 2020 at 16:51):

Mario Carneiro said:

I don't think there should be any global instances for fact

in this case, how about a linter that checks for instances of fact?

view this post on Zulip Mario Carneiro (Jul 25 2020 at 16:57):

sure, that sounds easy enough


Last updated: May 10 2021 at 19:16 UTC