## Stream: new members

### Topic: Why can't it find the [field F] definition?

#### Martin C. Martin (Jul 10 2023 at 20:09):

In trying to define a vector subspace, rw can't find the [field F] declaration. Why not, and how can I achieve the desired rw?

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 + v, by { apply p.add_mem', simp, simp} ⟩,
zero := ⟨0, p.zero_mem'⟩,
neg := λ v, ⟨-v, by {
rw ← vector_space.neg_one_smul_is_neg,
sorry
}⟩,
}

end subspace



Sorry the #mwe is so large. As indicated, some of it is boilerplate. Is there a better way to provide large MWEs like this?

#### Martin C. Martin (Jul 10 2023 at 20:11):

The message, on that last rw, is invalid rewrite tactic, failed to synthesize type class instance for field ?m_1. The state is:

F : Type u_1,
_inst_1 : field F,
V : Type u_2,
_inst_3 : vector_space F V,
p : subspace F V,
v : ↥p
⊢ -↑v ∈ p


#### Martin C. Martin (Jul 10 2023 at 20:16):

I understand that v : ↥p is a pair, where the first element is an element of V, and the second is a proof that the element is in the carrier set. Is ↑v just the first element of the pair, i.e. that element of V? I guess there could be multiple vector_space instances on that V, and it doesn't know which one to use? Even though there's only one in the search path?

(deleted)

#### Patrick Massot (Jul 10 2023 at 20:17):

Lean cannot guess what you mean here. You can help it with rw ← @vector_space.neg_one_smul_is_neg F _ V

#### Patrick Massot (Jul 10 2023 at 20:18):

But this isn't a good omen for your setup.

#### Reid Barton (Jul 10 2023 at 20:19):

Your definitions are sort of strange--starting already from add--because you write u + v for the first field of the result, but of course u + v should actually mean the very thing you are defining.
I guess Lean manages to figure out what you mean from the proof in the add case, but not the neg case.

#### Reid Barton (Jul 10 2023 at 20:20):

I would just write u.1 + v.1 and so on, but maybe more cultured people would write (u : V) + v or something.

#### Martin C. Martin (Jul 11 2023 at 18:29):

Thanks to everyone for the help, and I got the add_comm_group instance working. My next step is to add the following at the end (well, just before end subspace):

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 := by {intros, ext, simp, rw vector_space.left_distrib},
right_distrib := sorry
}


The rw in left_distrib fails, where the target is:
a • ↑(u + v) = ↑(⟨a • ↑u, _⟩ + ⟨a • ↑v, _⟩)
So it seems it's not applying the definition of add from the add_comm_group instance. How can I get it to do that? Shouldn't it be picking it up automatically? Here's the whole #mwe:

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 := by {intros, ext, simp, rw vector_space.left_distrib},
right_distrib := sorry
}

end subspace



#### Eric Wieser (Jul 11 2023 at 18:43):

Usually the approach would be:

• Provide has_add p
• Write some obvious lemmas about x + y where x y : p
• Prove more interesting results like add_comm_group p

You've skipped step 2!

#### Martin C. Martin (Jul 11 2023 at 18:46):

Ah, I think I see. Thanks!

#### Martin C. Martin (Jul 11 2023 at 19:09):

Great, I have that working. My final problem (in this task) is:
instance : vector_space F p := p.vector_space'
Fails because it can't prove ⊢ field ↥p. (Exact message: "failed to synthesize type class instance for")

Why is it trying to prove that ↥p is a field, and how do I get it to accept the above line? I'm following the pattern of module where, if q is a submodule, you can type q.module and get the module object corresponding to the submodule.

#### Eric Wieser (Jul 11 2023 at 19:14):

What does #check vector_space' show?

#### Martin C. Martin (Jul 11 2023 at 19:17):

unknown identifier 'vector_space'', which is odd, because you know it's defined right before that #check.

#### Martin C. Martin (Jul 11 2023 at 19:18):

subspace.vector_space' :
Π (F : Type u_3) {V : Type u_4} [_inst_1 : field F] [_inst_2 : add_comm_group V] [_inst_3 : vector_space F V]
{p : subspace F V}, vector_space F ↥p


for #check subspace.vector_space'

#### Martin C. Martin (Jul 11 2023 at 19:19):

Is this because the field is listed as an explicit, rather than implicit, argument?

#### Martin C. Martin (Jul 11 2023 at 19:24):

For submodule.module' I get:

submodule.module' :
Π (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


So, my subspace argument should be the first rather than last argument to subspace.vector_space'? Let's see if I can figure out how to reorder that.

#### Eric Wieser (Jul 11 2023 at 21:12):

Martin C. Martin said:

subspace.vector_space' :
Π (F : Type u_3) {V : Type u_4} [_inst_1 : field F] [_inst_2 : add_comm_group V] [_inst_3 : vector_space F V]
{p : subspace F V}, vector_space F ↥p


for #check subspace.vector_space'

This tells you that it is not expecting a p argument explicitly, and wants to be given F only

Last updated: Dec 20 2023 at 11:08 UTC