typeclass instance resolution trouble...

Stream: new members

[Jon Bannon]

To get some experience, I am working to formalize nets in Lean using all of the lovely things about filters in mathlib. (Trying to prepare the way for more analysis.)

There is something here that I don't understand about typeclass resolution. The following code generates a "failed to synthesize typeclass instance" error. I have a feeling that it has something to do with the instance of the topological space. I am not sure what the problem is, though. Thanks, in advance!

import tactic
import order.directed
import order.filter.bases
import topology.basic
import topology.subset_properties

universes u v

open set filter
open_locale topological_space

variables {α : Type u}[topological_space α]

def le (F : filter α) := λ (i j : F.1),  j ⊆ i

[Adam Topaz]

F.1has type set (set \a). So when you write i j : F.1, lean is automatically coercing F.1 to a type, given by the subtype associated to the set. This means that terms of this subtype are really dependent pairs $(a,h)$ where $a$ is a set and $h$ is a proof that $a$ is contained in the given set of sets. So to use set inclusion, you would need to write j.1 \subset i.1 (or use type ascription to coerce these terms to sets). E.g.:

def le (F : filter α) := λ (i j : F.1), (j : set α) ⊆ i

[Adam Topaz]

I only had to give lean the hint for j, since it is then able to figure out that i should be considered as a set as well, now that it knows that you're considering j as a set.

[Alex J. Best]

You might also consider using

def le (F : filter α) := λ (i j : set α) (hi : i ∈ F.sets) (hj : j ∈ F.sets), j ⊆ i

instead. Rather than coercing a set to a type

[Adam Topaz]

Right, I would follow what Alex said. It can be a bit of a pain to keep track of the various coercions.

[Patrick Johnson]

I think λ (i j ∈ F), j ⊆ i would work too.

[Adam Topaz]

Yes, that's essentially defeq to what Alex said.

[Reid Barton]

Really you should write the type of the def before the :=, which would forestall some of these issues, I think.

[Jon Bannon]

Fantastic! Thank you everyone.

[Kevin Buzzard]

Mathematically it's quite upsetting that a type is at one level of the heirarchy and a set is a term so it's at a lower level. Deciding whether to bump up subsets to subtypes can be a complicated design decision.

[Eric Wieser]

Are you sure you didn't mean ∀ instead of λ?

def le (F : filter α) : Prop :=
∀ (i j : set α) (hi : i ∈ F.sets) (hj : j ∈ F.sets), j ⊆ i

Your current definition is strange because it doesn't actually use hi or hj

[Reid Barton]

That can't possibly be what was meant, but again, writing the type of le would help to clarify

[Jon Bannon]

@Reid Barton: Come to think of it, I don't actually know how to write the type of "le" clearly. I'll think about this.

I'm trying to manufacture an le that depends on the filter F.

So le (F) : F.1 \to F.1 \to Prop.

I expect le: \Pi (F : \filter \a) F.1\to F.1 \to Prop...will try.

[Jon Bannon]

Hmm. I tried this:

def le (F : filter α) : F.1 → F.1 → Prop := λ(i j : F.1), j ⊆ i

in hopes that specifying the type of le would evade the need to use either \in or the type ascription. I still get the error. I'm wondering if I still haven't correctly assigned the type of le?

[Mario Carneiro]

i and j are not sets, so they don't have the ⊆ relation

[Mario Carneiro]

i has type {s : set A // s \in F.sets}

[Mario Carneiro]

so i.1 is a set

[Mario Carneiro]

so you probably want λ(i j : F.1), j.1 ⊆ i.1

[Jon Bannon]

Thank you, Mario. What you say agrees with Adam's comment above. I was exploring what Reid Barton suggested about trying to write the type of le, but I don't really see how that will get around having to write j.1 \ss i.1, unless I'm still not writing the type of le correctly.

[Mario Carneiro]

What, mathematically, are you trying to express? This definition looks a little weird, even after the various proposed fixes

[Jon Bannon]

I'm trying to define a directed order on the sets in a filter F, so that if i and j are sets in the filter, then i \le j when j \subseteq i.

[Mario Carneiro]

By the way, I think that subtype has a partial order instance, so while you need the .1 to use subset, you might be able to avoid it with i <= j instead

[Mario Carneiro]

The sets in a filter F already have an order on them

[Jon Bannon]

Cool. I hoped as much. Is the order inclusion reversing? (I can probably see this in the code, but am pretty new to this!)

[Mario Carneiro]

No, but IIRC there are a few theorems about directed orders in mathlib already, and I think the directedness can go either way

[Jon Bannon]

I want to work with nets, so I need the dual of the usual order on sets in the filter.

[Mario Carneiro]

You can use order_dual to explicitly get the reverse order

[Jon Bannon]

FABULOUS!

[Jon Bannon]

I can't wait to be more familiar with this...thanks again, Mario, and everyone!