Bijection between Char and Fin Char.numCodePoints

In this file, we construct a bijection between Char and Fin Char.numCodePoints and show that it is compatible with various operations. Since Fin is simpler than Char due to being based on natural numbers instead of UInt32 and not having a hole in the middle (surrogate code points), this is sometimes useful to simplify reasoning about Char.

We use these declarations in the construction of Char ranges, see the module Init.Data.Range.Polymorphic.Char.

@[reducible, inline]

abbrev Char.numSurrogates : Nat

The number of surrogate code points.

Equations

• Char.numSurrogates = 2048

@[reducible, inline]

abbrev Char.numCodePoints : Nat

The size of the Char type.

Equations

• Char.numCodePoints = 1112064

def Char.ordinal (c : Char) : Fin numCodePoints

Packs Char bijectively into Fin Char.numCodePoints by shifting code points which are greater than the surrogate code points by the number of surrogate code points.

The inverse of this function is called Char.ofOrdinal.

Equations

• c.ordinal = if h : c.val < 55296 then ⟨c.val.toNat, ⋯⟩ else ⟨c.val.toNat - Char.numSurrogates, ⋯⟩

def Char.ofOrdinal (f : Fin numCodePoints) : Char

Unpacks Fin Char.numCodePoints bijectively to Char by shifting code points which are greater than the surrogate code points by the number of surrogate code points.

The inverse of this function is called Char.ordinal.

Equations

• Char.ofOrdinal f = if h : ↑f < 55296 then { val := UInt32.ofNatLT ↑f ⋯, valid := ⋯ } else { val := UInt32.ofNatLT (↑f + Char.numSurrogates) ⋯, valid := ⋯ }

def Char.succ? (c : Char) : Option Char

Computes the next Char, skipping over surrogate code points (which are not valid Chars) as necessary.

This function is specified by its interaction with Char.ordinal, see Char.succ?_eq.

Equations

• One or more equations did not get rendered due to their size.

def Char.succMany? (m : Nat) (c : Char) : Option Char

Computes the m-th next Char, skipping over surrogate code points (which are not valid Chars) as necessary.

This function is specified by its interaction with Char.ordinal, see Char.succMany?_eq.

Equations

• Char.succMany? m c = Option.map Char.ofOrdinal (c.ordinal.addNat? m)

theorem Char.coe_ordinal {c : Char} : ↑c.ordinal = if c.val < 55296 then c.val.toNat else c.val.toNat - numSurrogates

@[simp]

theorem Char.ordinal_zero : '\x00'.ordinal = 0

theorem Char.val_ofOrdinal {f : Fin numCodePoints} : (ofOrdinal f).val = if h : ↑f < 55296 then UInt32.ofNatLT ↑f ⋯ else UInt32.ofNatLT (↑f + numSurrogates) ⋯

@[simp]

theorem Char.ofOrdinal_ordinal {c : Char} : ofOrdinal c.ordinal = c

@[simp]

theorem Char.ordinal_ofOrdinal {f : Fin numCodePoints} : (ofOrdinal f).ordinal = f

@[simp]

theorem Char.ordinal_comp_ofOrdinal : ordinal ∘ ofOrdinal = id

@[simp]

theorem Char.ofOrdinal_comp_ordinal : ofOrdinal ∘ ordinal = id

@[simp]

theorem Char.ordinal_inj {c d : Char} : c.ordinal = d.ordinal ↔ c = d

theorem Char.ordinal_injective : Function.Injective ordinal

@[simp]

theorem Char.ofOrdinal_inj {f g : Fin numCodePoints} : ofOrdinal f = ofOrdinal g ↔ f = g

theorem Char.ofOrdinal_injective : Function.Injective ofOrdinal

theorem Char.ordinal_le_of_le {c d : Char} (h : c ≤ d) : c.ordinal ≤ d.ordinal

theorem Char.ofOrdinal_le_of_le {f g : Fin numCodePoints} (h : f ≤ g) : ofOrdinal f ≤ ofOrdinal g

theorem Char.le_iff_ordinal_le {c d : Char} : c ≤ d ↔ c.ordinal ≤ d.ordinal

theorem Char.le_iff_ofOrdinal_le {f g : Fin numCodePoints} : f ≤ g ↔ ofOrdinal f ≤ ofOrdinal g

theorem Char.lt_iff_ordinal_lt {c d : Char} : c < d ↔ c.ordinal < d.ordinal

theorem Char.lt_iff_ofOrdinal_lt {f g : Fin numCodePoints} : f < g ↔ ofOrdinal f < ofOrdinal g

theorem Char.succ?_eq {c : Char} : c.succ? = Option.map ofOrdinal (c.ordinal.addNat? 1)

theorem Char.map_ordinal_succ? {c : Char} : Option.map ordinal c.succ? = c.ordinal.addNat? 1

theorem Char.succMany?_eq {m : Nat} {c : Char} : succMany? m c = Option.map ofOrdinal (c.ordinal.addNat? m)