Zulip Chat Archive

Stream: general

Topic: linter for `fact`

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?

Mario Carneiro (Jul 25 2020 at 06:35):

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

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?

Mario Carneiro (Jul 25 2020 at 06:49):

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

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.

Jalex Stark (Jul 25 2020 at 07:16):

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

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.

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

Mario Carneiro (Jul 25 2020 at 08:33):

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

Sebastien Gouezel (Jul 25 2020 at 13:42):

Like in #3549?

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

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?

Mario Carneiro (Jul 25 2020 at 16:57):

sure, that sounds easy enough

Last updated: Dec 20 2023 at 11:08 UTC