## Stream: new members

### Topic: Why is [field F] not an implicit argument?

#### Martin C. Martin (Aug 01 2023 at 20:11):

I'm re-implementing vector spaces and sub spaces. In mathlib's submodule, we show that a submodule is a module. I'm trying to do the same thing, but running into a difference that I don't understand.

#check submodule.module' : returns
Π (p : submodule ?M_2 ?M_3) [_inst_3 : semiring ?M_1] [_inst_4 : has_smul ?M_1 ?M_2] [_inst_5 : module ?M_1 ?M_3] [_inst_6 : is_scalar_tower ?M_1 ?M_2 ?M_3], module ?M_1 ↥p
i.e. there are implicit arguments for all the algebraic structure objects. However, in my code, I just get:
#check #check subspace.vector_space' returns
subspace.vector_space' : Π (q : subspace ?M_1 ?M_2), vector_space ?M_1 ↥q

In particular, there's no requirement for [field ?M_1].

Why doesn't that show up?
My #mwe, sorry it's so long:

import algebra.module.basic
import data.set_like.basic

set_option old_structure_cmd true

@[ext]
class vector_space (F : Type*) (V : Type*) [field F] [add_comm_group V]
extends has_smul F V :=
(smul_assoc :  a b : F,  v : V, (a * b)  v = a  (b  v))
(mul_ident :  v : V, (1 : F)  v = v)
(left_distrib :  a : F,  u v : V, a  (u + v) = (a  u) + (a  v))
(right_distrib :  a b :F,  v : V, (a + b)  v = (a  v) + (b  v))

variables {F : Type*} [field F]

namespace vector_space

variables {V : Type*} [add_comm_group V] [vector_space F V]

theorem neg_one_smul_is_neg {v : V} : (-1 : F)  v = - v := sorry

end vector_space

(carrier : set V)
(add_mem' :  {u v : V}, u  carrier  v  carrier  u + v  carrier)
(zero_mem' : (0 : V)  carrier)

-- **********  BOILERPLATE FOR set_like  **********

variables {V : Type*} [add_comm_group V] {v : V}

instance : set_like (add_comm_subgroup V) V :=
add_comm_subgroup.carrier, λ p q h, by cases p; cases q; congr'

@[simp] lemma mem_carrier {p : add_comm_subgroup V} : v  p.carrier  v  (p : set V) := iff.rfl

@[ext] theorem ext {p q : add_comm_subgroup V} (h :  v, v  p  v  q) : p = q := set_like.ext h

-- **********  BOILERPLATE ENDS  **********

structure subspace (F : Type*) (V : Type*)
(smul_mem' :  (c : F) {v : V}, v  carrier  c  v  carrier )

namespace subspace

variables {V : Type*} [add_comm_group V] [vector_space F V]
variable {v : V}

-- **********  BOILERPLATE FOR set_like  **********
instance : set_like (subspace F V) V :=
subspace.carrier, λ p q h, by cases p; cases q; congr'

@[simp] lemma mem_carrier {p : subspace F V} : v  p.carrier  v  (p : set V) := iff.rfl

@[ext] theorem ext {p q : subspace F V} (h :  v, v  p  v  q) : p = q := set_like.ext h
-- **********  BOILERPLATE ENDS  **********

variables (p : subspace F V)

instance fooblah : add_comm_group p := {
add := λ u v,  u.1 + v.1, by { apply p.add_mem', simp, simp} ⟩,
zero := 0, p.zero_mem'⟩,
neg := λ v, -v.1, by { rw  @vector_space.neg_one_smul_is_neg F _ V, apply p.smul_mem', simp }⟩,

}

instance vector_space' : vector_space F p := {
smul := λ s v,  s  v.1, by { apply p.smul_mem', simp} ⟩,
smul_assoc := by {intros, simp, apply vector_space.smul_assoc},
mul_ident := by {intros, ext, simp, rw vector_space.mul_ident},
left_distrib := sorry,
right_distrib := sorry
}

#check subspace.vector_space'

instance : vector_space F p := p.vector_space'

end subspace

#### Eric Wieser (Aug 01 2023 at 22:37):

You want #check @subspace.vector_space' not #check subspace.vector_space'

#### Eric Wieser (Aug 01 2023 at 22:37):

Note Lean 4 does this automatically for you

#### Martin C. Martin (Aug 02 2023 at 00:00):

Eric Wieser said:

You want #check @subspace.vector_space' not #check subspace.vector_space'

Ah, thanks! But why does [_inst_3 : semiring ?M_1] show up for module', without the @, but the equivalent not show up for vector_space'? Just some quirk of the printing logic, or is there something deeper, like the difference between variable and constant?

#### Scott Morrison (Aug 02 2023 at 00:57):

Could I ask why you're doing this in Lean 3 rather than Lean 4?

#### Eric Wieser (Aug 02 2023 at 01:34):

It shows up for one but not the other because one uses (p : submodule ...) and the other uses {p : submodule ...}

#### Eric Wieser (Aug 02 2023 at 01:35):

Roughly speaking, Lean fills in {} and [] until it hits the first () argument. @ tells it not to do this.

#### Martin C. Martin (Aug 02 2023 at 11:02):

Eric Wieser said:

Roughly speaking, Lean fills in {} and [] until it hits the first () argument. @ tells it not to do this.

Oh interesting! Is this documented somewhere? Such as the Lean reference manual?

#### Martin C. Martin (Aug 02 2023 at 17:36):

Scott Morrison said:

Could I ask why you're doing this in Lean 3 rather than Lean 4?

Which one is considered the best to use for new projects these days? How far along is the Lean 4 port of mathlib? Do enough people here on Zulip know about Lean 4 and can help?

#### Kyle Miller (Aug 02 2023 at 17:40):

All of mathlib is ported as of a couple weeks ago, and mathlib4 is now accepting contributions of new material

#### Martin C. Martin (Aug 02 2023 at 17:43):

Awesome! I guess I'll switch to that. Is there a document on the difference, "Lean 4 for the Lean 3 worker"?

#### Peter Hansen (Aug 02 2023 at 17:47):

Martin C. Martin said:

Awesome! I guess I'll switch to that. Is there a document on the difference, "Lean 4 for the Lean 3 worker"?

#### Pedro Sánchez Terraf (Aug 02 2023 at 17:48):

Martin C. Martin said:

Awesome! I guess I'll switch to that. Is there a document on the difference, "Lean 4 for the Lean 3 worker"?

#### Martin C. Martin (Aug 02 2023 at 18:41):

How long before we start porting mathlib to Lean 5? :wink:

#### Ruben Van de Velde (Aug 02 2023 at 18:45):

Do you want to give people nightmares?

#### Martin C. Martin (Aug 02 2023 at 18:55):

Is there a tool for converting Lean 3 projects to Lean 4, like Python's 2to3?

#### Kyle Miller (Aug 02 2023 at 19:06):

Yes, you can use mathport (the same tool that helped drive the mathlib port). I haven't used it myself yet, but I've seen these instructions: https://github.com/leanprover-community/mathport/blob/master/Oneshot/README.md

#### Scott Morrison (Aug 03 2023 at 03:49):

That link is for porting single files at a time. If you'd like to try a whole project (it's been done twice to my knowledge so far, besides mathlib) see that main mathport README.

Last updated: Dec 20 2023 at 11:08 UTC