chore: fixes for leanprover/lean4#2724 (Fin USize.size) #7853
Conversation
semorrison
changed the title
semorrison
added
v4.3.0
semorrison
changed the title
Mathlib/Data/UInt.lean
Outdated
| lemma UInt8.val_eq_of_lt {a : Nat} : a < UInt8.size -> (ofNat a).val = a := Nat.mod_eq_of_lt | ||
| lemma UInt8.val_eq_coe {a : Nat} : (ofNat a).val = a := rfl | ||
|
|
||
| lemma UInt16.val_eq_of_lt {a : Nat} : a < UInt16.size -> (ofNat a).val = a := Nat.mod_eq_of_lt | ||
| lemma UInt16.val_eq_coe {a : Nat} : (ofNat a).val = a := rfl | ||
|
|
||
| lemma UInt32.val_eq_of_lt {a : Nat} : a < UInt32.size -> (ofNat a).val = a := Nat.mod_eq_of_lt | ||
| lemma UInt32.val_eq_coe {a : Nat} : (ofNat a).val = a := rfl | ||
|
|
||
| lemma UInt64.val_eq_of_lt {a : Nat} : a < UInt64.size -> (ofNat a).val = a := Nat.mod_eq_of_lt | ||
| lemma UInt64.val_eq_coe {a : Nat} : (ofNat a).val = a := rfl | ||
|
|
||
| lemma USize.val_eq_of_lt {a : Nat} : a < USize.size -> (ofNat a).val = a := Nat.mod_eq_of_lt | ||
| lemma USize.val_eq_coe {a : Nat} : (ofNat a).val = a := rfl |
There was a problem hiding this comment.
Is there a reason you changed the statement rather than fixing the syntax here? What actually changed is that lean now puts the coercion on the RHS, but the lemma was hoping it would appear on the LHS.
Writing an explicit coercion seems like it would be the best approach
There was a problem hiding this comment.
Oh, I missed that the statement had changed. I wish our default for lemmas that are actually about coercions was that we always wrote the coercion explicitly in the statement, to make it obvious what the lemma is actually saying.
I've fixed this now, and this PR becomes trivial.
There was a problem hiding this comment.
I wish our default for lemmas that are actually about coercions was that we always wrote the coercion explicitly in the statement, to make it obvious what the lemma is actually saying.
Unfortunately there are still cases where writing the coercion in the place where the pretty-printer shows it actually changes the meaning of the lemma! An obvious example is the coercion on morphisms, which in my experience fails to roundtrip at all every time.
There was a problem hiding this comment.
Okay, but that is not a reason to not write the coercions wherever possible!
leanprover-community-mathlib4-bot
added
merge-conflict
|
bors d+ Sorry for not doing so earlier, I wasn't confident in my understanding of the diff any more (Though I understand this won't be merged) |
|
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
and removed
awaiting-review
This incorporates changes from * #7845 * #7847 * #7853 * #7872 (was never actually made to work, but the diffs in `nightly-testing` are unexciting: we need to fully qualify a few names) They can all be closed when this is merged. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
This was rolled into #8051. |
This incorporates changes from * #7845 * #7847 * #7853 * #7872 (was never actually made to work, but the diffs in `nightly-testing` are unexciting: we need to fully qualify a few names) They can all be closed when this is merged. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Patches required for leanprover/lean4#2724.
The only relevant diff is in Mathlib.Data.UInt. Any other changes are parts of
nightly-testingrequired to make this build.