Extentionality unfold Add.add with specific instance

Stream: new members

[Grant Yang]

Hi I'm learning lean and trying to prove that the space spanned by a set of vectors is a subspace by constructing an instance of AddCommGroup on a Subtype, but I'm getting stuck proving its properties since lean can't seem to find my definitions of addition etc.

instance zeroInst (S : Set V) : Zero {v : V // v ∈ span S} where
  zero := Subtype.mk 0 <| zero_in_span S

instance negInst (S : Set V) : Neg {v : V // v ∈ span S} where
  neg (a : {v : V // v ∈ span S}) :=
    Subtype.mk (-a.val) <| by
      have sub : -a.val = (-1 : ℝ) • a.val := by simp
      rw [sub]
      exact span_mul_closed S (-1) a

instance addInst (S : Set V) : Add {v : V // v ∈ span S} where
  add (a b : {v: V // v ∈ span S}) :=
    Subtype.mk (a.val + b.val) <| span_add_closed S a b

instance (S : Set V) : AddCommGroup {v: V // v ∈ span S} where
  -- add := (addInst S).add
  -- neg := (negInst S).neg
  -- zero := (zeroInst S).zero
  add_assoc := by
    intro a b c
    ext; simp only [] -- here, simp cannot make progress
  zero_add := sorry
  add_zero := sorry
  add_comm := sorry
  neg_add_cancel := sorry
  nsmul := nsmulRec
  zsmul := zsmulRec

I would expect lean to be able to unfold and prove the result from my definition of addition on the Subtype. Is there a way to fix this or am I approaching this wrong?

[Kenny Lau]

Please include import Mathlib and the needed lines on top so that the file can compile by itself. (#mwe)

[Kenny Lau]

without being able to check your code with Lean, when you define anything (in this case the addition instance) you need to provide the "API" (i.e. the required theorems to interact with it). In this case, you need to write down the lemma that coercion (a + b) = (coercion a) + (coercion b) which is the definition of your addition, and tag the lemma with simp.

simp only does not automatically unfold definitions.

[Grant Yang]

yeah i can't seem to expand the definition of addition to prove that (a+b).val = a.val + b.val.

import Mathlib.Algebra.Module.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable {V} [AddCommGroup V] [Module ℝ V]
def span (S : Set V) : Set V := sorry
theorem span_add_closed : ∀(S : Set V) (a b : {v : V // v ∈ span S}),
    a.val + b.val ∈ span S := by sorry

instance (S : Set V) : Add {v : V // v ∈ span S} where
  add (a b : {v: V // v ∈ span S}) :=
    Subtype.mk (a.val + b.val) <| span_add_closed S a b

@[simp]
theorem subtype_ext_add : ∀(S: Set V) (a b : {v : V // v ∈ span S}),
    (a + b).val = a.val + b.val := by
  intros S a b
  -- how do i prove this?
  sorry

[Grant Yang]

ok apparently writing

@[simp]
theorem subtype_ext_add : ∀(S: Set V) (a b : {v : V // v ∈ span S}),
    (a + b).val = a.val + b.val := by
  intros S a b
  rfl

just works lol?

[Kenny Lau]

yes, rw/simp and rfl are operating at different levels here and both are useful in different circumstances