Redirecting dot notation

Stream: general

[Yaël Dillies]

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]

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]

src#finset.mem_coe is refl, though.

[Adam Topaz]

Oh great

[Adam Topaz]

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

[Wrenna Robson]

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

[Yaël Dillies]

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

[Wrenna Robson]

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

[Wrenna Robson]

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]

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

[Wrenna Robson]

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]

@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]

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]

@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]

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

[Wrenna Robson]

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.