Why does "Finset a" require the assumption "DecidableEq a"?

Stream: maths

[Ching-Tsun Chou]

Why does "Finset a" require the assumption "DecidableEq a"? Why doesn't "Set a" need it?

[Quang Dao]

It's because for many operations on Finset, you need to be able to remove duplicates in a computable manner. Whereas with Set that's not an issue.

If you don't care about computability then you can always get DecidableEq via Classical.decEq.

[Ching-Tsun Chou]

Which operations on Finset need to remove duplicates? What do you mean by "removing duplicates"?

[Kyle Miller]

For example, if you compute the union of two Finsets, it appends the underlying lists and removes the duplicates. You need a way to compute equality to remove duplicates.

[Adam Topaz]

docs#Finset alone does not require any decidability assumption. Some functions involving Finsets do, as others have indicated above. Like Kyle said, when you take the union, you need to remove duplicates, so you need to be able to decide whether two elements in your type are equal.

[Ching-Tsun Chou]

@Kyle Miller But why doesn't the union of two Sets which happen to be finite also need that?

[Kyle Miller]

Set doesn't compute anything

[Kyle Miller]

A Set X is a predicate (remember that the definition is X -> Prop), which has no runtime representation. A Finset X is an actual data structure that's backed by a List enumerating its elements.

[Adam Topaz]

Note that we also have docs#Set.Finite which might more useful for you @Ching-Tsun Chou

[Adam Topaz]

And in particular Set.Finite.union

[Ching-Tsun Chou]

I guess I'm really asking: why does Lean care about "computability" (whatever that means) at all? Would the logic implemented by Lean become inconsistent if the computable vs non-computable distinction is completely ignored?

[Adam Topaz]

Lean is a programming language and a proof assistant. You can use Finsets to write programs.

[Kyle Miller]

No, the logic doesn't become inconsistent. It's just about whether you can extract runnable code, or about the likelihood of whether you can rely on definitional equality to prove things.

[Kyle Miller]

People use classical all the time to work with Finset without worrying about decidability. Or, better, you could work with Set.Finite as Adam suggested, since that keeps you in the world of Set and propositions.

[Kyle Miller]

I've wanted there to be a FiniteSet type that's a Set bundled with a Set.Finite proof. Right now the only options are manipulating these Set.Finite proofs by hand, when having lattice operations would be really convenient, or working with Finset and manipulating Decidable instances, which can be awkward and requires additional skills (like knowing about convert when exact fails).

[Ching-Tsun Chou]

Thanks for pointing out Set.Finite. I am working my way through "Mathematics in Lean" whose chapter 5 uses Finset.

[Ching-Tsun Chou]

@Kyle Miller , I have another question: Suppose there is a FiniteSet type as you wanted. Under the assumption that the underlying type \alpha is DecidableEq, how does one port a theorem stated using FiniteSet \alpha to one stated using Finset \alpha, and vice versa?

[Adam Topaz]

for docs#Set.Finite we have docs#Set.Finite.ofFinset and docs#Set.Finite.toFinset to go back and forth to Finsets.

[Adam Topaz]

Assuming someone makes a bundled Set with Set.Finite as Kyle suggests, this is how you could go back and forth between such an object and finsets. There is more API needed, of course, but it's all there, and you can read more about it in the documentation webpage for Set.Finite: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Finite.html

[Ching-Tsun Chou]

Thanks for the pointer! However, are those two maps sufficient for porting theorems from one representation to the other? For example, consider the commutativity of intersection. Does the commutativity of intersection on FiniteSet follow immediately from the commutativity on Finset? It seems not. It seems to me that one still needs to prove two commutative diagram involving the two intersection operations and the two mappings, right?

[Adam Topaz]

No, they’re not sufficient. That’s why I mentioned the API. Please take a look at the page I linked for the relevant results.

[Adam Topaz]

There are probably some results in other files as well, but the API to go back and forth is quite complete.

[Violeta Hernández]

Ching-Tsun Chou said:

I guess I'm really asking: why does Lean care about "computability" (whatever that means) at all? Would the logic implemented by Lean become inconsistent if the computable vs non-computable distinction is completely ignored?

Worth pointing out that computability can also sometimes be used to prove theorems more conveniently, by literally evaluating an expression or predicate to figure out its value

[Violeta Hernández]

This is basically what tactics like norm_num or decide do

[Ching-Tsun Chou]

Well, I just tried the following:

example : (1 : ℝ) + 2 = 3 := by norm_num

and found that it works. Of course, such computation does not work in general on reals. But that doesn't mean we can't compute with reals in many useful situations.

[Mario Carneiro]

yeah, the quote above is only half correct - decide uses decidability, norm_num uses proof term generation and is not limited to lean-computable functions

[Oliver Nash]

If we take axes of:

• bundled / unbundled
• computable / non-computable

Mathlib currently has 3 of the 2 x 2 = 4 ways that these two axes allow us to implement finite sets.

Our docs#Finset is extremely good but I sometimes think it should be renamed to something like CFinset with the C for computable so that we could introduce a non-computable version called Finset, and which would not demand any of the DecidableEq hypotheses in its API.

[Edward van de Meent]

what would a bundled (possibly infinite) set that is not computable look like?
nvm i misunderstood

[Edward van de Meent]

what is the third?

sets	bundled	unbundled
computable	docs#Finset	?
noncomputable	?	docs#Set.Finite

types	bundled	unbundled
computable	docs#Fintype	?
noncomputable	?	docs#Finite

[Mario Carneiro]

Fintype

[Edward van de Meent]

what hole does that go into?

[Edward van de Meent]

i'd say that's bundled and computable too, no?

[Edward van de Meent]

that goes into the third dimension of set/type

[Edward van de Meent]

or am i misinterpreting what "bundled" is supposed to mean?

[Edward van de Meent]

maybe i'm making the wrong kind of table...

thing	bundled	data carrying	computable	set	type
docs#Finset	:check:	:check:	:check:	:check:	:cross_mark:
docs#FintypeCat	:check:	:check:	:check:	:cross_mark:	:check:
docs#Fintype	:cross_mark:	:check:	:check:	:cross_mark:	:check:
docs#Set.Finite	:cross_mark:	:cross_mark:	:cross_mark:	:check:	:cross_mark:
docs#Finite	:cross_mark:	:cross_mark:	:cross_mark:	:cross_mark:	:check:

[Ching-Tsun Chou]

What does "bundled/unbundled" mean here?

[Ching-Tsun Chou]

For that matter, what does 'data carrying" mean here?

[Ching-Tsun Chou]

It also seems to me that the decidability of a theory is not necessarily related to the "computability" of the objects that the theory talks about. For example, there are decidable theories of real numbers (https://en.wikipedia.org/wiki/Decidability_of_first-order_theories_of_the_real_numbers), but I guess the reals are not considered computable in Lean?

[Kevin Buzzard]

Yes, mathematicians like there to be only one real numbers, so we go with the classical ones in classical logic.

[Kevin Buzzard]

Data carrying means that you can have two terms of type Fintype X and they're not definitionally equal.

[Ching-Tsun Chou]

Could you give an example?

[Trebor Huang]

The theoy of real numbers might as well be "talking about" real algebraic numbers, since there's no first order axioms stating anything about limits. Algebraic numbers are of course computable.

[Johan Commelin]

@Ching-Tsun Chou Data carrying means that Fintype X is not in Prop but in Type u for some u. Concretely, Fintype X under the hood carries a list that enumerates the elements of X, and that list can be used for computations. Different permutations of this list will lead to different terms of type Fintype X. They will be propositionally equal, because we've modded out by permutations, but they still will not be definitionally equal.

[Ching-Tsun Chou]

@Johan Commelin Thanks a lot for the explanation!

[Edward van de Meent]

Ching-Tsun Chou said:

What does "bundled/unbundled" mean here?

i didn't put docs#Fintype with "bundled" because Fintype a is an additional assumption on top of a:Type u, compared to something like a:TypeOfFiniteTypes.{u}

[Adam Topaz]

We do have docs#FintypeCat

[Edward van de Meent]

i'd say that fits the bill, yea :idea:

[Ching-Tsun Chou]

I still don't quite understand Fintype. I understand Finite: Finite(Nat) is a proposition which is (and can be proved to be) false. But what is Fintype(Nat)? It is not a proposition, but it must be false in some sense, right?

[Kyle Miller]

Fintype Nat is an empty type (concretely, it's equivalent to Empty)

[Adam Topaz]

You can think of elements of the type Fintype Nat as elements A : Finset Nat which contain every natural number. Of course there is no such A. In this case we would say that elements of Fintype X "contain data", namely the data of the Finset X which contain every element of X.

[Kyle Miller]

I'm probably missing some theorems here, but it's not hard to create this equvialence:

import Mathlib

theorem not_nonempty_fintype_of_infinite (α : Type*) [h : Infinite α] : ¬ Nonempty (Fintype α) := by
  rw [← not_finite_iff_infinite] at h
  rintro ⟨h'⟩
  exact absurd (inferInstance : Finite α) h

example : Fintype Nat ≃ Empty where
  toFun := by
    intro h
    exact (not_nonempty_fintype_of_infinite ℕ ⟨h⟩).elim
  invFun := nofun
  left_inv := by
    intro h
    exact (not_nonempty_fintype_of_infinite ℕ ⟨h⟩).elim
  right_inv := by
    rintro ⟨⟩

[Kyle Miller]

Of course there's also the following, but I sort of like seeing that Fintype Nat "is" Empty.

example : IsEmpty (Fintype Nat) := by
  rw [isEmpty_fintype]
  infer_instance

[Abraham Solomon]

Ching-Tsun Chou said:

I still don't quite understand Fintype. I understand Finite: Finite(Nat) is a proposition which is (and can be proved to be) false. But what is Fintype(Nat)? It is not a proposition, but it must be false in some sense, right?

In these situations it often helps to use #check and #print, using check you can see Fintype and Finset have the same signature; but Finite is different:

#check Fintype --Fintype.{u_4} (α : Type u_4) : Type u_4
#check Finset -- Finset.{u_4} (α : Type u_4) : Type u_4
#check Finite -- Finite.{u_1} (α : Sort u_1) : Prop

Now if you print them:

/-
class Fintype.{u_4} : Type u_4 → Type u_4
number of parameters: 1
constructor:
Fintype.mk : {α : Type u_4} → (elems : Finset α) → (∀ (x : α), x ∈ elems) → Fintype α
fields:
elems : Finset α
complete : ∀ (x : α), x ∈ Fintype.elems
-/

and

/-
structure Finset.{u_4} : Type u_4 → Type u_4
number of parameters: 1
constructor:
Finset.mk : {α : Type u_4} → (val : Multiset α) → val.Nodup → Finset α
fields:
val : Multiset α
nodup : self.val.Nodup
-/

You can see how Finset calls nodup on Multiset, and Fintype uses Finset

[Ching-Tsun Chou]

Thanks for the explanations! I understand now. Both Finite Nat and Fintype Nat are uninhabited types:

example (h : Finite Nat) : False := by
  simp [not_finite Nat]

example (h : Fintype Nat) : False := by
  simp [not_finite Nat]

The only difference is that Finite Nat is also a proposition, but in Lean propositions are types as well.