[Merged by Bors] - fix(Mathlib.Tactic.CC.Datatypes): `cc` raises panic by Komyyy · Pull Request #20422 · leanprover-community/mathlib4

Komyyy · 2025-01-03T09:43:34Z

The following cc raises a panic:

example (n k : ℤ) (hnk : n = 2 * k + 1)
    (hk : (2 * k + 1) * (2 * k + 1 + 1) = 2 * ((2 * k + 1) * (k + 1))) :
    n * (n + 1) = 2 * ((2 * k + 1) * (k + 1)) := by
  cc

This is because args₂[i]! is evaluated before compare args₁.size args₂.size in the following code:

scoped instance : Ord ACApps where
  compare
    | .ofExpr a, .ofExpr b => compare a b
    | .ofExpr _, .apps _ _ => .lt
    | .apps _ _, .ofExpr _ => .gt
    | .apps op₁ args₁, .apps op₂ args₂ =>
      compare op₁ op₂ |>.then <| compare args₁.size args₂.size |>.then <| Id.run do
        for i in [:args₁.size] do
          let o := compare args₁[i]! args₂[i]!
          if o != .eq then return o
        return .eq

Usually, if o₁ ≠ .eq, o₂ in o₁.then o₂ is never evaluated because Ordering.then is marked by @[macro_inline], however this doesn't work in this example.
I don't know how @[macro_inline] works, but this bug can be solved by using args₂[i]'h instead of args₂[i]!.

Also, this new definition is added to Mathlib.Data.Ordering.Basic:

/-- `o₁.dthen fun h => o₂(h)` is like `o₁.then o₂` but `o₂` is allowed to depend on
`h : o₁ = .eq`. -/
@[macro_inline] def dthen :
    (o : Ordering) → (o = .eq → Ordering) → Ordering
  | .eq, f => f rfl
  | o, _ => o

This PR increases imports percentage in Mathlib.Tactic.CC.Datatypes, but it doesn't matter because it's only 4 files.

github-actions · 2025-01-03T09:44:25Z

PR summary 62bede7e0d

Import changes exceeding 2%

%	File
+16.00%	`Mathlib.Tactic.CC.Datatypes`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.CC.Datatypes	25	29	+4 (+16.00%)

Import changes for all files

Files	Import difference
There are 4853 files with changed transitive imports taking up over 206263 characters: this is too many to display!
You can run `scripts/import_trans_difference.sh all` locally to see the whole output.

Declarations diff

+ dthen
+ dthen_eq_then

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Mathlib/Tactic/CC/Datatypes.lean

PatrickMassot · 2025-01-04T09:32:50Z

bors merge

[Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/cc.20bug/near/491678555) The following `cc` raises a panic: ```lean example (n k : ℤ) (hnk : n = 2 * k + 1) (hk : (2 * k + 1) * (2 * k + 1 + 1) = 2 * ((2 * k + 1) * (k + 1))) : n * (n + 1) = 2 * ((2 * k + 1) * (k + 1)) := by cc ``` This is because `args₂[i]!` is evaluated before `compare args₁.size args₂.size` in the following code: ```lean scoped instance : Ord ACApps where compare | .ofExpr a, .ofExpr b => compare a b | .ofExpr _, .apps _ _ => .lt | .apps _ _, .ofExpr _ => .gt | .apps op₁ args₁, .apps op₂ args₂ => compare op₁ op₂ |>.then <| compare args₁.size args₂.size |>.then <| Id.run do for i in [:args₁.size] do let o := compare args₁[i]! args₂[i]! if o != .eq then return o return .eq ``` Usually, if `o₁ ≠ .eq`, `o₂` in `o₁.then o₂` is never evaluated because `Ordering.then` is marked by `@[macro_inline]`, however this doesn't work in this example. I don't know how `@[macro_inline]` works, but this bug can be solved by using `args₂[i]'h` instead of `args₂[i]!`. Also, this new definition is added to `Mathlib.Data.Ordering.Basic`: ```lean /-- `o₁.dthen fun h => o₂(h)` is like `o₁.then o₂` but `o₂` is allowed to depend on `h : o₁ = .eq`. -/ @[macro_inline] def dthen : (o : Ordering) → (o = .eq → Ordering) → Ordering | .eq, f => f rfl | o, _ => o ``` This PR increases imports percentage in `Mathlib.Tactic.CC.Datatypes`, but it doesn't matter because it's only 4 files.

mathlib-bors · 2025-01-04T10:16:01Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (133 commits) chore(1000): remove nonexistent fields (#20493) chore(CategoryTheory/Adjunction.Basic, CategoryTheory/Equivalence): change definition of `Adjunction.comp` and `Equivalence.trans` (#20490) feat(Asymptotics): add `Asymptotics.*.*Prod` lemmas (#20458) feat: a conditional kernel is almost everywhere a probability measure (#20430) feat: if `f` is a measurable group hom, then every point has a neighborhood `s` such that `f '' s` is bounded (#20304) feat: `Ico`, `Ioc`, and `Ioo` are not closed or compact (#20479) chore: drop redundant hypothesis in `Module.Dual.eq_of_preReflection_mapsTo` (#20492) feat(FaaDiBruno): derive `DecidableEq` (#20482) chore(SetTheory/Ordinal/Basic): `{x // x < y}` → `Iio y` (#20413) chore: generalize `FormalMultilinearSeries.ofScalars_norm` to `Seminormed` (#20351) chore(MvPolynomial/Localization): golf using TensorProduct (#20309) chore(Combinatorics/Enumerative/Partition): auto-derive DecidableEq (#20277) chore(CategoryTheory): make relevant parameters explicit in `Arrow.homMk`. (#20259) feat: add `IsStarNormal (↑x⁻¹ : R)` instance for `x : Rˣ` (#20091) fix: Stop cancelling builds of master (#20435) chore: update Mathlib dependencies 2025-01-05 (#20485) feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas (#18933) chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (#20464) chore: bot validates lean-toolchain on bump/v4.X.0 branches (#20478) feat: shorthand lemmas for the L1 norm (#20383) chore: remove unnecessary adaptation notes (#20467) chore(Algebra/Category/MonCat/Colimits): remove smallness condition (#20473) chore(SetTheory/Ordinal/Arithmetic): `IsLeftCancelAdd Ordinal` (#19888) feat(Algebra): more on `OrthogonalIdempotents` (#18195) feat(Radical): `(radical a).natDegree ≤ a.natDegree` (#20468) feat(Polynomial): `(a^n)' = 0` iff `a' = 0` when `n` doesn't divide the characteristic (#20190) feat(Algebra/Lie): add Lie's theorem (#13480) chore(RingTheory/Generators): make algebra instance a def (#14265) feat(Topology/Group): Lemmas about profinite group (#20282) feat: the empty set is a topological basis iff the space is empty (#20441) chore: make uniqueness of conditionally complete linearly ordered archimedean fields independent of the construction of `Real` (#20242) chore: `inherit_doc`s for notations (#20376) chore: split AEEqOfIntegral into two files, one for each integral type (#20405) chore: split Kernel/MeasurableIntegral (#20427) feat(MeasureTheory/Group/Measure): add ContinuousMulEquiv.isHaarMeasure_map (#20469) fix(Mathlib.Tactic.CC.Datatypes): `cc` raises panic (#20422) feat(Probability/Moments): add lemmas about moment generating functions (#19886) feat(Algebra/Order/AddGroupWithTop): lemmas about LinearOrderedAddCommGroupWithTop (#18954) chore: bump toolchain to v4.15.0 (#20461) chore: update Mathlib dependencies 2025-01-04 (#20463) fix: make `Prod` projection delaborators respond to options, add option to disable (#20455) chore(Algebra): Improve attribute generation (#20451) feat(Polynomial): `(C a * p).degree = p.degree` if `a * p.leadingCoeff ≠ 0` (#20446) feat: add `ENNReal.finStronglyMeasurable_of_measurable` (#20404) doc(Algebra/Lie/Weights/Basic): fix typo (#20450) chore(1000): remove `identifiers` (#20445) feat: add sumPiEquivProdPi and piUnique (#20195) feat: add fst_compProd_apply (#20429) chore: use unsigned measures for Lebesgue decomposition (#20400) feat: Two lemmas on divisibility and coprimality of `expand` (#20143) ...

[Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/cc.20bug/near/491678555) The following `cc` raises a panic: ```lean example (n k : ℤ) (hnk : n = 2 * k + 1) (hk : (2 * k + 1) * (2 * k + 1 + 1) = 2 * ((2 * k + 1) * (k + 1))) : n * (n + 1) = 2 * ((2 * k + 1) * (k + 1)) := by cc ``` This is because `args₂[i]!` is evaluated before `compare args₁.size args₂.size` in the following code: ```lean scoped instance : Ord ACApps where compare | .ofExpr a, .ofExpr b => compare a b | .ofExpr _, .apps _ _ => .lt | .apps _ _, .ofExpr _ => .gt | .apps op₁ args₁, .apps op₂ args₂ => compare op₁ op₂ |>.then <| compare args₁.size args₂.size |>.then <| Id.run do for i in [:args₁.size] do let o := compare args₁[i]! args₂[i]! if o != .eq then return o return .eq ``` Usually, if `o₁ ≠ .eq`, `o₂` in `o₁.then o₂` is never evaluated because `Ordering.then` is marked by `@[macro_inline]`, however this doesn't work in this example. I don't know how `@[macro_inline]` works, but this bug can be solved by using `args₂[i]'h` instead of `args₂[i]!`. Also, this new definition is added to `Mathlib.Data.Ordering.Basic`: ```lean /-- `o₁.dthen fun h => o₂(h)` is like `o₁.then o₂` but `o₂` is allowed to depend on `h : o₁ = .eq`. -/ @[macro_inline] def dthen : (o : Ordering) → (o = .eq → Ordering) → Ordering | .eq, f => f rfl | o, _ => o ``` This PR increases imports percentage in `Mathlib.Tactic.CC.Datatypes`, but it doesn't matter because it's only 4 files.

cc panic

3c9e078

Komyyy added bug Something is not working t-meta Tactics, attributes or user commands awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jan 3, 2025

Komyyy requested a review from Vierkantor January 3, 2025 09:43

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jan 3, 2025

eric-wieser reviewed Jan 3, 2025

View reviewed changes

Mathlib/Tactic/CC/Datatypes.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 3, 2025

View reviewed changes

Mathlib/Tactic/CC/Datatypes.lean Outdated Show resolved Hide resolved

more readable

7655b4c

Komyyy added the WIP Work in progress label Jan 4, 2025

Komyyy added 2 commits January 4, 2025 13:01

Merge branch 'master' into Komyyy/cc_panic

4a485a6

move Ordering.dthen

62bede7

Komyyy added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed WIP Work in progress labels Jan 4, 2025

github-actions bot added large-import Automatically added label for PRs with a significant increase in transitive imports and removed awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jan 4, 2025

ghost added the ready-to-merge This PR has been sent to bors. label Jan 4, 2025

mathlib-bors bot changed the title ~~fix(Mathlib.Tactic.CC.Datatypes): cc raises panic~~ [Merged by Bors] - fix(Mathlib.Tactic.CC.Datatypes): cc raises panic Jan 4, 2025

mathlib-bors bot closed this Jan 4, 2025

mathlib-bors bot deleted the Komyyy/cc_panic branch January 4, 2025 10:16

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - fix(Mathlib.Tactic.CC.Datatypes): `cc` raises panic#20422

[Merged by Bors] - fix(Mathlib.Tactic.CC.Datatypes): `cc` raises panic#20422
Komyyy wants to merge 4 commits intomasterfrom
Komyyy/cc_panic

Komyyy commented Jan 3, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Jan 3, 2025 •

edited

Loading

Import changes for modified files

Uh oh!

Uh oh!

Uh oh!

PatrickMassot commented Jan 4, 2025

Uh oh!

mathlib-bors bot commented Jan 4, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

Komyyy commented Jan 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 62bede7e0d

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

PatrickMassot commented Jan 4, 2025

Uh oh!

mathlib-bors bot commented Jan 4, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Komyyy commented Jan 3, 2025 •

edited

Loading

github-actions bot commented Jan 3, 2025 •

edited

Loading