Why is [field F] not an implicit argument?

Stream: new members

[Martin C. Martin]

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


namespace LADR

@[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



structure add_comm_subgroup (V : Type*) [add_comm_group V] :=
(carrier : set V)
(add_mem' : ∀ {u v : V}, u ∈ carrier → v ∈ carrier → u + v ∈ carrier)
(zero_mem' : (0 : V) ∈ carrier)


-- **********  BOILERPLATE FOR set_like  **********
namespace add_comm_subgroup

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

end add_comm_subgroup
-- **********  BOILERPLATE ENDS  **********


structure subspace (F : Type*) (V : Type*)
  [field F] [add_comm_group V] [vector_space F V] extends add_comm_subgroup V :=
(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 }⟩,

  add_comm := sorry,
  add_assoc := sorry,
  add_zero := sorry,
  zero_add := sorry,
  add_left_neg := sorry,
}

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

end LADR

[Eric Wieser]

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

[Eric Wieser]

Note Lean 4 does this automatically for you

[Martin C. Martin]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Martin C. Martin]

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]

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]

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

[Martin C. Martin]

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

[Peter Hansen]

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"?

Maybe this https://leanprover.github.io/lean4/doc/lean3changes.html

[Pedro Sánchez Terraf]

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"?

And the Lean 4 survival guide for Lean 3 users.

[Martin C. Martin]

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

[Ruben Van de Velde]

Do you want to give people nightmares?

[Martin C. Martin]

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

[Kyle Miller]

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]

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.