[Merged by Bors] - chore: more `squeeze_simp`s arising from linter #11259

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 The author would like community review of the PR label Mar 9, 2024

adomani mentioned this pull request Mar 10, 2024

feat: a non-terminal simp linter #11246

Open

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR 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

Louddy 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.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: more `squeeze_simp`s arising from linter #11259

[Merged by Bors] - chore: more `squeeze_simp`s arising from linter #11259

adomani commented Mar 9, 2024

urkud commented Mar 10, 2024

mathlib-bors bot commented Mar 10, 2024

YaelDillies left a comment

YaelDillies Mar 17, 2024

adomani Mar 17, 2024

YaelDillies Mar 17, 2024

adomani Mar 17, 2024

YaelDillies Mar 17, 2024

adomani Mar 17, 2024

YaelDillies Mar 17, 2024

adomani Mar 17, 2024

YaelDillies Mar 17, 2024

adomani Mar 17, 2024

YaelDillies Mar 17, 2024

adomani Mar 17, 2024

YaelDillies Mar 17, 2024

adomani left a comment

adomani Mar 17, 2024

adomani Mar 17, 2024

adomani Mar 17, 2024

adomani Mar 17, 2024

adomani Mar 17, 2024

adomani Mar 17, 2024

		· 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]

[Merged by Bors] - chore: more squeeze_simps arising from linter #11259

[Merged by Bors] - chore: more squeeze_simps arising from linter #11259

Conversation

adomani commented Mar 9, 2024

urkud commented Mar 10, 2024

mathlib-bors bot commented Mar 10, 2024

YaelDillies left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

adomani left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

[Merged by Bors] - chore: more `squeeze_simp`s arising from linter #11259

[Merged by Bors] - chore: more `squeeze_simp`s arising from linter #11259