From ee4b11ddc59ae83d8a31f69c99943a05d90519b2 Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Fri, 25 Oct 2024 20:57:05 -0400
Subject: [PATCH] feat: add instance for `Char`

---
 Batteries/Data/Fin/Coding.lean | 50 ++++++++++++++++++++++++++++++++++
 Batteries/Data/Fin/Enum.lean   |  7 +++++
 2 files changed, 57 insertions(+)

diff --git a/Batteries/Data/Fin/Coding.lean b/Batteries/Data/Fin/Coding.lean
index 5cc54ac0e6..3a1f492d05 100644
--- 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
index 60670ed02f..299cabcb1c 100644
--- 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