has_neg for X → Y where Y has_neg?

Stream: new members

[Ryan Lahfa]

I have some lemma where I want to take the opposite function, but it seems like it does not work, at least for N → R, here's some MWE:

import data.set
import data.real.basic

section negative_sets

def negative_set (S: set ℝ): set ℝ := { x : ℝ | -x ∈ S}

def cv (x: ℕ → ℝ) (l: ℝ):= ∀ ε > 0, ∃ N ≥ 0, ∀ n ≥ N, abs ((x n) - l) < ε
def accu_point (S: set ℝ) (l: ℝ) :=
  ∃ (x: ℕ → ℝ), cv x l ∧ (∀ n, x n ∈ S)

-- where is it?
/-instance seq.neg : has_neg (ℕ → ℝ) := {
  neg := λ x, (λ n, - x n)
}-/

def negative_set.adhere_ens_iff {S: set ℝ} {l: ℝ}:
  accu_point S l ↔ accu_point (negative_set S) (-l) :=
begin
  split,
  intro adh,
  rw accu_point at adh,
  obtain ⟨ x, hx ⟩ := adh,
  use (-x),
  sorry
end

end negative_sets

I can trivially provide the instance, but maybe I'm missing something.

[Ryan Lahfa]

Also, I'm not sure "negative sets" should be something part of mathlib or not. It's somewhat useful, maybe it can be really a lot more useful for convex analysis, but unsure.

[Kevin Buzzard]

I agree that it's useful but unfortunately -S already means "the stuff not in S"

[Ryan Lahfa]

I'm not talking about -X for X: set Y but rather -x for $x : \mathbb{N} \to \mathbb{R}$

[Reid Barton]

isn't this already a ring?

[Ryan Lahfa]

@Reid Barton How could I check this fact?

[Kevin Buzzard]

you will need the right import. Probably algebra.pi_instances

[Ryan Lahfa]

Indeed, that was it.

[Kevin Buzzard]

I don't know how someone who doesn't know where stuff in mathlib is can find this instance. I think there's a way of importing all of mathlib somehow? Sometimes people write import all but they have to run some script beforehand I think

[Ryan Lahfa]

@Kevin Buzzard If the doc implemented a search based on types, I could have typed has_neg and see all instances of has_neg across mathlib, but search is not that advanced currently.

[Reid Barton]

Usually this won't even help, because nobody actually wrote a has_neg instance, they wrote a ring instance instead.

[Reid Barton]

In the case of pi_instances in particular it probably does work.

[Mario Carneiro]

You can search for all instances of a class using #print instances has_neg

[Reid Barton]

In Haskell you have to write out all the instances of parent classes explicitly, which has the side effect that they're easier to index/find.

[Mario Carneiro]

however one of those instances will be add_group.has_neg and you will have to follow that thread to find all the others

[Mario Carneiro]

and if you are wondering "why isn't there a way to print them all out recursively", that's called tracing the type class search

[Reid Barton]

It might be useful to have a way to only follow all the instances coming from extends, though

[Reid Barton]

that should at least be a finite list

[Ryan Lahfa]

Mario Carneiro said:

and if you are wondering "why isn't there a way to print them all out recursively", that's called tracing the type class search

How hard would it be to make Lean output some metadata about typeclasses search (as JSON or whatever makes sense)?

[Kevin Buzzard]

You can just turn the trace on

[Kevin Buzzard]

I can never remember how to do it, it tells you if typeclass inference fails in a certain way. It's not, but it's something like, set_option trace.class_inference true

[Kevin Buzzard]

set_option trace.class_instances true

[Ryan Lahfa]

Oh okay, I was more asking from a documentation standpoint, as we have Ctrl + P + "#" to search for lemmas/etc, I was wondering how hard would it be to have something to search for instances in VSCode

[Kevin Buzzard]

I am unclear what you're asking. Which instances do you want to search for? Everything apply_instance knows about or the ones used to solve one particular search?

[Kevin Buzzard]

#print instances for the former, and turn the trace on for the latter.

[Ryan Lahfa]

If we reconsider the previous context where pi_instances were not imported, i.e. not available in the file.

Would #print instances or the tracing find them?

[Ryan Lahfa]

My point was basically, it could be interesting to have something which search over all files, including not imported ones. Or to bake this kind of tracing search statically in the mathlib docs.

[Kevin Buzzard]

If you haven't imported a file then for sure #print and traces won't find the instances in that file.

[Bryan Gin-ge Chen]

Below each class definition, the docs show all the instances that are defined in mathlib, e.g. has_neg; click on "Instances".

[Bryan Gin-ge Chen]

I see pi.has_neg in that list, and clicking on it leads here.

[Ryan Lahfa]

Bryan Gin-ge Chen said:

Below each class definition, the docs show all the instances that are defined in mathlib, e.g. has_neg; click on "Instances".

It is just it's not obvious that pi.has_neg is the one I'm looking for.

[Kevin Buzzard]

If you know that a function is a pi type then it's more obvious

[Ryan Lahfa]

In this case, right

[Kevin Buzzard]

and I would venture that this is one of the most obscure examples

[Ryan Lahfa]

Hahaha, most likely

[Bryan Gin-ge Chen]

We could probably display the types of those instances. Please open an issue on doc-gen so we don't forget.

[Kevin Buzzard]

But note no real.has_neg

[Ryan Lahfa]

Kevin Buzzard said:

But note no real.has_neg

It comes from add_group.has_neg, I suppose?

[Kevin Buzzard]

I guess that makes sense

[Kevin Buzzard]

Note that there is rat.has_neg though. What I'm saying is that the results are in some sense random.

[Bryan Gin-ge Chen]

Is this a defined-in-core vs defined-in-mathlib thing? No, they're both defined in mathlib.

[Reid Barton]

No, it's just optional whether to define (for example) has_neg and ring simultaneously or separately. I wouldn't expect there to be much logic to it.

[Reid Barton]

One reason to define them separately might be that you want to talk about -x and prove lemmas about it before going on to define the ring structure.

[Reid Barton]

I didn't look to see if that is actually the case for rat though.

[Bryan Gin-ge Chen]

It looks like in both cases has_neg is defined and used before the ring instance is assembled, however with reals it's done at the level of Cauchy sequences, e.g. there's a has_neg Cauchy instance.

[Ryan Lahfa]

Bryan Gin-ge Chen said:

It looks like in both cases has_neg is defined and used before the ring instance is assembled, however with reals it's done at the level of Cauchy sequences, e.g. there's a has_neg Cauchy instance.

Wouldn't this be derived by quotient properties over rings?

[Bryan Gin-ge Chen]

Yes, it looks like that is how it's defined.