fintype

Stream: general

[Chris Hughes]

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

[Simon Hudon]

I think it can't be Prop because its accessor elems has a non-Prop type

[Chris Hughes]

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]

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]

I think allowing fintype to be Prop would render every constructivist paranoid

[Simon Hudon]

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

[Kevin Buzzard]

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]

Should I say "paranoider"?

[Chris Hughes]

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]

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

[Kevin Buzzard]

Try calculations with integers

[Kevin Buzzard]

What do you mean by "forever"?

[Simon Hudon]

wrong topic

[Kevin Buzzard]

damn topics

[Mario Carneiro]

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

[Chris Hughes]

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

[Reid Barton]

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]

(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]

Maybe another question is: is fintype "correct"?

[Floris van Doorn]

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]

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]

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]

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

[Chris Hughes]

Simon has a PR doing enumerable as a bijection with fin n. I'd rather fintype remained a subsingleton.

[Chris Hughes]

Or a Prop

[Reid Barton]

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]

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

[Floris van Doorn]

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]

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]

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]

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]

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]

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]

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