with or ..

Stream: new members

[Joachim Breitner]

Is there a difference between { foo with bar := baz, } and {bar := baz, ..foo}?

[Eric Wieser]

I think only the latter syntax lets you unpack multiple structures

[Eric Wieser]

Maybe there's more to it though

[Reid Barton]

According to my grep attempt, mathlib only uses the former a few times in tactics

[Reid Barton]

I didn't know it existed

[Joachim Breitner]

I find slightly odd that the .. syntax is preferred, when the { foo with …} is (IMHO) more readable and natural: You start with the object you want to extend, and then you list the additional fields.
But maybe uniformity is useful, and so with really shouldn’t be used in mathlib?

[Joachim Breitner]

The reference manual at <https://leanprover.github.io/reference/declarations.html#structures-and-records> doesn't give much guidance. Although unless I am blind it only documents with, but not ..foo syntax?

[Yaël Dillies]

I personally didn't even know this syntax existed.

[Adam Topaz]

Does { foo with ... } work when you want to have multiple foos?

[Adam Topaz]

E.g.

structure foo :=
(a : ℕ)

structure bar extends foo :=
(b : ℕ)

structure baz :=
(a : ℕ)
(b : ℕ)
(c : ℕ)

example (f : foo) (g : bar) (c : ℕ) : baz :=
{ c := c, .. f, .. g }

[Adam Topaz]

There might be some way to do this with the { foo with ... } syntax, but I don't know what it is.

[Joachim Breitner]

Sounds like the .. is more versatile and powerful, and conversely with simpler?

[Reid Barton]

Maybe there is a difference in intention (even if not technically, not sure): { x with a := t' } suggests we already have a structure of the same type and we are changing one of the fields, while { b := u, .. x } suggests that we are building a bigger structure reusing some fields from x.

[Reid Barton]

The first one would be relatively rare in math (for instance if the structure is a proposition, then it makes no sense).

[Joachim Breitner]

Hmm, in a language with extensible records I am not surprised that with allows extension, not just updates. But I see your point.

Is {.. x, b := u} legal? (On the phone right now)

[Alex J. Best]

It's not legal it seems

[Yaël Dillies]

The thing is that the .. fill in everything they can as soon as they're used. So you want to use them last.

[Joachim Breitner]

Isnt that odd? I can out a .. foo before.. bar, but not before individual field assignments? Anyways, probably all not so important, and I'll adjust to the mathlib style

[Yaël Dillies]

Are you using the old or new structure command? What is the value of old_structure_cmd?

[Yaël Dillies]

If you're using the new one, then usually what you consider a single field of a structure is actually a field of a parent one and the structure you have in hand has that parent as a field. If you understand this, then you'll see why the { := , := } is such a nice syntax sugar.

[Kyle Miller]

I thought I had remembered Mario discussing with vs .. and the history of .. in Lean 3, but all I managed to dig up was https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.22.2E.2Es.22.20in.20structure.20literals/near/224902754

Too bad "with" is a stop word for Zulip's search...

[Mario Carneiro]

By the way for the curious, the ..s notation has since been added as a mathlib4 extension written __ := s. I think it is also less restrictive in terms of its positioning wrt other fields