Zulip Chat Archive

Stream: general

Topic: Lean 3.21.0c

Bryan Gin-ge Chen (Oct 12 2020 at 02:01):

It's been another month, so here's Lean 3.21.0c! Thanks to @Scott Morrison, @Johan Commelin and @Edward Ayers for their contributions (and @Gabriel Ebner and @Rob Lewis for reviewing and merging their PRs)!

Features:

Simplify definition of band and bor (lean#466)
More advice in docstrings for Exists, not, and, and or (lean#296)

Bug fixes:

Fix typo in docstring for tactic.exact (lean#472)
Fix missing code block in widget server docs (lean#473)

Changes:

Remove global notation for vector.cons (lean#471)

Mathlib PR: #4578

Bryan Gin-ge Chen (Oct 12 2020 at 03:55):

In #4578, I'm slowly tearing out all the instances of :: notation applied to vectors. Did we want to replace it with some (other) localized notation or are we happy with having a bunch of vector.cons everywhere?

Bryan Gin-ge Chen (Oct 12 2020 at 03:56):

@Mario Carneiro I think most of the files I've been fixing were written by you, so let me know what your preference is.

Mario Carneiro (Oct 12 2020 at 04:53):

How about a global notation ::ᵥ or :ᵥ?

Bryan Gin-ge Chen (Oct 12 2020 at 05:14):

vector is defined in core. Where would be a good place to add ::ᵥ?

Yury G. Kudryashov (Oct 12 2020 at 05:24):

How about has_cons?

Mario Carneiro (Oct 12 2020 at 06:03):

No, this will break many uses of list.cons

Mario Carneiro (Oct 12 2020 at 06:04):

@Bryan Gin-ge Chen We have a data.vector2 file for additional foundational material supplementing core's data.vector

Mario Carneiro (Oct 12 2020 at 06:04):

maybe it's been renamed to data.vector.basic

Johan Commelin (Oct 12 2020 at 09:15):

@Mario Carneiro #4578 passes CI. A couple of files have changed, with :: replaced by vector.cons.

Johan Commelin (Oct 12 2020 at 09:15):

Personally, I would be happy to kick it on the queue like this.

Johan Commelin (Oct 12 2020 at 09:15):

Do you think reinstating the localized notation is worth it?

Mario Carneiro (Oct 12 2020 at 09:17):

localized isn't going to work here, because it clobbers list.cons when open

Johan Commelin (Oct 12 2020 at 09:18):

Ok, then I would be a big fan of just merging the PR as is

Mario Carneiro (Oct 12 2020 at 09:18):

it's not uncommon to be working with list.cons and vector.cons simultaneously, they aren't that separate in their definition

Mario Carneiro (Oct 12 2020 at 09:19):

Instead, I suggest using a global but disambiguated notation such as ::ᵥ (see above)

Johan Commelin (Oct 12 2020 at 09:21):

Yes, I read that suggestion. But is it worth it? vector.cons isn't used that much at all.

Mario Carneiro (Oct 12 2020 at 09:23):

I think a cons like operation for a vector like type is important, although perhaps the vector like type would be better suited as fin n -> A

Mario Carneiro (Oct 12 2020 at 09:24):

but looking at the files that were changed, I certainly would not have wanted to deal with the lack of notation while writing them

Johan Commelin (Oct 12 2020 at 09:55):

I pushed a patch using the notation

Johan Commelin (Oct 12 2020 at 10:16):

I think this is now ready for review

Floris van Doorn (Oct 12 2020 at 19:22):

Do we want to make ::ᵥ localized notation, so that we can also use it for finvec and potentially other vector-like structures?

Johan Commelin (Oct 12 2020 at 19:33):

Hmm, that might make sense

Johan Commelin (Oct 12 2020 at 19:33):

Yury G. Kudryashov: How about has_cons?
Mario Carneiro: No, this will break many uses of list.cons

Maybe we can nevertheless have a has_consv?

Mario Carneiro (Oct 13 2020 at 04:16):

I was hoping that with a disambiguated notation there wouldn't be name contention

Mario Carneiro (Oct 13 2020 at 04:16):

can't finvec use a different letter?

Johan Commelin (Oct 13 2020 at 06:23):

NOOOOOOOOOOOOOO!!!

configuring mathlib 0.1
/home/runner/work/mathlib/mathlib/src/tactic/linarith/verification.lean:162:20: error: ambiguous overload, possible interpretations
  hz :: ↑l'
  hz :: l'
Additional information:
/home/runner/work/mathlib/mathlib/src/tactic/linarith/verification.lean:162:20: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because it failed to disambiguate overload using the expected type
  ?m_1
the following overloaded terms were applicable
  multiset.cons
  list.cons

Johan Commelin (Oct 13 2020 at 06:24):

We went through all this trouble to get rid of vector.cons notation, and voila, there is the next conflict.

Johan Commelin (Oct 13 2020 at 06:24):

Fresh from #4593

Kyle Miller (Oct 13 2020 at 06:35):

Hmm... I was wondering about the focus on vector because of that. I guess I should get rid of the :: notation in https://github.com/leanprover-community/mathlib/blob/master/src/data/sym.lean as well?

Mario Carneiro (Oct 13 2020 at 07:08):

yep, IIRC it was a three-way conflict with list.cons, vector.cons and multiset.cons, although apparently sym has joined the party

Mario Carneiro (Oct 13 2020 at 07:08):

However the other occurrences are in mathlib so it's less hard to fix those

Johan Commelin (Oct 13 2020 at 07:09):

@Mario Carneiro So, what do you suggest?

Johan Commelin (Oct 13 2020 at 07:09):

::m ?

Mario Carneiro (Oct 13 2020 at 07:10):

sure, why not

Mario Carneiro (Oct 13 2020 at 07:11):

I mean it's either that or reserve a unicode block like category theory is doing with arrows

Johan Commelin (Oct 13 2020 at 07:12):

Hmpfz... I'll try to summon the courage for the refactor

Mario Carneiro (Oct 13 2020 at 07:12):

᠅ MONGOLIAN FOUR DOTS

Gabriel Ebner (Oct 13 2020 at 07:37):

For multisets we could also standardize on insert.

Gabriel Ebner (Oct 13 2020 at 07:38):

(I don't know if a notation for insert would conflict with the set notation or not.)

Kyle Miller (Oct 13 2020 at 07:38):

Is the reason there's no has_cons because there's no way to then make :: a pattern? Or would overloading still be a problem somehow?

Gabriel Ebner (Oct 13 2020 at 08:42):

:: can be a pattern, no problem. (Even x + 1 is a pattern, even though both + and 1 are type classes.)

Johan Commelin (Oct 13 2020 at 09:15):

@Mario Carneiro Can you be more specific about why has_cons would break uses of list.cons?

Mario Carneiro (Oct 13 2020 at 09:16):

Just a hunch, because list.cons is so fundamental, it's bound to be syntax matched in several places

Johan Commelin (Oct 13 2020 at 09:24):

#4600 introduces notation for multiset.const

Gabriel Ebner (Oct 13 2020 at 09:24):

I'd be more worried about type inference breaking in more places, e.g. (x::xs).length might no longer work, etc.

Gabriel Ebner (Oct 13 2020 at 09:29):

On the other hand, this could also open some wonderful new possibilities. If we additionally make a type class for nil, then the following could work:

([1,2,3] : list ℕ)
([1,2,3] : vector ℕ 3)
([1,2,3] : finvec ℕ 3)
([1,2,3] : multiset ℕ)

Gabriel Ebner (Oct 13 2020 at 09:33):

(['a', 'b', 'c'] : string)
([1,2,3] : buffer ℕ)

Johan Commelin (Oct 13 2020 at 09:33):

I am not qualified to weigh the pros and cons

Gabriel Ebner (Oct 13 2020 at 09:36):

Another con (that we already have for ℕ):

example : x ++ [] = x :=
begin
  induction x,
  refl,
  -- ⊢list.cons x_hd x_tl ++ [] = list.cons x_hd x_tl
  -- :-(
end

Johan Commelin (Oct 13 2020 at 09:49):

I guess reverting the ::\_m notation for multiset will be rather easy. You can just global search replace. So, does it make sense to merge #4600 for now, and maybe revert it when the experimens with has_cons are positive?

Gabriel Ebner (Oct 13 2020 at 09:52):

I like #4600. The cons/nil type classes are more risky and definitely more work, it doesn't make sense to block #4600 on it.

Johan Commelin (Oct 13 2020 at 12:36):

I've fixed the whitespace around the notation

Last updated: Dec 20 2023 at 11:08 UTC