fix(Tactic/Simps): use capital letter for namespace (#647)

* Custom simps projections now are declared as `def MyStructure.Simps.myProjection` instead of `def MyStructure.simps.myProjection`. This declaration was already used in the library multiple times, even though it did nothing before.
* Use `symm_apply` instead of `symmApply` for lemmas generated by `simps`.
* Remove custom `simps` projection for `Subtype`. It did nothing, since coercions expand to `Subtype.val`. (Do we also want to rename the generated lemmas to `foo_val` instead of `foo_coe`?)
* Simplify some proofs using definitional eta for structures

Author: fpvandoorn

Mathlib/Data/Subtype.lean

@@ -28,10 +28,6 @@ namespace Subtype
 
 variable {α β γ : Sort _} {p q : α → Prop}
 
-/-- See Note [custom simps projection] -/
-def Simps.coe (x : Subtype p) : α :=
-  x
-
 initialize_simps_projections Subtype (val → coe)
 
 /-- A version of `x.property` or `x.2` where `p` is syntactically applied to the coercion of `x`

Mathlib/Logic/Equiv/Defs.lean

@@ -132,9 +132,9 @@ instance inhabited' : Inhabited (α ≃ α) := ⟨Equiv.refl α⟩
 protected def symm (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun, e.right_inv, e.left_inv⟩
 
 /-- See Note [custom simps projection] -/
-def Simps.symmApply (e : α ≃ β) : β → α := e.symm
+def Simps.symm_apply (e : α ≃ β) : β → α := e.symm
 
-initialize_simps_projections Equiv (toFun → apply, invFun → symmApply)
+initialize_simps_projections Equiv (toFun → apply, invFun → symm_apply)
 
 /-- Composition of equivalences `e₁ : α ≃ β` and `e₂ : β ≃ γ`. -/
 -- Porting note: `trans` attribute rejects this lemma because of implicit arguments.
@@ -545,20 +545,20 @@ end
 section
 
 /-- A `PSigma`-type is equivalent to the corresponding `Sigma`-type. -/
-@[simps apply symmApply]
+@[simps apply symm_apply]
 def psigmaEquivSigma {α} (β : α → Type _) : (Σ' i, β i) ≃ Σ i, β i where
   toFun a := ⟨a.1, a.2⟩
   invFun a := ⟨a.1, a.2⟩
-  left_inv | ⟨_, _⟩ => rfl
-  right_inv | ⟨_, _⟩ => rfl
+  left_inv _ := rfl
+  right_inv _ := rfl
 
 /-- A `psigma`-type is equivalent to the corresponding `sigma`-type. -/
-@[simps apply symmApply]
+@[simps apply symm_apply]
 def psigmaEquivSigmaPLift {α} (β : α → Sort _) : (Σ' i, β i) ≃ Σ i : PLift α, PLift (β i.down) where
   toFun a := ⟨PLift.up a.1, PLift.up a.2⟩
   invFun a := ⟨a.1.down, a.2.down⟩
-  left_inv | ⟨_, _⟩ => rfl
-  right_inv | ⟨_, _⟩ => rfl
+  left_inv _ := rfl
+  right_inv _ := rfl
 #align equiv.psigma_equiv_sigma_plift Equiv.psigmaEquivSigmaPLift
 
 /-- A family of equivalences `Π a, β₁ a ≃ β₂ a` generates an equivalence between `Σ' a, β₁ a` and
@@ -684,7 +684,7 @@ def sigmaCongr {α₁ α₂} {β₁ : α₁ → Sort _} {β₂ : α₂ → Sort
   (sigmaCongrRight F).trans (sigmaCongrLeft f)
 
 /-- `sigma` type with a constant fiber is equivalent to the product. -/
-@[simps apply symmApply] def sigmaEquivProd (α β : Type _) : (Σ _ : α, β) ≃ α × β :=
+@[simps apply symm_apply] def sigmaEquivProd (α β : Type _) : (Σ _ : α, β) ≃ α × β :=
   ⟨fun a => ⟨a.1, a.2⟩, fun a => ⟨a.1, a.2⟩, fun ⟨_, _⟩ => rfl, fun ⟨_, _⟩ => rfl⟩
 
 /-- If each fiber of a `sigma` type is equivalent to a fixed type, then the sigma type

Mathlib/Tactic/Simps/Basic.lean

@@ -179,11 +179,11 @@ derives two `simp` lemmas:
   notation is used instead of the corresponding projection.
   [TODO: not yet implemented for heterogenous operations like `HMul` and `HAdd`]
 * You can specify custom projections, by giving a declaration with name
-  `{StructureName}.simps.{projectionName}`. See Note [custom simps projection].
+  `{StructureName}.Simps.{projectionName}`. See Note [custom simps projection].
 
   Example:
   ```lean
-  def Equiv.simps.invFun (e : α ≃ β) : β → α := e.symm
+  def Equiv.Simps.invFun (e : α ≃ β) : β → α := e.symm
   @[simps] def Equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
   ⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
   ```
@@ -339,13 +339,13 @@ Some common uses:
   then you have to specify explicitly that you want to use a coercion
   as a custom projection. For example
   ```
-    def relEmbedding.simps.apply (h : r ↪r s) : α → β := h
+    def relEmbedding.Simps.apply (h : r ↪r s) : α → β := h
     initialize_simps_projections relEmbedding (to_embedding_toFun → apply, -to_embedding)
   ```
 * If you have an isomorphism-like structure (like `Equiv`) you often want to define a custom
   projection for the inverse:
   ```
-    def Equiv.simps.symm_apply (e : α ≃ β) : β → α := e.symm
+    def Equiv.Simps.symm_apply (e : α ≃ β) : β → α := e.symm
     initialize_simps_projections Equiv (toFun → apply, invFun → symm_apply)
   ```
 -/
@@ -359,7 +359,7 @@ macro "initialize_simps_projections?" rest:simpsProj : command =>
 end Command
 end Lean.Parser
 
-initialize registerTraceClass `simps.verbose
+initialize registerTraceClass `Simps.verbose
 initialize registerTraceClass `simps.debug
 
 /-- Projection data for a single projection of a structure -/
@@ -527,7 +527,7 @@ def simpsFindCustomProjection (str : Name) (proj : ParsedProjectionData)
   (rawUnivs : List Level) (trc : Bool) : CoreM ParsedProjectionData := do
   let env ← getEnv
   let (rawExpr, nrs) ← MetaM.run' (getCompositeOfProjections str proj.origName.getString!)
-  match env.find? (str ++ `simps ++ proj.newName) with
+  match env.find? (str ++ `Simps ++ proj.newName) with
   | some d@(.defnInfo _) =>
     let customProj := d.instantiateValueLevelParams! rawUnivs
     if trc then
@@ -617,7 +617,7 @@ attribute instead. See the documentation for this attribute for the data this ta
 
 The returned universe levels are the universe levels of the structure. For the projections there
 are three cases
-* If the declaration `{StructureName}.simps.{projectionName}` has been declared, then the value
+* If the declaration `{StructureName}.Simps.{projectionName}` has been declared, then the value
   of this declaration is used (after checking that it is definitionally equal to the actual
   projection. If you rename the projection name, the declaration should have the *new* projection
   name.
@@ -685,7 +685,7 @@ def simpsGetRawProjections (str : Name) (traceIfExists : Bool := false)
 library_note "custom simps projection"/--
 You can specify custom projections for the `@[simps]` attribute.
 To do this for the projection `MyStructure.originalProjection` by adding a declaration
-`MyStructure.simps.myProjection` that is definitionally equal to
+`MyStructure.Simps.myProjection` that is definitionally equal to
 `MyStructure.originalProjection` but has the projection in the desired (simp-normal) form.
 Then you can call
 ```

test/Simps.lean

@@ -34,7 +34,7 @@ run_cmd liftTermElabM <| do
 structure Foo2 (α : Type _) : Type _ where
   elim : α × α
 
-def Foo2.simps.elim (α : Type _) : Foo2 α → α × α := fun x => (x.elim.1, x.elim.2)
+def Foo2.Simps.elim (α : Type _) : Foo2 α → α × α := fun x => (x.elim.1, x.elim.2)
 
 initialize_simps_projections Foo2
 
@@ -70,7 +70,7 @@ initialize_simps_projections Top
 
 structure NewTop (α β : Type _) extends Right α β, Left α
 
-def NewTop.simps.newElim {α β : Type _} (x : NewTop α β) : α × α := x.elim
+def NewTop.Simps.newElim {α β : Type _} (x : NewTop α β) : α × α := x.elim
 
 initialize_simps_projections NewTop (toRight_toFoo2_elim → newElim)
 
@@ -578,7 +578,7 @@ instance : CoeFun (α ≃ β) (λ _ => α → β) := ⟨Equiv.toFun⟩
 def Equiv.symm (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun⟩
 
 /-- See Note [custom simps projection] -/
-def Equiv.simps.invFun (e : α ≃ β) : β → α := e.symm
+def Equiv.Simps.invFun (e : α ≃ β) : β → α := e.symm
 
 /-- Composition of equivalences `e₁ : α ≃ β` and `e₂ : β ≃ γ`. -/
 @[simps (config := {simpRhs := true})]
@@ -602,7 +602,7 @@ local infix:25 (priority := high) " ≃ " => FaultyManualCoercion.Equiv
 variable {α β γ : Sort _}
 
 /-- See Note [custom simps projection] -/
-noncomputable def Equiv.simps.invFun (e : α ≃ β) : β → α := Classical.choice ⟨e.invFun⟩
+noncomputable def Equiv.Simps.invFun (e : α ≃ β) : β → α := Classical.choice ⟨e.invFun⟩
 
 run_cmd liftTermElabM <| do
   successIfFail (simpsGetRawProjections `FaultyManualCoercion.Equiv)
@@ -628,7 +628,7 @@ instance : CoeFun (α ≃ β) (λ _ => α → β) := ⟨Equiv.toFun⟩
 def Equiv.symm (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun⟩
 
 /-- See Note [custom simps projection] -/
-def Equiv.simps.invFun (e : α ≃ β) : β → α := e.symm
+def Equiv.Simps.invFun (e : α ≃ β) : β → α := e.symm
 
 initialize_simps_projections Equiv
 
@@ -660,7 +660,7 @@ instance : CoeFun (α ≃ β) (λ _ => α → β) := ⟨Equiv.toFun⟩
 def Equiv.symm (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun⟩
 
 /-- See Note [custom simps projection] -/
-def Equiv.simps.invFun {α : Type u} {β : Type v} (e : α ≃ β) : β → α := e.symm
+def Equiv.Simps.invFun {α : Type u} {β : Type v} (e : α ≃ β) : β → α := e.symm
 
 run_cmd liftTermElabM <| do
   successIfFail (simpsGetRawProjections `FaultyUniverses.Equiv)
@@ -690,7 +690,7 @@ def Equiv.symm (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun⟩
 
 /-- See Note [custom simps projection] -/
 -- test: intentionally using different unvierse levels for Equiv.symm than for Equiv
-def Equiv.simps.invFun {α : Sort w} {β : Sort u} (e : α ≃ β) : β → α := e.symm
+def Equiv.Simps.invFun {α : Sort w} {β : Sort u} (e : α ≃ β) : β → α := e.symm
 
 -- check whether we can generate custom projections even if the universe names don't match
 initialize_simps_projections Equiv
@@ -712,7 +712,7 @@ instance : CoeFun (α ≃ β) (λ _ => α → β) := ⟨Equiv.toFun⟩
 def Equiv.symm (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun⟩
 
 /-- See Note [custom simps projection] -/
-def Equiv.simps.symm_apply (e : α ≃ β) : β → α := e.symm
+def Equiv.Simps.symm_apply (e : α ≃ β) : β → α := e.symm
 
 initialize_simps_projections Equiv (toFun → apply, invFun → symm_apply)
 
@@ -752,7 +752,7 @@ instance : CoeFun (α ≃ β) (λ _ => α → β) := ⟨Equiv.toFun⟩
 def Equiv.symm (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun⟩
 
 /-- See Note [custom simps projection] -/
-def Equiv.simps.symm_apply (e : α ≃ β) : β → α := e.symm
+def Equiv.Simps.symm_apply (e : α ≃ β) : β → α := e.symm
 initialize_simps_projections Equiv (toFun → coe as_prefix, invFun → symm_apply)
 
 run_cmd liftTermElabM <| do
@@ -999,8 +999,8 @@ def DecoratedEquiv.symm {α β : Sort _} (e : DecoratedEquiv α β) : DecoratedE
   P_toFun := e.P_invFun
   P_invFun := e.P_toFun }
 
-def DecoratedEquiv.simps.apply {α β : Sort _} (e : DecoratedEquiv α β) : α → β := e
-def DecoratedEquiv.simps.symm_apply {α β : Sort _} (e : DecoratedEquiv α β) : β → α := e.symm
+def DecoratedEquiv.Simps.apply {α β : Sort _} (e : DecoratedEquiv α β) : α → β := e
+def DecoratedEquiv.Simps.symm_apply {α β : Sort _} (e : DecoratedEquiv α β) : β → α := e.symm
 
 initialize_simps_projections DecoratedEquiv
   (toEquiv'_toFun → apply, toEquiv'_invFun → symm_apply, -toEquiv')
@@ -1052,8 +1052,8 @@ def FurtherDecoratedEquiv.symm {α β : Sort _} (e : FurtherDecoratedEquiv α β
   Q_toFun := e.Q_invFun
   Q_invFun := e.Q_toFun }
 
-def FurtherDecoratedEquiv.simps.apply {α β : Sort _} (e : FurtherDecoratedEquiv α β) : α → β := e
-def FurtherDecoratedEquiv.simps.symm_apply {α β : Sort _} (e : FurtherDecoratedEquiv α β) :
+def FurtherDecoratedEquiv.Simps.apply {α β : Sort _} (e : FurtherDecoratedEquiv α β) : α → β := e
+def FurtherDecoratedEquiv.Simps.symm_apply {α β : Sort _} (e : FurtherDecoratedEquiv α β) :
   β → α := e.symm
 
 initialize_simps_projections FurtherDecoratedEquiv
@@ -1091,8 +1091,8 @@ def OneMore.symm {α β : Sort _} (e : OneMore α β) :
   OneMore β α :=
 { toFurtherDecoratedEquiv := e.toFurtherDecoratedEquiv.symm }
 
-def OneMore.simps.apply {α β : Sort _} (e : OneMore α β) : α → β := e
-def OneMore.simps.symm_apply {α β : Sort _} (e : OneMore α β) : β → α := e.symm
+def OneMore.Simps.apply {α β : Sort _} (e : OneMore α β) : α → β := e
+def OneMore.Simps.symm_apply {α β : Sort _} (e : OneMore α β) : β → α := e.symm
 
 initialize_simps_projections OneMore
   (toFurtherDecoratedEquiv_toDecoratedEquiv_toEquiv'_toFun → apply,
@@ -1137,7 +1137,7 @@ instance (M N : Type _) [AddMonoid M] [AddMonoid N] : CoeFun (M →+ N) (λ _ =>
 class AddHomPlus [Add ι] [∀ i, AddCommMonoid (A i)] :=
 (mul {i} : A i →+ A i)
 
-def AddHomPlus.simps.apply [Add ι] [∀ i, AddCommMonoid (A i)] [AddHomPlus A] {i : ι} (x : A i) :
+def AddHomPlus.Simps.apply [Add ι] [∀ i, AddCommMonoid (A i)] [AddHomPlus A] {i : ι} (x : A i) :
   A i :=
 AddHomPlus.mul x
 
@@ -1146,7 +1146,7 @@ initialize_simps_projections AddHomPlus (mul_toZeroHom_toFun → apply, -mul)
 class AddHomPlus2 [Add ι] :=
 (mul {i j} : A i ≃ (A j ≃ A (i + j)))
 
-def AddHomPlus2.simps.mul [Add ι] [AddHomPlus2 A] {i j : ι}
+def AddHomPlus2.Simps.mul [Add ι] [AddHomPlus2 A] {i j : ι}
   (x : A i) (y : A j) : A (i + j) :=
 AddHomPlus2.mul x y