What is Trunc?

Stream: new members

[Ching-Tsun Chou]

For example: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Fintype/Card.html#Fintype.truncEquivFinOfCardEq
I don't understand the discussion about "computable" at all.

[Kyle Miller]

Trunc X is the quotient of X by the relation fun x y => True. That is, every pair of elements becomes equal in the quotient.

It's a type-valued version of Nonempty X.

[Aaron Liu]

docs#Fintype is defined as a docs#Finset which does not miss any elements.
docs#Finset is defined as a docs#Multiset which has no duplicates.
docs#Multiset is defined as the quotient of docs#List by docs#List.Perm.
So when you have a Fintype α argument in docs#Fintype.truncEquivFinOfCardEq, to the compiler this is really just a list with some wrappers. Since you have a list of all the elements of your type, you can match up element-by-element the lists [a0, a1, a2, ...] with [0, 1, 2, ...], so a0 gets mapped to 0, a1 gets mapped to 1, etc.
But we have a problem! Since Fintype is a quotient, we need to make sure that equal Fintype instances get mapped to equal Equivs. This is not the case right now, so the α ≃ Fin n gets wrapped in a Trunc, which the quotient by the always-true relation. That way, Quot.sound will say that any two elements of Trunc (α ≃ Fin n) are equal.

[Ching-Tsun Chou]

Thanks for the explanation. But a Fintype is a type. What does it mean for two Fintype instances to be "equal"? Also, everything is finite here, what does the"computable" vs "noncomputable" distinction buy us?

[Aaron Liu]

Ching-Tsun Chou said:

But a Fintype is a type. What does it mean for two Fintype instances to be "equal"?

Exactly the same as it means for two LE instances to be equal, or two DecidableEq instances, or two Add instances. Equality works the same for all types.

[Aaron Liu]

Ching-Tsun Chou said:

Also, everything is finite here, what does the "computable" vs "noncomputable" distinction buy us?

What do you mean by this? "computable" means that I can #eval my code, which is better than not being able to #eval my code, all other things being equal.

[Ching-Tsun Chou]

How about leaving out the Trunc(namely, conflate Fintype.truncEquivFinOfCardEq and Fintype.equivFinOfCardEq) but having #eval do what it does now as if there is a Trunc?

[Aaron Liu]

That would be unsafe, and allow you to prove False. Basically, this is the distinction between docs#Quot.out and docs#Quot.unquot.

[Chris Wong]

Yeah, since Trunc introduces the idea that any two values are equal, bypassing it will mean that other code assumes that x = y but your code has x ≠ y.