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.

[Filippo A. E. Nuccio]

I cannot understand the behaviour of Fact here:

import Mathlib

noncomputable section

attribute [ -instance ] instInhabitedNat

def EvenInhab (a : ℕ) [Fact (Even a)] :
  Inhabited ℕ := ⟨(@Even.two_dvd ℕ _ a Fact.out).choose⟩

variable (a : ℕ) (haEv : Even a)
variable (b : ℕ) [Fact (Even b)]

local instance : Inhabited ℕ := @EvenInhab a ⟨haEv⟩ -- it works
local instance : Inhabited ℕ := EvenInhab b -- if fails, saying cannot find synthesization order for instance...

When I compare it to docs#ZMod.instFieldZMod it seems to me that leaving [Fact (Even b)] in the variables should work.

[Eric Wieser]

The difference with ZMod is that there the conclusion is parameterized by b

[Eric Wieser]

Here it is just ℕ, so Lean cannot guess b

[Filippo A. E. Nuccio]

Ah sure, it makes sense.

[Filippo A. E. Nuccio]

Yet I do not understand why the example with a works and that with b does not. I would argue as follows: in both cases, when lean looks for a default, it looks for a Inhabited instance that is activated locally, meaning that locally we have a term of the right type... and it seems to me that @EvenInhab a <haEv> and EvenInhab b are both terms of the right type. What am I missing?

[Floris van Doorn]

The error is just because you mark these declarations as instances. This works:

def h1 : Inhabited ℕ := @EvenInhab a ⟨haEv⟩ -- it works
def h2 : Inhabited ℕ := EvenInhab b -- also works

[Floris van Doorn]

The problem is with making the second declaration an instance is that it has type
instance [inst : Fact (Even b)] : Inhabited ℕ
But Lean complains that it doesn't know what b is when doing type-class inference, and it refused to search for Fact (Even _).

[Filippo A. E. Nuccio]

And why is it happy with the first being an instance? Because it does not "search" for "haEv" but it finds it straight away?

[Floris van Doorn]

I think that the first instance will never fire during type-class inference, but that Lean is not checking that part.

[Floris van Doorn]

That is a check that could (and should) be added to Lean core or a linter

[Filippo A. E. Nuccio]

Ah indeed, if I try

example : Inhabited ℕ := by infer_instance

after the one without the error, it cannot find anything.

[Filippo A. E. Nuccio]

And is there a way to declare an instance locally in the sense that I want, in a certain section, to "fix an even natural a and to use EvenInhab a as default term" thus accessing all results that begin with (X : Type) [Inhabited X]? (apart of course calling them with @)

[Riccardo Brasca]

def foo : Inhabited ℕ := ...

local attribute [instance ] foo

should do the trick

[Filippo A. E. Nuccio]

No, same problem as with @Floris van Doorn example.

[Filippo A. E. Nuccio]

def foo : Inhabited ℕ := @EvenInhab a ⟨haEv⟩ -- it works

attribute [local instance] foo

example : Inhabited ℕ := by infer_instance -- failed to synthetize

[Filippo A. E. Nuccio]

(I guess you suggested attribute [local instance] rather that local attribute [instance], no?)

[Filippo A. E. Nuccio]

This was indeed my first trial, who drove me through this rabbit hole.

[Riccardo Brasca]

Yes, sorry.

[Riccardo Brasca]

Ah, I have misunderstood your question.

[Riccardo Brasca]

Then I don't get your point, what should be the fixed element of N?

[Filippo A. E. Nuccio]

Well, I would like that it is a/2 in a section where I have fixed an even a.

[Filippo A. E. Nuccio]

It seems to me that this would be doable if the type depended on a, but not with a type independent of a like N.

[Floris van Doorn]

I don't know what you want this for, but I think it's not easy.
Depending on your use case (probably teaching?), maybe the following is close enough?

axiom a : ℕ
axiom haEv : Even a

instance : Inhabited ℕ := @EvenInhab a ⟨haEv⟩
instance : Inhabited ℕ := by infer_instance  -- works

[Filippo A. E. Nuccio]

Floris van Doorn said:

I don't know what you want this for, but I think it's not easy.
Depending on your use case (probably teaching?), maybe the following is close enough?

axiom a : ℕ
axiom haEv : Even a

instance : Inhabited ℕ := @EvenInhab a ⟨haEv⟩
instance : Inhabited ℕ := by infer_instance  -- works

Yes, I wanted to prepare a class about class instances and got stuck :smile: Thanks for the catch with axiom!

[Filippo A. E. Nuccio]

I do not know if it is a good thing to present, but at least I learnt a lot.

[Riccardo Brasca]

Ah, nice idea! axiom mimics parameter of Lean 3!

[Riccardo Brasca]

Anyway the problem is that typeclass inference looks for classes, and it never has a way to guess the a you want

[Filippo A. E. Nuccio]

Just to finish on this, this seems to work:

variable (a : ℕ) (ha₀ : 0 < a) (haEv : Even a)
variable (b : ℕ) [hb : Fact (0 < b)] [Fact (Even b)]

def bar_a : Inhabited (Fin a) :=
  ⟨(@Even.two_dvd ℕ _ a haEv).choose, by linarith [(@Even.two_dvd ℕ _ a haEv).choose_spec]⟩

def bar_b : Inhabited (Fin b) :=
  ⟨(@Even.two_dvd ℕ _ b Fact.out).choose, by linarith [(@Even.two_dvd ℕ _ b Fact.out).choose_spec,
    hb.out]⟩

attribute [local instance] bar_a
example : Inhabited (Fin a) := by infer_instance -- fails

attribute [local instance] bar_b
example : Inhabited (Fin b) := by infer_instance --succeeds

[Filippo A. E. Nuccio]

But as @Floris van Doorn pointed out, the fact that class inference does not fire for Fin a is not catched by a linter at the time of defining the local instance bar_a, and that might be useful.