unfolding definitions from type class

Stream: general

[Bernd Losert]

Say I have a goal like ⊢ f x where f is coming from a type class instance. How do I unfold the definition of f from the type class?

[Adam Topaz]

Generally the answer is to not unfold, and use and/or build the API for f instead. If you must unfold, you can dsimp [f] or unfold f or delta f.

[Bernd Losert]

I'm building the API for f, so that's why I need to unfold. Unfortunately, none of your suggestions worked.

[Alex J. Best]

It would be easier to help if you gave a more complete example, of a specific f and example that leaves you in that goal state, and what exactly you'd like the goal to look like after

[Bernd Losert]

Let me try to make a toy example.

[Bernd Losert]

Well, my toy example has the goal with the f expanded. Dang it.

[Bernd Losert]

Here's the real code:

import order.filter.ultrafilter
import order.filter.partial
import algebra.support

noncomputable theory
open set filter classical
open_locale classical filter
open has_sup

variables {a b : Type*}

class convergence_space (a : Type*) :=
(conv : filter a -> a -> Prop)
(pure_conv : forall {x : a}, conv (pure x) x)
(le_conv : forall {x : a} {l l' : filter a}, l <= l' -> conv l' x -> conv l x) -- l <= l' means l' ⊆ l

class kent_convergence_space (a : Type*) extends convergence_space a :=
(kent_conv : forall {x : a} {l : filter a}, conv l x -> conv (sup l (pure x)) x)

class limit_space (a : Type*) extends kent_convergence_space a :=
(sup_conv : forall {x : a} {l l' : filter a}, conv l x -> conv l' x -> conv (sup l l') x) -- l ⊔ l' means l ∩ l'

open convergence_space
open kent_convergence_space
open limit_space

def induced (f : a -> b) [convergence_space b] : convergence_space a := {
  conv := fun l x, conv (map f l) (f x),
  pure_conv := by simp [filter.map_pure, pure_conv],
  le_conv := begin
    assume x : a,
    assume l l' : filter a,
    assume : l <= l',
    assume : conv (map f l') (f x),
    have : map f l <= map f l',
      apply map_mono (by assumption : l <= l'),
    apply le_conv
      (by assumption : map f l <= map f l')
      (by assumption : conv (map f l') (f x))
  end,
}

def induced_kent (f : a -> b) [kent_convergence_space b] : kent_convergence_space a :=
let ind := induced f in {
  kent_conv :=
    begin
      intros x l h,
      delta conv -- HAS NO EFFECT
    end,
    ..ind
}

[Reid Barton]

You also don't usually have to actually unfold, you can just know what the next step is (maybe intro) and do it.

[Reid Barton]

In this case though you probably want something like

lemma induced_def (f : a -> b) [convergence_space b] {l : filter a} {x : a} :
  @convergence_space.conv a (induced f) l x ↔ conv (map f l) (f x) :=
iff.rfl

def induced_kent (f : a -> b) [kent_convergence_space b] : kent_convergence_space a :=
let ind := induced f in {
  kent_conv :=
    begin
      intros x l h,
      rw induced_def,
    end,
    ..ind
}

[Reid Barton]

This is where class is starting to make your life more difficult, and it would be more convenient to follow the pattern used by topological_space

[Bernd Losert]

I tried the approach of topological space, but it produces other problems.

[Bernd Losert]

Thanks for the induced_def hint. That works.

[Patrick Massot]

Why are you using ascii art everywhere?!?

[Eric Wieser]

(Patrick is referring to ∀ vs forall, → vs ->, λ vs fun, ...)

[Bernd Losert]

I'm trying to prove the following lemma:

lemma convergence_space.inf_iff (p q : convergence_space α) (f : filter α) (x : α) :
  converges_ (p ⊓ q) f x ↔ converges_ p f x ∧ converges_ q f x :=

I need to unfold what p ⊓ q here means. I can't seem to unfold it to the definition that was given in the complete_lattice (convergence_space α) instance. Any tips?

[Yaël Dillies]

Use change?

[Kyle Miller]

Or, define a convergence_space.inf_eq lemma.

tactic#unfold_projs might do something helpful as well.

[Violeta Hernández]

If the exact definition of something gives you any extra properties that the basic API doesn't, you can make an rfl lemma to unfold it.

[Bernd Losert]

Yaël Dillies said:

Use change?

I can't use change since I don't know what the definition is to begin with. It's the one autogenerated from complete_lattice_of_Inf .

Kyle Miller said:

Or, define a convergence_space.inf_eq lemma.
tactic#unfold_projs might do something helpful as well.

inf_eq is basically what I'm trying to define. I tried unfold_projs but it doesn't unfold to the point where I can see what p ⊓ q means.

[Bernd Losert]

I can dig into the code of complete_lattice_of_Inf to see what it is doing, but I would like a way unfold the definition to tell me what it is doing.

[Kyle Miller]

Are you using VS Code? Have you already tried clicking on the term in the widgets view and navigate through the instances until you can see what it is?

[Bernd Losert]

Yes, I'm using VS Code. I clicked around, but I couldn't find anything useful.

[Bernd Losert]

So p ⊓ q is Inf {p, q} according to complete_lattice_of_Inf so I can use change here with that. It bugs me that I have to dig this out instead of getting it from doing an unfold. This can't be that hard, can it?

[Eric Wieser]

The approach used by mathlib is to write a rfl lemma for every data field of an instance

[Eric Wieser]

Eg, see docs#submodule.inf_coe

[Bernd Losert]

I didn't know that. I have seen *_eq lemmas here and there, but I didn't really see a pattern or why they existed. So basically you are saying that I have no choice but to dig into the code?

[Eric Wieser]

In your case though, it would probably be best to provide to provide inf manually rather than getting the default Inf {x, y} definition

[Bernd Losert]

docs#submodule.inf_coe doesn't work.

[Eric Wieser]

I wasn't suggesting it would work; my point is that you should write a lemma that describes how everything was defined as soon as you define an instance

[Bernd Losert]

In your case though, it would probably be best to provide to provide inf manually rather than getting the default Inf {x, y} definition

I have done this in my master branch, but it requires proving stuff. In fact, in my master branch I define an instance of every single type class that makes up complete_lattice. But I want to avoid having to do all this work since I have to repeat this sort of thing for 4 more things in the convergence_space hierarchy.

[Bernd Losert]

you should write a lemma that describes how everything was defined as soon as you define an instance

I can do this, but the unfolding problem remains.

[Eric Wieser]

If the proof is rfl, then you don't need to manually unfold anything

[Bernd Losert]

I don't follow. How will I know that p ⊓ q is Inf {p, q} without digging into the code or unfolding?

[Eric Wieser]

If you don't know what the definition even ended up being, that's often a sign that you probably should define it differently

[Eric Wieser]

You're right that it creates more work, but you'll have to do that anyway later to prove that inf does the right thing

[Eric Wieser]

So you may as well just define it the right way to begin with

[Eric Wieser]

Perhaps you want docs#function.injective.complete_lattice instead of docs#complete_lattice_of_Inf

[Bernd Losert]

I have already done this in my master branch as I mentioned. My takeaway here is that unfold just does not work in the way I expect.

[Eric Wieser]

Scrolling up, I notice that you never actually mention how you tried to use unfold; I assume unfold has_inf.inf didn't work?

[Kevin Buzzard]

Can you post a #mwe ? Note how your previous question in this thread was resolved quickly after you posted one.

[Bernd Losert]

Here you go:

import tactic
import order.filter

variable {α : Type*}

class convergence_space (α : Type*) :=
(converges : filter α → α → Prop)

open convergence_space

def converges_ (p : convergence_space α) (f : filter α) (x : α) : Prop := @converges _ p f x

instance : partial_order (convergence_space α) := sorry
instance : has_Inf (convergence_space α) := sorry
instance : complete_lattice (convergence_space α) := complete_lattice_of_Inf (convergence_space α) sorry

lemma convergence_space.inf_iff (p q : convergence_space α) (f : filter α) (x : α) :
  converges_ (p ⊓ q) f x ↔ converges_ p f x ∧ converges_ q f x :=
begin
  split,
  { intros hconv,
    unfold has_inf.inf at hconv, },
  { sorry }
end

[Eric Wieser]

dunfold has_inf.inf semilattice_inf.inf lattice.inf conditionally_complete_lattice.inf
      complete_lattice.inf convergence_space.complete_lattice complete_lattice_of_Inf at hconv,

works

[Eric Wieser]

You needed to keep unfolding further

[Eric Wieser]

I don't quite get why unfold can't make progress beyond convergence_space.complete_lattice

[Bernd Losert]

Ah, I didn't realize that I could unfold multiple definitions in one unfold. I was actually writing unfold multiple times and I stopped at complete_lattice.inf since I thought that was the last place since that is instance I defined that would have it.

[Bernd Losert]

Oh wait, you used dunfold. First time seeing that tactic.

[Eric Wieser]

If you hover over complete_lattice.inf in the infoview you'll see that it's @complete_lattice.inf _ convergence_space.complete_lattice, which is why I unfolded convergence_space.complete_lattice next

[Eric Wieser]

I'm afraid I have no idea why unfold convergence_space.complete_lattice failed but dunfold convergence_space.complete_lattice worked

[Bernd Losert]

Should I report it as a possible bug?