Specifying subspaces in Lean

Stream: new members

[Martin C. Martin]

I’m translating Linear Algebra Done Right into Lean. Lean prefers types over sets, and prefers separate types over subtypes. For example, in Lean ℕ is not a subset of ℤ or ℝ, so we have three different types with e.g. three different objects called 5.

So my question is, what’s the best way to formalize subspaces in lean? Requiring that all vector spaces be Lean sets seems too restrictive. Does Lean have a notion of subtype that would be useful here, and e.g. allow you to say the null space of some arbitrary linear transformation is a subtype of the full vector space? Use an indicator function from V → bool (or Prop?) to say which elements are in the subspace? Something else?

For example, we want to prove that the sum of subspaces is the smallest containing subspace, that if U and W are subspaces, then U + W is a direct sum if and only if U ∩ W = {0}, etc.

[Yaël Dillies]

Have you looked at docs#submodule (or easier docs#subgroup).

[Martin C. Martin]

No, I'll look at that now, thanks!

[Martin C. Martin]

It's interesting the dichotomy between sets/predicates and types in Lean, and more generally in modern functional programming. The type framework seems much more rigid, in that you can't come up with some - perhaps undecidable - predicate and use that to define a type. Types, having well defined and easily decidable properties, make a lot of things easier. And of course avoids Russell's paradox. And yet there are times when we want something more flexible, and so use a set/predicate anyway, and need to have a separate definition like submodule.

Just thinking out loud.

[Pedro Sánchez Terraf]

Martin C. Martin said:

you can't come up with some - perhaps undecidable - predicate and use that to define a type.

Indeed you can, since everything is classical here---you only can't define a decidable type like that.

[Reid Barton]

Even in a constructive system you can define a subtype cut out by an undecidable predicate. It just means that whoever produces a term of that type has to provide a proof that the predicate holds.
Or did you mean something else by "use an undecidable predicate to define a type"?

[Martin C. Martin]

By "decidable" I'm think of inductive types, where the restrictions on the definition mean you can easily decide whether something exists, or whether two are the same. As opposed to, say, the set of all Godel numbers of machines that halt, which is famously undecidable.

In traditional math, we define group as a set with an operation that satisfies a few conditions. A subgroup just involves a subset of that original set; if you handed someone a subgroup, but didn't tell them about the larger original group, the subgroup would look just like a regular group to them. In Lean, we use type instead of set, but then when we define subgroup, we do use a set. If you hand this subgroup to someone, it doesn't quite fit the definition of a set, since the subgroup elements are "take this type and filter by this predicate", which is not the argument to the constructor of mathlib's group object.

It's just interesting that, while we try to stick to the nice world of inductively defined structures, we do sometimes find it useful to "break out" and allow an arbitrary predicate to be used to define the elements of our structures.

[Martin C. Martin]

@Yaël Dillies Is there a proof somewhere that a submodule is indeed a module? How are theorems about modules shown to also hold for submodules?

[Ruben Van de Velde]

docs#submodule.module

[Ruben Van de Velde]

Looks like another win for the naming convention

[Yaël Dillies]

I was about to type it myself (without first checking the docs, of course)

[Martin C. Martin]

Cool, thanks @Ruben Van de Velde (and @Yaël Dillies )

[Kyle Miller]

@Martin C. Martin There's some magic here that I think is worth elaborating. Every submodule is just a term (a structure), but you can regard it as being a type by taking its carrier set and coercing it to a type using subtype. Lean has a coercion facility where you can register coercion functions to convert terms to types, and it kicks in wherever you use something that's not a type where a type is expected.

So, if you have S : submodule M, then while module S isn't literally type correct since module expects a type, Lean coerces S to be a type, and it's that that is given the module structure, not S itself. But it's as-if S is a module.

This pattern is used for all algebraic sub-objects, and so some of the boilerplate has been abstracted into docs#set_like, for the very common case when your sub-object of an object can be identified with the set of elements of the object.

[Kyle Miller]

There are then two ways you can work with elements of submodules, and you can relatively freely go back and forth: either you work with terms of M itself along with proofs that they're elements of a submodule S, or you work with terms of (the coerced) S directly, which are each a bundled-up term+proof.

[Martin C. Martin]

Ah, interesting! So a type can correspond to some "crazy" subset, e.g. Godel numbers of programs that halt, through this coercion. Thanks!

[Martin C. Martin]

I guess docs#subgroup.to_group is the equivalent for groups?

[Yakov Pechersky]

if you handed someone a subgroup, but didn't tell them about the larger original group, the subgroup would look just like a regular group to them

If you didn't tell them about the larger original group, would you have really given them a subgroup?

So, similarly, when one writes a definition or a lemma that is general over any group as input, one can use it and apply it to subgroups (terms) that are promoted in-situ to types. However, in doing so, one can't rely on, in the body of that definition or lemma, on the subgroup-ness, since we are making a declaration that is general over any group.

Telling your interlocutor that you gave them a subgroup H -- how does that look like? In mathlib, that might mean providing the data of another group G along with an injective group hom H ->* G.

[Martin C. Martin]

Sorry, I wasn't very clear. When I say "I hand them a subgroup", I don't mean that I tell them it's a subgroup, I just give them a set & a function. For example, S = {(x, 3x) | x ∈ ℝ} is an additive group with the usual definition of addition, and I give them that. It doesn't matter whether I started from there, or started with G = {(x, y) | x, y ∈ ℝ } and then took the null space of some linear transformation.

Anyway, the fact that you can coerce a predicate into a type means that types can represent many types of sets.

[Eric Wieser]

If you hand them {(x, 3x) | x ∈ ℝ} then you have not met the conditions of

if you handed someone a subgroup, but didn't tell them about the larger original group

because you actually handed them ({(x, 3x) | x ∈ ℝ} : set (ℝ × ℝ)) which told them the original group was ℝ × ℝ

[Martin C. Martin]

@Kyle Miller @Eric Wieser I got part way with the set_like, but couldn't complete the definition for treating my custom subspace as a module. Some of the notation and concepts in set_like is foreign to me, and my attempts at monkey-see-monkey-do failed. Here's what I have:

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

structure subspace (F : Type*) (V : Type*)
  [field F] [add_comm_group V] [module F V]:=
(carrier : set V)
(add_mem' : ∀ {u v : V}, u ∈ carrier → v ∈ carrier → u + v ∈ carrier)
(zero_mem' : (0 : V) ∈ carrier)
(smul_mem' : ∀ (c : F) {v : V}, v ∈ carrier → c • v ∈ carrier )

namespace subspace

variables (F : Type*) {V : Type*} [field F] [add_comm_group V] [module F V]
variable {v : V}

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

variables {p : subspace F V}

instance module' [field F] [has_smul F V] [module F V] : module F p := sorry
instance : module F p := p.module'

end subspace

The instance module' gives the error in module F p, "failed to synthesize type class instance for". What do I need to get this working? Any hints? I'd like to prove that my subspace really is a module, have all module theorems apply to it.

Thanks in advance.

[Eric Wieser]

[has_smul F V] [module F V] is nonsense, it means "let there be two unrelated meanings of •, where only the second is a module"

[Martin C. Martin]

oh ok

[Eric Wieser]

failed to synthesize type class instance for

This is the first line of the message. The important lines come after it, but you didn't tell us what they were!

[Martin C. Martin]

I've replaced [has_smul F V] with [add_comm_group V] , but that doesn't seem to help. Here's the full error message:

failed to synthesize type class instance for
F : Type u_1,
V : Type u_2,
_inst_1 : field F,
_inst_2 : add_comm_group V,
_inst_3 : module F V,
p : subspace F V,
_inst_4 : field F,
_inst_5 : add_comm_group V,
_inst_6 : module F V
⊢ add_comm_monoid ↥p

[Martin C. Martin]

So I need to show my subspace is an add_comm_monoid? What is the ↥ symbol in ↥p?

[Martin C. Martin]

Should I define a subspace_class like the submodule_class in submodule?

[Kyle Miller]

I'm a bit of a monkey that sees and dos when it comes to the algebra hierarchy, but here's a potential way forward:

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

structure subspace (F : Type*) (V : Type*)
  [field F] [add_comm_group V] [module F V]:=
(carrier : set V)
(add_mem' : ∀ {u v : V}, u ∈ carrier → v ∈ carrier → u + v ∈ carrier)
(zero_mem' : (0 : V) ∈ carrier)
(smul_mem' : ∀ (c : F) {v : V}, v ∈ carrier → c • v ∈ carrier )

namespace subspace

variables (F : Type*) {V : Type*} [field F] [add_comm_group V] [module F V]
variable {v : V}

instance : set_like (subspace F V) V :=
⟨subspace.carrier, λ p q h, by cases p; cases q; congr'⟩

/-- This is a normalization lemma: we don't want to see `p.carrier` itself but rather its coercion
to `set V`. The coercion is inherited from `set_like`. -/
@[simp] lemma mem_carrier {p : subspace F V} : v ∈ p.carrier ↔ v ∈ (p : set V) := iff.rfl

/-- Standard extensionality lemma: if a type is like a set, then terms are equal if they
have the same elements. -/
@[ext] theorem ext {p q : subspace F V} (h : ∀ v, v ∈ p ↔ v ∈ q) : p = q := set_like.ext h

variables {p : subspace F V}

/-- `module F p` requires that `p` is an `add_comm_group` (when it's coerced to a type). -/
instance : add_comm_group p := sorry

/-- The module structure on `p` (when it's coerced to a type). -/
instance : module F p := sorry

end subspace

[Kyle Miller]

↥ is how Lean represents that it's inserted a coercion to turn something into a type

[Kyle Miller]

A Lean trick I always forget about: if you do instance : add_comm_group p := {! !} then this {! !} tells Lean to tell you available "hole commands" and if you select "Generate skeleton for the structure under construction" it replaces it with

instance : add_comm_group p := { add := _,
  add_assoc := _,
  zero := _,
  zero_add := _,
  add_zero := _,
  nsmul := _,
  nsmul_zero' := _,
  nsmul_succ' := _,
  neg := _,
  sub := _,
  sub_eq_add_neg := _,
  zsmul := _,
  zsmul_zero' := _,
  zsmul_succ' := _,
  zsmul_neg' := _,
  add_left_neg := _,
  add_comm := _ }

[Kyle Miller]

I'm not very familiar with the design behind submodule_class yet, but it's probably solving some engineering challenge that only shows up in the large scale, so you probably can avoid worrying about it for now.

[Eric Wieser]

docs#submodule_class no longer exists

[Kyle Miller]

Here's a start:

instance : add_comm_group p :=
{ add := λ x y, ⟨x + y, sorry⟩,
  zero := ⟨0, p.zero_mem'⟩,
  nsmul := λ c x, ⟨c • x, sorry⟩,
  zsmul := λ c x, ⟨c • x, sorry⟩,
  neg := λ x, ⟨-x, sorry⟩,
  sub := λ x y, ⟨x - y, sorry⟩,
  add_assoc := sorry,
  zero_add := sorry,
  add_zero := sorry,
  nsmul_zero' := sorry,
  nsmul_succ' := sorry,
  sub_eq_add_neg := sorry,
  zsmul_zero' := sorry,
  zsmul_succ' := sorry,
  zsmul_neg' := sorry,
  add_left_neg := sorry,
  add_comm := sorry }

I'm taking advantage of the coercions you get from p to V in these definitions

[Eric Wieser]

Building it that way is a lot more work that using docs#function.injective.add_comm_group, which saves you from all but the first 5 sorries