Zulip Chat Archive

Stream: new members

Topic: Instance resolution


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jun 13 2020 at 16:05):

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

view this post on Zulip Reid Barton (Jun 13 2020 at 16:05):

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

view this post on Zulip Reid Barton (Jun 13 2020 at 16:06):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Jun 13 2020 at 17:03):

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

view this post on Zulip Reid Barton (Jun 13 2020 at 17:06):

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

view this post on Zulip Bhavik Mehta (Jun 13 2020 at 18:02):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Jun 13 2020 at 20:57):

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

view this post on Zulip Reid Barton (Jun 13 2020 at 20:58):

ah no, I didn't use

view this post on Zulip Reid Barton (Jun 13 2020 at 20:58):

probably because of this same issue

view this post on Zulip Bhavik Mehta (Jun 13 2020 at 21:10):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Jun 13 2020 at 21:22):

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

view this post on Zulip Bhavik Mehta (Jun 13 2020 at 21:28):

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

view this post on Zulip Reid Barton (Jun 13 2020 at 21:30):

I guess you could just write S.1 f

view this post on Zulip Bhavik Mehta (Jun 13 2020 at 21:31):

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

view this post on Zulip 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 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  : topological_space α :=
topological_space.generate_from s

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

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

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

end

view this post on Zulip Pedro Minicz (Sep 17 2020 at 14:36):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Sep 17 2020 at 14:51):

or even which B to use

view this post on Zulip 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