Distributing ↑ over (v + 0)

Stream: new members

[Martin C. Martin]

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


namespace LADR

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


structure AddCommSubgroup (V : Type _) [AddCommGroup V] where
  carrier : Set V
  add_mem' : ∀ {u v : V}, u ∈ carrier → v ∈ carrier → u + v ∈ carrier
  zero_mem' : (0 : V) ∈ carrier

namespace AddCommSubgroup

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

end AddCommSubgroup

-- 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
    AddCommSubgroup V where
  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)

instance foo : AddCommGroup p
    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⟩
  add_comm := by intros; ext; apply AddCommGroup.add_comm
  add_assoc := by intros; ext; apply AddCommGroup.add_assoc
  add_zero := by intro v; ext; rw [AddCommGroup.add_zero] --  <-- This fails.
  add_right_inv := by intros; ext; rw [AddCommGroup.add_right_inv] --  <-- This also fails.

end Subspace
end LADR

[Eric Wieser]

(note that Lean comments are -- not #)

[Jireh Loreaux]

Note:

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

[Jireh Loreaux]

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]

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]

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]

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]

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]

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]

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]

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.