Fighting type class inference

Stream: new members

[Marc Masdeu]

Hi,

I understand that the point of declaring variables is to make them implicit in lemmas and theorems that will use them. I would assume that some of the hypotheses would be made using the square brackets notation, to be used when needed (?). So here is my M(N)WE:

import tactic

variables {n : ℕ} [0 < n]

lemma my_lemma : 0 < n^2+3*n:=
begin
    nlinarith,
end

lemma my_lemma_2: 0 < n^2 + 3*n :=
begin
    exact my_lemma, -- Lean complains
end

I would like my_lemma_2 to use my_lemma, and of course my_lemma needs n to be positive to work (which is assumed). What would be the clean way to state this? Or these kind of assumptions should not be put into the inference system? In my real example, I have assumptions like [nat.prime p] that get used in most of the lemmas...

Thank you!

[Anne Baanen]

The typeclass system isn't really set up to handle these kinds of assumptions, but there is a trick to make it work: fact : Prop -> Prop is a typeclass set up to do exactly this. So this should work:

import tactic

variables {n : ℕ} [fact (0 < n)]

lemma my_lemma : 0 < n^2+3*n:=
begin
    nlinarith, -- Fails for me, but I'm on an older version of mathlib right now.
end

lemma my_lemma_2: 0 < n^2 + 3*n :=
begin
    exact my_lemma
end

[Marc Masdeu]

Oh thanks! At some point I was told to avoid using facts...

[Marc Masdeu]

The way that does work is this one:

import tactic

variables {n : ℕ} [fact(0 < n)]

lemma my_lemma : 0 < n^2+3*n:=
begin
    have h : 0 < n, by assumption, -- removing this line makes it fail
    nlinarith,
end

lemma my_lemma_2: 0 < n^2 + 3*n :=
begin
    exact my_lemma,
end

[Anne Baanen]

The problem with fact is it doesn't scale very well: using fact like here to thread a single assumption about "the same" variable n in one section will work fine, but using those lemmas outside that file is annoying because you need to do @expansion or use haveI : fact (0 < n) := _. And as soon as you start making instances along the lines of fact (0 < a) -> fact (0 < b) -> fact (0 < a + b), the typeclass search time becomes unbearable.

[Marc Masdeu]

Oh! That problem is what I also was encountering, I was annoyed at having to do @-expansion, it looks terrible in the code.

[Marc Masdeu]

If I understand correctly, you suggest that I remove the assumption and just make it explicit at every lemma that requires it?

[Reid Barton]

variables makes variables implicit in the statements of lemmas and theorems, but not where the lemmas are used.
The "plain" way to write things like this would be:

import tactic

variables {n : ℕ} (h : 0 < n)
include h   -- this line is needed because otherwise Lean doesn't know that `my_lemma` uses `h`

lemma my_lemma : 0 < n^2+3*n:=
begin
    nlinarith,
end

lemma my_lemma_2: 0 < n^2 + 3*n :=
begin
    exact my_lemma h,
end

[Marc Masdeu]

Thanks @Anne Baanen and @Reid Barton . And the result of the above code (when using it in other files, for example) would be exactly the same as if I had put what goes after variables in each of the two statements of the lemmas? I do hope so...

[Reid Barton]

Yes. In the general case, there are some mildly complicated rules determining which variables get inserted into which lemmas, but the approximate version is "as needed, or as directed by include".

[Marc Masdeu]

Just a final confirmation (I am cleaning a bunch of code following this advice). If I am writing a file that I want to use later, would this be the correct way of writing this lemma? I am interested in the n_pos hypothesis, and note that I use zmod.val_lt that uses class inference to find the fact(0<n) thing. At the same time, another theorem that I am using has it as explicit hypothesis (mul_lt_iff_lt_one_right).

variables {n : ℕ}
lemma zero_iff_n_divides [n_pos : fact(0 < n)] (x : zmod n) : x = 0 ↔ n  ∣ x.val :=
begin
    split,
    {
        intro h,
        finish,
    },
    {
        intro h,
        cases h with w hw,
        suffices : w = 0, by finish,
        have H : x.val < n := zmod.val_lt x,
        rw hw at H,
        suffices : w < 1, by linarith,
        exact (mul_lt_iff_lt_one_right n_pos).mp H,
    }
end

[Reid Barton]

Well, I think the statement is also true for n = 0, so ideally you wouldn't take the n_pos argument at all

[Marc Masdeu]

You are right. The statement is true, but the proof I have doesn't work as is. Still, supposing that the statement needed n to be positive, this would be the right way to code it, right?

[Mario Carneiro]

You should use haveI to supply the 0 < n proof to zmod.val_lt

[Mario Carneiro]

or @zmod.val_lt ... if that's the only usage of it

[Marc Masdeu]

Mario Carneiro said:

You should use haveI to supply the 0 < n proof to zmod.val_lt

So how come the proof checks without the haveI statement? zmod.val_lt has [fact (0 < n)] in its hypotheses, but the inference system (or whatever it's called) seems to be able to find this with the code I supplied above.

[Mario Carneiro]

I mean you should delete the fact assumption from your theorem and then use haveI

[Marc Masdeu]

If I remove the fact assumption then how am I going to supply the proof to haveI??

[Mario Carneiro]

Either because it is a regular hypothesis, or because you've generated it in the proof by e.g. case analysis as in Reid's suggestion