[Merged by Bors] - chore: remove useless tactics#11333
[Merged by Bors] - chore: remove useless tactics#11333
Conversation
Honestly, I was not expecting that so many |
| instance evaluationPreservesLimits [HasLimits C] (k : K) : | ||
| PreservesLimits ((evaluation K C).obj k) where | ||
| preservesLimitsOfShape {J} 𝒥 := by skip; infer_instance | ||
| preservesLimitsOfShape {_} _𝒥 := inferInstance |
There was a problem hiding this comment.
Doesn't inferInstance add extra junk that by infer_instance doesn't? Can you check the term is syntactically the same as it was before?
There was a problem hiding this comment.
In its current form (with inferInstance):
#print evaluationPreservesLimits
def CategoryTheory.Limits.evaluationPreservesLimits.{v₂, u₂, v, u} : {C : Type u} →
[inst : Category.{v, u} C] →
{K : Type u₂} →
[inst_1 : Category.{v₂, u₂} K] → [inst_2 : HasLimits C] → (k : K) → PreservesLimits ((evaluation K C).obj k) :=
fun {C} [Category.{v, u} C] {K} [Category.{v₂, u₂} K] [HasLimits C] k ↦
{ preservesLimitsOfShape := fun {x} _𝒥 ↦ inferInstance }As it was before the change:
#print evaluationPreservesLimits
def CategoryTheory.Limits.evaluationPreservesLimits.{v₂, u₂, v, u} : {C : Type u} →
[inst : Category.{v, u} C] →
{K : Type u₂} →
[inst_1 : Category.{v₂, u₂} K] → [inst_2 : HasLimits C] → (k : K) → PreservesLimits ((evaluation K C).obj k) :=
fun {C} [Category.{v, u} C] {K} [Category.{v₂, u₂} K] [HasLimits C] k ↦
{ preservesLimitsOfShape := fun {J} 𝒥 ↦ inferInstance }Seems that the only difference are the variable names.
| theorem node4L_size {l x m y r} (hm : Sized m) : | ||
| size (@node4L α l x m y r) = size l + size m + size r + 2 := by | ||
| cases m <;> simp [node4L, node3L, node'] <;> [skip; simp [size, hm.1]] <;> abel | ||
| cases m <;> simp [node4L, node3L, node'] <;> [abel; (simp [size, hm.1]; abel)] |
There was a problem hiding this comment.
Not sure that one is necessarily an improvement
There was a problem hiding this comment.
I am happy to revert it back to where it was, but it is shorter and produces the same proof. (Really identical, very long, output of #print.)
| @@ -518,8 +518,7 @@ theorem linearIndependent_iUnion_of_directed {η : Type*} {s : η → Set M} (hs | |||
| (h : ∀ i, LinearIndependent R (fun x => x : s i → M)) : | |||
| LinearIndependent R (fun x => x : (⋃ i, s i) → M) := by | |||
| by_cases hη : Nonempty η | |||
There was a problem hiding this comment.
You will be able to golf further by doing cases isEmpty_or_nonempty η instead of that `by_cases
There was a problem hiding this comment.
Ok, but I would definitely say that this is out of scope for this PR!
| rcases n with ⟨_, ⟨⟩⟩ | ||
| -- Porting note: The proof errors unless `done` or a `;` is added after `rcases` | ||
| done | ||
| rcases n with ⟨_, ⟨⟩⟩; |
There was a problem hiding this comment.
Seems like you haven't addressed the porting note, and removing done isn't a particularly great idea either.
I suggest you nolint done calls by default.
There was a problem hiding this comment.
Isn't the issue that rcases does not realize that its pattern is over, since | could be an or? Again, I can put the porting note back, but replacing done by ; also "fixes" the error.
There was a problem hiding this comment.
Here is an example:
example (x : Bool) (h : false ∨ true) : True := by
match x with
| true => rcases h with ⟨⟩
| false -- <--- this is still part of `rcases`: I am calling `false` the `true` proof! x)
· exact .intro -- <--- the proof if `h` is `false`
· exact .intro -- <--- the proof if `h` is `true`
| false => exact .intro -- <--- the second `match` arm!
|
!bench |
|
Here are the benchmark results for commit 7e21612. Benchmark Metric Change
============================================================
- ~Mathlib.Computability.TuringMachine instructions 17.0% |
|
Seems like some tactics weren't useless after all. |
Preferring `assumption` over `aesop` has some performance implications!
|
🤦 the file that slowed down is a file where I replaced some splits and assumptions into a single |
|
!bench |
|
Here are the benchmark results for commit c8593e7. |
|
Thanks! bors merge |
The removal of some pointless tactics flagged by #11308.
|
Pull request successfully merged into master. Build succeeded: |
The removal of some pointless tactics flagged by #11308.
The removal of some pointless tactics flagged by #11308.
The removal of some pointless tactics flagged by #11308.
The removal of some pointless tactics flagged by #11308.
The removal of some pointless tactics flagged by #11308.
The `unusedTactic` linter emits a warning if a tactic does nothing. Previous PRs (see below) removed all the "unused tactics" that the linter flagged. Here is an overview of this PR: * the linter is defined in `Mathlib/Tactic/Linter/UnusedTactic.lean`; * the file `Mathlib/GroupTheory/Perm/Cycle/Concrete.lean` contains the "only" `set_option` to opt out of the linter, since it defines notation that uses `decide` that the notation itself does not use; * 17 test files that have surgically opted out of the linter; * noise to import the new file, place it low in the import hierarchy and update `noshake`. PRs removing some unused tactics: * #11333 * #11351 * #11365 * #11379 [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/pointless.20tactic.20linter)
The `unusedTactic` linter emits a warning if a tactic does nothing. Previous PRs (see below) removed all the "unused tactics" that the linter flagged. Here is an overview of this PR: * the linter is defined in `Mathlib/Tactic/Linter/UnusedTactic.lean`; * the file `Mathlib/GroupTheory/Perm/Cycle/Concrete.lean` contains the "only" `set_option` to opt out of the linter, since it defines notation that uses `decide` that the notation itself does not use; * 17 test files that have surgically opted out of the linter; * noise to import the new file, place it low in the import hierarchy and update `noshake`. PRs removing some unused tactics: * #11333 * #11351 * #11365 * #11379 [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/pointless.20tactic.20linter)
The removal of some pointless tactics flagged by #11308.