Zulip Chat Archive

Stream: Is there code for X?

Topic: finset.subset_iff_inter_eq_left / right


view this post on Zulip Damiano Testa (Apr 06 2021 at 02:22):

Dear All,

I needed the two lemmas below about finset that are the direct analogue of the corresponding lemmas on set. However, I was not able to find them. Is there a reason that they are not there? Should I make a PR to add them?

Do you also want to golf the proofs?

Thank you!

import data.finset.basic

namespace finset

theorem subset_iff_inter_eq_left {α : Type*} {s t : finset α} [decidable_eq α] :
  s  t  s  t = s :=
begin
  refine λ h, subset.antisymm (s.inter_subset_left t) (subset_inter (subset.refl s) h), λ h, _⟩,
  rw  h,
  exact s.inter_subset_right t,
end

theorem subset_iff_inter_eq_right {α : Type*} {s t : finset α} [decidable_eq α] :
  s  t  t  s = s :=
by { rw inter_comm, exact subset_iff_inter_eq_left }

end finset

view this post on Zulip Bryan Gin-ge Chen (Apr 06 2021 at 02:28):

Both these and their set analogues should follow from something at the level of (semi)lattices, right? cf. docs#inf_eq_left

view this post on Zulip Damiano Testa (Apr 06 2021 at 02:35):

The set versions exist and they are set.subset_iff_inter_eq_left/right. I will try to make the proof work with lattices, thanks!

view this post on Zulip Damiano Testa (Apr 06 2021 at 02:39):

... the statement looks like the one that I want, but I am unable to convince Lean that ≤ = ⊆ and that ⊓ = ∩.

view this post on Zulip Bryan Gin-ge Chen (Apr 06 2021 at 03:17):

In #6775, I changed a bunch of finset and set proofs to use lattice / (generalized) Boolean algebra versions instead; most of the time Lean is able to see that and are defeq, but sometimes I have to use show and some other tricks. Looking at the examples there might help

view this post on Zulip Damiano Testa (Apr 06 2021 at 03:26):

Indeed, thanks! This works:

theorem subset_iff_inter_eq_left {s t : finset α} [decidable_eq α] :
  s  t  s  t = s :=
(inf_eq_left.symm : s  t  s  t = s)

Now I am more doubtful: is this lemma worth a PR?

view this post on Zulip Damiano Testa (Apr 06 2021 at 03:27):

(Maybe with the two sides of the iff exchanged, to match the lattice version?)

view this post on Zulip Bryan Gin-ge Chen (Apr 06 2021 at 03:30):

I think so, at least judging by the existence of the set versions.

view this post on Zulip Damiano Testa (Apr 06 2021 at 03:44):

PR #7053

view this post on Zulip Damiano Testa (Apr 06 2021 at 03:45):

While placing these lemmas, I saw that the lattice instance is after a bunch of results that might also be proven via the lattice structure. Should these lemmas be reproven using lattice inf/sup stuff?

view this post on Zulip Damiano Testa (Apr 06 2021 at 03:46):

(I have not checked which ones of these lemmas are needed to get the lattice instance, I simply placed the two new ones after the instance and wondered...)

view this post on Zulip Bryan Gin-ge Chen (Apr 06 2021 at 03:48):

I noticed something similar when I was preparing #6775 and I wasn't sure either. It might be worth playing around with.

view this post on Zulip Damiano Testa (Apr 06 2021 at 03:50):

Ok, I will not do it in this PR, but, if this is something that should happen, I can add the comment

-- TODO: check which ones of these results now follow from the lattice structure

before the lemmas that might benefit from this. Maybe even at the beginning of the file, although the file is quite long.

view this post on Zulip Damiano Testa (Apr 06 2021 at 05:31):

CI successfully built the previous version did not finish yet!

However, I thought that it did and I added the TODO and I also flipped the iff's, since the subset side seems simpler than the side with the intersection and the equality.


Last updated: May 07 2021 at 21:10 UTC