[Merged by Bors] - chore(*): register global fact instances #11749
Conversation
sgouezel
added
the
awaiting-review
| @@ -71,8 +71,8 @@ def pi_Lp {ι : Type*} (p : ℝ) (α : ι → Type*) : Type* := Π (i : ι), α | |||
| instance {ι : Type*} (p : ℝ) (α : ι → Type*) [∀ i, inhabited (α i)] : inhabited (pi_Lp p α) := | |||
| ⟨λ i, default⟩ | |||
|
|
|||
| lemma fact_one_le_one_real : fact ((1:ℝ) ≤ 1) := ⟨rfl.le⟩ | |||
| lemma fact_one_le_two_real : fact ((1:ℝ) ≤ 2) := ⟨one_le_two⟩ | |||
| instance fact_one_le_one_real : fact ((1:ℝ) ≤ 1) := ⟨rfl.le⟩ | |||
There was a problem hiding this comment.
Is there any benefit to having this specialized instance, instead of a generic le_rfl instance?
There was a problem hiding this comment.
I can imagine some situations where the system would want to check fact (p ≤ q) and then it could try to see if by chance p = q and run into a heavy refl computation, while this wouldn't happen if it needed to check whether p is 1. But all this is completely theoretical, I don't have a concrete example in mind. I just went for the smallest possible change.
|
Is there a way to benchmark this change? I know performance was one of the reasons we avoided global fact instances in the past so it would be good to check that this doesn't have adverse effects |
|
Have you considered making these instances localized in some locale rather than global. I agree one of the big issues with the way we use fact is discoverability but perhaps putting them in a well-named locale would be newcomer friendly? |
|
I expect that these changes will have absolutely no performance impact whatsoever, because this will just be 7 global fact instances. Of course, I don't have concrete figures to back my claims :-) |
|
Jannis Limperg benchmarked the change, see https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/euclidean_space.20error/near/270164697. It makes no performance difference. |
|
Thanks 🎉 bors merge |
github-actions
bot
added
ready-to-merge
We register globally some fact instances which are necessary for integration or euclidean spaces. And also the fact that 2 and 3 are prime. See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/euclidean_space.20error/near/269992165
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
We register globally some fact instances which are necessary for integration or euclidean spaces. And also the fact that 2 and 3 are prime. See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/euclidean_space.20error/near/269992165