Why Finset?

Stream: new members

[Jakub Nowak]

In mathlib some theorems use Set, and some Finset. This sometimes leads to having to convert back-and-froth, or having to duplicate code for both Set and Finset. Wouldn't it be easier to use s : Set α with some s.Fin assumption (note that docs#Set.Finite is not the same as docs#Finset, because the latter also holds its elements as data)?

[Kenny Lau]

@Jakub Nowak do you have more context?

[Shreyas Srinivas]

There was Marcin's question from before, but it keeps happening all the time

[Shreyas Srinivas]

Finset is computable

[Shreyas Srinivas]

It requires its type to have an instance of DecidableEq

[Shreyas Srinivas]

Finite doesn't

[Jakub Nowak]

Yes, the point is docs#Set.Fin would also be computable. Smth like:

structure Set.Fin (s : Set α) where
  finset : Finset α
  eq : s = finset

[Mirek Olšák]

I agree that it is annoying when there are multiple ways to express the same idea, then one view supports well one part of reasoning, the other one another, etc. but I don't have a good solution.

[Dexin Zhang]

One thing I found that Finset has but Set.Finite does not is docs#Finset.strongInduction, which is indeed useful sometimes

[Jakub Nowak]

Kenny Lau said:

Jakub Nowak do you have more context?

I decided to ask because of that question: #new members > Hello & graph coloring exercises
But I agree with @Shreyas Srinivas, it's not the first time I had to deal with this.

[Shreyas Srinivas]

Fin is computable, but you can't say anything about computability of elements inside a Finite Set

[Shreyas Srinivas]

Note that I am not saying this justifies the Finset approach. I tend to use either Finite or Set.encard when required

[Snir Broshi]

Shreyas Srinivas said:

Fin is computable, but you can't say anything about computability of elements inside a Finite Set

But what about the structure suggestion above?

[Mirek Olšák]

I would not blame computability here, most notably, Finset is like Set bundled together with its Finite, so we don't have to carry the assumption along. When using Finsets for example, we get automatically that intersections / unions / filters / images of finsets are still finite without doing any extra reasoning. Regarding computability, Fintype / Finite is the mysterious pair.

[Jakub Nowak]

Dexin Zhang said:

One thing I found that Finset has but Set.Finite does not is docs#Finset.strongInduction, which is indeed useful sometimes

We could have:

def Set.finStrongInduction {α : Type u_1} {p : (s : Set α) → s.Fin → Sort u_4} (H : (s : Set α) → s.Fin → ((t : Set α) → t ⊂ s → p t) → p s) (s : Set α) → (h : s.Fin) :
  p s h

Though maybe, you also need t.Fin? Not sure t.Fin follows from s.Fin and t ⊂ s.

[Eric Wieser]

Jakub Nowak said:

Yes, the point is docs#Set.Fin would also be computable. Smth like:

structure Set.Fin (s : Set α) where
  finset : Finset α
  eq : s = finset

I think this becomes a question about bundled or unbundled data, rather than computability

[Jakub Nowak]

Eric Wieser said:

I think this becomes a question about bundled or unbundled data, rather than computability

Both Finset and Set.fin have bundled data. The point of the question is not about bundling data. It's about having "finite with bundled data" as a property of Set instead of separate type.

[Eric Wieser]

Set.Fin is (partially) unbundled because some of its data is in the type parameters

[Jakub Nowak]

Ah, yes, you're right. But I don't think that's the point of the question? Can you elaborate?

[Jakub Nowak]

My proposition is to:

• deprecate Finset
• for every instance where the are two definitions/theorems for both Set and Finset version, you would only keep Set version and add a separate theorems stating, the finiteness is preserved
• replace Finset arguments with two arguments s : Set α and s.Fin, possibly skipping some of the s.Fin assumptions if they follow from other
• replace Finset in return type with Set, and prove finiteness in a separate theorem

[Kevin Buzzard]

I'd vote for that but there will be strong opposition from people who want mathlib to be more constructivecomputable rather than less (sorry -- I don't know the difference)

[Jakub Nowak]

This wouldn't make mathlib less constructive, at least not directly. Though, it could be that after deprecation people will miss chances to add the finiteness theorems, when it's possible. We should hope for reviewers to also try and catch that.

[Shreyas Srinivas]

If you deprecate Finset you will not be able to define the Fin structure. Secondly the Fin name is already in use to bounded Nat

[Andrew Yang]

The right word might be less "computable" and not less "constructive"
e.g. you probably can't have this defeq example : ∑ i ∈ {1, 2, 3}, i = 6 := rfl without finsets.

[Jakub Nowak]

Shreyas Srinivas said:

If you deprecate Finset you will not be able to define the Fin structure.

We can just inline its fields.

Shreyas Srinivas said:

Secondly the Fin name is already in use to bounded Nat

I also agree that this name is bad, I'm not saying to use it, it's here just as an example.

[Shreyas Srinivas]

I think Finset is a useful structure to have in many cases. I just think we should be able to auto suggest typeclass instances that would make the Finset version of a lemma work with a Set version.

[Shreyas Srinivas]

Ideally there ought to be an open FiniteAll that works similar to open Classical but gives finite ness instances to everything that needs it.

[Jakub Nowak]

Andrew Yang said:

The right word might be less "computable" and not less "constructive"
e.g. you probably can't have this defeq example : ∑ i ∈ {1, 2, 3}, i = 6 := rfl without finsets.

It works with Set.Fin too:

code

import Mathlib

structure Set.Fin (s : Set α) where
  finset : Finset α
  eq : s = finset

@[aesop safe]
def Set.Fin.empty : (∅ : Set α).Fin where
  finset := ∅
  eq := by simp

@[aesop safe]
def Set.Fin.singleton : (Singleton.singleton x : Set α).Fin where
  finset := {x}
  eq := by simp

@[aesop safe]
def Set.Fin.insert [DecidableEq α] (h : s.Fin) : (Insert.insert x s : Set α).Fin where
  finset := Insert.insert x h.finset
  eq := by rw [Finset.coe_insert, ←h.eq]

@[to_additive]
def Set.Fin.prod [CommMonoid M] (s : Set ι) (h : s.Fin) (f : ι → M) : M :=
  Finset.prod h.finset f

namespace BigOperators

open Batteries.ExtendedBinder Lean Meta

def processBigOpBinder'' (processed : (Array (Term × Term))) (binder : TSyntax ``bigOpBinder) :
    MacroM (Array (Term × Term)) :=
  set_option hygiene false in
  withRef binder do
    match binder with
    | `(bigOpBinder| $x:term) =>
      match x with
      | `(($a + $b = $n)) => -- Maybe this is too cute.
        Macro.throwUnsupported
      | _ => return processed |>.push (x, ← ``(Set.univ))
    | `(bigOpBinder| $x : $t) => return processed |>.push (x, ← ``((Set.univ : Set $t)))
    | `(bigOpBinder| $x ∈ $s) => return processed |>.push (x, ← `($s))
    | `(bigOpBinder| $x ∉ $s) => return processed |>.push (x, ← `($sᶜ))
    | `(bigOpBinder| $x ≠ $n) => return processed |>.push (x, ← `(Set.univ.erase $n))
    | `(bigOpBinder| $x < $n) => return processed |>.push (x, ← `(Set.Iio $n))
    | `(bigOpBinder| $x ≤ $n) => return processed |>.push (x, ← `(Set.Iic $n))
    | `(bigOpBinder| $x > $n) => return processed |>.push (x, ← `(Set.Ioi $n))
    | `(bigOpBinder| $x ≥ $n) => return processed |>.push (x, ← `(Set.Ici $n))
    | _ => Macro.throwUnsupported


def processBigOpBinders'' (binders : TSyntax ``bigOpBinders) :
    MacroM (Array (Term × Term)) :=
  match binders with
  | `(bigOpBinders| $b:bigOpBinder) => processBigOpBinder'' #[] b
  | `(bigOpBinders| $[($bs:bigOpBinder)]*) => bs.foldlM processBigOpBinder'' #[]
  | _ => Macro.throwUnsupported

syntax (name := bigsum'')
  "∑'' " bigOpBinders ("with " atomic(binderIdent " : ")? term)? ", " term:67 : term

macro_rules (kind := bigsum'')
  | `(∑'' $bs:bigOpBinders $[with $[$hx??:binderIdent :]? $p?:term]?, $v) => do
    let processed ← processBigOpBinders'' bs
    let x ← bigOpBindersPattern processed
    let s ← bigOpBindersProd processed
    -- `a` is interpreted as the filtering proposition, unless `b` exists, in which case `a` is the
    -- proof and `b` is the filtering proposition
    match hx??, p? with
    | some (some hx), some p => Macro.throwUnsupported
    | _, some p => Macro.throwUnsupported
    | _, none => `(Set.Fin.sum $s (by aesop) (fun $x ↦ $v))


end BigOperators

example : ∑'' x ∈ {1, 2, 3}, x = 6 := rfl

[Kenny Lau]

I'm a bit wary of this approach of hiding by aesop under a notation

[Kenny Lau]

your suggestion is not very different from making Set.Finite a typeclass (with data)

[Jakub Nowak]

Kenny Lau said:

I'm a bit wary of this approach of hiding by aesop under a notation

I've used by aesop because it was easier. It would be better to implement separate tactic for this. Why do you think it's a problem?

[Kenny Lau]

ah right, the other thing is that once it contains data, then extensionality becomes a problem, this is also known as the "diamond"

[Jakub Nowak]

Kenny Lau said:

your suggestion is not very different from making Set.Finite a typeclass (with data)

It's not, but we also have separate Finite and Fintype typeclasses. It's probably reasonable to have separate versions with and without data for set finiteness too.

[Kenny Lau]

Jakub Nowak said:

I've used by aesop because it was easier. It would be better to implement separate tactic for this. Why do you think it's a problem?

if you use this notation in a statement, then you're using notation to hide away the fact that the statement uses an expensive tactic. This is not what notations are for.

[Jakub Nowak]

(deleted)

[Jakub Nowak]

Kenny Lau said:

if you use this notation in a statement, then you're using notation to hide away the fact that the statement uses an expensive tactic. This is not what notations are for.

I don't think it's an expensive tactic if it only proves that {a, b, c, ...} is a finite set by recursion over Insert.insert.

[Jakub Nowak]

It's basically the same work that the {a, b, c, ...} : Finset α notation does.

[Jakub Nowak]

The way I implemented it above, with aesop, it does way more. By we can write a separate tactic that's less expensive, and does only recursion on Insert.insert, nothing else. Just like {a, b, c, ...} : Finset α notation.

[Kenny Lau]

what do you think about using typeclass instead of aesop? and also please really consider the extensionality stuff, it's the same reason why we have Finset.sum_congr.

[Shreyas Srinivas]

You don’t need a new typeclass

[Shreyas Srinivas]

You just need to mixin Finite and DecidableEq

[Kenny Lau]

you won't get ∑ i ∈ {1, 2, 3}, i = 6 := rfl

[Jakub Nowak]

By typeclass you mean to use [Set.Fin s], right? One thing I don't like is that we would probably have to now have primed and non-primed version of theorems, one using [Set.Fin s] and one using {Set.Fin s}, e.g.:

def Set.Fin.subset (s₁ s₂ : Set α) [Set.Fin s₂] (sub : s₁ ⊆ s₂) : s₁.Fin := sorry

def Set.Fin.subset' (s₁ s₂ : Set α) {hs₂ : Set.Fin s₂} (sub : s₁ ⊆ s₂) : s₁.Fin := sorry

Unless we only use typeclass just to implement sum notation. But I don't understand why you think typeclass inference is better than custom tactic?

[Shreyas Srinivas]

Kenny Lau said:

you won't get ∑ i ∈ {1, 2, 3}, i = 6 := rfl

You’d have to redefine the notation to make is elaborate to a sum over Finvec. But I’d be surprised if that that was hard

[Jakub Nowak]

Kenny Lau said:

please really consider the extensionality stuff, it's the same reason why we have Finset.sum_congr.

Unfortunately I don't exactly understand. But I also never had to use docs#Finset.sum_congr. Would something like this work?

theorem Set.Fin.sum_congr {ι : Type*} {M : Type*} {s₁ s₂ : Set ι} {hs₁ : s₁.Fin} {hs₂ : s₂.Fin} [AddCommMonoid M] {f g : ι → M} (h : s₁ = s₂) :
  (∀ x ∈ s₂, f x = g x) → hs₁.sum f = hs₂.sum g

[Kenny Lau]

yes

[Jakub Nowak]

Although, not sure if that's provable, maybe we will also need (h' : (h ▸ hs₁) = hs₂) assumption.

[Kenny Lau]

Jakub Nowak said:

But I don't understand why you think typeclass inference is better than custom tactic?

I don't have a good answer to this question. Probably because typeclass is more predictable than tactics. A tactic could do any thing.

[Kenny Lau]

Jakub Nowak said:

Although, not sure if that's provable, maybe we will also need (h' : (h ▸ hs₁) = hs₂) assumption.

I am 100% sure that it is true (and provable, obviously).

[Kenny Lau]

you should also prove that it's extensional, meaning Subsingleton (Set.Fin s) (which also implies your h')

[Shreyas Srinivas]

In fact we already have docs#Finvec.sum

[Eric Wieser]

That's really an implementation detail for a tactic that hasn't been written

[Jakub Nowak]

@Kenny Lau

I've tried proving Set.Fin.sum_congr, though, I encountered some problems, is this the instance of a problem you had in mind, that can often arise with using this approach?

import Mathlib

@[grind cases, grind ext]
structure Set.Fin (s : Set α) where
  finset : Finset α
  eq : s = finset

theorem Set.Fin.congr (s₁ s₂ : Set α) (h : s₁ = s₂) : s₁.Fin = s₂.Fin := by rw [h]

@[to_additive]
def Set.Fin.prod [CommMonoid M] {s : Set ι} (h : s.Fin) (f : ι → M) : M :=
  Finset.prod h.finset f

instance Set.Fin.instSubsingleton (s : Set α) : Subsingleton (s.Fin) where
  allEq a b := by
    cases a
    cases b
    simp
    simp_all

theorem Set.Fin.sum_congr {ι : Type*} {M : Type*} {s₁ s₂ : Set ι} {hs₁ : s₁.Fin} {hs₂ : s₂.Fin} [AddCommMonoid M] {f g : ι → M} (h : s₁ = s₂) :
    (∀ x ∈ s₂, f x = g x) → hs₁.sum f = hs₂.sum g := by
  intro h₂
  have : hs₁ ≍ hs₂ := (Set.Fin.instSubsingleton s₁).helim (Set.Fin.congr s₁ s₂ h) hs₁ hs₂
  sorry -- what now?

[Robin Arnez]

cases on an equality is your friend!

import Mathlib

class Set.Fin (s : Set α) where
  finset : Finset α
  eq : s = finset

@[to_additive]
def Set.Fin.prod [CommMonoid M] (s : Set ι) [h : s.Fin] (f : ι → M) : M :=
  Finset.prod h.finset f

instance : Subsingleton (Set.Fin s) where
  allEq a b := by
    obtain ⟨s, hs⟩ := a
    obtain ⟨s', hs'⟩ := b
    rw [hs, Finset.coe_inj] at hs'
    cases hs'
    rfl

theorem Set.Fin.sum_congr {ι : Type*} {M : Type*} {s₁ s₂ : Set ι} {hs₁ : s₁.Fin} [s₂.Fin] [AddCommMonoid M] {f g : ι → M} (h : s₁ = s₂) :
    (∀ x ∈ s₂, f x = g x) → Set.Fin.sum s₁ f = Set.Fin.sum s₂ g := by
  cases h
  cases Subsingleton.allEq hs₁ ‹_›
  intro h
  simp only [hs₁.eq, SetLike.mem_coe] at h
  rw [sum, sum, Finset.sum_congr rfl h]