apply_instance for defs

Stream: new members

[Apurva Nakade]

In the following code

import data.complex.basic
import linear_algebra.finite_dimensional
import tactic

universes u
variables {n : Type u} [fintype n]

instance hn_fd : finite_dimensional ℂ (n → ℂ) :=
begin
  apply_instance,
end

def V := (n → ℂ)

instance hn_fd' : finite_dimensional ℂ V :=
begin
  apply_instance,
end

[Apurva Nakade]

The first instance works but the second gives an error

[Apurva Nakade]

Is def doing something more than just setting V definitionally equal to (n → ℂ)?

[Johan Commelin]

delta V, apply_instance

[Johan Commelin]

You need to tell Lean to "open the box" and look inside the definition. That's what the delta does.

[Apurva Nakade]

I tried this

instance hn_fd' : finite_dimensional ℂ V :=
begin
  delta V, --similar error with unfold
  apply_instance,
end

but I'm still getting

tactic.mk_instance failed to generate instance for
  finite_dimensional ℂ (?m_1 → ℂ)
state:
⊢ finite_dimensional ℂ (?m_1 → ℂ)

[Apurva Nakade]

looks like Lean is forgetting that n is fintype

[Sebastien Gouezel]

If I copy your code block, I get an error even earlier, in the statement of the lemma. Do you also get it, and do you understand what it means?

[Apurva Nakade]

Ah, I totally missed that, thanks! This is what I'm seeing

don't know how to synthesize placeholder
context:
⊢ Type ?

[Apurva Nakade]

I think Lean is unable to infer what n is

[Apurva Nakade]

This is very interesting. I thought that using variables {n : Type u} [fintype n] will pass n as an implicit variable to all the definitions and theorems in the namespace. I don't think I know how to fix this.

[Bryan Gin-ge Chen]

Maybe you need to use include n?

[Apurva Nakade]

Still getting error in the statement of the lemma :(

[Apurva Nakade]

Although the error has slightly changed now

don't know how to synthesize placeholder
context:
n : Type u,
_inst_1 : fintype n
⊢ Type ?

[Reid Barton]

It basically just means {n : Type u} [fintype n] is implictly in all your definitions (actually, only the ones which mention n).

[Reid Barton]

This isn't what you want, for the reason you are discovering.

[Apurva Nakade]

I honestly don't know what to do. My guess is that def V := (n → ℂ) is not the right way to ask Lean to treat V as a placeholder for (n → ℂ)

[Reid Barton]

variables (n : Type u) is the easiest

[Apurva Nakade]

This is giving me

type mismatch at application
  finite_dimensional ℂ V
term
  V
has type
  Π (n : Type ?) [_inst_1 : fintype n], Type ? : Type (max (?+1) ? (?+1) 1)
but is expected to have type
  Type ? : Type (?+1)

Wow, this is turning out to be more complicated than I expected!

[Bryan Gin-ge Chen]

This is because V now requires an explicit argument for n.

[Bryan Gin-ge Chen]

instance hn_fd' : finite_dimensional ℂ (V n) :=
begin
  apply_instance,
end

Now Lean complains that it can't find an add_comm_group instance on V n.

[Apurva Nakade]

Hmm... it seems to me that Lean does not like hiding the variable n in V.
For now, I'll just stick to using (n → ℂ) everywhere.
I'm a bit sad though that there is no straightforward way in Lean to simply rename a term like (n → ℂ)

[Apurva Nakade]

Although, in math, it is common to write statements like "In this section, we will let V decode ℂ^n." It would be good to know what the Lean variant of this is.

[Reid Barton]

parameter, but I wouldn't recommend using it unless you first know how to use variable

[Reid Barton]

You would still need to copy the instances you want anyways.

[Reid Barton]

Another option is local notation.

[Apurva Nakade]

Yess! This works, thanks so much!!

[Yakov Pechersky]

What's the issue with using delta? That's the Lean variant you asked for. When we say that V will encode, delta is the decoding step.

[Yakov Pechersky]

Although local notation is very easy too.

[Apurva Nakade]

delta did not work

[Apurva Nakade]

there was an error in the theorem statement itself

[Bryan Gin-ge Chen]

Well, this works, but this is worse than just using n → ℂ everywhere:

def V := (n → ℂ)

instance hn_fd' : @finite_dimensional ℂ (V n) _ (by { delta V, apply_instance }) (by { delta V, apply_instance }) :=
begin
  delta V,
  apply_instance,
end

[Yakov Pechersky]

def V n :=...

[Reid Barton]

@[derive add_comm_group, derive (vector_space ℂ), derive (finite_dimensional ℂ)]
def V (n : Type u) [fintype n] := (n → ℂ)

I don't know if it's possible to get [fintype n] on only the finite_dimensional instance

[Reid Barton]

or to avoid repeating derive

[Rob Lewis]

Reid Barton said:

or to avoid repeating derive

This yes, @[derive [..., ...]]. The other probably not.

[Bryan Gin-ge Chen]

We should really have a doc entry on derive here. Does anyone want to volunteer?

[Bryan Gin-ge Chen]

(I'll do it if someone gives me some pointers on how it works...)

[Utensil Song]

I also wonder how derive works. Some search (by git blaming the related tests) got me leanprover-community/mathlib#1475 then this Zulip chat and https://github.com/leanprover-community/lean/blob/master/library/init/meta/derive.lean .

I can't immediately tell how it works (from the source), only knowing that there's such a mechanism to register derive handlers and there're a few such handlers available in mathlib, each targeting a specific scenario.

By a few I mean two of them (found by searching derive_handler: inhabited_instance and delta_instance) and they seem to be well documented by themselves, it's just not easy for anyone to find the doc by just seeing @[derive ...].

P.S. Is it possible to make VSCode display the doc when hover @[derive ...] or make it clickable? I don't know where's related code in VSCode plugin.

[Bryan Gin-ge Chen]

Utensil Song said:

P.S. Is it possible to make VSCode display the doc when hover @[derive ...] or make it clickable? I don't know where's related code in VSCode plugin.

Most likely not without making changes to Lean itself. I don't know how hard it would be.

[Utensil Song]

Seems possible to address the hover part by modifying https://github.com/leanprover/vscode-lean/blob/master/src/hover.ts by manually write some doc in json and provide them to hover. To avoid becoming out of sync with the source, it could be just a link to an HTML doc generated from Lean /Mathlib. This would be enough for most users I guess.

As for the clickable part, modifying https://github.com/leanprover/vscode-lean/blob/master/src/definition.ts with the same naive manual approach would not work since the location has to be provided by Lean language server and there's no such an API to literal specify the symbol (out of context) to locate.

[Bryan Gin-ge Chen]

I think it'd be better overall to have the Lean server return the doc string and location from the attribute declaration. That would allow Emacs users to view such docstrings as well.

[Utensil Song]

Sure.

[Utensil Song]

#mwe

import algebra.category.Module.monoidal
import algebra.category.CommRing.basic

import tactic.delta_instance

open category_theory

variables {C : Type*} [category C] [monoidal_category C]

def tensor_power (X : C) : ℕ → C
| 0 := 𝟙_ C
| (n+1) := X ⊗ tensor_power n

example {R : CommRing} (M : Module R) : Module R := tensor_power M 17

-- And if you want to do this with unbundled objects:

universes u

variables (R : Type u) [comm_ring R] (M : Type u) [add_comm_group M] [module R M]

def foo : Type u :=
  (tensor_power (Module.of R M) 17 : Module R)

-- WORKS
-- instance : add_comm_group (foo R M) := by { delta foo, apply_instance, }
-- instance : module R (foo R M) := by { delta foo, apply_instance, }

-- WORKS
-- instance : add_comm_group (foo R M) := by delta_instance foo
-- instance : module R (foo R M) :=  by delta_instance foo

namespace foo

/-
tactic.mk_instance failed to generate instance for
  add_comm_group (foo R M)
-/
@[derive add_comm_group]
def to_add_comm_group := foo R M

/-
failed to synthesize type class instance for
R : Type u,
_inst_3 : comm_ring R,
M : Type u,
_inst_4 : add_comm_group M,
_inst_5 : module R M
⊢ add_comm_group (to_module R M)
-/
@[derive module R]
def to_module := foo R M

end foo

[Utensil Song]

I don't understand why derive doesn't work here.

[Utensil Song]

https://github.com/leanprover-community/mathlib/blob/master/src/linear_algebra/dual.lean#L39 is similar but works:

@[derive [add_comm_group, module R]] def dual := M →ₗ[R] R

[Scott Morrison]

This doesn't work because derive only unfolds the current definition (i.e. to_add_comm_group in your example). It would need to _also_ unfold foo before it could find the instance.

[Scott Morrison]

If you put another @[derive] on foo it should work.

[Utensil Song]

Oh, moving derive to where foo is defined works:

@[derive [add_comm_group, module R]]
def foo : Type u :=
  (tensor_power (Module.of R M) 17 : Module R)

[Utensil Song]

So does attribute [derive [add_comm_group, module R]] foo