[Merged by Bors] - refactor: New Colex API
#7715
Conversation
This fully rewrites `Combinatorics.Colex` to use a type synonym approach instead of abusing defeq. We also provide some API about initial segments of colex.
YaelDillies
added
awaiting-review
Co-authored-by: Bhavik Mehta <bm489@cam.ac.uk>
|
Switching this to WIP for the moment, Yaël and I have agreed on a different definition of this ordering, so I'll take it off queue while that gets organised. |
b-mehta
added
WIP
|
Note: I have pushed an update to the lean toolchain because this PR was on a buggy version of the toolchain. WARNING: checking out old commits of this PR using v4.2.0-rc2 or v4.2.0-rc3 can cause |
YaelDillies
added
awaiting-review
Mathlib/Algebra/GeomSum.lean
Outdated
| /-- If all the elements of a finset of naturals are less than `n`, then the sum of their powers of | ||
| `2` is less than `2 ^ n`. -/ | ||
| lemma Nat.sum_two_pow_lt {n : ℕ} {s : Finset ℕ} (hs : ∀ k ∈ s, k < n) : | ||
| ∑ k in s, 2 ^ k < 2 ^ n := by | ||
| calc | ||
| ∑ k in s, 2 ^ k ≤ ∑ k in range n, 2 ^ k := sum_le_sum_of_subset fun k hk ↦ mem_range.2 $ hs _ hk | ||
| _ = 2 ^ n - 1 := by | ||
| simp_rw [←one_add_one_eq_two, ←geom_sum_mul_add 1 n, mul_one, add_tsub_cancel_right] | ||
| _ < 2 ^ n := tsub_lt_self (by positivity) zero_lt_one |
There was a problem hiding this comment.
Can this be used to golf finPiFinEquiv or similar?
There was a problem hiding this comment.
Ah nevermind, I see this is just a move. If you PR this move separately I'll merge it immediately.
There was a problem hiding this comment.
I think I will need to generalise the lemma a bit. So I'll keep that for later.
There was a problem hiding this comment.
I've generalised the lemma and I now think it can't be used for finPiFinEquiv, at least not without being generalised further.
|
I don't think there's a good way to save the diff here. It is almost a rewrite from scratch. |
| refine ⟨d, hdu, fun hds ↦ ?_, had⟩ | ||
| exact hbmax d hds hdt had <| hbc.trans_lt <| hcd.lt_of_ne <| ne_of_mem_of_not_mem hct hdt | ||
|
|
||
| private lemma antisymm_aux (hst : toColex s ≤ toColex t) (hts : toColex t ≤ toColex s) : s ⊆ t := by |
There was a problem hiding this comment.
I really want wlog or some variant to be able to generate this...
There was a problem hiding this comment.
Actually I think it Just Works?
There was a problem hiding this comment.
Nevermind, we would need something like wlog_suffices or something.
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
|
bors merge |
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Colex APIColex API
This fully rewrites
Combinatorics.Colexto use a type synonym approach instead of abusing defeq.We also provide some API about initial segments of colex.