fact

Stream: general

[Jeremy Avigad]

I just learned that fact doesn't mean factorial in Lean, and if nat is open, #check fact is ambiguous. Doesn't that seem unfortunate?

[Simon Hudon]

It's a new design in mathlib. It's actually not a shorthand for anything but it helps us have propositions as type classes. We could put it in its own namespace to minimize this kind of surprise

[Johan Commelin]

I agree that it is a bit unfortunate. @Jeremy Avigad I usually write n.fact to get around this, and it also reads nice. Even better would be to add

localized "postfix `!` := nat.fact" in nat

To the data/nat/fact file. (Modulo trivial typos). Then we can simply write n! after open_locale nat.

[Reid Barton]

We could also rename nat.fact to nat.factorial

[Johan Commelin]

I think we should do all of those (-;

[Kevin Buzzard]

I'm fine with factorial, it's unambiguous. Mathematicians have this great notation ! for it though :-) How about getting that working then nobody needs to worry about the name :-)

[Chris Hughes]

The lemmas still use the name.

[Patrick Massot]

I think it makes sense that fact is the abbreviation of the word fact instead of the abbreviation of the word factorial.

[Gabriel Ebner]

There are other reasonable synonyms for fact: given or assuming come to mind quickly. But there aren't that many other names for factorial, and n.factorial is quite a bit longer than n.fact. Though the postfix notation also looks nice.

[Mario Carneiro]

In fact, fact is one of those "filler" words that conveys little meaning here. Why not something like to_typeclass that says something more informative?

[Scott Morrison]

[witness P]?

[Reid Barton]

What's the story with global instances of fact? I was under the vague impression that there weren't supposed to be any, but some do exist.

[Ruben Van de Velde]

My understanding was "don't make too many", rather than "don't many any at all"

[Floris van Doorn]

I prefer to only have local(ized) instances, but I'm also fine with the looser "don't have many"

[Scott Morrison]

I feel like this is something we could easily regret later. I'd vote for "none, unless they come with a detailed doc-string explaining exactly why local attribute [instance] won't cut it".

[Scott Morrison]

Ideally enforced by the linter! :-)

[Ashwin Iyengar]

Hi! I'm wondering why this lemma doesn't see hp and fails to synthesize a type class instance of fact p.prime.

import algebra.field
import algebra.char_p

variables (p : ℕ) (F : Type*) (hp : fact p.prime) [field F] [char_p F p]

lemma test : (frobenius F p) = sorry :=
sorry

[Ashwin Iyengar]

Oh nevermind this seems to work.

import algebra.field
import algebra.char_p

variables (p : ℕ) (F : Type*) [fact p.prime] [field F] [char_p F p]

lemma test : (frobenius F p) = sorry :=
sorry

Why is it that naming the fact hp suddenly makes it fail?

[Kevin Buzzard]

If you name an instance then it doesn't get included automatically in the local context unless the name is mentioned in the statement of the lemma. You can see just clicking before the final sorry that the instance is not present in the first situation and is there in the second.

[Eric Rodriguez]

(also, in your first example you didn't even have it in instance brackets!)

[Kyle Miller]

The first one also is using parentheses instead of square brackets, which is another reason it fails. I keep rediscovering and forgetting the rule Kevin's mentioned, that even if it were [hp : fact p.prime] it wouldn't be included.

[Ashwin Iyengar]

thanks all! that makes sense.

[Kevin Buzzard]

One thing that clarified this stuff for me is that Lean doesn't really care much about what kind of brackets you use before the colon when elaborating:

import algebra.char_p

-- works even though we use round brackets
lemma test (p : ℕ) (F : Type*) (h0 : fact p.prime) (hF : field F) (hp : char_p F p) :
  (frobenius F p) = sorry :=
sorry

/-
frobenius : Π (R : Type u) [_inst_1 : comm_semiring R] (p : ℕ)
[_inst_3 : fact (nat.prime p)] [_inst_4 : char_p R p], R →+* R
-/

My mental model a while ago was that this would fail because type class inference won't find comm_semiring F or fact p.prime -- but it finds them just fine. With a revised mental model it's easy to understand the labelling thing: I wouldn't expect variable (Y : Type) to be included in a lemma statement if it didn't mention Y, so similarly I wouldn't expect variable [hp : fact p.prime] to be included in a statement if it doesn't mention hp.