[Merged by Bors] - feat: Rat-dependent norm_num functionality#1441
[Merged by Bors] - feat: Rat-dependent norm_num functionality#1441
Rat-dependent norm_num functionality#1441Conversation
8b958c3 to
56a3115
Compare
This reverts commit 8af9269.
mysterious linarith failure; left porting note
Mathlib/Tactic/NormNum/Basic.lean
Outdated
| attribute [nolint defLemma] isRat_add isRat_neg isRat_sub isRat_mul isRat_pow isRat_inv_pos | ||
| isRat_inv_neg isRat_div -- FIXME: figure out how to get the linter to work with these |
There was a problem hiding this comment.
| attribute [nolint defLemma] isRat_add isRat_neg isRat_sub isRat_mul isRat_pow isRat_inv_pos | |
| isRat_inv_neg isRat_div -- FIXME: figure out how to get the linter to work with these |
Maybe IsRat should be in Prop, just like IsInt. I don't know if we ever need to extract the inverse of the denominator.
But if IsRat needs to stay in Prop, then these should all be defs and not theorems. So either way, the nolint needs to be removed.
There was a problem hiding this comment.
I tried to change as many to def as possible, but isRat_pow gives an error like "unsupported Mathlib.Meta.NormNum.IsNat.casesOn application during code generation" when changed to def, as do the ones in NormNum.Core. What's the fix for this?
There was a problem hiding this comment.
The fix is to move IsRat into Prop. Nothing seems to break because of that and all the theorems can remain theorems. (Sorries in defs are a big no-no, this will break mathport.)
inductive IsRat [Ring α] (a : α) (num : ℤ) (denom : ℕ) : Prop
| mk (inv : Invertible (denom : α)) (eq : a = num * ⅟(denom : α))There was a problem hiding this comment.
I was waiting for the green check to reply but looks like you beat me to it! Great! :)
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
|
Since this is blocking a lot, let's merge it with sorries. bors r+ |
As per #1102, we extend `norm_num` to handle `Rat`s. We leave most of the theorems sorried, but the evaluation and tests work! Co-authored-by: Mario Carneiro <di.gama@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
Rat-dependent norm_num functionalityRat-dependent norm_num functionality
As per #1102, we extend `norm_num` to handle `Rat`s. We leave most of the theorems sorried, but the evaluation and tests work! Co-authored-by: Mario Carneiro <di.gama@gmail.com>
As per #1102, we extend
norm_numto handleRats.We leave most of the theorems sorried, but the evaluation and tests work!