Instance resolution

Stream: new members

[Bhavik Mehta]

[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]

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]

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]

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

[Bhavik Mehta]

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]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Bhavik Mehta]

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]

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

[Reid Barton]

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

[Bhavik Mehta]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

ah no, I didn't use ∈

[Reid Barton]

probably because of this same issue

[Bhavik Mehta]

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

[Bhavik Mehta]

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]

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

[Reid Barton]

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

[Bhavik Mehta]

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

[Reid Barton]

I guess you could just write S.1 f

[Bhavik Mehta]

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

[Pedro Minicz]

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]

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

[Kenny Lau]

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

[Pedro Minicz]

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]

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]

@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]

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]

or even which B to use

[Kenny Lau]

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