[Merged by Bors] - chore: Remove unnecessary "rw"s by darabos · Pull Request #10704 · leanprover-community/mathlib4

darabos · 2024-02-18T21:38:51Z

Remove unnecessary "rw"s.

This is a non-forked and updated version of #10338. I figure if the proofs still work without these rewrites, then it's best if we remove them, right?

…-rws

Vierkantor

Impressive work! I hope you used some sort of automation for this, you didn't open up every file and go through every rw by hand, right?!

I think we should slightly more careful in removing rw rules here: if the two sides happen to be definitionally equal according to rfl, we don't always have that rw sees this too. The latter is important if the context changes and we need to add an additional rw step. So I went through and suggested to revert every change where the two sides did not end up exactly the same (at least, the same as far as rw is concerned). On the other hand, it seems much easier to implement automation for trimming a rw set if the only criteria are that the proof still goes through. And maybe some types of definitional equalities are more acceptable than others, so I labeled each of the suggestions.

What do you think?

Vierkantor · 2024-02-19T14:24:32Z

Mathlib/Algebra/DirectSum/Decomposition.lean


 theorem decompose_of_mem_same {x : M} {i : ι} (hx : x ∈ ℳ i) : (decompose ℳ x i : M) = x := by
-  rw [decompose_of_mem _ hx, DirectSum.of_eq_same, Subtype.coe_mk]
+  rw [decompose_of_mem _ hx, DirectSum.of_eq_same]


Closing this goal requires reducing the same projection as Subtype.coe_mk does, so let's keep it:

Suggested change

rw [decompose_of_mem _ hx, DirectSum.of_eq_same]

rw [decompose_of_mem _ hx, DirectSum.of_eq_same, Subtype.coe_mk]

Vierkantor · 2024-02-19T14:26:29Z

Mathlib/Algebra/Module/Zlattice.lean

  use (b.restrictScalars ℤ).repr ⟨v, h⟩ i
  rw [map_add, Finsupp.coe_add, Pi.add_apply, add_tsub_cancel_right,
-    ← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply, coe_mk]
+    ← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply]


This is another projection reduction that I would like to keep:

Suggested change

← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply]

← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply, coe_mk]

Vierkantor · 2024-02-19T14:27:03Z

Mathlib/Algebra/MonoidAlgebra/Grading.lean

      simp only [MonoidHom.coe_comp, MonoidHom.coe_coe, AlgHom.coe_comp, Function.comp_apply,
        of_apply, AlgHom.coe_id, id_eq]
-      rw [decomposeAux_single, DirectSum.coeAlgHom_of, Subtype.coe_mk])
+      rw [decomposeAux_single, DirectSum.coeAlgHom_of])


idem:

Suggested change

rw [decomposeAux_single, DirectSum.coeAlgHom_of])

rw [decomposeAux_single, DirectSum.coeAlgHom_of, Subtype.coe_mk])

Vierkantor · 2024-02-19T14:28:39Z

Mathlib/AlgebraicGeometry/StructureSheaf.lean

  Subtype.eq <|
    funext fun x =>
-      IsLocalization.mk'_eq_of_eq (by rw [mul_comm, Subtype.coe_mk, ← h, mul_comm, Subtype.coe_mk])
+      IsLocalization.mk'_eq_of_eq (by rw [mul_comm, Subtype.coe_mk, ← h, mul_comm])


idem:

Suggested change

IsLocalization.mk'_eq_of_eq (by rw [mul_comm, Subtype.coe_mk, ← h, mul_comm])

IsLocalization.mk'_eq_of_eq (by rw [mul_comm, Subtype.coe_mk, ← h, mul_comm, Subtype.coe_mk])

Vierkantor · 2024-02-19T14:29:03Z

Mathlib/Analysis/Analytic/Composition.lean

  obtain rfl : j = 0 := by linarith
  refine' congr_arg v _
-  rw [Fin.ext_iff, Fin.coe_castLE, Composition.ones_embedding, Fin.val_mk]
+  rw [Fin.ext_iff, Fin.coe_castLE, Composition.ones_embedding]


idem:

Suggested change

rw [Fin.ext_iff, Fin.coe_castLE, Composition.ones_embedding]

rw [Fin.ext_iff, Fin.coe_castLE, Composition.ones_embedding, Fin.val_mk]

Vierkantor · 2024-02-19T15:22:40Z

Mathlib/RingTheory/IsAdjoinRoot.lean

        rw [h.basis.repr_self, ← Finsupp.single_eq_pi_single,
          Finsupp.single_apply_left Fin.val_injective]
-      _ = Pi.single (f := fun _ => R) n 1 i := by rw [Fin.val_mk, Fin.val_mk]
+      _ = Pi.single (f := fun _ => R) n 1 i := by rw [Fin.val_mk]


Structure projection:

Suggested change

_ = Pi.single (f := fun _ => R) n 1 i := by rw [Fin.val_mk]

_ = Pi.single (f := fun _ => R) n 1 i := by rw [Fin.val_mk, Fin.val_mk]

or alternatively:

Suggested change

_ = Pi.single (f := fun _ => R) n 1 i := by rw [Fin.val_mk]

_ = Pi.single (f := fun _ => R) n 1 i := rfl

Vierkantor · 2024-02-19T15:26:20Z

Mathlib/RingTheory/UniqueFactorizationDomain.lean

    (by
      rw [Associates.factors_prod, FactorSet.prod]
-      dsimp; rw [Multiset.map_replicate, Multiset.prod_replicate, Subtype.coe_mk])
+      dsimp; rw [Multiset.map_replicate, Multiset.prod_replicate])


Structure projection:

Suggested change

dsimp; rw [Multiset.map_replicate, Multiset.prod_replicate])

dsimp; rw [Multiset.map_replicate, Multiset.prod_replicate, Subtype.coe_mk])

Vierkantor · 2024-02-19T15:27:16Z

Mathlib/RingTheory/WittVector/Truncated.lean

 @[simp]
 theorem coeff_out (x : TruncatedWittVector p n R) (i : Fin n) : x.out.coeff i = x.coeff i := by
-  rw [out]; dsimp only; rw [dif_pos i.is_lt, Fin.eta]
+  rw [out]; dsimp only; rw [dif_pos i.is_lt]


Structure eta:

Suggested change

rw [out]; dsimp only; rw [dif_pos i.is_lt]

rw [out]; dsimp only; rw [dif_pos i.is_lt, Fin.eta]

Vierkantor · 2024-02-19T15:27:30Z

Mathlib/RingTheory/WittVector/Truncated.lean

  dsimp [TruncatedWittVector.out, init, select, coeff_mk]
  split_ifs with hi; swap; · rfl
-  rw [coeff_truncateFun, Fin.val_mk]
+  rw [coeff_truncateFun]


Structure projection:

Suggested change

rw [coeff_truncateFun]

rw [coeff_truncateFun, Fin.val_mk]

Vierkantor · 2024-02-19T15:30:43Z

Mathlib/Topology/MetricSpace/GromovHausdorff.lean

      let i : ℕ := E q ⟨y, ys⟩
      let hi := ((E q) ⟨y, ys⟩).2
-      have ihi_eq : (⟨i, hi⟩ : Fin (N q)) = (E q) ⟨y, ys⟩ := by rw [Fin.ext_iff, Fin.val_mk]
+      have ihi_eq : (⟨i, hi⟩ : Fin (N q)) = (E q) ⟨y, ys⟩ := by rw [Fin.ext_iff]


Structure projection:

Suggested change

have ihi_eq : (⟨i, hi⟩ : Fin (N q)) = (E q) ⟨y, ys⟩ := by rw [Fin.ext_iff]

have ihi_eq : (⟨i, hi⟩ : Fin (N q)) = (E q) ⟨y, ys⟩ := by rw [Fin.ext_iff, Fin.val_mk]

…actly the same.

darabos · 2024-02-19T17:31:18Z

Impressive work! I hope you used some sort of automation for this, you didn't open up every file and go through every rw by hand, right?!

Haha, no! We're working on a system (machine learning) where the unnecessary rws manifested as errors. I thought this accidental detection may actually be useful for something.

I think we should slightly more careful in removing rw rules here: if the two sides happen to be definitionally equal according to rfl, we don't always have that rw sees this too. The latter is important if the context changes and we need to add an additional rw step. So I went through and suggested to revert every change where the two sides did not end up exactly the same (at least, the same as far as rw is concerned). On the other hand, it seems much easier to implement automation for trimming a rw set if the only criteria are that the proof still goes through. And maybe some types of definitional equalities are more acceptable than others, so I labeled each of the suggestions.

What do you think?

Sorry, I'm too new to Lean to have an opinion on this. I implemented your suggested changes. Thanks for the careful review!

Vierkantor

Thanks! I really appreciate the time you took to deal with these little annoyances.

bors r+

Remove unnecessary "rw"s.

mathlib-bors · 2024-02-20T11:30:20Z

Pull request successfully merged into master.

Build succeeded:

Remove unnecessary "rw"s.

darabos added 2 commits February 18, 2024 22:01

Remove unnecessary "rw"s.

f636b35

Merge remote-tracking branch 'public/master' into darabos-unnecessary…

5350bd2

…-rws

darabos mentioned this pull request Feb 18, 2024

Remove two unnecessary rws #10338

Closed

Vierkantor self-assigned this Feb 19, 2024

Vierkantor added the awaiting-review label Feb 19, 2024

Vierkantor changed the title ~~Remove unnecessary "rw"s~~ chore: Remove unnecessary "rw"s Feb 19, 2024

Vierkantor reviewed Feb 19, 2024

View reviewed changes

Vierkantor added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Feb 19, 2024

darabos added 2 commits February 19, 2024 18:23

Revert the "rw" simplifications where the two sides did not end up ex…

0ec56ba

…actly the same.

Resolve porting note per @Vierkantor's suggestion.

646dfd9

Vierkantor approved these changes Feb 20, 2024

View reviewed changes

ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Feb 20, 2024

mathlib-bors bot pushed a commit that referenced this pull request Feb 20, 2024

chore: Remove unnecessary "rw"s (#10704)

db5a937

Remove unnecessary "rw"s.

mathlib-bors bot changed the title ~~chore: Remove unnecessary "rw"s~~ [Merged by Bors] - chore: Remove unnecessary "rw"s Feb 20, 2024

mathlib-bors bot closed this Feb 20, 2024

mathlib-bors bot deleted the darabos-unnecessary-rws branch February 20, 2024 11:30

thorimur pushed a commit that referenced this pull request Feb 24, 2024

chore: Remove unnecessary "rw"s (#10704)

ce60eaa

Remove unnecessary "rw"s.

thorimur pushed a commit that referenced this pull request Feb 26, 2024

chore: Remove unnecessary "rw"s (#10704)

04ab60b

Remove unnecessary "rw"s.

riccardobrasca pushed a commit that referenced this pull request Mar 1, 2024

chore: Remove unnecessary "rw"s (#10704)

45f1499

Remove unnecessary "rw"s.

dagurtomas pushed a commit that referenced this pull request Mar 22, 2024

chore: Remove unnecessary "rw"s (#10704)

ad24340

Remove unnecessary "rw"s.

	rw [decompose_of_mem _ hx, DirectSum.of_eq_same]
	rw [decompose_of_mem _ hx, DirectSum.of_eq_same, Subtype.coe_mk]

	← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply]
	← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply, coe_mk]

	rw [decomposeAux_single, DirectSum.coeAlgHom_of])
	rw [decomposeAux_single, DirectSum.coeAlgHom_of, Subtype.coe_mk])

	IsLocalization.mk'_eq_of_eq (by rw [mul_comm, Subtype.coe_mk, ← h, mul_comm])
	IsLocalization.mk'_eq_of_eq (by rw [mul_comm, Subtype.coe_mk, ← h, mul_comm, Subtype.coe_mk])

	rw [Fin.ext_iff, Fin.coe_castLE, Composition.ones_embedding]
	rw [Fin.ext_iff, Fin.coe_castLE, Composition.ones_embedding, Fin.val_mk]

	_ = Pi.single (f := fun _ => R) n 1 i := by rw [Fin.val_mk]
	_ = Pi.single (f := fun _ => R) n 1 i := by rw [Fin.val_mk, Fin.val_mk]

	dsimp; rw [Multiset.map_replicate, Multiset.prod_replicate])
	dsimp; rw [Multiset.map_replicate, Multiset.prod_replicate, Subtype.coe_mk])

	rw [out]; dsimp only; rw [dif_pos i.is_lt]
	rw [out]; dsimp only; rw [dif_pos i.is_lt, Fin.eta]

	have ihi_eq : (⟨i, hi⟩ : Fin (N q)) = (E q) ⟨y, ys⟩ := by rw [Fin.ext_iff]
	have ihi_eq : (⟨i, hi⟩ : Fin (N q)) = (E q) ⟨y, ys⟩ := by rw [Fin.ext_iff, Fin.val_mk]

Conversation

darabos commented Feb 18, 2024

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

darabos commented Feb 19, 2024

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Feb 20, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants