[Merged by Bors] - chore(Order/Defs/LinearOrder): avoid grind in very fundamental lemmas#35841
[Merged by Bors] - chore(Order/Defs/LinearOrder): avoid grind in very fundamental lemmas#35841astrainfinita wants to merge 8 commits intoleanprover-community:masterfrom
grind in very fundamental lemmas#35841Conversation
PR summary ba4b2e5a2cImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
|
You're also moving a few lemmas, right? Can you say why the new location is better (or maybe split that into a separate PR)? And can you add a comment to the file that using |
grunweg
added
the
awaiting-author
astrainfinita
removed
the
awaiting-author
Komyyy
left a comment
Komyyy
left a comment
There was a problem hiding this comment.
Thank you for your contribution!
If you want to make the proofs more understandable, you can prove these lemma elegantly without simps!
Mathlib/Order/Defs/LinearOrder.lean
Outdated
| rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq] | ||
| grind | ||
| simpa [apply_ite (· = Ordering.gt), ne_iff_lt_or_gt, and_or_left, - not_lt] using not_lt_of_gt |
There was a problem hiding this comment.
rw [LinearOrder.compare_eq_compareOfLessAndEq,
compareOfLessAndEq_eq_gt le_antisymm le_total not_le]There was a problem hiding this comment.
Since some people expressed concern about the axiom of choice on zulip, I used a slightly more verbose proof instead.
There was a problem hiding this comment.
I recall that change avoiding choice should only be done when the change is small.
Rather than avoiding compareOfLessAndEq_eq_gt, we should fix the proof of lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le, which compareOfLessAndEq_eq_gt depends on.
With this small change, we can indeed eliminate the use of choice. The current proof appears to mistakenly use DecidableLT where DecidableLE is needed:
theorem lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le
{α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α]
(antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
(total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬ x ≤ y ↔ y < x) (x y : α) :
x < y ↔ ¬ y < x ∧ x ≠ y := by
simp only [← not_le, Classical.not_not]
constructor
· intro h
have refl := by cases total y y <;> assumption
exact ⟨(total _ _).resolve_left h, fun h' => (h' ▸ h) refl⟩
· intro ⟨h₁, h₂⟩ h₃
exact h₂ (antisymm h₁ h₃)↓
theorem lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le
{α : Type u} [LT α] [LE α] [DecidableLE α] [DecidableEq α]
(antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
(total : ∀ (x y : α), x ≤ y ∨ y ≤ x) (not_le : ∀ {x y : α}, ¬ x ≤ y ↔ y < x) (x y : α) :
x < y ↔ ¬ y < x ∧ x ≠ y := by
simp only [← not_le, Decidable.not_not]
constructor
· intro h
have refl := by cases total y y <;> assumption
exact ⟨(total _ _).resolve_left h, fun h' => (h' ▸ h) refl⟩
· intro ⟨h₁, h₂⟩ h₃
exact h₂ (antisymm h₁ h₃)There was a problem hiding this comment.
This will add [DecidableLE α] to other APIs, and AFAIK, Lean core is unlikely to accept contributions for avoiding choice. But indeed, compareOfLessAndEq needs refactoring, so let's just go ahead with this.
There was a problem hiding this comment.
I think Lean core will accept this change, as it seems more like an argument type fix than a change to avoid choice, and the number of affected lemmas does not seem to be much.
Komyyy
added
the
awaiting-author
astrainfinita
removed
the
awaiting-author
Komyyy
added
the
awaiting-author
astrainfinita
removed
the
awaiting-author
Komyyy
left a comment
Komyyy
left a comment
There was a problem hiding this comment.
Thank you!
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by Komyyy. trigger_name: pull_request_review |
mathlib-triage
bot
added
the
maintainer-merge
|
bors r+ |
…as (#35841) Some lemmas can be optimized more elegantly, but it requires moving lemmas from other files, so I will do it in a subsequent PR.
mathlib-triage
bot
added
ready-to-merge
| (lt_or_ge a b).imp_right (fun h ↦ (Decidable.lt_or_eq_of_le' h).symm) | ||
|
|
||
| @[to_dual self] | ||
| lemma le_of_not_gt (h : ¬b < a) : a ≤ b := (le_or_gt a b).resolve_right h |
There was a problem hiding this comment.
That is a much nicer proof! 🎉
|
|
||
| @[to_dual] | ||
| lemma min_assoc (a b c : α) : min (min a b) c = min a (min b c) := by grind | ||
| lemma min_assoc (a b c : α) : min (min a b) c = min a (min b c) := |
There was a problem hiding this comment.
This is a bit dubious to me, since we can also prove this by case analysis (on who is the smallest element of {a, b, c}). But it matches the original proof pre-grind so I can live with this!
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
grind in very fundamental lemmasgrind in very fundamental lemmas
4 participants
Some lemmas can be optimized more elegantly, but it requires moving lemmas from other files, so I will do it in a subsequent PR.
Zulip