Zulip Chat Archive

Stream: general

Topic: Redirecting dot notation

Yaël Dillies (Aug 31 2022 at 12:55):

Would it be possible to make dot notation resolve s.nonempty, s.subsingleton, s.nontrivial to set.nonempty (s : set α), set.subsingleton (s : set α), set.nontrivial (s : set α) when s : finset α? This would avoid another lot of duplication.

Adam Topaz (Aug 31 2022 at 13:04):

These probably all boil down to the has_mem instance, which is not defeq to has_mem for the coercion to set, which is presumably due to computational reasons.

Yaël Dillies (Aug 31 2022 at 13:05):

src#finset.mem_coe is refl, though.

Adam Topaz (Aug 31 2022 at 13:06):

Oh great

Adam Topaz (Aug 31 2022 at 13:06):

I guess the coercion to set is via the has mem ;)

Wrenna Robson (Aug 31 2022 at 13:48):

Is there any dot notation exclusive to finset? Would that cause issues with this?

Yaël Dillies (Aug 31 2022 at 13:49):

There currently is docs#finset.nonempty but the above idea would get rid of it, if that's what you meant.

Wrenna Robson (Aug 31 2022 at 13:50):

Well what I was thinking was, obviously we don't want to redirect every s.foo where s is a finset.

Wrenna Robson (Aug 31 2022 at 13:52):

I think the idea is desirable though. These predicates are really set-like, in the sense that they are not about properties of the finset structure but simply whether or not certain elements have mem.

(You probably need to duplicate things like finset.mem_off_diag and set.mem_off_diag for your off_diag PR, for instance, because finset.off_diag and set.off_diag are constructed in different ways.)

Wrenna Robson (Aug 31 2022 at 13:54):

(That being said, one is a filtered finset and one is set comprehension, which are morally "the same", so go figure.)

Wrenna Robson (Aug 31 2022 at 14:01):

Basically I agree with your goal here and that we should minimise duplication as much as possible. I'm sure there's more one could do but perfect shouldn't be the enemy of good. Things should line up, though, unless there's a good reason why they ought not to.

Kyle Miller (Aug 31 2022 at 15:21):

@Yaël Dillies If you promise not to use this feature in any mathlib PR's until we know whether it can be ported to Lean 4, I'll show you a consequence to the new dot notation that essentially gives you this. There are no guarantees the feature will last long -- this works because we were preserving a (misused?) Lean 3 feature to make it easier to do the Lean version bump.

Lean 4 has a way to use dot notation with aliases, which was backported. However, Lean 3 will currently insert the object of the dot notation as the first argument if the usual rule doesn't succeed (insert it at the first explicit argument whose head matches), which is not compatible with Lean 4. For example:

import tactic

protected def has_mem.nonempty' {α β} [has_mem α β] (s : β) : Prop :=  x, x  s

export has_mem (renaming nonempty'  finset.nonempty')

example {α : Type*} (s : finset α) : Prop := s.nonempty'

For the alias feature to work, the field name must match (renaming nonempty' -> finset.my_nonempty won't work)

I would have written it the following way, but it's triggering an error for reasons I don't understand at the moment:

-- redefine so that it has a name that won't conflict with `finset.nonempty` once we export it
protected def set.nonempty' {α : Type*} (s : set α) : Prop := s.nonempty

export set (renaming nonempty'  finset.nonempty')

example {α : Type*} (s : finset α) : Prop := s.nonempty'
-- failure (switched to simple elaboration procedure)

Kyle Miller (Aug 31 2022 at 15:30):

I should mention that this export line in Lean 4 would be

namespace finset
export has_mem (nonempty')
end finset

I don't understand Lean 3 aliases well enough to know why #check finset.nonempty' doesn't resolve. But if it did, then this namespace/export block should work in place of the export ... (renaming ...) command.

Wrenna Robson (Aug 31 2022 at 15:52):

@Yaël Dillies it occurs to me that (though I suppose this might lose the dot notation?) you could define has_mem.nonempty etc.? Like make it so that anything which has_mem would get it.

Yaël Dillies (Aug 31 2022 at 15:52):

Dot notation is the only reason docs#finset.nonempty exists, so it's definitely important.

Wrenna Robson (Aug 31 2022 at 17:45):

Aye. I couldn't remember if the way it worked for typeclasses, dot notation would work on anything whose type was of the right typeclass.

Last updated: Aug 03 2023 at 10:10 UTC