finset coercion strangeness

Stream: general

[Peter Nelson]

I am trying to define a coercion of finsets of a subtype to finsets of a type, by just taking the image of the subtype-type coercion. The instance below seems to define this coercion correctly, but when I try to give some simple lemmas, I get strange behaviour:

instance coe_subtype_subset {α : Type*}{Y: set α} :
    has_coe (finset ↥Y) (finset α) := ⟨λ X, X.image subtype.val⟩

lemma coe_subtype_union {α : Type*}{Y: set α}(X₁ X₂ : finset ↥Y) :
    ((X₁ ∪ X₂) : finset α) = ((X₁ : finset α) ∪ (X₂ : finset α)) :=
begin
    exact rfl,
end

The fact that exact rfl works as a proof for the lemma seems odd to me, but what is odder is that when I invoke the lemma at some X₁ X₂ later, I get the trivial hypothesis this: ↑X₁ ∪ ↑X₂ = ↑X₁ ∪ ↑X₂ rather than the intended this: ↑(X₁ ∪ X₂) = ↑X₁ ∪ ↑X₂. I don't see another way to state that my coercion commutes with union - what am I doing wrong?

[Ruben Van de Velde]

I think this is because Lean does "outside-in elaboration" (?): it sees ((X₁ ∪ X₂) : finset α), realizes that you want X₁ ∪ X₂ to be a finset α, and derives that you want ∪ to be a function ? → ? → finset α, and the only ∪ that matches is finset α → finset α → finset α´, so it coerces X₁ and X₂ to finset α` before taking the union.

I haven't tried, but maybe (((X₁ ∪ X₂) : finset ↥Y) : finset α) on the LHS will yield better results

[Heather Macbeth]

I also haven't tried it, but assuming the problem is indeed the outside-in elaboration, here's a previous thread where I hit the same problem and was offered some solutions:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60has_inv.60.20in.20rings

[Kevin Buzzard]

Ruben Van de Velde said:

I think this is because Lean does "outside-in elaboration" (?): it sees ((X₁ ∪ X₂) : finset α), realizes that you want X₁ ∪ X₂ to be a finset α, and derives that you want ∪ to be a function ? → ? → finset α, and the only ∪ that matches is finset α → finset α → finset α´, so it coerces X₁ and X₂ to finset α` before taking the union.

I haven't tried, but maybe (((X₁ ∪ X₂) : finset ↥Y) : finset α) on the LHS will yield better results

and then you shouldn't need any type annotations on the RHS.

[Peter Nelson]

Thank you, that did the trick - however, I'm getting some more strange behaviour. I am running into a problem when applying the lemma within a structure. The below is a minimal problematic example isomorphic to my own:

Essentially, when I invoke the union lemma above, I can get into a situation where a seemingly tautological goal state involving the equality of two coerced finsets can't be proved by rw/refl/simp/trivial. I have tried extensive unfolding to try to find how the two sides of the equality are actually different, to no avail. The only suggestion I can find that they differ is with --set_option pp.all true, but the difference is so deeply buried in abstraction that I can't make any sense of it.

In this example, apply image_union does solve my problem, but I am running into similar issues with more complicated examples that cause linarith to break, so I would really like to understand the issue.

import data.finset

noncomputable theory
open_locale classical
open finset
universe u

-- Coercion stuff

instance coe_subtype_finset {α : Type*}{Y: set α} :
    has_coe (finset Y) (finset α) := ⟨λ X, X.image subtype.val⟩

lemma union_lemma {α : Type*}{Y: set α}(S T : finset Y):
    (((S ∪ T): finset Y): finset α) = S ∪ T := by apply image_union

-- Structure

structure subadditive_fn_on (γ : Type u) :=
(f : finset γ → ℕ )
(hf : ∀ (S T : finset γ), f (S ∪ T) ≤ f S + f T)

-- restrict the subadditive function to a subset Y of the domain

def restr {γ : Type u}(F : subadditive_fn_on γ)(Y: set γ) : subadditive_fn_on (↥Y):=
{
    f := λ S, F.f (S: finset γ),
    hf := λ S T,
    begin
         convert F.hf S T,
        -- we now have S T: finset ↥Y
        -- goal state is ⊢ ↑(S ∪ T) = ↑S ∪ ↑T
        -- apply image_union, WORKS
        rw ← union_lemma,
        -- goal state is now ⊢ ↑(S ∪ T) = ↑(S ∪ T)
        refl, -- Doesn't work...
    end
}

[Reid Barton]

This is a decidable_eq instance mismatch issue

[Reid Barton]

convert rfl can take care of it

[Peter Nelson]

Thank you!

What would be the best way to, say, handle an invocation of linarith involving multiple expressions that are 'equal' in this way? Do I have to explicitly insert hypotheses that assert the equality of all relevant pairs (how do I even do this when they are syntatically identical?), or is there a way to equip linarith with the ability to see such equalities automatically?

[Floris van Doorn]

convert rfl does basically the same as congr', right?

[Mario Carneiro]

pretty much

[Peter Nelson]

Is there a way to stop the mismatch from happening in the first place?

[Floris van Doorn]

In this case: union_lemma states something about the union of two finsets, which is only defined for finsets over a decidable type. If you add [decidable_eq \a](or maybe {h : decidable_eq \a}) as an argument to union_lemma, I expect that the issue will resolve.

[Floris van Doorn]

In this case, adding [hY : decidable_eq Y] to union_lemma works, but I think that might result in problems in other examples.

[Peter Nelson]

Is there a good general solution to this? By this I mean one where [decidable_eq Y] is not being thrown indiscriminately into various lemma statements, and yet where apparently equal expressions are actually equal in a way that doesn't need to be explicitly nailed down and hit with congr each time. All I can think of is to bundle decidable_eq with finset in its own type, and essentially rewrite the finset API with that. All this will be occuring with multiple types, so a variable declaration isn't a solution.

[Peter Nelson]

A more specific question - is there a way to make sure that all instances of decidable_eq come from open_locale classical rather than from elsewhere?

[Mario Carneiro]

Unfortunately this won't help, because there are theorems that contain partial dec_eq proofs in them that are not the classical one

[Mario Carneiro]

for example "finset A has dec_eq if A does"

[Mario Carneiro]

which will cause diamond problems along the lines finset.dec_eq (classical.dec A) != classical.dec (finset A)

[Mario Carneiro]

@Pim Spelier Take note, I think this is an example that helps show why we made polynomials classical

[Mario Carneiro]

(referencing https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Noncomputable.20polynomials/near/208745260 )

[Peter Nelson]

For what I'm doing, (I think) I don't care about decidable_eq in any sense explicitly - it just apparently crops up implicitly when I want to describe the union of finsets. Does this mean there is no solution to my problems that doesn't involve keeping track of instances very carefully?

[Bryan Gin-ge Chen]

I think the issue that prompted @Yakov Pechersky to open #5622 is another example of pain arising from decidable_eq + classical. Are there some general recommendations here? Some linter, or something to add to a library note?

[Yakov Pechersky]

(deleted)

[Yury G. Kudryashov]

In my experience, the best we can do in API lemmas is to assume decidability of all propositions used both in LHS and RHS. In particular, do not assume [decidable_eq α] if we actually need [decidable_pred (s : finset α)]

[Yury G. Kudryashov]

This way lemmas will work both in classical and non-classical settings.

[Yakov Pechersky]

The issue with equiv.perm.sign in the PR was that the definition of sign is explicit in requiring [decidable_eq α] but some lemmas provided it just by open_locale classical instead of having it as a constraint in the arguments.

[Bryan Gin-ge Chen]

@Yury G. Kudryashov Can you give an example where [decidable_pred (s : finset α)] is needed? Is there a typo or is there a coercion from finsets to predicates that I'm missing?

[Yury G. Kudryashov]

This is a typo. I meant [∀ x, decidable (x ∈ s)]

[Yury G. Kudryashov]

I don't remember if we have definitions that take [∀ x, decidable (x ∈ s)] as an argument. If not, then my example is irrelevant.

[Yury G. Kudryashov]

Yes, we have: docs#finset.piecewise

[Yury G. Kudryashov]

E.g., docs#finset.piecewise_coe takes two [decidable] arguments instead of deducing one of them from the other.

[Yury G. Kudryashov]

And docs#finset.piecewise_insert takes all [decidable] arguments it needs to use.

[Yury G. Kudryashov]

Possibly, we should require that the type of a lemma (not a proof term) involves no non-trivial [decidable] instances.

[Yury G. Kudryashov]

In particular, if we need both [decidable_eq α] and [decidable_eq (option α)] to state the lemma, then both should be present as arguments.

[Bryan Gin-ge Chen]

Concretely, that means some lemmas in src/group_theory/perm/option.lean in #5593 should take [decidable_eq (option α)] as well?

[Yakov Pechersky]

I think just on α is fine, because:

import group_theory.perm.sign
import data.equiv.option

variables {α : Type*} [decidable_eq α]
#check (show decidable_eq (option α), by apply_instance)
/-
show decidable_eq (option α), from λ (a b : option α), option.decidable_eq a b : decidable_eq (option α)
-/

[Eric Wieser]

Can we have a linter that verifies lemma statements do not use classical.decideable?

[Mario Carneiro]

I don't think we should necessarily do something about all such examples