fintype implies decidable_eq

Stream: general

[Thorsten Altenkirch]

It seems to me that fintype A shoud imply decidable_eq A but there doesn't seem to be such a proof in the mathlib. Why is this?

[Kyle Miller]

Here's an indirect reason why not: docs#Prop.fintype

@Reid Barton has commented about how mathlib's fintype is strange in this way.

[Kyle Miller]

For example, you need decidable equality to get docs#fintype.trunc_equiv_fin, and having such an equivalence would imply decidable equality.

[David Renshaw]

You can use docs#classical.dec_eq

[Kevin Buzzard]

fintype is neither truly classical or truly constructive, so in some sense it's a good fit for nobody.

[Eric Wieser]

I don't know what you mean by "truly constructive"

[Eric Wieser]

It's just maybe not the same meaning of fintype as some constructivists would use

[Eric Wieser]

If you want _that_ meaning, it's [fintype X] [decidable_eq X]

[Eric Wieser]

Just like [semiring R] [add_comm_monoid M] [module R M] is not the meaning of "module" that most mathematicians use; if you want that meaning, you write [ring R] [add_comm_group M] [module R M]

[Reid Barton]

It's more like... not any of the meanings of "finite" that constructivists use

[Kyle Miller]

I think it's fair to say that it's not not what you want out of a constructive fintype :smile:

[Reid Barton]

Actually from fintype I think you can prove the propositional version of decidable equality. So it's Lean's Prop vs data distinction getting in the way.

[David Renshaw]

How would that proof go?

[Reid Barton]

So you have a list of elements of your type that is known to contain every element (in the list.mem sense) with no duplicates. So now you take your two elements x and y that you want to compare for equality. From the list.mem hypothesis, each one is either equal to the first element of the list or contained in the rest of the list.
If they are both the first element, then of course they are equal. If only one is the first element, then they are distinct (because the list has no duplicates).
Otherwise, recurse on the rest of the list.

[Reid Barton]

You get the original list by doing cases on the quotient multiset, since the conclusion is a proposition.

[Eric Wieser]

propositional version of decidable equality.

that would have the same staetment as docs#decidable.eq_or_ne (but obviously without the decidable_eq argument), right?

[Eric Rodriguez]

so specifically {a} [fintype a] (x y : a) : x = y ∨ x ≠ y? with the axiom list empty?

[Eric Rodriguez]

  have hx := fintype.complete x,
  have hy := fintype.complete y,
  rw [←finset.mem_val, ←multiset.mem_to_list] at *,
  induction h : (fintype.elems a).val.to_list,

seems to be the intended proof, but then ih : (fintype.elems a).val.to_list = tl → x = y ∨ x ≠ y which is clear nonsense

[Reid Barton]

Well no LEM/choice anyways, no promises about other axioms

[Eric Wieser]

Can you give the mwe so that I can try your proof, @Eric Rodriguez?

[Eric Rodriguez]

import data.fintype.basic

example {a} [fintype a] (x y : a) : x = y ∨ x ≠ y :=
begin
  have hx := fintype.complete x,
  have hy := fintype.complete y,
  rw [←finset.mem_val, ←multiset.mem_to_list] at *,
  induction h : (fintype.elems a).val.to_list,
end

[Reid Barton]

You will need to figure out the exact induction hypothesis

[David Renshaw]

If a is Prop and x is True, isn't this example basically stating the law of excluded middle?

[Reid Barton]

If you have fintype Prop.

[Reid Barton]

Which isn't true, constructively

[Eric Rodriguez]

Ah, I think the correct way to do it is to prove the lemma for a general list l and just apply it in this specific case

[Eric Rodriguez]

Well, some nodup list.

[Eric Wieser]

I think lists are a distraction

[Eric Wieser]

Using the generalize tactic

import data.fintype.basic

example {a} [fintype a] (x y : a) : x = y ∨ x ≠ y :=
begin
  have hx := fintype.complete x,
  have hy := fintype.complete y,
  revert hx hy,
  generalize : fintype.elems a = s,
  intros hx hy,
  induction s using finset.cons_induction_on with z s hz ih generalizing hx hy,
  { cases hx },
  { simp_rw finset.mem_cons at hx hy,
    obtain rfl | hy := hy; obtain rfl | hx := hx,
    { left, refl },
    { right, exact ne_of_mem_of_not_mem hx hz },
    { right, exact (ne_of_mem_of_not_mem hy hz).symm },
    { exact ih hx hy} },
end

[Eric Wieser]

Or more concisely

import data.fintype.basic

lemma finset.eq_or_ne_of_mem {α} {s : finset α} {x y : α} (hx : x ∈ s) (hy : y ∈ s) : x = y ∨ x ≠ y :=
begin
  induction s using finset.cons_induction_on with z s hz ih generalizing hx hy,
  { cases hx },
  { simp_rw finset.mem_cons at hx hy,
    obtain rfl | hy := hy; obtain rfl | hx := hx,
    { left, refl },
    { right, exact ne_of_mem_of_not_mem hx hz },
    { right, exact (ne_of_mem_of_not_mem hy hz).symm },
    { exact ih hx hy} },
end

lemma fintype.eq_or_ne {a} [fintype a] (x y : a) : x = y ∨ x ≠ y :=
finset.eq_or_ne_of_mem (fintype.complete x) (fintype.complete y)

#print axioms fintype.eq_or_ne

[Thorsten Altenkirch]

Sorry. I didn't read all the responses. FinType means that for every element you have a proof that it appears in a finite set (ie a finite multiset without repetitions). The proof gives you a unique position for any element, and equality of positions is decidable. Hence equality of elements is decidable. Indeed the definition of FinType is equivalent to saying that there is an isomorphism of A with an initial segment of Nat.

However, I don't know wether strict Prop gets in your way here. Maybe the definition of FinType needs to be changed by replacing the exists with a Sigma. Being a FinType is not a proposition but a structure.

[Eric Wieser]

Thorsten Altenkirch said:

FinType means that for every element you have a proof that it appears in a finite set (ie a finite multiset without repetitions).

Yes

The proof gives you a unique position for any element

No, there is no concept of position in a finite set.

[Mario Carneiro]

A fintype is a structure, and it carries the list of elements in the type, but one of the components is the assertion that every element is in the list, and this is not a data-carrying assertion. For example if the list is [a, b] then we have ∀ x, x = a ∨ x = b but not ∀ x, x = a ⊕ x = b. You can't use a proof of an 'or' to construct an actual boolean telling you which side of the 'or' is true.

[Eric Wieser]

Maybe the definition of FinType needs to be changed by replacing the exists with a Sigma

Note that the "need" here, if there is one at all, is purely cosmetic. You can get exactly the behavior you want by writing [fintype X] [decidable_eq X].

[Mario Carneiro]

(and this decidable_eq X instance supplied directly by typeclass inference will almost certainly be better than the one based on fintype X, which is linear in the best case and would in most cases involve O(n) equality comparisons)

[Mario Carneiro]

In most cases when this kind of diamond situation arises we would bake the weaker typeclass as a field or parent of the stronger one, i.e. class fintype X extends decidable_eq X, so we would not be using this theorem in the first place, it would just be true by fiat

[Kyle Miller]

@Thorsten Altenkirch Just to elaborate upon the indirect reason I gave earlier, with mathlib's fintype you can construct fintype Prop (that's docs#Prop.fintype) since the underlying list [false, true] represents the finite set of elements by Lean's axioms and choice. If you could get a computable decidable_eq out of this, then you'd get that every proposition is decidable.

The other definition I mentioned, docs#fintype.trunc_equiv_fin, is the existence (via trunc) of an isomorphism with an initial segment with Nat that you mention, but it requires decidable_eq.

[Kyle Miller]

I'm ignorant of some terminology here: what does "strict Prop" mean?

[Eric Wieser]

I think it refers to Coq's SProp, which IIRC is Lean's Prop.

[Junyan Xu]

I think "strict Prop" means any two proofs of a Prop are equal (aka proof irrelevance). I think it's separate from propext, but let me note that if you use docs#psum (which isn't Prop) instead of docs#or to define list membership, then you lose access to propext and will have to use docs#trunc in order to pass list membership down to multiset membership.

[Thorsten Altenkirch]

Eric Wieser said:

Thorsten Altenkirch said:

FinType means that for every element you have a proof that it appears in a finite set (ie a finite multiset without repetitions).

Yes

The proof gives you a unique position for any element

No, there is no concept of position in a finite set.

And how do you define that an element occurs in a fintype. Ok, I suppose the problem is that you define this as a strict Prop. If you define it as a type this gives you a unique position.

This just confirms my suspicion that classical logic is the consequence of reducing everything to propositions.

[Thorsten Altenkirch]

Kyle Miller said:

Thorsten Altenkirch Just to elaborate upon the indirect reason I gave earlier, with mathlib's fintype you can construct fintype Prop (that's docs#Prop.fintype) since the underlying list [false, true] represents the finite set of elements by Lean's axioms and choice. If you could get a computable decidable_eq out of this, then you'd get that every proposition is decidable.

The other definition I mentioned, docs#fintype.trunc_equiv_fin, is the existence (via trunc) of an isomorphism with an initial segment with Nat that you mention, but it requires decidable_eq.

It is the definition of Prop in Lean 3+ where any two proofs of a proposition are definitionally equal. I think I may have started this with my 1999 LICS paper. In HoTT we use HProp, a proposition is a type with at most one element. In many situations strict Props are more convenient but they don't support important principles such as unique choice which holds in any topos and is provable in HoTT.

[Eric Wieser]

You might be looking for docs#fin_enum, which does give you a unique index for each element

[Thorsten Altenkirch]

Kyle Miller said:

Thorsten Altenkirch Just to elaborate upon the indirect reason I gave earlier, with mathlib's fintype you can construct fintype Prop (that's docs#Prop.fintype) since the underlying list [false, true] represents the finite set of elements by Lean's axioms and choice. If you could get a computable decidable_eq out of this, then you'd get that every proposition is decidable.

The other definition I mentioned, docs#fintype.trunc_equiv_fin, is the existence (via trunc) of an isomorphism with an initial segment with Nat that you mention, but it requires decidable_eq.

To respond to the first part: One can use Lean without exploiting non-classical principles. Or has this been outlawed?

[Eric Wieser]

What do you mean by "without exploiting non-classical principles"? That sounds like it means "by only exploiting classical principles", ie only usingclassical.choice!

[Kyle Miller]

@Thorsten Altenkirch I was hoping to address your original question: "there doesn't seem to be such a proof in the mathlib. Why is this?" That seems to me to be a concrete question about mathlib's fintype A and decidable_eq A, but I'm gathering that you're actually asking a counterfactual about why mathlib isn't designed in a different way?

With classical vs constructive math, I think there's also a third option that we seem to care more about here, which is Lean's computability, i.e., whether there exists a program that's able to compute the value in question while allowing one to rely on classical correctness proofs.

The Prop.fintype instance is computable in this sense. If you could compute a decidable_eq instance from a fintype instance in a Lean-computable way, then you'd get a Lean-computable decision procedure for every proposition (but we know there can't be such a program!)

Of course, if you embrace classical proofs and don't care about Lean computability, mathlib has docs#classical.dec_eq as @David Renshaw pointed out, and you don't need a fintype instance for that.

[Thorsten Altenkirch]

I wasn't intending to ask a general question about mathlib. It just seems to me that if I can constructively prove that A is a fintype then I can also constructively prove that it has a decidable equality. However, it seems that this implication isn't constructively provable in Lean.

I think constructive and classical Mathematics can live happily next to each other if there is some respect for each other. Forcing everything to be classical for no good reason isn't very respectful.

[Chris Hughes]

One of the main reasons we are classical even when they constructive proof is basically the same as the classical one, is because there are a lot of type class diamonds caused by different ways of proving decidability. This means that rewrites end up failing when there there is a different proof of decidability of the same proposition in the lemma I am using to rewrite and the goal. For example, if I had an instance saying fintypes had decidable equality, then there would be two ways of proving decidable equality of α ⊕ β when α and β are fintypes. One would be via the fact that the sum of fintype is a fintype and the other because the sum of two types with decidable eqaulity has decidable equality.

import data.fintype.basic
import logic.equiv.fin

class fintype2 (α : Type*) :=
( trunc_fin_equiv : trunc (Σ  n : ℕ, fin n ≃ α) )

instance {α : Type*} : subsingleton (fintype2 α) :=
⟨λ x y, by cases x; cases y; congr⟩

instance fintype2.decidable_eq {α : Type} [fintype2 α] : decidable_eq α :=
λ x y, show decidable (x = y), from
  trunc.rec_on_subsingleton (@fintype2.trunc_fin_equiv α _)
  (λ e, decidable_of_iff (e.2.symm x = e.2.symm y) (by simp))

instance sum.fintype2 {α β : Type} [fintype2 α] [fintype2 β] : fintype2 (α ⊕ β) :=
trunc.rec_on_subsingleton
  (@fintype2.trunc_fin_equiv α _) $
  trunc.rec_on_subsingleton
    (@fintype2.trunc_fin_equiv β _)
      (λ eβ eα, ⟨trunc.mk $
        ⟨eα.1 + eβ.1, fin_sum_fin_equiv.symm.trans
          (equiv.sum_congr eα.2 eβ.2)⟩⟩)


example {α β : Type} [fintype2 α] [fintype2 β] :
  @fintype2.decidable_eq (α ⊕ β) _ = @sum.decidable_eq α _ β _ := rfl --fails

[Eric Wieser]

@Thorsten Altenkirch said:

I wasn't intending to ask a general question about mathlib. It just seems to me that if I can constructively prove that A is a fintype then I can also constructively prove that it has a decidable equality.

I think the spelling of "constructively a fintype" the you're looking for is fin_enum.

[Reid Barton]

No. Being a "fintype" constructively is still a proposition (hProp). fin_enum is extra data.

[Reid Barton]

It would be trunc (fin_enum A).

[Chris Hughes]

This is a very good reason to remain classical in my opinion. It's not much fun battling around these diamonds and we really don't learn very much by battling these diamonds. I think we could be persuaded to remain constructive in many places if type theorists came up with some solution to this diamond problem, although I think any solution would necessarily give up some other nice properties of type checking. We're even thinking of making fintype a strict Prop to get rid of these problems.

[Rémi Bottinelli]

What would the point of a Proped fintype be given that finite exists (not a rethorical question)?

[Eric Wieser]

I think @Chris Hughes' claim is that it was considered to remove fintype entirely and only use finite. Personally I don't think we should do this, but it has certainly been discussed.

[Eric Wieser]

I'd pose the question in the other direction; what would be the point in a [constructive_fintype X] given we have [fintype X] [decidable_eq X]?

Thorsten Altenkirch said:

Forcing everything to be classical for no good reason isn't very respectful.

I don't think that this applies to requiring a longer spelling.

[Thorsten Altenkirch]

Ok so the suggestion is that I replace fintype by fin_enum? Is there a proof to show that fin_enum entails decidable_eq.
Ok another option is to define constructive_fintype in the way suggested by @Eric Wieser In this case I would remark that the current definition of fintype is a bit of an overkill. Instead of referring to a multiset with no duplicates one could just use a list. I thought that the current definition of fintype is just so that we always have decidable_eq.

[Bolton Bailey]

docs#fin_enum indicates that decidable_eq \alpha is in fact a field of the fin_enum class.
This is surprising because my intuition would be that you could derive decidable eq by sending elements through the mapping and using the decidable_eq on fin. Is there a reason why that field has to be there?

[Eric Wieser]

Yes, it's for the same reason that pow is a field of monoid even though you can derive it from one and mul. Mario already alluded to that above.

[Eric Wieser]

Instead of referring to a multiset with no duplicates one could just use a list.

If you do this, then there are two different ways to say that bool is finite; [tt, ff] or [ff, tt]. Using a multiset with no duplicates makes these two ways equal, but using a list does not.