Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix: initialize_simps_projections print warning when projection data already exists #20339

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
+62 −67
Open

fix: initialize_simps_projections print warning when projection data already exists #20339

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
14c4fac
warning when projections already exists
fpvandoorn Dec 30, 2024
8946bf5
fix
fpvandoorn Jan 6, 2025
eb9b33c
fix
fpvandoorn Jan 6, 2025
ceec3f0
Merge remote-tracking branch 'origin/master' into simps-already-exists
fpvandoorn Jan 22, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 7 additions & 10 deletions Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,13 +45,10 @@ structure ContinuousAffineEquiv (k P₁ P₂ : Type*) {V₁ V₂ : Type*} [Ring
notation:25 P₁ " ≃ᵃL[" k:25 "] " P₂:0 => ContinuousAffineEquiv k P₁ P₂

variable {k P₁ P₂ P₃ P₄ V₁ V₂ V₃ V₄ : Type*} [Ring k]
[AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁]
[AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂]
[AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃]
[AddCommGroup V₄] [Module k V₄] [AddTorsor V₄ P₄]
[TopologicalSpace P₁]
[TopologicalSpace P₂]
[TopologicalSpace P₃] [TopologicalSpace P₄]
[AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁]
[AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂]
[AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃]
[AddCommGroup V₄] [Module k V₄] [AddTorsor V₄ P₄] [TopologicalSpace P₄]

namespace ContinuousAffineEquiv

Expand Down Expand Up @@ -102,10 +99,10 @@ def Simps.apply (e : P₁ ≃ᵃL[k] P₂) : P₁ → P₂ :=
e

/-- See Note [custom simps projection]. -/
def Simps.coe (e : P₁ ≃ᵃL[k] P₂) : P₁ ≃ᵃ[k] P₂ :=
e
def Simps.symm_apply (e : P₁ ≃ᵃL[k] P₂) : P₂ → P₁ :=
e.symm

initialize_simps_projections ContinuousLinearMap (toFun → apply, toAffineEquiv → coe)
initialize_simps_projections ContinuousAffineEquiv (toFun → apply, invFun → symm_apply)

@[ext]
theorem ext {e e' : P₁ ≃ᵃL[k] P₂} (h : ∀ x, e x = e' x) : e = e' :=
Expand Down
35 changes: 14 additions & 21 deletions Mathlib/RingTheory/Bialgebra/Equiv.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -145,14 +145,6 @@ variable [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B]

variable (e e' : A ≃ₐc[R] B)

/-- See Note [custom simps projection] -/
def Simps.apply {R : Type u} [CommSemiring R] {α : Type v} {β : Type w}
[Semiring α] [Semiring β] [Algebra R α]
[Algebra R β] [CoalgebraStruct R α] [CoalgebraStruct R β]
(f : α ≃ₐc[R] β) : α → β := f

initialize_simps_projections BialgEquiv (toFun → apply)

@[simp, norm_cast]
theorem coe_coe : ⇑(e : A →ₐc[R] B) = e :=
rfl
Expand Down Expand Up @@ -202,17 +194,27 @@ protected theorem congr_fun (h : e = e') (x : A) : e x = e' x :=

end

section
/-- See Note [custom simps projection] -/
def Simps.apply {R : Type u} [CommSemiring R] {α : Type v} {β : Type w}
[Semiring α] [Semiring β] [Algebra R α]
[Algebra R β] [CoalgebraStruct R α] [CoalgebraStruct R β]
(f : α ≃ₐc[R] β) : α → β := f

/-- See Note [custom simps projection] -/
def Simps.symm_apply {R : Type*} [CommSemiring R]
{A : Type*} {B : Type*} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
[CoalgebraStruct R A] [CoalgebraStruct R B]
(e : A ≃ₐc[R] B) : B → A :=
e.symm

variable (A R)
initialize_simps_projections BialgEquiv (toFun → apply, invFun → symm_apply)

variable (A R) in
/-- The identity map is a bialgebra equivalence. -/
@[refl, simps!]
def refl : A ≃ₐc[R] A :=
{ CoalgEquiv.refl R A, BialgHom.id R A with }

end

@[simp]
theorem refl_toCoalgEquiv : refl R A = CoalgEquiv.refl R A := rfl

Expand All @@ -229,15 +231,6 @@ def symm (e : A ≃ₐc[R] B) : B ≃ₐc[R] A :=
theorem symm_toCoalgEquiv (e : A ≃ₐc[R] B) :
e.symm = (e : A ≃ₗc[R] B).symm := rfl

/-- See Note [custom simps projection] -/
def Simps.symm_apply {R : Type*} [CommSemiring R]
{A : Type*} {B : Type*} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
[CoalgebraStruct R A] [CoalgebraStruct R B]
(e : A ≃ₐc[R] B) : B → A :=
e.symm

initialize_simps_projections BialgEquiv (invFun → symm_apply)

theorem invFun_eq_symm : e.invFun = e.symm :=
rfl

Expand Down
61 changes: 27 additions & 34 deletions Mathlib/RingTheory/Coalgebra/Equiv.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -118,14 +118,6 @@ variable [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [Module R A] [Mod

variable (e e' : A ≃ₗc[R] B)

/-- See Note [custom simps projection] -/
def Simps.apply {R : Type*} [CommSemiring R] {α β : Type*}
[AddCommMonoid α] [AddCommMonoid β] [Module R α]
[Module R β] [CoalgebraStruct R α] [CoalgebraStruct R β]
(f : α ≃ₗc[R] β) : α → β := f

initialize_simps_projections CoalgEquiv (toFun → apply)

@[simp, norm_cast]
theorem coe_coe : ⇑(e : A →ₗc[R] B) = e :=
rfl
Expand Down Expand Up @@ -165,37 +157,47 @@ protected theorem congr_fun (h : e = e') (x : A) : e x = e' x :=

end

section
/-- Coalgebra equivalences are symmetric. -/
@[symm]
def symm (e : A ≃ₗc[R] B) : B ≃ₗc[R] A :=
{ (e : A ≃ₗ[R] B).symm with
counit_comp := (LinearEquiv.comp_toLinearMap_symm_eq _ _).2 e.counit_comp.symm
map_comp_comul := by
show (TensorProduct.congr (e : A ≃ₗ[R] B) (e : A ≃ₗ[R] B)).symm.toLinearMap ∘ₗ comul
= comul ∘ₗ (e : A ≃ₗ[R] B).symm
rw [LinearEquiv.toLinearMap_symm_comp_eq]
simp only [TensorProduct.congr, toLinearEquiv_toLinearMap,
LinearEquiv.ofLinear_toLinearMap, ← LinearMap.comp_assoc, CoalgHomClass.map_comp_comul,
LinearEquiv.eq_comp_toLinearMap_symm] }

/-- See Note [custom simps projection] -/
def Simps.apply {R : Type*} [CommSemiring R] {α β : Type*}
[AddCommMonoid α] [AddCommMonoid β] [Module R α]
[Module R β] [CoalgebraStruct R α] [CoalgebraStruct R β]
(f : α ≃ₗc[R] β) : α → β := f

/-- See Note [custom simps projection] -/
def Simps.symm_apply {R : Type*} [CommSemiring R]
{A : Type*} {B : Type*} [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B]
[CoalgebraStruct R A] [CoalgebraStruct R B]
(e : A ≃ₗc[R] B) : B → A :=
e.symm

variable (A R)
initialize_simps_projections CoalgEquiv (toFun → apply, invFun → symm_apply)

variable (A R) in
/-- The identity map is a coalgebra equivalence. -/
@[refl, simps!]
def refl : A ≃ₗc[R] A :=
{ CoalgHom.id R A, LinearEquiv.refl R A with }

end

@[simp]
theorem refl_toLinearEquiv : refl R A = LinearEquiv.refl R A := rfl

@[simp]
theorem refl_toCoalgHom : refl R A = CoalgHom.id R A :=
rfl

/-- Coalgebra equivalences are symmetric. -/
@[symm]
def symm (e : A ≃ₗc[R] B) : B ≃ₗc[R] A :=
{ (e : A ≃ₗ[R] B).symm with
counit_comp := (LinearEquiv.comp_toLinearMap_symm_eq _ _).2 e.counit_comp.symm
map_comp_comul := by
show (TensorProduct.congr (e : A ≃ₗ[R] B) (e : A ≃ₗ[R] B)).symm.toLinearMap ∘ₗ comul
= comul ∘ₗ (e : A ≃ₗ[R] B).symm
rw [LinearEquiv.toLinearMap_symm_comp_eq]
simp only [TensorProduct.congr, toLinearEquiv_toLinearMap,
LinearEquiv.ofLinear_toLinearMap, ← LinearMap.comp_assoc, CoalgHomClass.map_comp_comul,
LinearEquiv.eq_comp_toLinearMap_symm] }

@[simp]
theorem symm_toLinearEquiv (e : A ≃ₗc[R] B) :
e.symm = (e : A ≃ₗ[R] B).symm := rfl
Expand All @@ -217,15 +219,6 @@ theorem apply_symm_apply (e : A ≃ₗc[R] B) (x) :
e (e.symm x) = x :=
LinearEquiv.apply_symm_apply (e : A ≃ₗ[R] B) x

/-- See Note [custom simps projection] -/
def Simps.symm_apply {R : Type*} [CommSemiring R]
{A : Type*} {B : Type*} [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B]
[CoalgebraStruct R A] [CoalgebraStruct R B]
(e : A ≃ₗc[R] B) : B → A :=
e.symm

initialize_simps_projections CoalgEquiv (invFun → symm_apply)

@[simp]
theorem invFun_eq_symm : e.invFun = e.symm :=
rfl
Expand Down
6 changes: 4 additions & 2 deletions Mathlib/Tactic/Simps/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -783,8 +783,10 @@ def getRawProjections (stx : Syntax) (str : Name) (traceIfExists : Bool := false
-- We always print the projections when they already exists and are called by
-- `initialize_simps_projections`.
withOptions (· |>.updateBool `trace.simps.verbose (traceIfExists || ·)) <| do
trace[simps.debug]
projectionsInfo data.2.toList "Already found projection information for structure" str
trace[simps.verbose]
projectionsInfo data.2.toList "The projections for this structure have already been \
initialized by a previous invocation of `initialize_simps_projections` or `@[simps]`.\n\
Generated projections for" str
return data
trace[simps.verbose] "generating projection information for structure {str}."
trace[simps.debug] "Applying the rules {rules}."
Expand Down
10 changes: 10 additions & 0 deletions MathlibTest/Simps.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,16 @@ def Foo2.Simps.elim (α : Type _) : Foo2 α → α × α := fun x ↦ (x.elim.1,

initialize_simps_projections Foo2


/--
info: [simps.verbose] The projections for this structure have already been initialized by a previous invocation of `initialize_simps_projections` or `@[simps]`.
Generated projections for Foo2:
Projection elim: fun α x => (x.elim.1, x.elim.2)
-/
#guard_msgs in
initialize_simps_projections Foo2


@[simps]
def Foo2.foo2 : Foo2 Nat := ⟨(0, 0)⟩

Expand Down
Loading