Stream: new members

Topic: Fighting type class inference

Marc Masdeu (Sep 04 2020 at 14:23):

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 (Sep 04 2020 at 14:29):

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 (Sep 04 2020 at 14:31):

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

Marc Masdeu (Sep 04 2020 at 14:33):

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 (Sep 04 2020 at 14:36):

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 (Sep 04 2020 at 16:11):

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 (Sep 04 2020 at 16:13):

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

Reid Barton (Sep 04 2020 at 16:14):

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 (Sep 04 2020 at 16:17):

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 (Sep 04 2020 at 16:19):

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 (Sep 04 2020 at 16:28):

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 (Sep 04 2020 at 16:35):

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 (Sep 04 2020 at 19:01):

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 (Sep 04 2020 at 23:39):

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

Mario Carneiro (Sep 04 2020 at 23:39):

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

Marc Masdeu (Sep 05 2020 at 21:10):

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 (Sep 05 2020 at 21:16):

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

Marc Masdeu (Sep 05 2020 at 21:20):

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

Mario Carneiro (Sep 05 2020 at 21:21):

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

Last updated: May 16 2021 at 05:21 UTC