[Merged by Bors] - chore: more `squeeze_simp`s arising from linter by adomani · Pull Request #11259 · leanprover-community/mathlib4

adomani · 2024-03-09T10:50:35Z

The squeezing continues! All found by the linter at #11246.

urkud · 2024-03-10T16:40:13Z

Thanks! 🎉
bors merge

The squeezing continues! All found by the linter at #11246.

mathlib-bors · 2024-03-10T17:43:42Z

Pull request successfully merged into master.

Build succeeded:

The squeezing continues! All found by the linter at #11246.

YaelDillies

Would you mind opening a PR addressing my comments?

YaelDillies · 2024-03-17T16:16:42Z

Mathlib/Algebra/Group/Conj.lean

+  · simp only [zpow_negSucc, conj_pow, mul_inv_rev, inv_inv]
    rw [mul_assoc]


Make the proof more robust by not squeezing the simp:

Suggested change

· simp only [zpow_negSucc, conj_pow, mul_inv_rev, inv_inv]

rw [mul_assoc]

· simp [zpow_negSucc, conj_pow, mul_assoc]

YaelDillies · 2024-03-17T16:18:08Z

Mathlib/Data/List/Permutation.lean

+  · simp only [foldr_cons, ih, cons_bind, append_assoc]
    rw [← permutationsAux2_append]


Suggested change

· simp only [foldr_cons, ih, cons_bind, append_assoc]

rw [← permutationsAux2_append]

· simp [ih, ← permutationsAux2_append]

This says

tactic 'simp' failed, nested error: maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)

YaelDillies · 2024-03-17T16:19:28Z

Mathlib/Data/Seq/Computation.lean

-      · simp at h
-        simp [*]


Sure that's a golf, but please reassure me that your linter does not flag this as a non-terminal simp!

I am still working on the internal mechanics of the linter. The first simp was indeed flagged, but a newer version of the linter will hopefully be aware of the tactic immediately following a simp and will use this information to decide whether a simp is considered terminal or not. So,

I will not revert this change,

I agree with you that this should not have been flagged,

I do think that the current version is more robust than what it was before, though!

😄

YaelDillies · 2024-03-17T16:20:14Z

Mathlib/Data/Seq/WSeq.lean

@@ -1157,7 +1159,7 @@ theorem liftRel_flatten {R : α → β → Prop} {c1 : Computation (WSeq α)} {c
    match s, t, h with
    | _, _, ⟨c1, c2, rfl, rfl, h⟩ => by
      -- Porting note: `exists_and_left` should be excluded.


Suggested change

-- Porting note: `exists_and_left` should be excluded.

Removed the note.

YaelDillies · 2024-03-17T16:21:33Z

Mathlib/Data/Seq/WSeq.lean

+  destruct_eq_think <| by
+    unfold toList
+    simp only [toList'_cons, Computation.destruct_think, Sum.inr.injEq]
+    rw [toList'_map]
+    simp only [List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append]
+    rfl


This looks like a symptom of the simp bug that was fixed by letting simp not resynthesize everything anymore. Hence I'm pretty sure something like this will work:

Suggested change

destruct_eq_think <| by

unfold toList

simp only [toList'_cons, Computation.destruct_think, Sum.inr.injEq]

rw [toList'_map]

simp only [List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append]

rfl

destruct_eq_think <| by unfold toList; simp [toList'_map]; rfl

Literally what you suggest gives

type mismatch HEq.rfl has type HEq ?m.129498 ?m.129498 : Prop but is expected to have type Computation.destruct (toList (cons a s)) = Sum.inr (List.cons a <$> toList s) : Prop

I could not find a better proof...

YaelDillies · 2024-03-17T16:22:06Z

Mathlib/Data/Seq/WSeq.lean

-  simp [head]; cases Seq.head s <;> rfl
+  simp only [head, Option.map_eq_map, destruct_ofSeq, Computation.map_pure, Option.map_map]
+  cases Seq.head s <;> rfl


I'm honestly not sure this kind of changes is an improvement

I reverted this change.

YaelDillies · 2024-03-17T16:23:11Z

Mathlib/Tactic/NormNum/OfScientific.lean

+  | _, _, _, _, _, σh, ⟨rfl⟩, ⟨rfl⟩, h => ⟨by
+    simp only [Nat.cast_id, σh, Rat.ofScientific_false_def, Nat.cast_mul, Nat.cast_pow,
+      Nat.cast_ofNat, h, Nat.mul_eq]
+    norm_cast⟩


This is a false positive. norm_cast is a simp-like tactic, hence the simp is not terminal. Please revert.

adomani

@YaelDillies I addressed the comments that I could in #11455.

adomani · 2024-03-17T18:04:11Z

Mathlib/Data/List/Permutation.lean

+  · simp only [foldr_cons, ih, cons_bind, append_assoc]
    rw [← permutationsAux2_append]


This says

tactic 'simp' failed, nested error: maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)

adomani · 2024-03-17T18:07:02Z

Mathlib/Data/Seq/Computation.lean

-      · simp at h
-        simp [*]


I am still working on the internal mechanics of the linter. The first simp was indeed flagged, but a newer version of the linter will hopefully be aware of the tactic immediately following a simp and will use this information to decide whether a simp is considered terminal or not. So,

I will not revert this change,

I agree with you that this should not have been flagged,

I do think that the current version is more robust than what it was before, though!

😄

adomani · 2024-03-17T18:07:38Z

Mathlib/Data/Seq/WSeq.lean

@@ -1157,7 +1159,7 @@ theorem liftRel_flatten {R : α → β → Prop} {c1 : Computation (WSeq α)} {c
    match s, t, h with
    | _, _, ⟨c1, c2, rfl, rfl, h⟩ => by
      -- Porting note: `exists_and_left` should be excluded.


Removed the note.

adomani · 2024-03-17T18:11:27Z

Mathlib/Data/Seq/WSeq.lean

+  destruct_eq_think <| by
+    unfold toList
+    simp only [toList'_cons, Computation.destruct_think, Sum.inr.injEq]
+    rw [toList'_map]
+    simp only [List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append]
+    rfl


Literally what you suggest gives

type mismatch HEq.rfl has type HEq ?m.129498 ?m.129498 : Prop but is expected to have type Computation.destruct (toList (cons a s)) = Sum.inr (List.cons a <$> toList s) : Prop

I could not find a better proof...

adomani · 2024-03-17T18:12:27Z

Mathlib/Data/Seq/WSeq.lean

-  simp [head]; cases Seq.head s <;> rfl
+  simp only [head, Option.map_eq_map, destruct_ofSeq, Computation.map_pure, Option.map_map]
+  cases Seq.head s <;> rfl


I reverted this change.

adomani · 2024-03-17T18:15:10Z

Mathlib/Algebra/Group/Conj.lean

+  · simp only [zpow_negSucc, conj_pow, mul_inv_rev, inv_inv]
    rw [mul_assoc]


The squeezing continues! All found by the linter at #11246.

adomani added 2 commits March 9, 2024 11:46

More squeezes

eb35359

remove false positives

36c242b

adomani added the awaiting-review label Mar 9, 2024

adomani mentioned this pull request Mar 10, 2024

feat: a non-terminal simp linter #11246

Closed

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Mar 10, 2024

mathlib-bors bot pushed a commit that referenced this pull request Mar 10, 2024

chore: more squeeze_simps arising from linter (#11259)

927ac92

The squeezing continues! All found by the linter at #11246.

mathlib-bors bot changed the title ~~chore: more squeeze_simps arising from linter~~ [Merged by Bors] - chore: more squeeze_simps arising from linter Mar 10, 2024

mathlib-bors bot closed this Mar 10, 2024

mathlib-bors bot deleted the adomani/squeeze_simps branch March 10, 2024 17:43

kbuzzard pushed a commit that referenced this pull request Mar 12, 2024

chore: more squeeze_simps arising from linter (#11259)

b1d2c3c

The squeezing continues! All found by the linter at #11246.

YaelDillies reviewed Mar 17, 2024

View reviewed changes

adomani added a commit that referenced this pull request Mar 17, 2024

fix: unsqueeze simp, re Yaël's comments on #11259

028d7ce

adomani mentioned this pull request Mar 17, 2024

fix: unsqueeze simp, re Yaël's comments on #11259 #11455

Open

adomani commented Mar 17, 2024

View reviewed changes

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

chore: more squeeze_simps arising from linter (#11259)

870e5fe

The squeezing continues! All found by the linter at #11246.

utensil pushed a commit that referenced this pull request Mar 26, 2024

chore: more squeeze_simps arising from linter (#11259)

4980e10

The squeezing continues! All found by the linter at #11246.

Ruben-VandeVelde mentioned this pull request Apr 11, 2024

[Merged by Bors] - chore: tidy various files #12042

Closed

xgenereux pushed a commit that referenced this pull request Apr 15, 2024

chore: more squeeze_simps arising from linter (#11259)

d285694

The squeezing continues! All found by the linter at #11246.

uniwuni pushed a commit that referenced this pull request Apr 19, 2024

chore: more squeeze_simps arising from linter (#11259)

3d2cc05

The squeezing continues! All found by the linter at #11246.

callesonne pushed a commit that referenced this pull request Apr 22, 2024

chore: more squeeze_simps arising from linter (#11259)

486df9a

The squeezing continues! All found by the linter at #11246.

		· simp only [zpow_negSucc, conj_pow, mul_inv_rev, inv_inv]
		rw [mul_assoc]

	· simp only [zpow_negSucc, conj_pow, mul_inv_rev, inv_inv]
	rw [mul_assoc]
	· simp [zpow_negSucc, conj_pow, mul_assoc]

		· simp only [foldr_cons, ih, cons_bind, append_assoc]
		rw [← permutationsAux2_append]

	· simp only [foldr_cons, ih, cons_bind, append_assoc]
	rw [← permutationsAux2_append]
	· simp [ih, ← permutationsAux2_append]

Conversation

adomani commented Mar 9, 2024

Uh oh!

urkud commented Mar 10, 2024

Uh oh!

mathlib-bors bot commented Mar 10, 2024

Uh oh!

YaelDillies 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!

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!

adomani 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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants