## Stream: new members

### Topic: Instance resolution

#### Bhavik Mehta (Jun 12 2020 at 23:51):

[class_instances] trying next solution, current solution has metavars
Instance resolution is failing in my example (mwe coming in a moment) and on printing the class instance trace, the first try is the one I want, but it gives the above message and moves on - any idea how to fix?

#### Bhavik Mehta (Jun 12 2020 at 23:53):

import category_theory.comma

universes v u
namespace category_theory

/-- A sieve on X is a set of morphisms to X that is closed under left composition. -/
structure sieve {C : Type u} [category.{v} C] (X : C) :=
(arrows : set (over X))
(subs : ∀ {f : over X} (_ : f ∈ arrows) {Z : C} (g : Z ⟶ f.left), over.mk (g ≫ f.hom) ∈ arrows)

variables {C : Type u} [category.{v} C]

instance {X Y : C} : has_mem (Y ⟶ X) (sieve X) := ⟨λ x p, over.mk x ∈ p.arrows⟩

#check @category_theory.has_mem

set_option trace.class_instances true
set_option pp.all true

example {X Y : C} (f : Y ⟶ X) (S : sieve X) : f ∈ S :=
begin
end


#### Reid Barton (Jun 13 2020 at 15:39):

BTW, @Bhavik Mehta, if you plan to eventually PR sheaves to mathlib, it might be worth starting with a discussion of the planned design

#### Reid Barton (Jun 13 2020 at 15:40):

For subjects like this, a PR is not really the right place to start the discussion, I think.

#### Bhavik Mehta (Jun 13 2020 at 15:49):

I started a brief discussion in #maths earlier - at the moment though I'm doing it with enough generality to do forcing, and I'm happy to be guided by the geometry-minded people for the specialised API about sheaves on a site/space

#### Bhavik Mehta (Jun 13 2020 at 15:52):

Right now I'm making sure the specialisation to a site works like I think it should, and that sheafification of a presheaf on a space has the properties I want - then I'll do the stuff mentioned there about moving between spaces/toposes

#### Reid Barton (Jun 13 2020 at 16:03):

For me "forcing" is a foreign word--when I try to understand it seems not to mean anything. I hope this doesn't end up totally disconnected from what is needed for geometry.

#### Reid Barton (Jun 13 2020 at 16:05):

I also don't even know what an elementary topos is, or a Lawvere-Tierney topology.

#### Reid Barton (Jun 13 2020 at 16:05):

This is why I think writing Lean code is not necessarily the correct starting point.

#### Reid Barton (Jun 13 2020 at 16:06):

The :elephant: nature is really difficult to work with here, I think.

#### Bhavik Mehta (Jun 13 2020 at 16:14):

These are reasonable concerns, do you have a suggestion of how we could go about starting this? My perspective is that I'm just providing some of the categorical machinery so that the people who need it for geometry don't have to

#### Reid Barton (Jun 13 2020 at 17:03):

Maybe an informal roadmap, or just a pile of Lean defs with lots of stuff omitted?

#### Reid Barton (Jun 13 2020 at 17:06):

(also #maths would be a better place for this)

#### Bhavik Mehta (Jun 13 2020 at 18:02):

Will do! Though I'd still appreciate any help on the original question :)

#### Reid Barton (Jun 13 2020 at 20:57):

I think your instance is no good because it violates the out_param--X doesn't determine Y

#### Reid Barton (Jun 13 2020 at 20:57):

although I seem to recall something like this working in practice...

#### Reid Barton (Jun 13 2020 at 20:58):

ah no, I didn't use ∈

#### Reid Barton (Jun 13 2020 at 20:58):

probably because of this same issue

#### Bhavik Mehta (Jun 13 2020 at 21:10):

Surely there should be an error message at the definition site then?

#### Bhavik Mehta (Jun 13 2020 at 21:11):

My mental model of out_param was like Haskell's fundeps, and in this case I don't have any other instance which clashes/overlaps with that one

#### Reid Barton (Jun 13 2020 at 21:22):

It's also wrong in Haskell... it doesn't surprise me that Lean doesn't give an error though

#### Reid Barton (Jun 13 2020 at 21:22):

Anyways, ∈ is kind of useless because it's generalized in the wrong ways

#### Bhavik Mehta (Jun 13 2020 at 21:28):

Oh right, I was misreading which one the outparam was on - that makes sense

#### Reid Barton (Jun 13 2020 at 21:30):

I guess you could just write S.1 f

#### Bhavik Mehta (Jun 13 2020 at 21:31):

Yeah I was just wondering if I could make the notation prettier

#### Pedro Minicz (Sep 17 2020 at 14:35):

How do I change class-instance resolution priority for a given instance? In the following example, I believe a fiddling with the priority of hα could fix things. Also, if its not a priority problem, what is?

import topology.order
import tactic

section

parameters {α β : Type} [topological_space β] {f : α → β}

def s : set (set α) := set.preimage f '' is_open

instance hα : topological_space α :=
topological_space.generate_from s

-- Maximum class-instance resolution depth reached
example : continuous f :=
sorry

example : @continuous _ _ hα _ f :=
begin
intros s hs,
-- Maximum class-instance resolution depth reached
refine is_open.preimage _ hs,
end

lemma hf : @continuous _ _ hα _ f :=
begin
intros s hs,
refine @is_open.preimage _ _ hα _ _ _ _ hs,
sorry
end

end


#### Pedro Minicz (Sep 17 2020 at 14:36):

Apparently I created a topic with an already existing name? :octopus:

#### Kenny Lau (Sep 17 2020 at 14:40):

@Pedro Minicz the issue is that Lean doesn't know to use f to form the topology on alpha

#### Pedro Minicz (Sep 17 2020 at 14:43):

Isn't there a way to tell lean to "just use the first thing that fits the goal?" Specially when there is only one thing in the context.

#### Reid Barton (Sep 17 2020 at 14:49):

It's tempting to think that because you wrote an instance which mentions parameters, the instance is somehow "bound" to those parameters. But I think that's not really how it works; instead what you did is create a global instance for topological_space (anything) that first tries to synthesize an instance for topological_space (anything else), and clearly this is going to lead to problems

#### Kenny Lau (Sep 17 2020 at 14:51):

@Pedro Minicz your instance says: given a function f : A -> B and an instance of topological_space B, create an instance of topological_space A

#### Kenny Lau (Sep 17 2020 at 14:51):

the issue is that f is not mentioned in the target instance at all, so Lean doesn't know which function A -> B to use

#### Kenny Lau (Sep 17 2020 at 14:51):

or even which B to use

#### Kenny Lau (Sep 17 2020 at 14:52):

the goal is topological_space A when Lean is creating the instance in your example

Last updated: May 17 2021 at 21:12 UTC