Strange type error with fintype_sdiff

Stream: maths

[Jake Levinson]

I ran into a strange error where (A \ B).to_finset appears to acquire two incompatible meanings. Here is a #mwe:

import tactic
import data.set.basic

open_locale classical

example {X : Type} [fintype X]
  (p : finset X → Prop)
  (h : ∀ (A : set X), p A.to_finset)
  (A B : set X) : p (A \ B).to_finset :=
begin
  exact h (A \ B),  -- error!
end

The error message is:

invalid type ascription, term has type
  p
    (@set.to_finset X (A \ B)
       (@subtype.fintype X (λ (x : X), x ∈ A \ B) (λ (a : X), classical.prop_decidable (a ∈ A \ B)) _inst_2))
but is expected to have type
  p
    (@set.to_finset X (A \ B)
       (@set.fintype_sdiff X (λ (a b : X), classical.prop_decidable (a = b)) A B
          (@subtype.fintype X (λ (x : X), x ∈ A) (λ (a : X), classical.prop_decidable (a ∈ A)) _inst_2)
          (@subtype.fintype X (λ (x : X), x ∈ B) (λ (a : X), classical.prop_decidable (a ∈ B)) _inst_2)))
state:
X : Type,
_inst_2 : fintype X,
p : finset X → Prop,
h : ∀ (A : set X), p A.to_finset,
A B : set X
⊢ p (A \ B).to_finset

If I'm reading this correctly, the issue is that (A \ B).to_finset is in interpreted as subtype.fintype X (λ (x : X), x ∈ A \ B) when created using the hypothesis h, but has set.fintype_sdiff in the goal.

Replacing exact h (A \ B) by refine h (A \ B) or change h (A \ B) doesn't work, but convert h (A \ B) does. (change gives a "not definitionally equal to the goal" error, while refine gives the same error message as above). Similarly apply h fails to unify.

Any idea why this happens? It would be nice not to have to unexpectedly replace various hypotheses h' by (by convert h') in random downstream places.

[Jake Levinson]

Actually, I just tried this in term mode and the error message simplifies:

example {X : Type} [fintype X]
  (p : finset X → Prop)
  (h : ∀ (A : set X), p A.to_finset)
  (A B : set X) : p (A \ B).to_finset := h (A \ B)

--synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
--  A.fintype_sdiff B
--inferred
--  subtype.fintype (λ (x : X), x ∈ A \ B)

[Eric Wieser]

Removing open_locale classical might help

[Jake Levinson]

If I remove it, I have to supply decidability instances myself, everywhere I want to use finite set stuff...

[Mario Carneiro]

the issue is that the decidability instance (here fintype instance) is not the "natural" one for the expression so you get diamond problems

[Eric Wieser]

Yes, but by doing so you'd be saying "this lemma is true for any algorithm for decidability" and not the current "this lemma only applies for this particular non-algorithm"

[Eric Wieser]

It's possible that's not enough to fix your problem here though

[Mario Carneiro]

your mwe is missing imports btw

[Eric Wieser]

Probably you want

open_locale classical

example {X : Type} [fintype X]
  (p : finset X → Prop)
  (h : ∀ (A : set X) [fintype A], p A.to_finset)
  (A B : set X) : p (A \ B).to_finset :=
begin
  exact h (A \ B),
end

(untested)

[Jake Levinson]

Oh sorry, I'll edit those in.

[Jake Levinson]

Eric, that seems to give the same error (diamond).

[Jake Levinson]

My goal here was to be able to work with finite sets without having to think about decidability. I've mostly been using variables {X : Type} [fintype X] and then working with set X and set.finite. But, there was a lemma where I needed to say something about cardinalities, so I was using set.to_finset.card which led to this situation.

[Kevin Buzzard]

You can do this but setting it up is more delicate than you think. As Eric says, we've discovered a problem with open_locale classical at the top of a file: you end up creating statements which say "this lemma is true but you have to use the classical algorithm to prove decidability" as opposed to "this lemma is true regardless of which algorithm the type class inference system discovers for decidability" (and it might well find a non-classical one even if you have classical decidability switched on, because there are others around). The fix is something like this: remove open_locale classical and see what breaks. If the proof of your lemma breaks, add the classical tactic in the proof. If the statement breaks because lean can't define a decidability instance, add the decidability assumption in square brackets in the statement.

[Kevin Buzzard]

Basically open_locale classical creates diamonds

[Kevin Buzzard]

So this works:

import tactic
import data.set.basic

open_locale classical

example {X : Type} [fintype X]
  (p : finset X → Prop)
  (h : ∀ (A : set X) [fintype A], p A.to_finset)
  (A B : set X) : p (A \ B).to_finset :=
begin
  convert h (A \ B),
end

[Kevin Buzzard]

and this works too:

import tactic
import data.set.basic

example {X : Type} [fintype X]
  (p : finset X → Prop)
  (h : ∀ (A : set X) [fintype A], by exactI p A.to_finset)
  (A B : set X) [fintype (↥(A \ B : set X))] : p (A \ B).to_finset :=
begin
  exact h (A \ B)
end

[Kevin Buzzard]

and if you think that's ugly, you might want to consider switching to the Prop valued version of everything i.e. set.finite (make p a function on finite sets instead of finsets etc and completely remove all the constructive stuff)

[Reid Barton]

Is fincard or whatever it was called a thing yet?

[Yaël Dillies]

docs#nat.card ?

[Reid Barton]

Was there a version for sets specifically? I mean, nat.card s would work if s : set X too, I suppose.

[Jake Levinson]

Thanks all for the explanations, that makes more sense now. I have indeed been trying to stick to set.finite in order to avoid issues around constructive stuff. The only place I needed it so far was for cardinalities and I only used set.tofinset because I didn't know what else to use other than finset.card. Is nat.card s the right thing to use for set.finite instead?

[Jake Levinson]

Some followups to this. I am still finding it hard to work with / around this. For example, previously I could write

open_locale classical

lemma card_of_diff_singleton {X : Type} [fintype X]
  (B : set X) (b : X) (hb : b ∈ B) :
  (B \ {b}).to_finset.card + 1 = B.to_finset.card := sorry

To fix this, I have to add [fintype B] [fintype (B \ {b} : set X)] (I'm not sure why [fintype (B \ {b})] doesn't work; it says it is missing a has_singleton instance). The proof I had also required [decidable_eq X].

Is there a way to use this directly with the dot notation? Lean is still not able to understand (B \ {b}).to_finset, so altogether the new lemma statement is

lemma card_of_diff_singleton' {X : Type} [fintype X] [decidable_eq X]
  (B : set X) [fintype B]
  (b : X) (hb : b ∈ B) [fintype (B \ {b} : set X)] :
  (@set.to_finset _ (B \ {b}) _inst_4).card + 1 = B.to_finset.card := sorry

This seems a lot more complicated than the original one, I don't know if this is unavoidable or if there is a better way. I have also taken a look at nat.card but am not sure where to find lemmas related to it (the file defining it doesn't have any and Lean autocomplete doesn't seem to know many lemmas related to it).

[Jake Levinson]

Kevin Buzzard said:

and if you think that's ugly, you might want to consider switching to the Prop valued version of everything i.e. set.finite (make p a function on finite sets instead of finsets etc and completely remove all the constructive stuff)

This is indeed what I am doing (everywhere else), except I occasionally want to use some cardinality facts.

[Ruben Van de Velde]

Did you try nat.card?

[Yaël Dillies]

I would advise you to stick to finset and deal with the few decidability instances you'll need. It's much cleaner in my experience.

[Kevin Buzzard]

This is probably true but I want it to be not true. I would like to see a usable propositional finite type typeclass and to guide people away from this constructivist nonsense when it has nothing to do with what they actually want to do

[Bhavik Mehta]

Kevin Buzzard said:

This is probably true but I want it to be not true. I would like to see a usable propositional finite type typeclass and to guide people away from this constructivist nonsense when it has nothing to do with what they actually want to do

I don't think finset is at all constructive, it's often exactly the useful notion for formalising actual mathematics!

[Kevin Buzzard]

My motivation is simply the observation that Jake has written some perfectly reasonable-looking lean code at the top of this thread and it doesn't work

[Kevin Buzzard]

I agree that finset must have its uses somewhere but to give a counterpoint Maria just formalised finite adeles as elements of products of p-adic fields which were integral at all but finitely many places and here set.finite worked like a charm

[Jake Levinson]

Yaël Dillies said:

I would advise you to stick to finset and deal with the few decidability instances you'll need. It's much cleaner in my experience.

I actually started out using finset and switched to set.finite because I kept wanting to do various constructions that were more convenient to express using set than finset. For example, compare

example {X : Type} [fintype X] (A : set X) (p : set X → Prop) :
  set (set X) := {B : set X | p B ∧ B ⊆ A}

open_locale classical
example {X : Type} [fintype X] (A : finset X) (p : finset X → Prop) :
  finset (finset X) := {B : finset X | p B ∧ B ⊆ A}.to_finset

That extra .to_finset is pretty minor in this example, but (a) it relies on open_locale classical, and (b) I think there were more significant cases where I either didn't know how to express something using finset, or it became challenging to convert it from a set. (Without open_locale classical I'm also not sure how to make the finset (finset X) object work!)

I thought using set.finite would be easier because everything would just be a set which seems to have a bigger library. But then I still needed to occasionally use cardinality.

[Bhavik Mehta]

For your second case, you can use A.powerset.filter p

[Yaël Dillies]

Also, finset (finset X) just works!

[Jake Levinson]

Okay, so

example {X : Type} [fintype X] (A : finset X)
  (p : finset X → Prop) [decidable_pred p] :
  finset (finset X) := A.powerset.filter p

I see... but then what if p is something I have introduced in the middle of a proof? I have to supply extra decidable_pred (blah blah) assumptions in my lemma statement?

[Jake Levinson]

Yaël Dillies said:

Also, finset (finset X) just works!

Hmm, what do you mean?

[Yaël Dillies]

finset (finset X) is a type like any other.

[Yaël Dillies]

Jake Levinson said:

what if p is something I have introduced in the middle of a proof? I have to supply extra decidable_pred (blah blah) assumptions in my lemma statement?

Yes, but there is a handful of common decidability assumptions that cover basically everything. For example, docs#decidable_eq.

[Jake Levinson]

@Yaël Dillies I have managed to follow your instructions a little. It leads me a bit down the rabbit hole of trying to understand decidability (and the library around it), which I have very little intuition for... but I did manage to get those lemmas fixed now. Thanks :smile:

On the whole, set.finite seems to be OK as a general-purpose way to work with an "arbitrary-ish" finite set X and various subsets of it -- with the exception of this one statement involving cardinality, I haven't otherwise had to think much about decidability. And the code is otherwise relatively short and readable (going back to using open_locale classical now that the one lemma is fixed).