feat: make Rat.ofScientific @[irreducible]
#109
Conversation
Std/Data/Rat/Basic.lean
Outdated
| /-- Implements "scientific notation" `123.4e-5` for rational numbers. (This definition is | ||
| `@[irreducible]` because you don't want to unfold it over e.g. `RatCast.ratCast`.) -/ |
There was a problem hiding this comment.
| /-- Implements "scientific notation" `123.4e-5` for rational numbers. (This definition is | |
| `@[irreducible]` because you don't want to unfold it over e.g. `RatCast.ratCast`.) -/ | |
| /-- Implements "scientific notation" `123.4e-5` for rational numbers. (This definition is | |
| `@[irreducible]` because you don't want to unfold it. Use `Rat.ofScientific_def` instead.) -/ |
Wording copied from Rat.mul. (Yes, you should also add ofScientific_def in Data.Rat.Lemmas)
There was a problem hiding this comment.
(Got it, for some reason was under the impression the needed lemmas were autogenerated.)
Does this mean we want something like Rat.ofScientific_true_def and Rat.ofScientific_false_def, or are we ok with that if being in the type?
There was a problem hiding this comment.
Actually the rhs of the equality even for the true version looks odd:
normalize m (10 ^ e) <| Nat.ne_of_gt <| Nat.pos_pow_of_pos _ (by decide)
...is there a better lemma we could state here? Or is this fine?
There was a problem hiding this comment.
I pushed one possible solution, patterned off of sub_def, sub_def'; if it's not right I'll change it. :) (Also not sure if it should be ofScientific_of_true_def or not, or if brevity is better.)
There was a problem hiding this comment.
you should use mkRat instead of normalize in both cases. I agree that it would also be better to have separate true and false cases, and it is optional whether you want to add ofScientific_def itself.
There was a problem hiding this comment.
ofScientific_true_def and ofScientific_false_def seem fine to me as names.
There was a problem hiding this comment.
👍 Ok, I've removed the normalize version of ofScientific_true_def and just left the mkRat version. (Note that ofScientific_false_def just has a Nat on the rhs.) Also added ofScientific_def for completeness' sake.
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Std/Data/Rat/Lemmas.lean
Outdated
| unfold Rat.ofScientific | ||
| exact normalize_eq_mkRat (Nat.ne_of_gt <| Nat.pos_pow_of_pos _ (by decide)) | ||
|
|
||
| theorem ofScientific_false_def : Rat.ofScientific m false e = (m * 10 ^ e : Nat) := by | ||
| unfold Rat.ofScientific | ||
| rfl |
There was a problem hiding this comment.
| unfold Rat.ofScientific | |
| exact normalize_eq_mkRat (Nat.ne_of_gt <| Nat.pos_pow_of_pos _ (by decide)) | |
| theorem ofScientific_false_def : Rat.ofScientific m false e = (m * 10 ^ e : Nat) := by | |
| unfold Rat.ofScientific | |
| rfl | |
| unfold Rat.ofScientific; apply normalize_eq_mkRat | |
| theorem ofScientific_false_def : Rat.ofScientific m false e = (m * 10 ^ e : Nat) := by | |
| unfold Rat.ofScientific; rfl |
There was a problem hiding this comment.
It didn't like apply normalize_eq_mkRat; the alternative along that direction is unfold Rat.ofScientific; apply normalize_eq_mkRat ∘ Nat.ne_of_gt ∘ Nat.pos_pow_of_pos _; decide, but I thought that was less clear than an exact. Though, saves a line, so I could put that back if you'd like.
There was a problem hiding this comment.
no you shouldn't be providing the proof at all here, it is supposed to be found by unification on the existing term. did you try rw [normalize_eq_mkRat]?
There was a problem hiding this comment.
Ah gotcha. Yup, that followed by a rfl worked.
thorimur
force-pushed
the
Rat-ofScientific-irreducible
branch
2 times, most recently
from
2caf9a1
to
e9f08b5
Compare
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
thorimur
force-pushed
the
Rat-ofScientific-irreducible
branch
from
e9f08b5
to
a19460b
Compare
Notably incorporates leanprover-community/batteries#98 and leanprover-community/batteries#109. leanprover-community/batteries#98 moves a number of lemmas from Mathlib to Std, so the bump requires deleting them in Mathlib. I did check on each lemma whether its attributes were kept in the move (and gave attribute markings in Mathlib if they were not present in Std), but a reviewer may wish to re-check. `List.mem_map` changed statement from `b ∈ l.map f ↔ ∃ a, a ∈ l ∧ b = f a` to `b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b`. Similarly for `List.exists_of_mem_map`. This was a deliberate change, so I have simply adjusted proofs (many become simpler, which supports the change). I also deleted `List.mem_map'`, `List.exists_of_mem_map'`, which were temporary versions in Mathlib while waiting for this change (replacing their uses with the unprimed versions). Also, the lemma `sublist_nil_iff_eq_nil` seems to have been renamed to `sublist_nil` during the move, so I added an alias for the old name. (another issue fixed during review by @digama0) ~~`List.Sublist.filter` had an argument change from explicit to implicit. This appears to have been an oversight (cc @JamesGallicchio). I have temporarily introduced `List.Sublist.filter'` with the argument explicit, and replaced Mathlib uses of `Sublist.filter` with `Sublist.filter'`. Later we can fix the argument in Std, and then delete `List.Sublist.filter'`.~~
We make
Rat.ofScientificirreducible to prevent it from being unfolded during defeq checks in which we'd rather unfold e.g.RatCast.ratCaston the rhs. See zulip.