# Zulip Chat Archive

## Stream: general

### Topic: fintype

#### Chris Hughes (Feb 27 2018 at 21:23):

What's the reason fintype isn't marked as Prop?

#### Simon Hudon (Feb 27 2018 at 21:28):

I think it can't be `Prop`

because its accessor `elems`

has a non-`Prop`

type

#### Chris Hughes (Feb 27 2018 at 21:35):

Exists is a Prop, so presumably it's possible to define it in a way such that it is a Prop. I thought that since it's a subsingleton, it may as well be a Prop, but there's probably a good reason why not.

#### Simon Hudon (Feb 27 2018 at 21:37):

That's true. The difference is that `Exists`

is defined using `inductive`

not `structure`

. Inductive doesn't come with accessors (in the case of `Exists`

, the accessors could also be called the axiom of choice).

#### Simon Hudon (Feb 27 2018 at 21:38):

I think allowing `fintype`

to be `Prop`

would render every constructivist paranoid

#### Simon Hudon (Feb 27 2018 at 21:38):

(because merely declaring a structure could quietly add the axiom of choice into your development)

#### Kevin Buzzard (Feb 27 2018 at 21:39):

I think allowing

`fintype`

to be`Prop`

would render every constructivist paranoid

I think they're already pretty paranoid if they're constructivists...

#### Simon Hudon (Feb 27 2018 at 21:40):

Should I say "paranoider"?

#### Chris Hughes (Feb 27 2018 at 21:41):

Mario mentioned that he wanted his proofs of `[fintype \a] \r [fintype \b] \r [fintype (\a \r \b)]`

to be computable. Not sure why, especially since choice is everywhere in mathlib

#### Simon Hudon (Feb 27 2018 at 21:44):

Even when you assume the axiom of choice, constructive functions are great. They allow you to build programs without efforts

#### Kevin Buzzard (Feb 27 2018 at 21:55):

Try calculations with integers

#### Kevin Buzzard (Feb 27 2018 at 21:56):

What do you mean by "forever"?

#### Simon Hudon (Feb 27 2018 at 21:56):

wrong topic

#### Kevin Buzzard (Feb 27 2018 at 21:56):

damn topics

#### Mario Carneiro (Feb 28 2018 at 00:55):

`fintype`

and `finite`

exist exactly so that you can decide whether or not you want to work in Prop

#### Chris Hughes (Feb 28 2018 at 01:01):

Didn't know about finite. I'll have to look at it.

#### Reid Barton (Sep 10 2019 at 14:36):

Prompted by Scott's PR #1427, I just realized that `fintype`

is not the same as the usual constructive notion of finite. I'm not really sure how to think about this though. What is an example of a `fintype`

which is not finite?

#### Reid Barton (Sep 10 2019 at 14:36):

(Here, finite means there is a bijection to `fin n`

for some `n`

and so in particular it implies that the type has decidable equality)

#### Reid Barton (Sep 10 2019 at 14:37):

Maybe another question is: is `fintype`

"correct"?

#### Floris van Doorn (Sep 10 2019 at 15:49):

Good point. Maybe we can prove that every `fintype`

has decidable equality.

You can definitely prove `nonempty (decidable_eq \a)`

, and maybe you can do some trickery to get decidable equality, since that is a subsingleton?

import data.fintype def dec {α : Type*} [h : fintype α] : ∀x y : α, x = y ∨ x ≠ y := begin unfreezeI, rcases h with ⟨⟨s, hs⟩, h2s⟩, revert hs h2s, refine quotient.rec_on_subsingleton s _, intros l hl h2l x y, have hx := h2l x, have hy := h2l y, simp [list.mem_iff_nth_le] at hx hy, rcases hx with ⟨n, hn, rfl⟩, rcases hy with ⟨m, hm, rfl⟩, by_cases h : n = m, { simp [h] }, { right, refine mt _ h, simp [list.nodup_iff_nth_le_inj] at hl, apply hl } end

#### Floris van Doorn (Sep 10 2019 at 16:04):

So to answer your question, Our notion of `fintype`

is (at least) very close to the correct one.

I have a very bad intuition of the failure to eliminate from propositions to subsingletons: in HoTT that is provable.

If we replace `(complete : ∀ x : α, x ∈ elems)`

by something which is type-valued and says the same thing, then we can definitely prove decidable equality.

#### Reid Barton (Sep 10 2019 at 16:05):

I'm pretty sure you can't obtain `decidable_eq`

constructively, because `fintype`

just gives you a bunch of elements of the type and some useless props.

#### Reid Barton (Sep 10 2019 at 16:05):

It doesn't give you any way to consume an element of the type

#### Chris Hughes (Sep 10 2019 at 16:32):

Simon has a PR doing `enumerable`

as a bijection with `fin n`

. I'd rather `fintype`

remained a subsingleton.

#### Chris Hughes (Sep 10 2019 at 16:37):

Or a `Prop`

#### Reid Barton (Sep 10 2019 at 17:23):

I agree it should be a subsingleton. For example one "fix" (if it is a fix) would be to just add a field with a `decidable_eq`

instance.

#### Reid Barton (Sep 10 2019 at 17:23):

As far as I can tell, this is ehat ssreflect does

#### Floris van Doorn (Sep 10 2019 at 17:38):

When I say something type-valued, it will remain a subsingleton. But probably the easiest is to just add a `decidable_eq`

instance, which I think would be very helpful.

#### Mario Carneiro (Sep 11 2019 at 05:15):

I gave an example to Simon recently about this. Consider the quotient `Q`

of nat (treated as enumerating programs) that identifies programs that both halt or both do not halt. Classically, this is a two element set, and we can computably construct a `fintype Q`

with two elements (the proof that this enumeration is complete requires LEM, but it is still lean-computable). But deciding equality on this type is equivalent to the halting problem.

#### Mario Carneiro (Sep 11 2019 at 05:18):

I also argued that putting a decidable_eq argument in the definition would mean an instance `fintype A -> decidable_eq A`

and I'm not sure we want to make the `decidable`

typeclass search any larger than it already is

#### Mario Carneiro (Sep 11 2019 at 05:23):

By the way, it's not actually clear if we follow the letter of that definition of finite. `fintype`

is equivalent to a `bijection`

from `fin n`

for some `n`

(not an `equiv`

)

#### Reid Barton (Sep 11 2019 at 11:20):

Nice example. It also gives me a better appreciation for Floris's `dec`

. We need LEM to hold for equality on our type, just not computably. (Contrast with examples of subfinite sets which are not finite, which can be constructed from failures of LEM.)

#### Reid Barton (Sep 11 2019 at 11:22):

I'm pretty sure that in this context, "bijection" is supposed to be interpreted as `equiv`

. (I'm not as sure how "there exists" is meant to be interpreted...) At any rate, that nlab page claims further down that finite sets have decidable equality (but maybe one can quibble over the meaning of "have"?)

#### Johan Commelin (Sep 11 2019 at 11:28):

The joys of constructive math... all of a sudden not only your nouns have multiple interpretations, but also your adjectives, your verbs, and everything...

Last updated: May 10 2021 at 00:31 UTC