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

Stream: new members

[Martin C. Martin]

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


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 + 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

end LADR

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]

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_2 : add_comm_group V,
_inst_3 : vector_space F V,
p : subspace F V,
v : ↥p
⊢ -↑v ∈ p

[Martin C. Martin]

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?

[Patrick Massot]

(deleted)

[Patrick Massot]

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

[Patrick Massot]

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

[Reid Barton]

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]

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]

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


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

end subspace

end LADR

[Eric Wieser]

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]

Ah, I think I see. Thanks!

[Martin C. Martin]

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]

What does #check vector_space' show?

[Martin C. Martin]

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

[Martin C. Martin]

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]

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

[Martin C. Martin]

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]

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