Zulip Chat Archive

Stream: general

Topic: Lean 3.21.0c


view this post on Zulip 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:

Changes:

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

Mathlib PR: #4578

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 12 2020 at 04:53):

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

view this post on Zulip Bryan Gin-ge Chen (Oct 12 2020 at 05:14):

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

view this post on Zulip Yury G. Kudryashov (Oct 12 2020 at 05:24):

How about has_cons?

view this post on Zulip Mario Carneiro (Oct 12 2020 at 06:03):

No, this will break many uses of list.cons

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 12 2020 at 06:04):

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

view this post on Zulip Johan Commelin (Oct 12 2020 at 09:15):

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

view this post on Zulip Johan Commelin (Oct 12 2020 at 09:15):

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

view this post on Zulip Johan Commelin (Oct 12 2020 at 09:15):

Do you think reinstating the localized notation is worth it?

view this post on Zulip Mario Carneiro (Oct 12 2020 at 09:17):

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

view this post on Zulip Johan Commelin (Oct 12 2020 at 09:18):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 12 2020 at 09:19):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 12 2020 at 09:55):

I pushed a patch using the notation

view this post on Zulip Johan Commelin (Oct 12 2020 at 10:16):

I think this is now ready for review

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Oct 12 2020 at 19:33):

Hmm, that might make sense

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Oct 13 2020 at 04:16):

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

view this post on Zulip Mario Carneiro (Oct 13 2020 at 04:16):

can't finvec use a different letter?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 13 2020 at 06:24):

Fresh from #4593

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 13 2020 at 07:08):

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

view this post on Zulip Johan Commelin (Oct 13 2020 at 07:09):

@Mario Carneiro So, what do you suggest?

view this post on Zulip Johan Commelin (Oct 13 2020 at 07:09):

::m ?

view this post on Zulip Mario Carneiro (Oct 13 2020 at 07:10):

sure, why not

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 13 2020 at 07:12):

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

view this post on Zulip Mario Carneiro (Oct 13 2020 at 07:12):

MONGOLIAN FOUR DOTS

view this post on Zulip Gabriel Ebner (Oct 13 2020 at 07:37):

For multisets we could also standardize on insert.

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 13 2020 at 09:24):

#4600 introduces notation for multiset.const

view this post on Zulip 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.

view this post on Zulip 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 )

view this post on Zulip Gabriel Ebner (Oct 13 2020 at 09:33):

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

view this post on Zulip Johan Commelin (Oct 13 2020 at 09:33):

I am not qualified to weigh the pros and cons

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 13 2020 at 12:36):

I've fixed the whitespace around the notation


Last updated: May 11 2021 at 23:11 UTC