From 69b058dc82edfff0cf2787eb5aa0cdd42c12ab2c Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Thu, 22 Jan 2026 08:44:55 +0100 Subject: [PATCH] feat: `Fin` and `Char` ranges (#12058) This PR implements iteration over ranges for `Fin` and `Char`. To this end, we introduce machinery for pulling back lawfulness of `UpwardEnumerable` along an injective map and study the function `Char.ordinal : Char -> Fin Char.numCodePoints`. --- src/Init/Data/Char.lean | 1 + src/Init/Data/Char/Ordinal.lean | 242 ++++++++++++++++++++++ src/Init/Data/Fin.lean | 1 + src/Init/Data/Fin/OverflowAware.lean | 51 +++++ src/Init/Data/Option.lean | 1 + src/Init/Data/Option/Function.lean | 26 +++ src/Init/Data/Option/Lemmas.lean | 13 ++ src/Init/Data/Range/Polymorphic.lean | 3 + src/Init/Data/Range/Polymorphic/Char.lean | 79 +++++++ src/Init/Data/Range/Polymorphic/Fin.lean | 92 ++++++++ src/Init/Data/Range/Polymorphic/Map.lean | 195 +++++++++++++++++ src/Init/Prelude.lean | 2 + tests/lean/run/charrange.lean | 29 +++ 13 files changed, 735 insertions(+) create mode 100644 src/Init/Data/Char/Ordinal.lean create mode 100644 src/Init/Data/Fin/OverflowAware.lean create mode 100644 src/Init/Data/Option/Function.lean create mode 100644 src/Init/Data/Range/Polymorphic/Char.lean create mode 100644 src/Init/Data/Range/Polymorphic/Fin.lean create mode 100644 src/Init/Data/Range/Polymorphic/Map.lean create mode 100644 tests/lean/run/charrange.lean diff --git a/src/Init/Data/Char.lean b/src/Init/Data/Char.lean index d920537fe8..80d098519c 100644 --- a/src/Init/Data/Char.lean +++ b/src/Init/Data/Char.lean @@ -9,3 +9,4 @@ prelude public import Init.Data.Char.Basic public import Init.Data.Char.Lemmas public import Init.Data.Char.Order +public import Init.Data.Char.Ordinal diff --git a/src/Init/Data/Char/Ordinal.lean b/src/Init/Data/Char/Ordinal.lean new file mode 100644 index 0000000000..2e8160d913 --- /dev/null +++ b/src/Init/Data/Char/Ordinal.lean @@ -0,0 +1,242 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Markus Himmel +-/ +module + +prelude +public import Init.Data.Fin.OverflowAware +public import Init.Data.UInt.Basic +public import Init.Data.Function +import Init.Data.Char.Lemmas +import Init.Data.Char.Order +import Init.Grind + +/-! +# 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`. +-/ + +set_option doc.verso true + +public section + +namespace Char + +/-- The number of surrogate code points. -/ +abbrev numSurrogates : Nat := + -- 0xe000 - 0xd800 + 2048 + +/-- The size of the {name}`Char` type. -/ +abbrev numCodePoints : Nat := + -- 0x110000 - numSurrogates + 1112064 + +/-- +Packs {name}`Char` bijectively into {lean}`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 {name (scope := "Init.Data.Char.Ordinal")}`Char.ofOrdinal`. +-/ +def ordinal (c : Char) : Fin Char.numCodePoints := + if h : c.val < 0xd800 then + ⟨c.val.toNat, by grind [UInt32.lt_iff_toNat_lt]⟩ + else + ⟨c.val.toNat - Char.numSurrogates, by grind [UInt32.lt_iff_toNat_lt]⟩ + +/-- +Unpacks {lean}`Fin Char.numCodePoints` bijectively to {name}`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 {name}`Char.ordinal`. +-/ +def ofOrdinal (f : Fin Char.numCodePoints) : Char := + if h : (f : Nat) < 0xd800 then + ⟨UInt32.ofNatLT f (by grind), by grind [UInt32.toNat_ofNatLT]⟩ + else + ⟨UInt32.ofNatLT (f + Char.numSurrogates) (by grind), by grind [UInt32.toNat_ofNatLT]⟩ + +/-- +Computes the next {name}`Char`, skipping over surrogate code points (which are not valid +{name}`Char`s) as necessary. + +This function is specified by its interaction with {name}`Char.ordinal`, see +{name (scope := "Init.Data.Char.Ordinal")}`Char.succ?_eq`. +-/ +def succ? (c : Char) : Option Char := + if h₀ : c.val < 0xd7ff then + some ⟨c.val + 1, by grind [UInt32.lt_iff_toNat_lt, UInt32.toNat_add]⟩ + else if h₁ : c.val = 0xd7ff then + some ⟨0xe000, by decide⟩ + else if h₂ : c.val < 0x10ffff then + some ⟨c.val + 1, by + simp only [UInt32.lt_iff_toNat_lt, UInt32.reduceToNat, Nat.not_lt, ← UInt32.toNat_inj, + UInt32.isValidChar, Nat.isValidChar, UInt32.toNat_add, Nat.reducePow] at * + grind⟩ + else none + +/-- +Computes the {name}`m`-th next {name}`Char`, skipping over surrogate code points (which are not +valid {name}`Char`s) as necessary. + +This function is specified by its interaction with {name}`Char.ordinal`, see +{name (scope := "Init.Data.Char.Ordinal")}`Char.succMany?_eq`. +-/ +def succMany? (m : Nat) (c : Char) : Option Char := + c.ordinal.addNat? m |>.map Char.ofOrdinal + +@[grind =] +theorem coe_ordinal {c : Char} : + (c.ordinal : Nat) = + if c.val < 0xd800 then + c.val.toNat + else + c.val.toNat - Char.numSurrogates := by + grind [Char.ordinal] + +@[simp] +theorem ordinal_zero : '\x00'.ordinal = 0 := by + ext + simp [coe_ordinal] + +@[grind =] +theorem val_ofOrdinal {f : Fin Char.numCodePoints} : + (Char.ofOrdinal f).val = + if h : (f : Nat) < 0xd800 then + UInt32.ofNatLT f (by grind) + else + UInt32.ofNatLT (f + Char.numSurrogates) (by grind) := by + grind [Char.ofOrdinal] + +@[simp] +theorem ofOrdinal_ordinal {c : Char} : Char.ofOrdinal c.ordinal = c := by + ext + simp only [val_ofOrdinal, coe_ordinal, UInt32.ofNatLT_add] + split + · grind [UInt32.lt_iff_toNat_lt, UInt32.ofNatLT_toNat] + · rw [dif_neg] + · simp only [← UInt32.toNat_inj, UInt32.toNat_add, UInt32.toNat_ofNatLT, Nat.reducePow] + grind [UInt32.toNat_lt, UInt32.lt_iff_toNat_lt] + · grind [UInt32.lt_iff_toNat_lt] + +@[simp] +theorem ordinal_ofOrdinal {f : Fin Char.numCodePoints} : (Char.ofOrdinal f).ordinal = f := by + ext + simp [coe_ordinal, val_ofOrdinal] + split + · rw [if_pos, UInt32.toNat_ofNatLT] + simpa [UInt32.lt_iff_toNat_lt] + · rw [if_neg, UInt32.toNat_add, UInt32.toNat_ofNatLT, UInt32.toNat_ofNatLT, Nat.mod_eq_of_lt, + Nat.add_sub_cancel] + · grind + · simp only [UInt32.lt_iff_toNat_lt, UInt32.toNat_add, UInt32.toNat_ofNatLT, Nat.reducePow, + UInt32.reduceToNat, Nat.not_lt] + grind + +@[simp] +theorem ordinal_comp_ofOrdinal : Char.ordinal ∘ Char.ofOrdinal = id := by + ext; simp + +@[simp] +theorem ofOrdinal_comp_ordinal : Char.ofOrdinal ∘ Char.ordinal = id := by + ext; simp + +@[simp] +theorem ordinal_inj {c d : Char} : c.ordinal = d.ordinal ↔ c = d := + ⟨fun h => by simpa using congrArg Char.ofOrdinal h, (· ▸ rfl)⟩ + +theorem ordinal_injective : Function.Injective Char.ordinal := + fun _ _ => ordinal_inj.1 + +@[simp] +theorem ofOrdinal_inj {f g : Fin Char.numCodePoints} : + Char.ofOrdinal f = Char.ofOrdinal g ↔ f = g := + ⟨fun h => by simpa using congrArg Char.ordinal h, (· ▸ rfl)⟩ + +theorem ofOrdinal_injective : Function.Injective Char.ofOrdinal := + fun _ _ => ofOrdinal_inj.1 + +theorem ordinal_le_of_le {c d : Char} (h : c ≤ d) : c.ordinal ≤ d.ordinal := by + simp only [le_def, UInt32.le_iff_toNat_le] at h + simp only [Fin.le_def, coe_ordinal, UInt32.lt_iff_toNat_lt, UInt32.reduceToNat] + grind + +theorem ofOrdinal_le_of_le {f g : Fin Char.numCodePoints} (h : f ≤ g) : + Char.ofOrdinal f ≤ Char.ofOrdinal g := by + simp only [Fin.le_def] at h + simp only [le_def, val_ofOrdinal, UInt32.ofNatLT_add, UInt32.le_iff_toNat_le] + split + · simp only [UInt32.toNat_ofNatLT] + split + · simpa + · simp only [UInt32.toNat_add, UInt32.toNat_ofNatLT, Nat.reducePow] + grind + · simp only [UInt32.toNat_add, UInt32.toNat_ofNatLT, Nat.reducePow] + rw [dif_neg (by grind)] + simp only [UInt32.toNat_add, UInt32.toNat_ofNatLT, Nat.reducePow] + grind + +theorem le_iff_ordinal_le {c d : Char} : c ≤ d ↔ c.ordinal ≤ d.ordinal := + ⟨ordinal_le_of_le, fun h => by simpa using ofOrdinal_le_of_le h⟩ + +theorem le_iff_ofOrdinal_le {f g : Fin Char.numCodePoints} : + f ≤ g ↔ Char.ofOrdinal f ≤ Char.ofOrdinal g := + ⟨ofOrdinal_le_of_le, fun h => by simpa using ordinal_le_of_le h⟩ + +theorem lt_iff_ordinal_lt {c d : Char} : c < d ↔ c.ordinal < d.ordinal := by + simp only [Std.lt_iff_le_and_not_ge, le_iff_ordinal_le] + +theorem lt_iff_ofOrdinal_lt {f g : Fin Char.numCodePoints} : + f < g ↔ Char.ofOrdinal f < Char.ofOrdinal g := by + simp only [Std.lt_iff_le_and_not_ge, le_iff_ofOrdinal_le] + +theorem succ?_eq {c : Char} : c.succ? = (c.ordinal.addNat? 1).map Char.ofOrdinal := by + fun_cases Char.succ? with + | case1 h => + rw [Fin.addNat?_eq_some] + · simp only [coe_ordinal, Option.map_some, Option.some.injEq, Char.ext_iff, val_ofOrdinal, + UInt32.ofNatLT_add, UInt32.reduceOfNatLT] + split + · simp only [UInt32.ofNatLT_toNat, dite_eq_ite, left_eq_ite_iff, Nat.not_lt, + Nat.reduceLeDiff, UInt32.left_eq_add] + grind [UInt32.lt_iff_toNat_lt] + · grind + · simp [coe_ordinal] + grind [UInt32.lt_iff_toNat_lt] + | case2 => + rw [Fin.addNat?_eq_some] + · simp [coe_ordinal, *, Char.ext_iff, val_ofOrdinal, numSurrogates] + · simp [coe_ordinal, *, numCodePoints] + | case3 => + rw [Fin.addNat?_eq_some] + · simp only [coe_ordinal, Option.map_some, Option.some.injEq, Char.ext_iff, val_ofOrdinal, + UInt32.ofNatLT_add, UInt32.reduceOfNatLT] + split + · grind + · rw [dif_neg] + · simp only [← UInt32.toNat_inj, UInt32.toNat_add, UInt32.reduceToNat, Nat.reducePow, + UInt32.toNat_ofNatLT, Nat.mod_add_mod] + grind [UInt32.lt_iff_toNat_lt, UInt32.toNat_inj] + · grind [UInt32.lt_iff_toNat_lt, UInt32.toNat_inj] + · grind [UInt32.lt_iff_toNat_lt] + | case4 => + rw [eq_comm] + grind [UInt32.lt_iff_toNat_lt] + +theorem map_ordinal_succ? {c : Char} : c.succ?.map ordinal = c.ordinal.addNat? 1 := by + simp [succ?_eq] + +theorem succMany?_eq {m : Nat} {c : Char} : + c.succMany? m = (c.ordinal.addNat? m).map Char.ofOrdinal := by + rfl + +end Char diff --git a/src/Init/Data/Fin.lean b/src/Init/Data/Fin.lean index 18cce10f8d..1cd06405c5 100644 --- a/src/Init/Data/Fin.lean +++ b/src/Init/Data/Fin.lean @@ -11,3 +11,4 @@ public import Init.Data.Fin.Log2 public import Init.Data.Fin.Iterate public import Init.Data.Fin.Fold public import Init.Data.Fin.Lemmas +public import Init.Data.Fin.OverflowAware diff --git a/src/Init/Data/Fin/OverflowAware.lean b/src/Init/Data/Fin/OverflowAware.lean new file mode 100644 index 0000000000..d6dcbed5d1 --- /dev/null +++ b/src/Init/Data/Fin/OverflowAware.lean @@ -0,0 +1,51 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Markus Himmel +-/ +module + +prelude +public import Init.Data.Fin.Basic +import Init.Data.Fin.Lemmas + +set_option doc.verso true + +public section + +namespace Fin + +/-- +Overflow-aware addition of a natural number to an element of {lean}`Fin n`. + +Examples: +* {lean}`(2 : Fin 3).addNat? 1 = (none : Option (Fin 3))` +* {lean}`(2 : Fin 4).addNat? 1 = (some 3 : Option (Fin 4))` +-/ +@[inline] +protected def addNat? (i : Fin n) (m : Nat) : Option (Fin n) := + if h : i + m < n then some ⟨i + m, h⟩ else none + +theorem addNat?_eq_some {i : Fin n} (h : i + m < n) : i.addNat? m = some ⟨i + m, h⟩ := by + simp [Fin.addNat?, h] + +theorem addNat?_eq_some_iff {i : Fin n} : + i.addNat? m = some j ↔ i + m < n ∧ j = i + m := by + simp only [Fin.addNat?] + split <;> simp [Fin.ext_iff, eq_comm, *] + +@[simp] +theorem addNat?_eq_none_iff {i : Fin n} : i.addNat? m = none ↔ n ≤ i + m := by + simp only [Fin.addNat?] + split <;> simp_all [Nat.not_lt] + +@[simp] +theorem addNat?_zero {i : Fin n} : i.addNat? 0 = some i := by + simp [addNat?_eq_some_iff] + +@[grind =] +theorem addNat?_eq_dif {i : Fin n} : + i.addNat? m = if h : i + m < n then some ⟨i + m, h⟩ else none := by + rfl + +end Fin diff --git a/src/Init/Data/Option.lean b/src/Init/Data/Option.lean index ea1f54855e..3ab5b8a2fc 100644 --- a/src/Init/Data/Option.lean +++ b/src/Init/Data/Option.lean @@ -15,3 +15,4 @@ public import Init.Data.Option.Attach public import Init.Data.Option.List public import Init.Data.Option.Monadic public import Init.Data.Option.Array +public import Init.Data.Option.Function diff --git a/src/Init/Data/Option/Function.lean b/src/Init/Data/Option/Function.lean new file mode 100644 index 0000000000..e1034b9ed7 --- /dev/null +++ b/src/Init/Data/Option/Function.lean @@ -0,0 +1,26 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +module + +prelude +public import Init.Data.Function +import Init.Data.Option.Lemmas + +public section + +namespace Option + +theorem map_injective {f : α → β} (hf : Function.Injective f) : + Function.Injective (Option.map f) := by + intros a b hab + cases a <;> cases b + · simp + · simp at hab + · simp at hab + · simp only [map_some, some.injEq] at hab + simpa using hf hab + +end Option diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean index 21133a4251..d54624f459 100644 --- a/src/Init/Data/Option/Lemmas.lean +++ b/src/Init/Data/Option/Lemmas.lean @@ -307,12 +307,20 @@ theorem map_id' {x : Option α} : (x.map fun a => a) = x := congrFun map_id x theorem map_id_apply' {α : Type u} {x : Option α} : Option.map (fun (a : α) => a) x = x := by simp +/-- See `Option.apply_get` for a version that can be rewritten in the reverse direction. -/ @[simp, grind =] theorem get_map {f : α → β} {o : Option α} {h : (o.map f).isSome} : (o.map f).get h = f (o.get (by simpa using h)) := by cases o with | none => simp at h | some a => simp +/-- See `Option.get_map` for a version that can be rewritten in the reverse direction. -/ +theorem apply_get {f : α → β} {o : Option α} {h} : + f (o.get h) = (o.map f).get (by simp [h]) := by + cases o + · simp at h + · simp + @[simp] theorem map_map (h : β → γ) (g : α → β) (x : Option α) : (x.map g).map h = x.map (h ∘ g) := by cases x <;> simp only [map_none, map_some, ·∘·] @@ -732,6 +740,11 @@ theorem get_merge {o o' : Option α} {f : α → α → α} {i : α} [Std.Lawful theorem elim_guard : (guard p a).elim b f = if p a then f a else b := by cases h : p a <;> simp [*, guard] +@[simp] +theorem Option.elim_map {f : α → β} {g' : γ} {g : β → γ} (o : Option α) : + (o.map f).elim g' g = o.elim g' (g ∘ f) := by + cases o <;> simp + -- I don't see how to construct a good grind pattern to instantiate this. @[simp] theorem getD_map (f : α → β) (x : α) (o : Option α) : (o.map f).getD (f x) = f (getD o x) := by cases o <;> rfl diff --git a/src/Init/Data/Range/Polymorphic.lean b/src/Init/Data/Range/Polymorphic.lean index 4893f752d9..1ca3273dae 100644 --- a/src/Init/Data/Range/Polymorphic.lean +++ b/src/Init/Data/Range/Polymorphic.lean @@ -10,7 +10,10 @@ public import Init.Data.Range.Polymorphic.Basic public import Init.Data.Range.Polymorphic.Iterators public import Init.Data.Range.Polymorphic.Stream public import Init.Data.Range.Polymorphic.Lemmas +public import Init.Data.Range.Polymorphic.Map +public import Init.Data.Range.Polymorphic.Fin +public import Init.Data.Range.Polymorphic.Char public import Init.Data.Range.Polymorphic.Nat public import Init.Data.Range.Polymorphic.Int public import Init.Data.Range.Polymorphic.BitVec diff --git a/src/Init/Data/Range/Polymorphic/Char.lean b/src/Init/Data/Range/Polymorphic/Char.lean new file mode 100644 index 0000000000..6388518c95 --- /dev/null +++ b/src/Init/Data/Range/Polymorphic/Char.lean @@ -0,0 +1,79 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Markus Himmel +-/ +module + +prelude +public import Init.Data.Char.Ordinal +public import Init.Data.Range.Polymorphic.Fin +import Init.Data.Range.Polymorphic.Lemmas +import Init.Data.Range.Polymorphic.Map +import Init.Data.Char.Order + +open Std Std.PRange Std.PRange.UpwardEnumerable + +namespace Char + +public instance : UpwardEnumerable Char where + succ? + succMany? + +@[simp] +public theorem pRangeSucc?_eq : PRange.succ? (α := Char) = Char.succ? := rfl + +@[simp] +public theorem pRangeSuccMany?_eq : PRange.succMany? (α := Char) = Char.succMany? := rfl + +public instance : Rxc.HasSize Char where + size lo hi := Rxc.HasSize.size lo.ordinal hi.ordinal + +public instance : Rxo.HasSize Char where + size lo hi := Rxo.HasSize.size lo.ordinal hi.ordinal + +public instance : Rxi.HasSize Char where + size hi := Rxi.HasSize.size hi.ordinal + +public instance : Least? Char where + least? := some '\x00' + +@[simp] +public theorem least?_eq : Least?.least? (α := Char) = some '\x00' := rfl + +def map : Map Char (Fin Char.numCodePoints) where + toFun := Char.ordinal + injective := ordinal_injective + succ?_toFun := by simp [succ?_eq] + succMany?_toFun := by simp [succMany?_eq] + +@[simp] +theorem toFun_map : map.toFun = Char.ordinal := rfl + +instance : Map.PreservesLE map where + le_iff := by simp [le_iff_ordinal_le] + +instance : Map.PreservesRxcSize map where + size_eq := rfl + +instance : Map.PreservesRxoSize map where + size_eq := rfl + +instance : Map.PreservesRxiSize map where + size_eq := rfl + +instance : Map.PreservesLeast? map where + map_least? := by simp + +public instance : LawfulUpwardEnumerable Char := .ofMap map +public instance : LawfulUpwardEnumerableLE Char := .ofMap map +public instance : LawfulUpwardEnumerableLT Char := .ofMap map +public instance : LawfulUpwardEnumerableLeast? Char := .ofMap map +public instance : Rxc.LawfulHasSize Char := .ofMap map +public instance : Rxc.IsAlwaysFinite Char := .ofMap map +public instance : Rxo.LawfulHasSize Char := .ofMap map +public instance : Rxo.IsAlwaysFinite Char := .ofMap map +public instance : Rxi.LawfulHasSize Char := .ofMap map +public instance : Rxi.IsAlwaysFinite Char := .ofMap map + +end Char diff --git a/src/Init/Data/Range/Polymorphic/Fin.lean b/src/Init/Data/Range/Polymorphic/Fin.lean new file mode 100644 index 0000000000..01b7eaa33f --- /dev/null +++ b/src/Init/Data/Range/Polymorphic/Fin.lean @@ -0,0 +1,92 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +module + +prelude +public import Init.Data.Range.Polymorphic.Instances +public import Init.Data.Fin.OverflowAware +import Init.Grind + +public section + +open Std Std.PRange + +namespace Fin + +instance : UpwardEnumerable (Fin n) where + succ? i := i.addNat? 1 + succMany? m i := i.addNat? m + +@[simp, grind =] +theorem pRangeSucc?_eq : PRange.succ? (α := Fin n) = (·.addNat? 1) := rfl + +@[simp, grind =] +theorem pRangeSuccMany?_eq : PRange.succMany? m (α := Fin n) = (·.addNat? m) := + rfl + +instance : LawfulUpwardEnumerable (Fin n) where + ne_of_lt a b := by grind [UpwardEnumerable.LT] + succMany?_zero a := by simp + succMany?_add_one m a := by grind + +instance : LawfulUpwardEnumerableLE (Fin n) where + le_iff x y := by + simp only [le_def, UpwardEnumerable.LE, pRangeSuccMany?_eq, Fin.addNat?_eq_dif, + Option.dite_none_right_eq_some, Option.some.injEq, ← val_inj, exists_prop] + exact ⟨fun h => ⟨y - x, by grind⟩, by grind⟩ + +instance : Least? (Fin 0) where + least? := none + +instance : LawfulUpwardEnumerableLeast? (Fin 0) where + least?_le a := False.elim (Nat.not_lt_zero _ a.isLt) + +@[simp] +theorem least?_eq_of_zero : Least?.least? (α := Fin 0) = none := rfl + +instance [NeZero n] : Least? (Fin n) where + least? := some 0 + +instance [NeZero n] : LawfulUpwardEnumerableLeast? (Fin n) where + least?_le a := ⟨0, rfl, (LawfulUpwardEnumerableLE.le_iff 0 a).1 (Fin.zero_le _)⟩ + +@[simp] +theorem least?_eq [NeZero n] : Least?.least? (α := Fin n) = some 0 := rfl + +instance : LawfulUpwardEnumerableLT (Fin n) := inferInstance + +instance : Rxc.HasSize (Fin n) where + size lo hi := hi + 1 - lo + +@[grind =] +theorem rxcHasSize_eq : + Rxc.HasSize.size (α := Fin n) = fun (lo hi : Fin n) => (hi + 1 - lo : Nat) := rfl + +instance : Rxc.LawfulHasSize (Fin n) where + size_eq_zero_of_not_le bound x := by grind + size_eq_one_of_succ?_eq_none lo hi := by grind + size_eq_succ_of_succ?_eq_some lo hi x := by grind + +instance : Rxc.IsAlwaysFinite (Fin n) := inferInstance + +instance : Rxo.HasSize (Fin n) := .ofClosed +instance : Rxo.LawfulHasSize (Fin n) := inferInstance +instance : Rxo.IsAlwaysFinite (Fin n) := inferInstance + +instance : Rxi.HasSize (Fin n) where + size lo := n - lo + +@[grind =] +theorem rxiHasSize_eq : + Rxi.HasSize.size (α := Fin n) = fun (lo : Fin n) => (n - lo : Nat) := rfl + +instance : Rxi.LawfulHasSize (Fin n) where + size_eq_one_of_succ?_eq_none x := by grind + size_eq_succ_of_succ?_eq_some lo lo' := by grind + +instance : Rxi.IsAlwaysFinite (Fin n) := inferInstance + +end Fin diff --git a/src/Init/Data/Range/Polymorphic/Map.lean b/src/Init/Data/Range/Polymorphic/Map.lean new file mode 100644 index 0000000000..80f7b79671 --- /dev/null +++ b/src/Init/Data/Range/Polymorphic/Map.lean @@ -0,0 +1,195 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +module + +prelude +public import Init.Data.Range.Polymorphic.Instances +public import Init.Data.Function +import Init.Data.Order.Lemmas +import Init.Data.Option.Function + +public section + +/-! +# Mappings between `UpwardEnumerable` types + +In this file we build machinery for pulling back lawfulness properties for `UpwardEnumerable` along +injective functions that commute with the relevant operations. +-/ + +namespace Std + +namespace PRange + +namespace UpwardEnumerable + +/-- +An injective mapping between two types implementing `UpwardEnumerable` that commutes with `succ?` +and `succMany?`. + +Having such a mapping means that all of the `Prop`-valued lawfulness classes around +`UpwardEnumerable` can be pulled back. +-/ +structure Map (α : Type u) (β : Type v) [UpwardEnumerable α] [UpwardEnumerable β] where + toFun : α → β + injective : Function.Injective toFun + succ?_toFun (a : α) : succ? (toFun a) = (succ? a).map toFun + succMany?_toFun (n : Nat) (a : α) : succMany? n (toFun a) = (succMany? n a).map toFun + +namespace Map + +variable [UpwardEnumerable α] [UpwardEnumerable β] + +theorem succ?_eq_none_iff (f : Map α β) {a : α} : + succ? a = none ↔ succ? (f.toFun a) = none := by + rw [← (Option.map_injective f.injective).eq_iff, Option.map_none, ← f.succ?_toFun] + +theorem succ?_eq_some_iff (f : Map α β) {a b : α} : + succ? a = some b ↔ succ? (f.toFun a) = some (f.toFun b) := by + rw [← (Option.map_injective f.injective).eq_iff, Option.map_some, ← f.succ?_toFun] + +theorem le_iff (f : Map α β) {a b : α} : + UpwardEnumerable.LE a b ↔ UpwardEnumerable.LE (f.toFun a) (f.toFun b) := by + simp only [UpwardEnumerable.LE, f.succMany?_toFun, Option.map_eq_some_iff] + refine ⟨fun ⟨n, hn⟩ => ⟨n, b, by simp [hn]⟩, fun ⟨n, c, hn⟩ => ⟨n, ?_⟩⟩ + rw [hn.1, Option.some_inj, f.injective hn.2] + +theorem lt_iff (f : Map α β) {a b : α} : + UpwardEnumerable.LT a b ↔ UpwardEnumerable.LT (f.toFun a) (f.toFun b) := by + simp only [UpwardEnumerable.LT, f.succMany?_toFun, Option.map_eq_some_iff] + refine ⟨fun ⟨n, hn⟩ => ⟨n, b, by simp [hn]⟩, fun ⟨n, c, hn⟩ => ⟨n, ?_⟩⟩ + rw [hn.1, Option.some_inj, f.injective hn.2] + +theorem succ?_toFun' (f : Map α β) : succ? ∘ f.toFun = Option.map f.toFun ∘ succ? := by + ext + simp [f.succ?_toFun] + +/-- Compatibility class for `Map` and `≤`. -/ +class PreservesLE [LE α] [LE β] (f : Map α β) where + le_iff : a ≤ b ↔ f.toFun a ≤ f.toFun b + +/-- Compatibility class for `Map` and `<`. -/ +class PreservesLT [LT α] [LT β] (f : Map α β) where + lt_iff : a < b ↔ f.toFun a < f.toFun b + +/-- Compatibility class for `Map` and `Rxc.HasSize`. -/ +class PreservesRxcSize [Rxc.HasSize α] [Rxc.HasSize β] (f : Map α β) where + size_eq : Rxc.HasSize.size a b = Rxc.HasSize.size (f.toFun a) (f.toFun b) + +/-- Compatibility class for `Map` and `Rxo.HasSize`. -/ +class PreservesRxoSize [Rxo.HasSize α] [Rxo.HasSize β] (f : Map α β) where + size_eq : Rxo.HasSize.size a b = Rxo.HasSize.size (f.toFun a) (f.toFun b) + +/-- Compatibility class for `Map` and `Rxi.HasSize`. -/ +class PreservesRxiSize [Rxi.HasSize α] [Rxi.HasSize β] (f : Map α β) where + size_eq : Rxi.HasSize.size b = Rxi.HasSize.size (f.toFun b) + +/-- Compatibility class for `Map` and `Least?`. -/ +class PreservesLeast? [Least? α] [Least? β] (f : Map α β) where + map_least? : Least?.least?.map f.toFun = Least?.least? + +end UpwardEnumerable.Map + +open UpwardEnumerable + +variable [UpwardEnumerable α] [UpwardEnumerable β] + +theorem LawfulUpwardEnumerable.ofMap [LawfulUpwardEnumerable β] (f : Map α β) : + LawfulUpwardEnumerable α where + ne_of_lt a b := by + simpa only [f.lt_iff, ← f.injective.ne_iff] using LawfulUpwardEnumerable.ne_of_lt _ _ + succMany?_zero a := by + apply Option.map_injective f.injective + simpa [← f.succMany?_toFun] using LawfulUpwardEnumerable.succMany?_zero _ + succMany?_add_one n a := by + apply Option.map_injective f.injective + rw [← f.succMany?_toFun, LawfulUpwardEnumerable.succMany?_add_one, + f.succMany?_toFun, Option.bind_map, Map.succ?_toFun', Option.map_bind] + +instance [LE α] [LT α] [LawfulOrderLT α] [LE β] [LT β] [LawfulOrderLT β] (f : Map α β) + [f.PreservesLE] : f.PreservesLT where + lt_iff := by simp [lt_iff_le_and_not_ge, Map.PreservesLE.le_iff (f := f)] + +theorem LawfulUpwardEnumerableLE.ofMap [LE α] [LE β] [LawfulUpwardEnumerableLE β] (f : Map α β) + [f.PreservesLE] : LawfulUpwardEnumerableLE α where + le_iff := by simp [Map.PreservesLE.le_iff (f := f), f.le_iff, LawfulUpwardEnumerableLE.le_iff] + +theorem LawfulUpwardEnumerableLT.ofMap [LT α] [LT β] [LawfulUpwardEnumerableLT β] (f : Map α β) + [f.PreservesLT] : LawfulUpwardEnumerableLT α where + lt_iff := by simp [Map.PreservesLT.lt_iff (f := f), f.lt_iff, LawfulUpwardEnumerableLT.lt_iff] + +theorem LawfulUpwardEnumerableLeast?.ofMap [Least? α] [Least? β] [LawfulUpwardEnumerableLeast? β] + (f : Map α β) [f.PreservesLeast?] : LawfulUpwardEnumerableLeast? α where + least?_le a := by + obtain ⟨l, hl, hl'⟩ := LawfulUpwardEnumerableLeast?.least?_le (f.toFun a) + have : (Least?.least? (α := α)).isSome := by + rw [← Option.isSome_map (f := f.toFun), Map.PreservesLeast?.map_least?, + hl, Option.isSome_some] + refine ⟨Option.get _ this, by simp, ?_⟩ + rw [f.le_iff, Option.apply_get (f := f.toFun)] + simpa [Map.PreservesLeast?.map_least?, hl] using hl' + +end PRange + +open PRange PRange.UpwardEnumerable + +variable [UpwardEnumerable α] [UpwardEnumerable β] + +theorem Rxc.LawfulHasSize.ofMap [LE α] [LE β] [Rxc.HasSize α] [Rxc.HasSize β] [Rxc.LawfulHasSize β] + (f : Map α β) [f.PreservesLE] [f.PreservesRxcSize] : Rxc.LawfulHasSize α where + size_eq_zero_of_not_le a b := by + simpa [Map.PreservesRxcSize.size_eq (f := f), Map.PreservesLE.le_iff (f := f)] using + Rxc.LawfulHasSize.size_eq_zero_of_not_le _ _ + size_eq_one_of_succ?_eq_none lo hi := by + simpa [Map.PreservesRxcSize.size_eq (f := f), Map.PreservesLE.le_iff (f := f), + f.succ?_eq_none_iff] using + Rxc.LawfulHasSize.size_eq_one_of_succ?_eq_none _ _ + size_eq_succ_of_succ?_eq_some lo hi lo' := by + simpa [Map.PreservesRxcSize.size_eq (f := f), Map.PreservesLE.le_iff (f := f), + f.succ?_eq_some_iff] using + Rxc.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _ _ + +theorem Rxo.LawfulHasSize.ofMap [LT α] [LT β] [Rxo.HasSize α] [Rxo.HasSize β] [Rxo.LawfulHasSize β] + (f : Map α β) [f.PreservesLT] [f.PreservesRxoSize] : Rxo.LawfulHasSize α where + size_eq_zero_of_not_le a b := by + simpa [Map.PreservesRxoSize.size_eq (f := f), Map.PreservesLT.lt_iff (f := f)] using + Rxo.LawfulHasSize.size_eq_zero_of_not_le _ _ + size_eq_one_of_succ?_eq_none lo hi := by + simpa [Map.PreservesRxoSize.size_eq (f := f), Map.PreservesLT.lt_iff (f := f), + f.succ?_eq_none_iff] using + Rxo.LawfulHasSize.size_eq_one_of_succ?_eq_none _ _ + size_eq_succ_of_succ?_eq_some lo hi lo' := by + simpa [Map.PreservesRxoSize.size_eq (f := f), Map.PreservesLT.lt_iff (f := f), + f.succ?_eq_some_iff] using + Rxo.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _ _ + +theorem Rxi.LawfulHasSize.ofMap [Rxi.HasSize α] [Rxi.HasSize β] [Rxi.LawfulHasSize β] + (f : Map α β) [f.PreservesRxiSize] : Rxi.LawfulHasSize α where + size_eq_one_of_succ?_eq_none lo := by + simpa [Map.PreservesRxiSize.size_eq (f := f), f.succ?_eq_none_iff] using + Rxi.LawfulHasSize.size_eq_one_of_succ?_eq_none _ + size_eq_succ_of_succ?_eq_some lo lo' := by + simpa [Map.PreservesRxiSize.size_eq (f := f), f.succ?_eq_some_iff] using + Rxi.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _ + +theorem Rxc.IsAlwaysFinite.ofMap [LE α] [LE β] [Rxc.IsAlwaysFinite β] (f : Map α β) + [f.PreservesLE] : Rxc.IsAlwaysFinite α where + finite init hi := by + obtain ⟨n, hn⟩ := Rxc.IsAlwaysFinite.finite (f.toFun init) (f.toFun hi) + exact ⟨n, by simpa [f.succMany?_toFun, Map.PreservesLE.le_iff (f := f)] using hn⟩ + +theorem Rxo.IsAlwaysFinite.ofMap [LT α] [LT β] [Rxo.IsAlwaysFinite β] (f : Map α β) + [f.PreservesLT] : Rxo.IsAlwaysFinite α where + finite init hi := by + obtain ⟨n, hn⟩ := Rxo.IsAlwaysFinite.finite (f.toFun init) (f.toFun hi) + exact ⟨n, by simpa [f.succMany?_toFun, Map.PreservesLT.lt_iff (f := f)] using hn⟩ + +theorem Rxi.IsAlwaysFinite.ofMap [Rxi.IsAlwaysFinite β] (f : Map α β) : Rxi.IsAlwaysFinite α where + finite init := by + obtain ⟨n, hn⟩ := Rxi.IsAlwaysFinite.finite (f.toFun init) + exact ⟨n, by simpa [f.succMany?_toFun] using hn⟩ + +end Std diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index b5e2a91bf0..7c8d2a8b75 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -2810,6 +2810,8 @@ structure Char where /-- The value must be a legal scalar value. -/ valid : val.isValidChar +grind_pattern Char.valid => self.val + private theorem isValidChar_UInt32 {n : Nat} (h : n.isValidChar) : LT.lt n UInt32.size := match h with | Or.inl h => Nat.lt_trans h (of_decide_eq_true rfl) diff --git a/tests/lean/run/charrange.lean b/tests/lean/run/charrange.lean new file mode 100644 index 0000000000..e9a2ce4b95 --- /dev/null +++ b/tests/lean/run/charrange.lean @@ -0,0 +1,29 @@ +module + +def s₁ : String := Id.run do + let mut ans := "" + for c in 'a'...='z' do + ans := ans.push c + return ans + +/-- info: "abcdefghijklmnopqrstuvwxyz" -/ +#guard_msgs in +#eval s₁ + +def s₂ : String := Id.run do + let mut ans := "" + for c in 'a'...'z' do + ans := ans.push c + return ans + +/-- info: "abcdefghijklmnopqrstuvwxy" -/ +#guard_msgs in +#eval s₂ + +/-- info: 122 -/ +#guard_msgs in +#eval (*...'z').size + +/-- info: 1112064 -/ +#guard_msgs in +#eval (*...* : Std.Rii Char).size