max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: make proof for Char.toUpper easier to typecheck (#12431)

Browse source 
This PR changes the proof for `Char.toUpper` to make it easier to
typecheck for external checkers (nanoda in particular).

---------

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This commit is contained in:
Rob23oba 2026-02-11 15:00:00 +01:00 • committed by GitHub
parent 8f0b67a92e
commit 964d6a3082
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Init/Data/Char/Basic.lean
View file

@ -163,16 +163,19 @@ The lowercase ASCII letters are the following: `abcdefghijklmnopqrstuvwxyz`.
-/
@[inline]
def toUpper (c : Char) : Char :=
if h : c.val ≥ 'a'.val ∧ c.val ≤ 'z'.val then
if h : 'a'.val ≤ c.val ∧ c.val ≤ 'z'.val then
⟨c.val + ('A'.val - 'a'.val), ?_⟩
else
c
where finally
have h₁ : 2^32 ≤ c.val.toNat + ('A'.val - 'a'.val).toNat :=
@Nat.add_le_add 'a'.val.toNat _ (2^32 - 'a'.val.toNat) _ h.1 (by decide)
have h₂ : c.val.toBitVec.toNat + ('A'.val - 'a'.val).toNat < 2^32 + 0xd800 :=
Nat.add_lt_add_right (Nat.lt_of_le_of_lt h.2 (by decide)) _
have add_eq {x y : UInt32} : (x + y).toNat = (x.toNat + y.toNat) % 2^32 := rfl
-- This expression is a ground non-value; generalize for better
-- control on where it is evaluated.
generalize hx : 'A'.val - 'a'.val = x
have h₁ : 2^32 ≤ c.val.toNat + x.toNat :=
@Nat.add_le_add 'a'.val.toNat _ (2^32 - 'a'.val.toNat) _ h.1 (by rw [← hx]; decide)
have h₂ : c.val.toBitVec.toNat + x.toNat < 2^32 + 0xd800 :=
Nat.add_lt_of_lt_sub (Nat.lt_of_le_of_lt h.2 (by rw [← hx]; decide))
have add_eq {x y : UInt32} : (x + y).toNat = (x.toNat + y.toNat) % 2^32 := id rfl
replace h₂ := Nat.sub_lt_left_of_lt_add h₁ h₂
exact .inl <| lt_of_eq_of_lt (add_eq.trans (Nat.mod_eq_sub_mod h₁) |>.trans
(Nat.mod_eq_of_lt (Nat.lt_trans h₂ (by decide)))) h₂