Zulip Chat Archive

Stream: general

Topic: working out where a typeclass instance is defined

Kevin Buzzard (Jul 05 2019 at 16:04):

So here I am in the middle of a Lean file, with lots of imports and variables and so on, I'm learning Lean, and I just noticed that

example : submodule R M := ⊤

typechecks. This means that submodule R M has some structure which I don't know about -- it will be some kind of lattice. So now I want to go straight to the place in mathlib where this lattice structure is defined. I try looking at where submodule is defined, but I can't see anything there, and so then I figure I'll investigate with #print and #check. But I can't do it! And I even guessed at some point.

example : submodule R M := ⊤

#print notation ⊤ -- lattice.has_top.top _

#print lattice.has_top.top -- comes from typeclass lattice.has_top

def ABC : lattice.has_top (submodule R M) := by apply_instance

#print ABC -- lattice.has_top -- ??? Where is the definition??

-- so probably `submodule R M` is a lattice. Let's start there.

def guess1 : lattice.lattice (submodule R M) := by apply_instance
#print guess1 -- lattice.conditionally_complete_lattice.to_lattice (submodule R M)

def guess2 : lattice.conditionally_complete_lattice (submodule R M) := by apply_instance
#print guess2 --   lattice.conditionally_complete_lattice_of_complete_lattice

-- I am getting bored now.

def guess3 : lattice.complete_lattice (submodule R M) := by apply_instance
#print guess3 -- ??? lattice.complete_lattice ???

-- I am now stuck

Kevin Buzzard (Jul 05 2019 at 16:06):

Somewhere some instance is defined. How do I get to that definition without having to ask or guess or search?

Kenny Lau (Jul 05 2019 at 16:11):

pp.implicit

Kevin Buzzard (Jul 05 2019 at 16:11):

nice

Kevin Buzzard (Jul 05 2019 at 16:11):

There are a bunch of things open

Kevin Buzzard (Jul 05 2019 at 16:12):

I did pp.all

Kevin Buzzard (Jul 05 2019 at 16:13):

You need pp.all. Here's the last guess with implicit:

def guess3 : Π {R M : Type u} [_inst_1 : ring R] [_inst_2 : add_comm_group M] [_inst_3 : @module R M _inst_1 _inst_2],
  lattice.complete_lattice (@submodule R M _inst_1 _inst_2 _inst_3) :=
λ {R M : Type u} [_inst_1 : ring R] [_inst_2 : add_comm_group M] [_inst_3 : @module R M _inst_1 _inst_2],
  @lattice.complete_lattice R M _inst_1 _inst_2 _inst_3

Kevin Buzzard (Jul 05 2019 at 16:13):

with pp.all it's submodule.lattice.complete_lattice

Kevin Buzzard (Jul 05 2019 at 16:17):

Aah I see, you use implicit at another point in the investigation

Mario Carneiro (Jul 05 2019 at 16:20):

I agree this is not nice. Here's what I did to jump to the location:

import linear_algebra.basic

variables (R M : Type) [ring R] [add_comm_group M] [module R M]

set_option pp.implicit true
set_option pp.notation false
#check (⊤ : submodule R M) -- copy-paste below
#check (@lattice.has_top.top (@submodule R M _inst_1 _inst_2 _inst_3)
  (@submodule.lattice.has_top /- <- ctrl-click -/ R M _inst_1 _inst_2 _inst_3) :
  @submodule R M _inst_1 _inst_2 _inst_3)

Mario Carneiro (Jul 05 2019 at 16:24):

If you know that \top is provided by has_top, you can skip the pp.notation line like so:

set_option pp.implicit true
#check (by apply_instance : lattice.has_top (submodule R M))
#check (@submodule.lattice.has_top /- <- ctrl-click -/ R M _inst_1 _inst_2 _inst_3 :
  lattice.has_top (@submodule R M _inst_1 _inst_2 _inst_3)

Kevin Buzzard (Jul 05 2019 at 16:25):

If you have submodule open, your results might be different.

Kevin Buzzard (Jul 05 2019 at 16:25):

And you can't close it, and you're 400 lines in

Mario Carneiro (Jul 05 2019 at 16:25):

You can still do the same thing, the printout only looks a bit different

Kevin Buzzard (Jul 05 2019 at 16:26):

yeah, submodule was suppressed so you couldn't copy paste and then click!

Mario Carneiro (Jul 05 2019 at 16:26):

Oh! That looks like a pp bug

Mario Carneiro (Jul 05 2019 at 16:27):

since submodule.lattice.has_top is protected, the pretty printer should not show it without the namespace

Kevin Buzzard (Jul 05 2019 at 16:27):

set_option pp.implicit true
#check (by apply_instance : lattice.has_top (submodule R M))
/-
@lattice.has_top R M _inst_1 _inst_2 _inst_3 : lattice.has_top (@submodule R M _inst_1 _inst_2 _inst_3)
-/