feat: add instance for Char

leanprover-community · Oct 26, 2024 · ee4b11d · ee4b11d
1 parent 4e209ef
commit ee4b11d
Show file tree

Hide file tree

Showing 2 changed files with 57 additions and 0 deletions.
diff --git a/Batteries/Data/Fin/Coding.lean b/Batteries/Data/Fin/Coding.lean
@@ -49,6 +49,56 @@ def encodeBool : Bool → Fin 2
   | false => rfl
   | true => rfl
 
+#print Char.isValidCharNat
+-- n < 55296 ∨ 57343 < n ∧ n < 1114112
+
+#eval 55296 + 1114112 - 57343
+#eval 57343 - 55296
+#print isValidChar
+
+/-- Encode a character value as a `Fin` type. -/
+@[pp_nodot] def encodeChar (c : Char) : Fin 1112064 :=
+  have : c.toNat < 1114112 := by
+    match c.valid with
+    | .inl h => apply Nat.lt_trans h; decide
+    | .inr h => exact h.right
+  if _ : c.toNat < 55296 then
+    ⟨c.toNat, by omega⟩
+  else
+    ⟨c.toNat - 2048, by omega⟩
+
+/-- Decode a character value as a `Fin` type. -/
+def decodeChar (i : Fin 1112064) : Char :=
+  if h : i.val < 55296 then
+    Char.ofNatAux i.val (by omega)
+  else
+    Char.ofNatAux (i.val + 2048) (by omega)
+
+@[simp] theorem encodeChar_decodeChar (x) : encodeChar (decodeChar x) = x := by
+  simp only [decodeChar]
+  split
+  · simp [encodeChar, Char.ofNatAux, Char.toNat, UInt32.toNat]; intro; omega
+  · simp [encodeChar, Char.ofNatAux, Char.toNat, UInt32.toNat]; intro; omega
+
+@[simp] theorem decodeChar_encodeChar (x) : decodeChar (encodeChar x) = x := by
+  ext
+  simp [decodeChar, encodeChar]
+  split
+  · next h =>
+    simp only [Char.toNat] at h
+    simp [decodeChar, Char.ofNatAux, Char.toNat, dif_pos h]; rfl
+  · next h =>
+    have h0 : 57344 ≤ x.toNat ∧ x.toNat < 1114112 := by
+      match x.valid with
+      | .inl h => contradiction
+      | .inr h =>
+        constructor
+        · exact Nat.add_one_le_of_lt h.left
+        · exact h.right
+    have h1 : ¬ x.toNat - 2048 < 55296 := by omega
+    have h2 : 2048 ≤ x.toNat := by omega
+    simp [dif_neg h1, Char.ofNatAux, Nat.sub_add_cancel h2]; rfl
+
 /-- Decode an optional `Fin` types. -/
 def encodeOption : Option (Fin n) → Fin (n+1)
   | none => 0

diff --git a/Batteries/Data/Fin/Enum.lean b/Batteries/Data/Fin/Enum.lean
@@ -45,6 +45,13 @@ instance : Fin.Enum Bool where
   decode_encode := decodeBool_encodeBool
   encode_decode := encodeBool_decodeBool
 
+instance : Fin.Enum Char where
+  size := 1112064
+  decode := decodeChar
+  encode := encodeChar
+  decode_encode := decodeChar_encodeChar
+  encode_decode := encodeChar_decodeChar
+
 instance [Fin.Enum α] : Fin.Enum (Option α) where
   size := size α + 1
   decode i := decodeOption i |>.map decode