Rewrite with <- vs symm

Stream: general

[Bolton Bailey]

This is something I encountered a while ago, but I don't think I've posted about it before. Can someone offer an explanation of why the first rewrite works, but the second, which seems like it is applying an equivalent transformation, does not? This arose because I was trying to switch a simp statement that looked like simp only [<-finset.mul_sum] with my_attribute to one where my_mul_sum was included in the attribute in order to make it look a little cleaner.

import algebra.big_operators.ring

open_locale big_operators classical

section

universes u v

parameter {F : Type u}
parameter [field F]

lemma my_mul_sum {α : Type u} {β : Type v} {s : finset α} {b : β} {f : α → β}
  [non_unital_non_assoc_semiring β] :
  ∑ (x : α) in s, b * f x = b * ∑ (x : α) in s, f x := finset.mul_sum.symm

example (n : ℕ) (a : F) (b : fin n -> F) : (∑ (i : fin n) in finset.fin_range n, a * b i) = 0 :=
begin
  -- rw <-finset.mul_sum, -- works fine
  rw my_mul_sum, -- this fails where above succeeds
end

end

[Kyle Miller]

I tried specializing my_mul_sum to see what's going wrong, but I'm confused about this error:

example (n : ℕ) (a : F) (b : fin n -> F) : (∑ (i : fin n) in finset.fin_range n, a * b i) = 0 :=
begin
  have := @my_mul_sum (fin n),
/-
20:12: type mismatch at application
  my_mul_sum
term
  fin n
has type
  Type : Type 1
but is expected to have type
  Type u : Type (u+1)
-/
end

[Kyle Miller]

Oh, the problem is that universes is inside the section. Bring it outside the section, and the rewrite goes through.

[Yaël Dillies]

Elaboration issue?

[Floris van Doorn]

Replace the line universes u v by universe variables u v. That should fix the issue.

I've mentioned a couple times that I think universes should never be used, and always be replaced by universe variables. However, somehow universes has become the de factor standard in mathlib (I think). [EDIT: it seems that as long as you're outside a section it doesn't matter]

The difference between the two is that universes fixes the universes for the section. So the lemma my_mul_sum can only be applied to α living in the (fixed) universe parameter u, not to a type living in any other universe (at least until the end of the section/namespace/file). universe parameter generalizes the universes immediately, so the lemma my_mul_sum is available immediately to any type in any universe desired (which is usually what you want, even though it rarely makes a difference).

[Yaël Dillies]

Oh no, the dreaded universes-section interaction :fear:

[Floris van Doorn]

Oh, if we use universes outside a section does it behave the same as universe variable?

[Yaël Dillies]

I think so, yeah. We do all the time without any trouble as far as I know.

[Yaël Dillies]

Bhavik and I had a funky example with an added layer of complexity using namespace.

[Floris van Doorn]

I thought the "without any trouble" was just because you rarely apply a lemma to a type in a different universe. But I guess it's not that uncommon.

[Yaël Dillies]

Here it is: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/section.2C.20universe.2C.20namespace.20deadly.20interaction/near/241180594

[Yaël Dillies]

I didn't know what you just explained at the time, so you might well be right.

[Riccardo Brasca]

Is there a difference between variable and parameter?

[Yaël Dillies]

Yes.

[Floris van Doorn]

Parameters are "fixed" for the section: you can only apply the lemmas (in that section) to that parameter, not any other value.

[Yaël Dillies]

parameter appends silently the arguments to any call of the defs/lemmas within the same section.

[Mario Carneiro]

Floris van Doorn said:

The difference between the two is that universes fixes the universes for the section.

Oh, I spent a lot of time trying to figure out what the difference was during synport. Even after staring at the code for a while I could only deduce that the distinction is maintained, but it didn't seem to have any visible effects

[Yaël Dillies]

Have a look at docs#zorn.chain for an example.

[Floris van Doorn]

However, the implementation of parameters is leaky, so sometimes this behavior doesn't work as this description says, and therefore parameter should generally not be used

[Riccardo Brasca]

Ah yes, it is even explained in TPL

[Floris van Doorn]

Mario Carneiro said:

Oh, I spent a lot of time trying to figure out what the difference was during synport. Even after staring at the code for a while I could only deduce that the distinction is maintained, but it didn't seem to have any visible effects

Haha, that's fair. It rarely has visible effects.

[Yaël Dillies]

I personally don't like parameter because when I look at the API code I have the assumption that this is how I'm going to use the lemmas. And then I always forget the arguments that were parametrized.

[Yaël Dillies]

I assume language models could get as confused as I am?

[Mario Carneiro]

universe variable / universe parameter was banished years ago, this distinction is entirely a relic of when "fixed universes" were a thing

[Floris van Doorn]

Until a couple minutes ago I thought that universes still had the behavior of universe parameters. My heuristic "don't use universe" is maybe outdated by a couple of years :)

[Mario Carneiro]

I think mathlib uses universe almost exclusively

[Floris van Doorn]

A quick search seems to suggest that it's used about 20x as much as universe variable.

[Mario Carneiro]

I find 33 uses of universe variable[s], 946 uses of universe[s], and 0 for universe parameter[s]

[Mario Carneiro]

and most of the uses of universe variable are from the old files like logic.basic, and some uses in witt vectors and category theory for some reason

[Mario Carneiro]

From a quick glance it looks like they are all at the top level, they aren't doing it to avoid undesired behavior in a section

[Floris van Doorn]

and at least one of which I added, in tests/simps :)

[Mario Carneiro]

#9794

[Anne Baanen]

Do we see any value in keeping the universes/section interaction, does it exist in Lean 4? If not, why don't we update Lean 3 so that universes always means universe variables (unless opted-in with universe parameters)?

[Gabriel Ebner]

We don't need universes at all in Lean 4.

[Reid Barton]

Oh wow, I knew about the universe/section interaction, but I never knew that universe variables meant something different--I thought it was just a verbose way of writing universes, and vaguely wondered why it was allowed or why anyone would write it.

[Johan Commelin]

I've been using universe variables ever since I heard that it was better behaved then universes in some corner cases. I never understood the details, so I just used it everywhere as a cargo cult plaster.

[Reid Barton]

Yaël Dillies said:

I personally don't like parameter because when I look at the API code I have the assumption that this is how I'm going to use the lemmas. And then I always forget the arguments that were parametrized.

parameter is for sections that prove a bunch of lemmas that build up to a main theorem, that could just as well be private (at least that's how I use it). It's an alternative organization strategy to writing single 500-line proofs.

[Johan Commelin]

I've used it in LTE once or twice, and it made the resulting file more readable, instead of less.

[Yury G. Kudryashov]

Do they exist in Lean 4?

[Yury G. Kudryashov]

I use a structure in branch#picard-lindelof

[Kyle Miller]

There's a sort of complicated feature that could be nice for reusing code: parameterized namespaces. If it existed, then it would give a different way to implement to_additive for example.

Here's an example of how it could work, in this case for adding some additional boilerplate that typeclasses can't add:

import data.set_like.basic

universes u v

namespace set_like_boilerplate
parameters (α : Type u → Type v) (X : Type u) [set_like (α X) X]

@[ext] lemma ext {p q : α X} (h : ∀ (x : X), x ∈ p ↔ x ∈ q) : p = q := set_like.ext h

end set_like_boilerplate


structure my_subobject (X : Type*) :=
(carrier : set X)

namespace my_subobject
variables (X : Type*)

instance : set_like (my_subobject X) X :=
⟨my_subobject.carrier, λ p q h, by cases p; cases q; congr'⟩

open set_like_boilerplate with my_subobject X

end my_subobject

I imagine it would create a namespace like normal (if namespace were like section and admitted parameters). But then in the open syntax there'd be an option to pass in parameters. Rather than including symbols, however, it would have to create new symbols. Adding to the complexity, there could be a way to give open a name rewrite function to be able to replace parts of symbol names (so for example, op to mul or add).

There are many many questions for how this would work. I've imagined that parameters was originally envisioned for some kind of parameterized modules, but the complexity was deferred, and it was realized that they're not essential.

[Reid Barton]

This is like ML modules I guess?

[Kyle Miller]

I think they're like ML functors in particular, but set up so that each declaration is still at the top level and can be typechecked individually like usual. It's also not aiming to do anything like having predefined signatures that the namespace is implementing -- that's what structure is for. This is trying to solve the problem "how do I specialize lemmas to have the correct syntax for rewriting, possibly giving the lemmas appropriate names?"