Finset vs. finite Set

Stream: new members

[Christoph Spiegel]

Assuming I am working exclusively with finite sets in some finite universe (e.g. the lattice of subsets of {1, ..., n} representing the Hypercube graph), should I be using using Finset (Fin n) or (s : Set (Fin n)) [Finite s]?

I started working with the former, but am getting the impression that Finset is for more "base level" arguments. For example, I cannot use set notation (without always coercing to Finset) and Set generally seems to be more developed. On the other hand I am going to use double counting, which is build on Finset (though coercing to Finset here should be less of notational hassle than the alternative). The proof of the Sensitivity Conjecture in mathlib uses a fourth option with Fin n → Bool and defining adjacency from a functional perspective, but I wanted to use symmetric differences since it seems to be the easiest notion for simp to take advantage of.

[Yaël Dillies]

Definitely use Finset

[Yaël Dillies]

If you have more precise questions, I am happy to answer

[Christoph Spiegel]

Thanks! Is there any way to get back Set notation while exclusively working with Finset of a Fintype? Some setting that means I can use {· ∣ · } and · ∆ · instead of Finset.filter, Finset.univ and symmDiff?

Also, what are the "correct" Finset analogues to Set.Pairwise and Set.offDiag?

[Yaël Dillies]

∆ already exists, although @Patrick Massot recently made it very undiscoverable

[Yaël Dillies]

You need to open scoped symmDiff to get it

[Yaël Dillies]

docs#Set.Pairwise doesn't need a finset analog since all it uses is the membership relation. If s : Finset α, simply do (s : Set α).Pairwise

[Yaël Dillies]

We don't yet have docs#Sep notation for finset. @Kyle Miller and I talked about it, but I'm not sure where it's at right now

[Christoph Spiegel]

Yaël Dillies said:

You need to open scoped symmDiff to get it

You're right, I wasn't working with Finset of Fintype, that's why it was complaining, not bc of the Finset.

[Yaël Dillies]

A common trap is that you need [DecidableEq α] as soon as you want to use lattice operations on Finset α

[Christoph Spiegel]

Yaël Dillies said:

A common trap is that you need [DecidableEq α] as soon as you want to use lattice operations on Finset α

I think that I have sorted out, using abbrev vertex (n : ℕ) := Finset (Fin n) should inherit the decidability from Fintype and Finset

[Christoph Spiegel]

Yaël Dillies said:

docs#Set.Pairwise doesn't need a finset analog since all it uses is the membership relation. If s : Finset α, simply do (s : Set α).Pairwise

Would it make sense to still define Finset.Pairwise and simply have it coerce to Setin the background? Explicitly casting to Set seems superfluous and doesn't produce readable proofs?

[Yaël Dillies]

Yeah, we could just have abbrev Finset.pairwise (s : Finset α) := (s : Set α).Pairwise

[Christoph Spiegel]

Yaël Dillies said:

We don't yet have docs#Sep notation for finset. Kyle Miller and I talked about it, but I'm not sure where it's at right now

Sounds like a good idea to me. I'm not that fluent yet in the fundamentals of Lean, but if there's something that I can do for that, let me know.

[Yaël Dillies]

The issue is that we would want {x ∈ s | p x} to be syntactically s.filter p (or s.filter fun x ↦ p x, whatever), not Sep.sep p s.

[Yaël Dillies]

Or maybe we could give up docs#Finset.filter entirely, since it's simply sep?

[Christoph Spiegel]

I guess while I have your attention another question only partially related to Finset vs Set: how would you obtain "two distinct vertices in a Finset of vertices that minize hamming distance"? Is Function.argminthe right place? (And seems like this kind of argument might be well suited for a custom tactic?)

[Yaël Dillies]

Kyle, is your fancy sep notation hardcoded for Set, or is it generic over Sep instances?

[Yaël Dillies]

I would do obtain ⟨(x, y), hxy, hxymin⟩ := (s ×ˢ s).exists_min_image (fun (x, y) ↦ hammingDist x y) (hs.prod hs); rw [mem_product] at hxy where hs : s.Nonempty

[Christoph Spiegel]

Yaël Dillies said:

I would do obtain ⟨(x, y), hxy, hxymin⟩ := (s ×ˢ s).exists_min_image (fun (x, y) ↦ hammingDist x y) (hs.prod hs); rw [mem_product] at hxy where hs : s.Nonempty

Thanks, exists_min_image I hadn't found yet!