Stream: new members

Topic: Distributing ↑ over (v + 0)

Martin C. Martin (Nov 06 2023 at 18:49):

As an exercise, I'm defining vector spaces in Lean. However, I'm having trouble proving v + 0 = v in a subspace.

intro v; ext reduces the goal to ↑(v + 0) = ↑v, and next I'm hoping for something to distribute the ↑ on the left hand side. In Lean 3, simp would do that, but in Lean 4, simp just undoes the ext. I want to get to where I can use rw [AddCommGroup.add_zero] to finish the proof.

Here's my #mwe, sorry it's so long:

import Mathlib.Algebra.Field.Basic
import Mathlib.Data.SetLike.Basic

@[ext]
class AddCommGroup (V : Type _) extends Add V, Zero V, Neg V where
add_comm : ∀ u v : V, u + v = v + u
add_assoc : ∀ u v w : V, u + v + w = u + (v + w)
add_zero : ∀ v : V, v + 0 = v
add_right_inv : ∀ v : V, v + -v = 0

@[ext]
class VectorSpace (F : Type _) (V : Type _) [Field F] [AddCommGroup V] extends SMul F V where
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

variable {F : Type _} [field_f: Field F]

namespace VectorSpace

variable {V : Type _} [AddCommGroup V] [VectorSpace F V]

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

end VectorSpace

carrier : Set V
add_mem' : ∀ {u v : V}, u ∈ carrier → v ∈ carrier → u + v ∈ carrier
zero_mem' : (0 : V) ∈ carrier

variable {V : Type _} [AddCommGroup V] {v : V}

instance : SetLike (AddCommSubgroup V) V :=
⟨AddCommSubgroup.carrier, fun p q h => by cases p ; cases q ; congr⟩

@[simp]
theorem mem_carrier {p : AddCommSubgroup V} : v ∈ p.carrier ↔ v ∈ (p : Set V) :=
Iff.rfl

@[ext]
theorem ext {p q : AddCommSubgroup V} (h : ∀ v, v ∈ p ↔ v ∈ q) : p = q :=
SetLike.ext h

-- Because this is a structure rather than a class, it's ok to extend add_comm_subgroup
structure Subspace (F : Type _) (V : Type _) [Field F] [AddCommGroup V] [VectorSpace F V] extends
smul_mem' : ∀ (c : F) {v : V}, v ∈ carrier → c • v ∈ carrier

namespace Subspace

variable {F : Type _} {V : Type _} [Field F] [AddCommGroup V] [VectorSpace F V]

variable {v : V}

instance : SetLike (Subspace F V) V where
coe s := s.carrier
coe_injective' p q h := by cases p; cases q; congr; exact SetLike.coe_injective' h

@[simp]
theorem 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 :=
SetLike.ext h

variable (p : Subspace F V)

where
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 [← @VectorSpace.neg_one_smul_is_neg F _ V]; apply p.smul_mem'; simp⟩

end Subspace


Eric Wieser (Nov 06 2023 at 18:51):

(note that Lean comments are -- not #)

Jireh Loreaux (Nov 06 2023 at 18:52):

Note:

  add_zero := by intro v; ext; exact AddCommGroup.add_zero _ -- This works.


Jireh Loreaux (Nov 06 2023 at 18:53):

The issue is that you are defining addition on the subspace at the same time as you are proving properties about it. If you define the addition first, then you can have a coe_add lemma (proved by rfl) which you can then rewrite with when you create the AddCommGroup instance for subspaces.

Eric Wieser (Nov 06 2023 at 18:55):

Which would look like:

instance : Add p where
add u v := ⟨u.1 + v.1, by apply p.add_mem'; simp; simp⟩

@[simp] theorem val_add (a b : p) : (a + b).val = a.val + b.val := rfl

instance foo : AddCommGroup p where
add_zero := by intro v; ext; rw [val_add] -- this makes more progress
-- other fields,except add, as before


Martin C. Martin (Nov 06 2023 at 19:35):

Thanks to both of you! It's odd that exact works but apply and rw did not. Is this related to using an underscore with exact, but not with apply or rw?

Eric Wieser (Nov 06 2023 at 19:39):

I'm surprised it didn't work with apply, but it wouldn't work with rw because rw refuses to unfold definitions

Martin C. Martin (Nov 06 2023 at 19:40):

In general, I do struggle to understand when to use simp vs dsimp vs rw vs apply vs exact. I always thought anything that works with exact would also work with apply, that apply is a kind of recursive exact, but I guess that's not right.

Martin C. Martin (Nov 06 2023 at 19:42):

Actually, it does work with apply. I swore I tried that a few weeks ago and it didn't work. You can see I used it on the earlier ones. Maybe I still had the simp in there? Definitely doesn't work if you use simp before the apply.

Martin C. Martin (Nov 06 2023 at 19:43):

It seems odd that simp is undoing ext, but there's certainly a sense in which that's simpler. Still, I expect simp to unfold definitions, rather than the opposite.

Jireh Loreaux (Nov 06 2023 at 21:27):

I would not expect simp to unfold definitions in general (unless you pass them explicitly to the simp call). Often that would defeat the purpose of having the definition, which is to hide some object behind the default semireducible transparency.

Last updated: Dec 20 2023 at 11:08 UTC