[Merged by Bors] - feat: define List.offDiag#33812
[Merged by Bors] - feat: define List.offDiag#33812urkud wants to merge 11 commits intoleanprover-community:masterfrom
List.offDiag#33812Conversation
PR summary 6f741b69cb
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Data.List.Nodup | 232 | 226 | -6 (-2.59%) |
| Mathlib.Data.Finset.Prod | 405 | 407 | +2 (+0.49%) |
| Mathlib.Algebra.BigOperators.Group.Finset.Basic | 417 | 419 | +2 (+0.48%) |
| Mathlib.Data.Fintype.Prod | 429 | 431 | +2 (+0.47%) |
| Mathlib.Data.Finite.Prod | 441 | 443 | +2 (+0.45%) |
| Mathlib.Data.Finset.Sym | 488 | 490 | +2 (+0.41%) |
| Mathlib.Topology.MetricSpace.Infsep | 962 | 964 | +2 (+0.21%) |
Import changes for all files
| Files | Import difference |
|---|---|
| There are 4814 files with changed transitive imports taking up over 217233 characters: this is too many to display! | |
You can run scripts/import_trans_difference.sh all locally to see the whole output. |
Declarations diff
+ Nodup.mem_offDiag
+ Nodup.of_offDiag
+ Nodup.offDiag
+ Perm.offDiag
+ Sublist.flatMap_right
+ count_offDiag_eq_mul_sub_ite
+ length_offDiag
+ length_offDiag'
+ map_prodMap_offDiag
+ mem_offDiag_iff_getElem
+ nodup_offDiag
+ offDiag_cons_perm
+ offDiag_nil
+ toFinset_offDiag
++- offDiag
++- offDiag_singleton
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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
|
What do you think of this pseudo code definition? Is it faster? def offDiag :=
(aux l).flatten
where aux : List α → List (List (α × α))
| [] := []
| (x :: xs) := xs.map (fun y => (x, y)) ::
zipWith (fun x' l => (x', x) :: l) xs (aux xs) |
|
@eric-wieser Try this: namespace List
variable {α : Type _}
def offDiag (l : List α) : List (α × α) :=
l.zipIdx.flatMap fun (x, n) ↦ map (Prod.mk x) <| l.eraseIdx n
def offDiag₂ (l : List α) : List (α × α) :=
aux l |>.flatten
where aux : List α → List (List (α × α))
| [] => []
| x :: xs => map (x, ·) xs :: zipWith (fun y l ↦ (y, x) :: l) xs (aux xs)
def offDiag₃ : List α → List (α × α)
| [] => []
| x :: xs => map (x, ·) xs ++ map (·, x) xs ++ offDiag₃ xs
def offDiag₃TR (l : List α) : List (α × α) :=
loop [] l
where loop : List (α × α) → List α → List (α × α)
| l, [] => l
| l, x :: xs => loop (map (x, ·) xs ++ map (·, x) xs ++ l) xs
#time #eval (List.range 5000).offDiag.length
#time #eval (List.range 5000).offDiag₂.length
#time #eval (List.range 5000).offDiag₃.length
#time #eval (List.range 5000).offDiag₃TR.lengthI'm getting (rounded) 2100ms, 4900ms, 2200ms, 2000ms on my desktop. |
|
@eric-wieser What do you want to do about this PR? Do you want me to change the definition? If yes, then which one do you prefer? |
|
Apologies, I missed your ping. Thanks for the comparison, I think those results make it clear that your definition is the right one. Would you mind adding that to the PR description? |
| def offDiag := | ||
| (s ×ˢ s).filter fun a : α × α => a.fst ≠ a.snd | ||
| def offDiag : Finset (α × α) := | ||
| .mk (Quotient.map List.offDiag (fun _ _ ↦ List.Perm.offDiag) s.1) <| by |
There was a problem hiding this comment.
It's tempting to extract this to a Multiset.offDiag; do you think it's ok to do this without writing API for it? Otherwise perhaps lets just leave a TODO.
Mathlib/Data/Finset/Prod.lean
Outdated
|
|
||
| @[simp] | ||
| theorem diag_union_offDiag : s.diag ∪ s.offDiag = s ×ˢ s := by | ||
| theorem diag_union_offDiag [DecidableEq (α × α)] : s.diag ∪ s.offDiag = s ×ˢ s := by |
There was a problem hiding this comment.
This generalization makes me feel a little uneasy; certainly it feels a little out of scope for the PR. Would you mind changing back to [DecidableEq α] throughout for now, and then making a separate PR with the [DecidableEq (α × α)] generalization?
eric-wieser
left a comment
There was a problem hiding this comment.
Otherwise looks great, thanks!
bors d+
|
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
As this PR is labelled bors merge |
Use it to drop decidability assumption in `Finset.offDiag`. Also redefine `Finset.diag`.
|
Build failed (retrying...): |
Use it to drop decidability assumption in `Finset.offDiag`. Also redefine `Finset.diag`.
|
Timed out. |
|
bors r+ |
Use it to drop decidability assumption in `Finset.offDiag`. Also redefine `Finset.diag`.
|
Build failed (retrying...): |
Use it to drop decidability assumption in `Finset.offDiag`. Also redefine `Finset.diag`.
|
Pull request successfully merged into master. Build succeeded: |
List.offDiagList.offDiag
Use it to drop decidability assumption in `Finset.offDiag`. Also redefine `Finset.diag`.
This proves that the new definition of Finset.diag (from leanprover-community#33812) is equivalent to the old one.
This proves that the new definition of Finset.diag (from #33812) is equivalent to the old one.
Use it to drop decidability assumption in `Finset.offDiag`. Also redefine `Finset.diag`.
This proves that the new definition of Finset.diag (from leanprover-community#33812) is equivalent to the old one.
Use it to drop decidability assumption in
Finset.offDiag. Also redefineFinset.diag.Built on top of #12632, reopened from a fork.