From 84122012fb01e6470bafc23cf0b486ba03068b22 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Mon, 23 Sep 2024 01:56:51 -0400 Subject: [PATCH 01/31] feat: add Data.Fin.Coding and Data.Fin.Enum --- Batteries/Data/Fin.lean | 2 + Batteries/Data/Fin/Basic.lean | 40 +++ Batteries/Data/Fin/Coding.lean | 497 +++++++++++++++++++++++++++++++++ Batteries/Data/Fin/Enum.lean | 188 +++++++++++++ Batteries/Data/Fin/Lemmas.lean | 106 +++++++ 5 files changed, 833 insertions(+) create mode 100644 Batteries/Data/Fin/Coding.lean create mode 100644 Batteries/Data/Fin/Enum.lean diff --git a/Batteries/Data/Fin.lean b/Batteries/Data/Fin.lean index 5fe5cc41ca..67c5fdb14a 100644 --- a/Batteries/Data/Fin.lean +++ b/Batteries/Data/Fin.lean @@ -1,2 +1,4 @@ import Batteries.Data.Fin.Basic +import Batteries.Data.Fin.Coding +import Batteries.Data.Fin.Enum import Batteries.Data.Fin.Lemmas diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean index b61481e33a..8438128674 100644 --- a/Batteries/Data/Fin/Basic.lean +++ b/Batteries/Data/Fin/Basic.lean @@ -68,3 +68,43 @@ Fin.foldrM n f xₙ = do loop : {i // i ≤ n} → α → m α | ⟨0, _⟩, x => pure x | ⟨i+1, h⟩, x => f ⟨i, h⟩ x >>= loop ⟨i, Nat.le_of_lt h⟩ + +/-- Sum of a list indexed by `Fin n`. -/ +protected def sum [OfNat α (nat_lit 0)] [Add α] (x : Fin n → α) : α := + foldr n (x · + ·) 0 + +/-- Product of a list indexed by `Fin n`. -/ +protected def prod [OfNat α (nat_lit 1)] [Mul α] (x : Fin n → α) : α := + foldr n (x · * ·) 1 + +/-- Count the number of true values of a decidable predicate on `Fin n`. -/ +protected def count (P : Fin n → Prop) [DecidablePred P] : Nat := + Fin.sum (if P · then 1 else 0) + +/-- Find the first true value of a decidable predicate on `Fin n`, if there is one. -/ +protected def find? (P : Fin n → Prop) [inst : DecidablePred P] : Option (Fin n) := + match n, P, inst with + | 0, _, _ => none + | _+1, P, _ => + if P 0 then + some 0 + else + match Fin.find? fun i => P i.succ with + | some i => some i.succ + | none => none + +/-- Custom recursor for `Fin (n+1)`. -/ +def recZeroSuccOn {motive : Fin (n+1) → Sort _} (x : Fin (n+1)) + (zero : motive 0) (succ : (x : Fin n) → motive x.castSucc → motive x.succ) : motive x := + match x with + | 0 => zero + | ⟨x+1, hx⟩ => + let x : Fin n := ⟨x, Nat.lt_of_succ_lt_succ hx⟩ + succ x <| recZeroSuccOn x.castSucc zero succ + +/-- Custom recursor for `Fin (n+1)`. -/ +def casesZeroSuccOn {motive : Fin (n+1) → Sort _} (x : Fin (n+1)) + (zero : motive 0) (succ : (x : Fin n) → motive x.succ) : motive x := + match x with + | 0 => zero + | ⟨x+1, hx⟩ => succ ⟨x, Nat.lt_of_succ_lt_succ hx⟩ diff --git a/Batteries/Data/Fin/Coding.lean b/Batteries/Data/Fin/Coding.lean new file mode 100644 index 0000000000..5cc54ac0e6 --- /dev/null +++ b/Batteries/Data/Fin/Coding.lean @@ -0,0 +1,497 @@ +/- +Copyright (c) 2024 François G. Dorais. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: François G. Dorais +-/ +import Batteries.Data.Fin.Lemmas +import Batteries.Tactic.Basic +import Batteries.Tactic.Trans +import Batteries.Tactic.Lint + +namespace Fin + +/-- Encode a unit value as a `Fin` type. -/ +@[nolint unusedArguments] +def encodePUnit : PUnit → Fin 1 + | .unit => 0 + +/-- Decode a unit value as a `Fin` type. -/ +@[pp_nodot] def decodePUnit : Fin 1 → PUnit + | 0 => .unit + +/-- Encode a unit value as a `Fin` type. -/ +abbrev encodeUnit : Unit → Fin 1 := encodePUnit + +/-- Decode a unit value as a `Fin` type. -/ +@[pp_nodot] abbrev decodeUnit : Fin 1 → Unit := decodePUnit + +@[simp] theorem encodePUnit_decodePUnit : (x : Fin 1) → encodePUnit (decodePUnit x) = x + | 0 => rfl + +@[simp] theorem decodePUnit_encodePUnit : (x : PUnit) → decodePUnit (encodePUnit x) = x + | .unit => rfl + +/-- Encode a boolean value as a `Fin` type. -/ +def encodeBool : Bool → Fin 2 + | false => 0 + | true => 1 + +/-- Decode a boolean value as a `Fin` type. -/ +@[pp_nodot] def decodeBool : Fin 2 → Bool + | 0 => false + | 1 => true + +@[simp] theorem encodeBool_decodeBool : (x : Fin 2) → encodeBool (decodeBool x) = x + | 0 => rfl + | 1 => rfl + +@[simp] theorem decodeBool_encodeBool : (x : Bool) → decodeBool (encodeBool x) = x + | false => rfl + | true => rfl + +/-- Decode an optional `Fin` types. -/ +def encodeOption : Option (Fin n) → Fin (n+1) + | none => 0 + | some x => x.succ + +/-- Decode an optional `Fin` types. -/ +@[pp_nodot] def decodeOption (x : Fin (n+1)) : Option (Fin n) := + if h : x = 0 then + none + else + some (x.pred h) + +@[simp] theorem encodeOption_decodeOption (x : Fin (n+1)) : encodeOption (decodeOption x) = x := by + simp only [encodeOption, decodeOption] + split + · next hd => + split at hd + · next he => cases he; rfl + · contradiction + · next hd => + split at hd + · contradiction + · next he => cases hd; simp + +@[simp] theorem decodeOption_encodeOption (x : Option (Fin n)) : + decodeOption (encodeOption x) = x := by + simp only [encodeOption, decodeOption] + split + · next he => + split at he + · rfl + · simp only [Fin.succ] at he; cases he + · next he => + split at he + · simp at he + · rfl + +/-- Encode a sum of `Fin` types. -/ +def encodeSum : Sum (Fin n) (Fin m) → Fin (n + m) + | .inl x => x.castLE (Nat.le_add_right _ _) + | .inr x => x.natAdd n + +/-- Decode a sum of `Fin` types. -/ +@[pp_nodot] def decodeSum (x : Fin (n + m)) : Sum (Fin n) (Fin m) := + if h : x < n then + .inl ⟨x, h⟩ + else + .inr ⟨x - n, by omega⟩ + +@[simp] theorem encodeSum_decodeSum (x : Fin (n + m)) : encodeSum (decodeSum x) = x := by + simp only [encodeSum, decodeSum] + split + · next hd => + split at hd + · cases hd; rfl + · contradiction + · next hd => + split at hd + · contradiction + · next he => + cases x; cases hd + simp at he ⊢; omega + +@[simp] theorem decodeSum_encodeSum (x : Sum (Fin n) (Fin m)) : decodeSum (encodeSum x) = x := by + simp only [encodeSum, decodeSum] + split + · next hd => + split + · simp + · simp at hd; omega + · next hd => + split + · simp at hd + · next x => + cases x + simp; omega + +/-- Encode a product of `Fin` types. -/ +def encodeProd : Fin m × Fin n → Fin (m * n) + | (⟨i, hi⟩, ⟨j, hj⟩) => Fin.mk (n * i + j) <| calc + _ < n * i + n := Nat.add_lt_add_left hj .. + _ = n * (i + 1) := Nat.mul_succ .. + _ ≤ n * m := Nat.mul_le_mul_left n (Nat.succ_le_of_lt hi) + _ = m * n := Nat.mul_comm .. + +/-- Decode a product of `Fin` types. -/ +@[pp_nodot] def decodeProd (z : Fin (m * n)) : Fin m × Fin n := + ⟨left, right⟩ +where + hn : 0 < n := by + apply Nat.zero_lt_of_ne_zero + intro h + absurd z.is_lt + simp [h] + /-- Left case of `decodeProd`. -/ + left := ⟨z / n, by rw [Nat.div_lt_iff_lt_mul hn]; exact z.is_lt⟩ + /-- Right case of `decodeProd`. -/ + right := ⟨z % n, Nat.mod_lt _ hn⟩ + +@[simp] theorem encodeProd_decodeProd (x : Fin (m * n)) : encodeProd (decodeProd x) = x := by + simp [encodeProd, decodeProd, decodeProd.left, decodeProd.right, Nat.div_add_mod] + +@[simp] theorem decodeProd_encodeProd (x : Fin m × Fin n) : decodeProd (encodeProd x) = x := by + match x with + | ⟨⟨_, _⟩, ⟨_, h⟩⟩ => simp [encodeProd, decodeProd, decodeProd.left, decodeProd.right, + Nat.mul_add_div (Nat.zero_lt_of_lt h), Nat.div_eq_of_lt h, Nat.mul_add_mod, Nat.mod_eq_of_lt h] + +/-- Encode a dependent sum of `Fin` types. -/ +def encodeSigma (f : Fin n → Nat) (x : (i : Fin n) × Fin (f i)) : Fin (Fin.sum f) := + match n, f, x with + | _+1, _, ⟨⟨0, _⟩, ⟨j, hj⟩⟩ => + ⟨j, Nat.lt_of_lt_of_le hj (sum_succ .. ▸ Nat.le_add_right ..)⟩ + | _+1, f, ⟨⟨i+1, hi⟩, ⟨j, hj⟩⟩ => + match encodeSigma ((f ∘ succ)) ⟨⟨i, Nat.lt_of_succ_lt_succ hi⟩, ⟨j, hj⟩⟩ with + | ⟨k, hk⟩ => ⟨f 0 + k, sum_succ .. ▸ Nat.add_lt_add_left hk ..⟩ + +/-- Decode a dependent sum of `Fin` types. -/ +@[pp_nodot] def decodeSigma (f : Fin n → Nat) (x : Fin (Fin.sum f)) : (i : Fin n) × Fin (f i) := + match n, f, x with + | 0, _, ⟨_, h⟩ => False.elim (by simp at h) + | n+1, f, ⟨x, hx⟩ => + if hx0 : x < f 0 then + ⟨0, ⟨x, hx0⟩⟩ + else + have hxf : x - f 0 < Fin.sum (f ∘ succ) := by + apply Nat.sub_lt_left_of_lt_add + · exact Nat.le_of_not_gt hx0 + · rw [← sum_succ]; exact hx + match decodeSigma ((f ∘ succ)) ⟨x - f 0, hxf⟩ with + | ⟨⟨i, hi⟩, y⟩ => ⟨⟨i+1, Nat.succ_lt_succ hi⟩, y⟩ + +@[simp] theorem encodeSigma_decodeSigma (f : Fin n → Nat) (x : Fin (Fin.sum f)) : + encodeSigma f (decodeSigma f x) = x := by + induction n with + | zero => absurd x.is_lt; simp + | succ n ih => + simp only [decodeSigma] + split + · simp [encodeSigma] + · next h1 => + have h2 : x - f 0 < Fin.sum (f ∘ succ) := by + apply Nat.sub_lt_left_of_lt_add + · exact Nat.le_of_not_gt h1 + · rw [← sum_succ]; exact x.is_lt + have : encodeSigma (f ∘ succ) (decodeSigma (f ∘ succ) ⟨x - f 0, h2⟩) = ↑x - f 0 := by + rw [ih] + ext; simp only [encodeSigma] + conv => rhs; rw [← Nat.add_sub_of_le (Nat.le_of_not_gt h1)] + congr + +@[simp] theorem decodeSigma_encodeSigma (f : Fin n → Nat) (x : (i : Fin n) × Fin (f i)) : + decodeSigma f (encodeSigma f x) = x := by + induction n with + | zero => nomatch x + | succ n ih => + simp only [decodeSigma] + match x with + | ⟨0, x⟩ => simp [encodeSigma] + | ⟨⟨i+1, hi⟩, ⟨x, hx⟩⟩ => + have : ¬ encodeSigma f ⟨⟨i+1, hi⟩, ⟨x, hx⟩⟩ < f 0 := by simp [encodeSigma] + rw [dif_neg this] + have : (encodeSigma f ⟨⟨i+1, hi⟩, ⟨x, hx⟩⟩).1 - f 0 = + (encodeSigma (f ∘ Fin.succ) ⟨⟨i, Nat.lt_of_succ_lt_succ hi⟩, ⟨x, hx⟩⟩).1 := by + simp [encodeSigma, Nat.add_sub_cancel_left] + have h := ih (f ∘ Fin.succ) ⟨⟨i, Nat.lt_of_succ_lt_succ hi⟩, ⟨x, hx⟩⟩ + simp [Sigma.ext_iff, Fin.ext_iff] at h ⊢ + constructor + · conv => rhs; rw [← h.1] + apply congrArg + apply congrArg Sigma.fst + congr + · apply HEq.trans _ h.2; congr + +/-- Encode a function between `Fin` types. -/ +def encodeFun : {m : Nat} → (Fin m → Fin n) → Fin (n ^ m) + | 0, _ => ⟨0, by simp⟩ + | m+1, f => Fin.mk (n * (encodeFun fun k => f k.succ).val + (f 0).val) <| calc + _ < n * (encodeFun fun k => f k.succ).val + n := Nat.add_lt_add_left (f 0).isLt _ + _ = n * ((encodeFun fun k => f k.succ).val + 1) := Nat.mul_succ .. + _ ≤ n * n ^ m := Nat.mul_le_mul_left n (Nat.succ_le_of_lt (encodeFun fun k => f k.succ).isLt) + _ = n ^ m * n := Nat.mul_comm .. + _ = n ^ (m+1) := Nat.pow_succ .. + +/-- Decode a function between `Fin` types. -/ +@[pp_nodot] def decodeFun : {m : Nat} → Fin (n ^ m) → Fin m → Fin n + | 0, _ => (nomatch .) + | m+1, ⟨k, hk⟩ => + have hn : n > 0 := by + apply Nat.zero_lt_of_ne_zero + intro h + rw [h, Nat.pow_succ, Nat.mul_zero] at hk + contradiction + fun + | 0 => ⟨k % n, Nat.mod_lt k hn⟩ + | ⟨i+1, hi⟩ => + have h : k / n < n ^ m := by rw [Nat.div_lt_iff_lt_mul hn]; exact hk + decodeFun ⟨k / n, h⟩ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ + +@[simp] theorem encodeFun_decodeFun (x : Fin (n ^ m)) : encodeFun (decodeFun x) = x := by + induction m with simp only [encodeFun, decodeFun, Fin.succ] + | zero => simp; omega + | succ m ih => cases x; simp [ih]; rw [← Fin.zero_eta, Nat.div_add_mod] + +@[simp] theorem decodeFun_encodeFun (x : Fin m → Fin n) : decodeFun (encodeFun x) = x := by + funext i; induction m with simp only [encodeFun, decodeFun] + | zero => nomatch i + | succ m ih => + have hn : 0 < n := Nat.zero_lt_of_lt (x 0).is_lt + split + · ext; simp [Nat.mul_add_mod, Nat.mod_eq_of_lt] + · next i hi => + have : decodeFun (encodeFun fun k => x k.succ) ⟨i, Nat.lt_of_succ_lt_succ hi⟩ + = x ⟨i+1, hi⟩ := by rw [ih]; rfl + simp [← this, Nat.mul_add_div hn, Nat.div_eq_of_lt] + +/-- Encode a dependent product of `Fin` types. -/ +def encodePi (f : Fin n → Nat) (x : (i : Fin n) → Fin (f i)) : Fin (Fin.prod f) := + match n, f, x with + | 0, _, _ => ⟨0, by simp [Fin.prod]⟩ + | _+1, f, x => + match encodePi ((f ∘ succ)) (fun ⟨i, hi⟩ => x ⟨i+1, Nat.succ_lt_succ hi⟩) with + | ⟨k, hk⟩ => Fin.mk (f 0 * k + (x 0).val) $ calc + _ < f 0 * k + f 0 := Nat.add_lt_add_left (x 0).isLt .. + _ = f 0 * (k + 1) := Nat.mul_succ .. + _ ≤ f 0 * Fin.prod (f ∘ succ) := Nat.mul_le_mul_left _ (Nat.succ_le_of_lt hk) + _ = Fin.prod f := Eq.symm <| prod_succ .. + +/-- Decode a dependent product of `Fin` types. -/ +def decodePi (f : Fin n → Nat) (x : Fin (Fin.prod f)) : (i : Fin n) → Fin (f i) := + match n, f, x with + | 0, _, _ => (nomatch ·) + | n+1, f, ⟨x, hx⟩ => + have h : f 0 > 0 := by + apply Nat.zero_lt_of_ne_zero + intro h + rw [prod_succ, h, Nat.zero_mul] at hx + contradiction + have : x / f 0 < Fin.prod (f ∘ succ) := by + rw [Nat.div_lt_iff_lt_mul h, Nat.mul_comm, ← prod_succ] + exact hx + match decodePi ((f ∘ succ)) ⟨x / f 0, this⟩ with + | t => fun + | ⟨0, _⟩ => ⟨x % f 0, Nat.mod_lt x h⟩ + | ⟨i+1, hi⟩ => t ⟨i, Nat.lt_of_succ_lt_succ hi⟩ + +@[simp] theorem encodePi_decodePi (f : Fin n → Nat) (x : Fin (Fin.prod f)) : + encodePi f (decodePi f x) = x := by + induction n with + | zero => + match x with + | ⟨0, _⟩ => rfl + | ⟨_+1, h⟩ => simp at h + | succ n ih => + simp only [encodePi, decodePi, ih] + ext + conv => rhs; rw [← Nat.div_add_mod x (f 0)] + congr + +@[simp] theorem decodePi_encodePi (f : Fin n → Nat) (x : (i : Fin n) → Fin (f i)) : + decodePi f (encodePi f x) = x := by + induction n with + | zero => funext i; nomatch i + | succ n ih => + have h0 : 0 < f 0 := Nat.zero_lt_of_lt (x 0).is_lt + funext i + simp only [decodePi] + split + · simp [Nat.mul_add_mod, Nat.mod_eq_of_lt (x 0).is_lt] + · next i hi => + have h : decodePi (f ∘ succ) (encodePi (f ∘ succ) fun i => x i.succ) + ⟨i, Nat.lt_of_succ_lt_succ hi⟩ = x ⟨i+1, hi⟩ := by rw [ih]; rfl + conv => rhs; rw [← h] + congr; simp [Nat.mul_add_div h0, Nat.div_eq_of_lt (x 0).is_lt]; rfl + +/-- Encode a decidable subtype of a `Fin` type. -/ +def encodeSubtype (P : Fin n → Prop) [inst : DecidablePred P] (i : { i // P i }) : + Fin (Fin.count P) := + match n, P, inst, i with + | n+1, P, inst, ⟨0, hp⟩ => + have : Fin.count P > 0 := by simp [count_succ, hp] + ⟨0, this⟩ + | n+1, P, inst, ⟨⟨i+1, hi⟩, hp⟩ => + match encodeSubtype (fun i => P i.succ) ⟨⟨i, Nat.lt_of_succ_lt_succ hi⟩, hp⟩ with + | ⟨k, hk⟩ => + if h0 : P 0 then + have : Fin.count P = (Fin.count fun i => P i.succ) + 1 := by + simp_arith only [count_succ, Function.comp_def, if_pos h0] + this ▸ ⟨k+1, Nat.succ_lt_succ hk⟩ + else + have : Fin.count P = Fin.count fun i => P i.succ := by simp [count_succ, h0] + this ▸ ⟨k, hk⟩ + +/-- Decode a decidable subtype of a `Fin` type. -/ +def decodeSubtype (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (Fin.count p)) : + { i // p i } := + match n, p, inst, k with + | 0, _, _, ⟨_, h⟩ => False.elim (by simp at h) + | n+1, p, inst, ⟨k, hk⟩ => + if h0 : p 0 then + have : Fin.count p = (Fin.count fun i => p i.succ) + 1 := by simp [count_succ, h0] + match k with + | 0 => ⟨0, h0⟩ + | k + 1 => + match decodeSubtype (fun i => p i.succ) ⟨k, Nat.lt_of_add_lt_add_right (this ▸ hk)⟩ with + | ⟨⟨i, hi⟩, hp⟩ => ⟨⟨i+1, Nat.succ_lt_succ hi⟩, hp⟩ + else + have : Fin.count p = Fin.count fun i => p i.succ := by simp [count_succ, h0] + match decodeSubtype (fun i => p (succ i)) ⟨k, this ▸ hk⟩ with + | ⟨⟨i, hi⟩, hp⟩ => ⟨⟨i+1, Nat.succ_lt_succ hi⟩, hp⟩ + +@[simp] theorem encodeSubtype_decodeSubtype (P : Fin n → Prop) [DecidablePred P] + (x : Fin (Fin.count P)) : encodeSubtype P (decodeSubtype P x) = x := by + induction n with + | zero => absurd x.is_lt; simp + | succ n ih => + simp only [decodeSubtype] + split + · ext; split <;> simp [encodeSubtype, count_succ, *] + · ext; simp [encodeSubtype, count_succ, *] + +theorem encodeSubtype_zero_pos {P : Fin (n+1) → Prop} [DecidablePred P] (h₀ : P 0) : + encodeSubtype P ⟨0, h₀⟩ = ⟨0, by simp [count_succ, *]⟩ := by + ext; simp [encodeSubtype] + +theorem encodeSubtype_succ_pos {P : Fin (n+1) → Prop} [DecidablePred P] (h₀ : P 0) {i : Fin n} + (h : P i.succ) : encodeSubtype P ⟨i.succ, h⟩ = + (encodeSubtype (fun i => P i.succ) ⟨i, h⟩).succ.cast (by simp [count_succ, *]) := by + ext; simp [encodeSubtype, count_succ, *] + +theorem encodeSubtype_succ_neg {P : Fin (n+1) → Prop} [DecidablePred P] (h₀ : ¬ P 0) {i : Fin n} + (h : P i.succ) : encodeSubtype P ⟨i.succ, h⟩ = + (encodeSubtype (fun i => P i.succ) ⟨i, h⟩).cast (by simp [count_succ, *]) := by + ext; simp [encodeSubtype, count_succ, *] + +@[simp] theorem decodeSubtype_encodeSubtype (P : Fin n → Prop) [DecidablePred P] (x : { x // P x}) : + decodeSubtype P (encodeSubtype P x) = x := by + match x with + | ⟨i, h⟩ => + induction n with + | zero => absurd x.val.is_lt; simp + | succ n ih => + if h₀ : P 0 then + simp only [decodeSubtype, dif_pos h₀] + cases i using Fin.casesZeroSuccOn with + | zero => rw [encodeSubtype_zero_pos h₀] + | succ i => + rw [encodeSubtype_succ_pos h₀] + simp only [coe_cast, val_succ, Subtype.mk.injEq] + congr + rw [ih (fun i => P i.succ) ⟨i, h⟩] + else + simp only [decodeSubtype, dif_neg h₀] + cases i using Fin.casesZeroSuccOn with + | zero => contradiction + | succ i => + rw [encodeSubtype_succ_neg h₀] + simp only [coe_cast, Subtype.mk.injEq] + congr + rw [ih (fun i => P i.succ) ⟨i, h⟩] + +/-- Get representative for the equivalence class of `x`. -/ +abbrev getRepr (s : Setoid (Fin n)) [DecidableRel s.r] (x : Fin n) : Fin n := + match h : Fin.find? (s.r x) with + | some y => y + | none => False.elim <| by + have : Fin.find? (s.r x) |>.isSome := by + rw [find?_isSome_iff_exists] + exists x + exact Setoid.refl x + simp [h] at this + +@[simp] theorem equiv_getRepr (s : Setoid (Fin n)) [DecidableRel s.r] (x : Fin n) : + s.r x (getRepr s x) := by + apply find?_prop + simp only [getRepr] + split + · assumption + · next h => + have : Fin.find? (s.r x) |>.isSome := by + rw [find?_isSome_iff_exists] + exists x + exact Setoid.refl x + simp [h] at this + +@[simp] theorem getRepr_equiv (s : Setoid (Fin n)) [DecidableRel s.r] (x : Fin n) : + s.r (getRepr s x) x := Setoid.symm (equiv_getRepr ..) + +theorem getRepr_eq_getRepr_of_equiv (s : Setoid (Fin n)) [DecidableRel s.r] (h : s.r x y) : + getRepr s x = getRepr s y := by + have hfind : Fin.find? (s.r x) = Fin.find? (s.r y) := by + congr + funext z + apply propext + constructor + · exact Setoid.trans (Setoid.symm h) + · exact Setoid.trans h + simp only [getRepr] + split + · next hx => + rw [hfind] at hx + split + · next hy => + rwa [hx, Option.some_inj] at hy + · next hy => + rw [hx] at hy + contradiction + · next hx => + rw [hfind] at hx + split + · next hy => + rw [hx] at hy + contradiction + · rfl + +@[simp] theorem getRepr_getRepr (s : Setoid (Fin n)) [DecidableRel s.r] (x : Fin n) : + getRepr s (getRepr s x) = getRepr s x := by + apply getRepr_eq_getRepr_of_equiv + exact getRepr_equiv .. + +/-- Encode decidable quotient of a `Fin` type. -/ +def encodeQuotient (s : Setoid (Fin n)) [DecidableRel s.r] (x : Quotient s) : + Fin (Fin.count fun i => getRepr s i = i) := + encodeSubtype _ <| Quotient.liftOn x (fun i => ⟨getRepr s i, getRepr_getRepr s i⟩) <| by + intro _ _ h + simp only [Subtype.mk.injEq] + exact getRepr_eq_getRepr_of_equiv s h + +/-- Decode decidable quotient of a `Fin ` type. -/ +def decodeQuotient (s : Setoid (Fin n)) [DecidableRel s.r] + (i : Fin (Fin.count fun i => getRepr s i = i)) : Quotient s := + Quotient.mk s (decodeSubtype _ i) + +@[simp] theorem encodeQuotient_decodeQuotient (s : Setoid (Fin n)) [DecidableRel s.r] (x) : + encodeQuotient s (decodeQuotient s x) = x := by + simp only [decodeQuotient, encodeQuotient, Quotient.liftOn, Quotient.mk, Quot.liftOn] + conv => rhs; rw [← encodeSubtype_decodeSubtype _ x] + congr + exact (decodeSubtype _ x).property + +@[simp] theorem decodeQuotient_encodeQuotient (s : Setoid (Fin n)) [DecidableRel s.r] (x) : + decodeQuotient s (encodeQuotient s x) = x := by + induction x using Quotient.inductionOn with + | _ x => + simp only [decodeQuotient, encodeQuotient, Quotient.liftOn, Quotient.mk, Quot.liftOn] + apply Quot.sound + simp diff --git a/Batteries/Data/Fin/Enum.lean b/Batteries/Data/Fin/Enum.lean new file mode 100644 index 0000000000..93a73516da --- /dev/null +++ b/Batteries/Data/Fin/Enum.lean @@ -0,0 +1,188 @@ +/- +Copyright (c) 2024 François G. Dorais. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: François G. Dorais +-/ +import Batteries.Data.Fin.Coding + +namespace Fin + +/-- Class of types that are in bijection with a `Fin` type. -/ +protected class Enum (α : Type _) where + /-- Size of type. -/ + size : Nat + /-- Enumeration of the type elements. -/ + enum : Fin size → α + /-- Find the index of a type element. -/ + find : α → Fin size + /-- Inverse relation for `enum` and `find`. -/ + enum_find (x) : enum (find x) = x + /-- Inverse relation for `enum` and `find`. -/ + find_enum (i) : find (enum i) = i + +attribute [simp] Enum.enum_find Enum.find_enum + +namespace Enum + +instance : Fin.Enum Empty where + size := 0 + enum := nofun + find := nofun + enum_find := nofun + find_enum := nofun + +instance : Fin.Enum PUnit where + size := 1 + enum := decodePUnit + find := encodePUnit + enum_find := decodePUnit_encodePUnit + find_enum := encodePUnit_decodePUnit + +instance : Fin.Enum Bool where + size := 2 + enum := decodeBool + find := encodeBool + enum_find := decodeBool_encodeBool + find_enum := encodeBool_decodeBool + +instance [Fin.Enum α] : Fin.Enum (Option α) where + size := size α + 1 + enum i := decodeOption i |>.map enum + find x := encodeOption <| x.map find + enum_find := by simp [Function.comp_def] + find_enum := by simp [Function.comp_def] + +instance [Fin.Enum α] [Fin.Enum β] : Fin.Enum (α ⊕ β) where + size := size α + size β + enum i := + match decodeSum i with + | .inl i => .inl <| enum i + | .inr i => .inr <| enum i + find x := + match x with + | .inl x => encodeSum <| .inl (find x) + | .inr x => encodeSum <| .inr (find x) + enum_find _ := by + simp only; split + · next h => + split at h; + · simp at h; cases h; simp + · simp at h + · next h => + split at h; + · simp at h + · simp at h; cases h; simp + find_enum _ := by + simp only; split + · next h => + split at h + · next h' => cases h; simp [← h'] + · simp at h + · next h => + split at h + · simp at h + · next h' => cases h; simp [← h'] + +instance [Fin.Enum α] [Fin.Enum β] : Fin.Enum (α × β) where + size := size α * size β + enum i := (enum (decodeProd i).fst, enum (decodeProd i).snd) + find x := encodeProd (find x.fst, find x.snd) + find_enum := by simp [Prod.eta] + enum_find := by simp + +instance [Fin.Enum α] [Fin.Enum β] : Fin.Enum (β → α) where + size := size α ^ size β + enum i x := enum (decodeFun i (find x)) + find f := encodeFun fun x => find (f (enum x)) + find_enum := by simp + enum_find := by simp + +instance (β : α → Type _) [Fin.Enum α] [(x : α) → Fin.Enum (β x)] : Fin.Enum ((x : α) × β x) where + size := Fin.sum fun i => size (β (enum i)) + enum i := + match decodeSigma _ i with + | ⟨i, j⟩ => ⟨enum i, enum j⟩ + find | ⟨x, y⟩ => encodeSigma _ ⟨find x, find (_root_.cast (by simp) y)⟩ + find_enum i := by + simp only [] + conv => rhs; rw [← encodeSigma_decodeSigma _ i] + congr 1 + ext + · simp + · simp only [] + conv => rhs; rw [← find_enum (decodeSigma _ i).snd] + congr <;> simp + enum_find + | ⟨x, y⟩ => by + ext + simp only [cast, decodeSigma_encodeSigma, enum_find] + simp [] + rw [decodeSigma_encodeSigma] + simp + +instance (β : α → Type _) [Fin.Enum α] [(x : α) → Fin.Enum (β x)] : Fin.Enum ((x : α) → β x) where + size := Fin.prod fun i => size (β (enum i)) + enum i x := enum <| (decodePi _ i (find x)).cast (by rw [enum_find]) + find f := encodePi _ fun i => find (f (enum i)) + find_enum i := by + simp only [find_enum] + conv => rhs; rw [← encodePi_decodePi _ i] + congr + ext + simp only [cast] + rw [find_enum] + enum_find f := by + funext x + simp only [] + conv => rhs; rw [← enum_find (f x)] + congr 1 + ext + simp only [cast, decodePi_encodePi] + rw [enum_find] + done + +instance (P : α → Prop) [DecidablePred P] [Fin.Enum α] : Fin.Enum { x // P x} where + size := Fin.count fun i => P (enum i) + enum i := ⟨enum (decodeSubtype _ i).val, (decodeSubtype _ i).property⟩ + find x := encodeSubtype _ ⟨find x.val, (enum_find x.val).symm ▸ x.property⟩ + find_enum i := by simp [Subtype.eta] + enum_find := by simp + +private def enumSetoid (s : Setoid α) [DecidableRel s.r] [Fin.Enum α] : + Setoid (Fin (size α)) where + r i j := s.r (enum i) (enum j) + iseqv := { + refl := fun i => Setoid.refl (enum i) + symm := Setoid.symm + trans := Setoid.trans + } + +private instance (s : Setoid α) [DecidableRel s.r] [Fin.Enum α] : DecidableRel (enumSetoid s).r := + fun _ _ => inferInstanceAs (Decidable (s.r _ _)) + +instance (s : Setoid α) [DecidableRel s.r] [Fin.Enum α] : Fin.Enum (Quotient s) where + size := Fin.count fun i => getRepr (enumSetoid s) i = i + enum i := Quotient.liftOn (decodeQuotient (enumSetoid s) i) (fun i => Quotient.mk s (enum i)) + (fun _ _ h => Quotient.sound h) + find x := Quotient.liftOn x + (fun x => encodeQuotient (enumSetoid s) (Quotient.mk _ (find x))) <| by + intro _ _ h + simp only [] + congr 1 + apply Quotient.sound + simp only [HasEquiv.Equiv, enumSetoid, enum_find] + exact h + enum_find x := by + induction x using Quotient.inductionOn with + | _ x => + simp only [decodeQuotient, encodeQuotient, decodeSubtype_encodeSubtype, Quotient.liftOn, + Quotient.mk, Quot.liftOn] + apply Quot.sound + conv => rhs; rw [← enum_find x] + exact getRepr_equiv (enumSetoid s) .. + find_enum i := by + conv => rhs; rw [← encodeSubtype_decodeSubtype _ i] + simp only [Quotient.liftOn, Quot.liftOn, encodeQuotient, Quotient.mk, decodeQuotient, + find_enum] + congr + rw [(decodeSubtype _ i).property] diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean index 5010e1310f..e2edb35f03 100644 --- a/Batteries/Data/Fin/Lemmas.lean +++ b/Batteries/Data/Fin/Lemmas.lean @@ -5,11 +5,16 @@ Authors: Mario Carneiro -/ import Batteries.Data.Fin.Basic import Batteries.Data.List.Lemmas +import Batteries.Tactic.Lint.Simp namespace Fin attribute [norm_cast] val_last +@[nolint simpNF, simp] +theorem val_ndrec (x : Fin n) (h : m = n) : (h ▸ x).val = x.val := by + cases h; rfl + /-! ### clamp -/ @[simp] theorem coe_clamp (n m : Nat) : (clamp n m : Nat) = min n m := rfl @@ -214,3 +219,104 @@ theorem foldr_rev (f : α → Fin n → α) (x) : induction n generalizing x with | zero => simp | succ n ih => rw [foldl_succ_last, foldr_succ, ← ih]; simp [rev_succ] + +/-! ### sum -/ + +@[simp] theorem sum_zero [OfNat α (nat_lit 0)] [Add α] (x : Fin 0 → α) : + Fin.sum x = 0 := by + simp [Fin.sum] + +theorem sum_succ [OfNat α (nat_lit 0)] [Add α] (x : Fin (n + 1) → α) : + Fin.sum x = x 0 + Fin.sum (x ∘ Fin.succ) := by + simp [Fin.sum, foldr_succ] + +/-! ### prod -/ + +@[simp] theorem prod_zero [OfNat α (nat_lit 1)] [Mul α] (x : Fin 0 → α) : + Fin.prod x = 1 := by + simp [Fin.prod] + +theorem prod_succ [OfNat α (nat_lit 1)] [Mul α] (x : Fin (n + 1) → α) : + Fin.prod x = x 0 * Fin.prod (x ∘ Fin.succ) := by + simp [Fin.prod, foldr_succ] + +/-! ### count -/ + +@[simp] theorem count_zero (P : Fin 0 → Prop) [DecidablePred P] : Fin.count P = 0 := by + simp [Fin.count] + +theorem count_succ (P : Fin (n + 1) → Prop) [DecidablePred P] : Fin.count P = + if P 0 then Fin.count (fun i => P i.succ) + 1 else Fin.count (fun i => P i.succ) := by + split <;> simp [Fin.count, Fin.sum_succ, Nat.one_add, Function.comp_def, *] + +theorem count_le (P : Fin n → Prop) [DecidablePred P] : Fin.count P ≤ n := by + induction n with + | zero => simp + | succ n ih => + rw [count_succ] + split + · simp [ih] + · apply Nat.le_trans _ (Nat.le_succ n); simp [ih] + +/-! ### find? -/ + +theorem find?_prop {P : Fin n → Prop} [DecidablePred P] (h : Fin.find? P = some x) : P x := by + induction n with + | zero => contradiction + | succ n ih => + simp [Fin.find?] at h + split at h + · cases h; assumption + · split at h + · cases h + apply ih (P := fun i => P i.succ) + assumption + · contradiction + +theorem exists_of_find?_isSome {P : Fin n → Prop} [DecidablePred P] (h : (Fin.find? P).isSome) : + ∃ x, P x := by + match heq : Fin.find? P with + | some x => exists x; exact find?_prop heq + | none => rw [heq] at h; contradiction + +theorem find?_isSome_of_exists {P : Fin n → Prop} [DecidablePred P] (h : ∃ x, P x) : + (Fin.find? P).isSome := by + induction n with + | zero => match h with | ⟨x, _⟩ => nomatch x + | succ n ih => + simp only [Fin.find?] + split + · rfl + · have h : ∃ (x : Fin n), P x.succ := by + match h with + | ⟨0, _⟩ => contradiction + | ⟨⟨i+1, hi⟩, _⟩ => exists ⟨i, Nat.lt_of_succ_lt_succ hi⟩ + have h : (Fin.find? fun x => P x.succ).isSome := ih h + split + · rfl + · next heq => + rw [heq] at h + contradiction + +theorem find?_isSome_iff_exists {P : Fin n → Prop} [DecidablePred P] : + (Fin.find? P).isSome ↔ ∃ x, P x := ⟨exists_of_find?_isSome, find?_isSome_of_exists⟩ + +/-! ### recZeroSuccOn -/ + +unseal Fin.recZeroSuccOn in +@[simp] theorem recZeroSuccOn_zero {motive : Fin (n+1) → Sort _} (zero : motive 0) + (succ : (x : Fin n) → motive x.castSucc → motive x.succ) : + Fin.recZeroSuccOn 0 zero succ = zero := rfl + +unseal Fin.recZeroSuccOn in +theorem recZeroSuccOn_succ {motive : Fin (n+1) → Sort _} (x : Fin n) (zero : motive 0) + (succ : (x : Fin n) → motive x.castSucc → motive x.succ) : + Fin.recZeroSuccOn x.succ zero succ = succ x (Fin.recZeroSuccOn x.castSucc zero succ) := rfl + +/-! ### casesZeroSuccOn -/ + +@[simp] theorem casesZeroSuccOn_zero {motive : Fin (n+1) → Sort _} (zero : motive 0) + (succ : (x : Fin n) → motive x.succ) : Fin.casesZeroSuccOn 0 zero succ = zero := rfl + +@[simp] theorem casesZeroSuccOn_succ {motive : Fin (n+1) → Sort _} (x : Fin n) (zero : motive 0) + (succ : (x : Fin n) → motive x.succ) : Fin.casesZeroSuccOn x.succ zero succ = succ x := rfl From aef93925a4f3d4c54d6c464410f20b7f4468242e Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Fri, 25 Oct 2024 12:19:00 -0400 Subject: [PATCH 02/31] chore: use encode/decode --- Batteries/Data/Fin/Enum.lean | 150 +++++++++++++++++------------------ 1 file changed, 75 insertions(+), 75 deletions(-) diff --git a/Batteries/Data/Fin/Enum.lean b/Batteries/Data/Fin/Enum.lean index 93a73516da..20f4c34590 100644 --- a/Batteries/Data/Fin/Enum.lean +++ b/Batteries/Data/Fin/Enum.lean @@ -12,57 +12,57 @@ protected class Enum (α : Type _) where /-- Size of type. -/ size : Nat /-- Enumeration of the type elements. -/ - enum : Fin size → α + decode : Fin size → α /-- Find the index of a type element. -/ - find : α → Fin size - /-- Inverse relation for `enum` and `find`. -/ - enum_find (x) : enum (find x) = x - /-- Inverse relation for `enum` and `find`. -/ - find_enum (i) : find (enum i) = i + encode : α → Fin size + /-- Inverse relation for `decode` and `encode`. -/ + decode_encode (x) : decode (encode x) = x + /-- Inverse relation for `decode` and `encode`. -/ + encode_decode (i) : encode (decode i) = i -attribute [simp] Enum.enum_find Enum.find_enum +attribute [simp] Enum.decode_encode Enum.encode_decode namespace Enum instance : Fin.Enum Empty where size := 0 - enum := nofun - find := nofun - enum_find := nofun - find_enum := nofun + decode := nofun + encode := nofun + decode_encode := nofun + encode_decode := nofun instance : Fin.Enum PUnit where size := 1 - enum := decodePUnit - find := encodePUnit - enum_find := decodePUnit_encodePUnit - find_enum := encodePUnit_decodePUnit + decode := decodePUnit + encode := encodePUnit + decode_encode := decodePUnit_encodePUnit + encode_decode := encodePUnit_decodePUnit instance : Fin.Enum Bool where size := 2 - enum := decodeBool - find := encodeBool - enum_find := decodeBool_encodeBool - find_enum := encodeBool_decodeBool + decode := decodeBool + encode := encodeBool + decode_encode := decodeBool_encodeBool + encode_decode := encodeBool_decodeBool instance [Fin.Enum α] : Fin.Enum (Option α) where size := size α + 1 - enum i := decodeOption i |>.map enum - find x := encodeOption <| x.map find - enum_find := by simp [Function.comp_def] - find_enum := by simp [Function.comp_def] + decode i := decodeOption i |>.map decode + encode x := encodeOption <| x.map encode + decode_encode := by simp [Function.comp_def] + encode_decode := by simp [Function.comp_def] instance [Fin.Enum α] [Fin.Enum β] : Fin.Enum (α ⊕ β) where size := size α + size β - enum i := + decode i := match decodeSum i with - | .inl i => .inl <| enum i - | .inr i => .inr <| enum i - find x := + | .inl i => .inl <| decode i + | .inr i => .inr <| decode i + encode x := match x with - | .inl x => encodeSum <| .inl (find x) - | .inr x => encodeSum <| .inr (find x) - enum_find _ := by + | .inl x => encodeSum <| .inl (encode x) + | .inr x => encodeSum <| .inr (encode x) + decode_encode _ := by simp only; split · next h => split at h; @@ -72,7 +72,7 @@ instance [Fin.Enum α] [Fin.Enum β] : Fin.Enum (α ⊕ β) where split at h; · simp at h · simp at h; cases h; simp - find_enum _ := by + encode_decode _ := by simp only; split · next h => split at h @@ -85,104 +85,104 @@ instance [Fin.Enum α] [Fin.Enum β] : Fin.Enum (α ⊕ β) where instance [Fin.Enum α] [Fin.Enum β] : Fin.Enum (α × β) where size := size α * size β - enum i := (enum (decodeProd i).fst, enum (decodeProd i).snd) - find x := encodeProd (find x.fst, find x.snd) - find_enum := by simp [Prod.eta] - enum_find := by simp + decode i := (decode (decodeProd i).fst, decode (decodeProd i).snd) + encode x := encodeProd (encode x.fst, encode x.snd) + encode_decode := by simp [Prod.eta] + decode_encode := by simp instance [Fin.Enum α] [Fin.Enum β] : Fin.Enum (β → α) where size := size α ^ size β - enum i x := enum (decodeFun i (find x)) - find f := encodeFun fun x => find (f (enum x)) - find_enum := by simp - enum_find := by simp + decode i x := decode (decodeFun i (encode x)) + encode f := encodeFun fun x => encode (f (decode x)) + encode_decode := by simp + decode_encode := by simp instance (β : α → Type _) [Fin.Enum α] [(x : α) → Fin.Enum (β x)] : Fin.Enum ((x : α) × β x) where - size := Fin.sum fun i => size (β (enum i)) - enum i := + size := Fin.sum fun i => size (β (decode i)) + decode i := match decodeSigma _ i with - | ⟨i, j⟩ => ⟨enum i, enum j⟩ - find | ⟨x, y⟩ => encodeSigma _ ⟨find x, find (_root_.cast (by simp) y)⟩ - find_enum i := by + | ⟨i, j⟩ => ⟨decode i, decode j⟩ + encode | ⟨x, y⟩ => encodeSigma _ ⟨encode x, encode (_root_.cast (by simp) y)⟩ + encode_decode i := by simp only [] conv => rhs; rw [← encodeSigma_decodeSigma _ i] congr 1 ext · simp · simp only [] - conv => rhs; rw [← find_enum (decodeSigma _ i).snd] + conv => rhs; rw [← encode_decode (decodeSigma _ i).snd] congr <;> simp - enum_find + decode_encode | ⟨x, y⟩ => by ext - simp only [cast, decodeSigma_encodeSigma, enum_find] + simp only [cast, decodeSigma_encodeSigma, decode_encode] simp [] rw [decodeSigma_encodeSigma] simp instance (β : α → Type _) [Fin.Enum α] [(x : α) → Fin.Enum (β x)] : Fin.Enum ((x : α) → β x) where - size := Fin.prod fun i => size (β (enum i)) - enum i x := enum <| (decodePi _ i (find x)).cast (by rw [enum_find]) - find f := encodePi _ fun i => find (f (enum i)) - find_enum i := by - simp only [find_enum] + size := Fin.prod fun i => size (β (decode i)) + decode i x := decode <| (decodePi _ i (encode x)).cast (by rw [decode_encode]) + encode f := encodePi _ fun i => encode (f (decode i)) + encode_decode i := by + simp only [encode_decode] conv => rhs; rw [← encodePi_decodePi _ i] congr ext simp only [cast] - rw [find_enum] - enum_find f := by + rw [encode_decode] + decode_encode f := by funext x simp only [] - conv => rhs; rw [← enum_find (f x)] + conv => rhs; rw [← decode_encode (f x)] congr 1 ext simp only [cast, decodePi_encodePi] - rw [enum_find] + rw [decode_encode] done instance (P : α → Prop) [DecidablePred P] [Fin.Enum α] : Fin.Enum { x // P x} where - size := Fin.count fun i => P (enum i) - enum i := ⟨enum (decodeSubtype _ i).val, (decodeSubtype _ i).property⟩ - find x := encodeSubtype _ ⟨find x.val, (enum_find x.val).symm ▸ x.property⟩ - find_enum i := by simp [Subtype.eta] - enum_find := by simp + size := Fin.count fun i => P (decode i) + decode i := ⟨decode (decodeSubtype _ i).val, (decodeSubtype _ i).property⟩ + encode x := encodeSubtype _ ⟨encode x.val, (decode_encode x.val).symm ▸ x.property⟩ + encode_decode i := by simp [Subtype.eta] + decode_encode := by simp -private def enumSetoid (s : Setoid α) [DecidableRel s.r] [Fin.Enum α] : +private def decodeSetoid (s : Setoid α) [DecidableRel s.r] [Fin.Enum α] : Setoid (Fin (size α)) where - r i j := s.r (enum i) (enum j) + r i j := s.r (decode i) (decode j) iseqv := { - refl := fun i => Setoid.refl (enum i) + refl := fun i => Setoid.refl (decode i) symm := Setoid.symm trans := Setoid.trans } -private instance (s : Setoid α) [DecidableRel s.r] [Fin.Enum α] : DecidableRel (enumSetoid s).r := +private instance (s : Setoid α) [DecidableRel s.r] [Fin.Enum α] : DecidableRel (decodeSetoid s).r := fun _ _ => inferInstanceAs (Decidable (s.r _ _)) instance (s : Setoid α) [DecidableRel s.r] [Fin.Enum α] : Fin.Enum (Quotient s) where - size := Fin.count fun i => getRepr (enumSetoid s) i = i - enum i := Quotient.liftOn (decodeQuotient (enumSetoid s) i) (fun i => Quotient.mk s (enum i)) + size := Fin.count fun i => getRepr (decodeSetoid s) i = i + decode i := Quotient.liftOn (decodeQuotient (decodeSetoid s) i) (fun i => Quotient.mk s (decode i)) (fun _ _ h => Quotient.sound h) - find x := Quotient.liftOn x - (fun x => encodeQuotient (enumSetoid s) (Quotient.mk _ (find x))) <| by + encode x := Quotient.liftOn x + (fun x => encodeQuotient (decodeSetoid s) (Quotient.mk _ (encode x))) <| by intro _ _ h simp only [] congr 1 apply Quotient.sound - simp only [HasEquiv.Equiv, enumSetoid, enum_find] + simp only [HasEquiv.Equiv, decodeSetoid, decode_encode] exact h - enum_find x := by + decode_encode x := by induction x using Quotient.inductionOn with | _ x => simp only [decodeQuotient, encodeQuotient, decodeSubtype_encodeSubtype, Quotient.liftOn, Quotient.mk, Quot.liftOn] apply Quot.sound - conv => rhs; rw [← enum_find x] - exact getRepr_equiv (enumSetoid s) .. - find_enum i := by + conv => rhs; rw [← decode_encode x] + exact getRepr_equiv (decodeSetoid s) .. + encode_decode i := by conv => rhs; rw [← encodeSubtype_decodeSubtype _ i] simp only [Quotient.liftOn, Quot.liftOn, encodeQuotient, Quotient.mk, decodeQuotient, - find_enum] + encode_decode] congr rw [(decodeSubtype _ i).property] From 146f718bcf1b2d225d7146c79fab5ba644c14c6e Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Fri, 25 Oct 2024 17:17:13 -0400 Subject: [PATCH 03/31] feat: make find? tail recursive --- Batteries/Data/Fin/Basic.lean | 21 ++++++----- Batteries/Data/Fin/Lemmas.lean | 67 ++++++++++++++++++++-------------- 2 files changed, 51 insertions(+), 37 deletions(-) diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean index 8438128674..39db490057 100644 --- a/Batteries/Data/Fin/Basic.lean +++ b/Batteries/Data/Fin/Basic.lean @@ -82,16 +82,17 @@ protected def count (P : Fin n → Prop) [DecidablePred P] : Nat := Fin.sum (if P · then 1 else 0) /-- Find the first true value of a decidable predicate on `Fin n`, if there is one. -/ -protected def find? (P : Fin n → Prop) [inst : DecidablePred P] : Option (Fin n) := - match n, P, inst with - | 0, _, _ => none - | _+1, P, _ => - if P 0 then - some 0 - else - match Fin.find? fun i => P i.succ with - | some i => some i.succ - | none => none +protected def find? (P : Fin n → Prop) [DecidablePred P] : Option (Fin n) := + foldr n (fun i v => if P i then some i else v) none + -- match n, P, inst with + -- | 0, _, _ => none + -- | _+1, P, _ => + -- if P 0 then + -- some 0 + -- else + -- match Fin.find? fun i => P i.succ with + -- | some i => some i.succ + -- | none => none /-- Custom recursor for `Fin (n+1)`. -/ def recZeroSuccOn {motive : Fin (n+1) → Sort _} (x : Fin (n+1)) diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean index e2edb35f03..0059075263 100644 --- a/Batteries/Data/Fin/Lemmas.lean +++ b/Batteries/Data/Fin/Lemmas.lean @@ -220,6 +220,12 @@ theorem foldr_rev (f : α → Fin n → α) (x) : | zero => simp | succ n ih => rw [foldl_succ_last, foldr_succ, ← ih]; simp [rev_succ] +theorem map_foldr {g : α → β} {f : Fin n → α → α} {f' : Fin n → β → β} + (h : ∀ i x, g (f i x) = f' i (g x)) (x) : g (foldr n f x) = foldr n f' (g x) := by + induction n generalizing x with + | zero => simp + | succ n ih => simp [foldr_succ, ih, h] + /-! ### sum -/ @[simp] theorem sum_zero [OfNat α (nat_lit 0)] [Add α] (x : Fin 0 → α) : @@ -260,46 +266,53 @@ theorem count_le (P : Fin n → Prop) [DecidablePred P] : Fin.count P ≤ n := b /-! ### find? -/ +@[simp] theorem find?_zero {P : Fin 0 → Prop} [DecidablePred P] : Fin.find? P = none := by + simp [Fin.find?] + +theorem find?_succ (P : Fin (n+1) → Prop) [DecidablePred P] : + Fin.find? P = if P 0 then some 0 else (Fin.find? fun i => P i.succ).map Fin.succ := by + have h (i : Fin n) (v : Option (Fin n)) : + (if P i.succ then some i else v).map Fin.succ = + if P i.succ then some i.succ else v.map Fin.succ := by + intros; split <;> simp + simp [Fin.find?, foldr_succ, map_foldr h] + theorem find?_prop {P : Fin n → Prop} [DecidablePred P] (h : Fin.find? P = some x) : P x := by induction n with - | zero => contradiction + | zero => simp at h | succ n ih => - simp [Fin.find?] at h + simp [find?_succ] at h split at h · cases h; assumption - · split at h - · cases h - apply ih (P := fun i => P i.succ) - assumption - · contradiction - -theorem exists_of_find?_isSome {P : Fin n → Prop} [DecidablePred P] (h : (Fin.find? P).isSome) : - ∃ x, P x := by - match heq : Fin.find? P with - | some x => exists x; exact find?_prop heq - | none => rw [heq] at h; contradiction - -theorem find?_isSome_of_exists {P : Fin n → Prop} [DecidablePred P] (h : ∃ x, P x) : + · simp [Option.map_eq_some] at h + match h with + | ⟨i, h', hi⟩ => cases hi; exact ih h' + +theorem find?_isSome_of_prop {P : Fin n → Prop} [DecidablePred P] (h : P x) : (Fin.find? P).isSome := by induction n with - | zero => match h with | ⟨x, _⟩ => nomatch x + | zero => nomatch x | succ n ih => - simp only [Fin.find?] + rw [find?_succ] split · rfl - · have h : ∃ (x : Fin n), P x.succ := by - match h with - | ⟨0, _⟩ => contradiction - | ⟨⟨i+1, hi⟩, _⟩ => exists ⟨i, Nat.lt_of_succ_lt_succ hi⟩ - have h : (Fin.find? fun x => P x.succ).isSome := ih h - split - · rfl - · next heq => - rw [heq] at h + · have hx : x ≠ 0 := by + intro hx + rw [hx] at h contradiction + have h : P (x.pred hx).succ := by simp [h] + rw [Option.isSome_map'] + exact ih h theorem find?_isSome_iff_exists {P : Fin n → Prop} [DecidablePred P] : - (Fin.find? P).isSome ↔ ∃ x, P x := ⟨exists_of_find?_isSome, find?_isSome_of_exists⟩ + (Fin.find? P).isSome ↔ ∃ x, P x := by + constructor + · intro h + match heq : Fin.find? P with + | some x => exists x; exact find?_prop heq + | none => rw [heq] at h; contradiction + · intro ⟨_, h⟩ + exact find?_isSome_of_prop h /-! ### recZeroSuccOn -/ From 401211b4adbf9c3ccf4623ecbdc03f287b9df98c Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Fri, 25 Oct 2024 17:19:52 -0400 Subject: [PATCH 04/31] chore: fix long line --- Batteries/Data/Fin/Enum.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Batteries/Data/Fin/Enum.lean b/Batteries/Data/Fin/Enum.lean index 20f4c34590..60670ed02f 100644 --- a/Batteries/Data/Fin/Enum.lean +++ b/Batteries/Data/Fin/Enum.lean @@ -162,8 +162,8 @@ private instance (s : Setoid α) [DecidableRel s.r] [Fin.Enum α] : DecidableRel instance (s : Setoid α) [DecidableRel s.r] [Fin.Enum α] : Fin.Enum (Quotient s) where size := Fin.count fun i => getRepr (decodeSetoid s) i = i - decode i := Quotient.liftOn (decodeQuotient (decodeSetoid s) i) (fun i => Quotient.mk s (decode i)) - (fun _ _ h => Quotient.sound h) + decode i := Quotient.liftOn (decodeQuotient (decodeSetoid s) i) + (fun i => Quotient.mk s (decode i)) (fun _ _ h => Quotient.sound h) encode x := Quotient.liftOn x (fun x => encodeQuotient (decodeSetoid s) (Quotient.mk _ (encode x))) <| by intro _ _ h From 4e209effe5c38bb592c11e4ad06f7796980175cc Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Fri, 25 Oct 2024 17:23:01 -0400 Subject: [PATCH 05/31] chore: cleanup --- Batteries/Data/Fin/Basic.lean | 9 --------- 1 file changed, 9 deletions(-) diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean index 39db490057..e3970e08c9 100644 --- a/Batteries/Data/Fin/Basic.lean +++ b/Batteries/Data/Fin/Basic.lean @@ -84,15 +84,6 @@ protected def count (P : Fin n → Prop) [DecidablePred P] : Nat := /-- Find the first true value of a decidable predicate on `Fin n`, if there is one. -/ protected def find? (P : Fin n → Prop) [DecidablePred P] : Option (Fin n) := foldr n (fun i v => if P i then some i else v) none - -- match n, P, inst with - -- | 0, _, _ => none - -- | _+1, P, _ => - -- if P 0 then - -- some 0 - -- else - -- match Fin.find? fun i => P i.succ with - -- | some i => some i.succ - -- | none => none /-- Custom recursor for `Fin (n+1)`. -/ def recZeroSuccOn {motive : Fin (n+1) → Sort _} (x : Fin (n+1)) From 9927b6c0c01376666407a7fec6ed603f5867c96f Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Fri, 25 Oct 2024 20:57:05 -0400 Subject: [PATCH 06/31] feat: add instance for `Char` --- Batteries/Data/Fin/Coding.lean | 40 ++++++++++++++++++++++++++++++++++ Batteries/Data/Fin/Enum.lean | 7 ++++++ 2 files changed, 47 insertions(+) diff --git a/Batteries/Data/Fin/Coding.lean b/Batteries/Data/Fin/Coding.lean index 5cc54ac0e6..a910ffe471 100644 --- a/Batteries/Data/Fin/Coding.lean +++ b/Batteries/Data/Fin/Coding.lean @@ -49,6 +49,46 @@ def encodeBool : Bool → Fin 2 | false => rfl | true => rfl +/-- Encode a character value as a `Fin` type. -/ +def encodeChar (c : Char) : Fin 1112064 := + have : c.toNat < 1114112 := + match c.valid with + | .inl h => Nat.lt_trans h (by decide) + | .inr h => 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. -/ +@[pp_nodot] 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, encodeChar] + split + · simp [Char.ofNatAux, Char.toNat, UInt32.toNat, *] + · have : ¬ x.val + 2048 < 55296 := by omega + simp [Char.ofNatAux, Char.toNat, UInt32.toNat, *] + +@[simp] theorem decodeChar_encodeChar (x) : decodeChar (encodeChar x) = x := by + ext; simp only [decodeChar, encodeChar] + split + · simp only [Char.ofNatAux, Char.toNat]; rfl + · 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 only [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 From 2b8b7ac1f74d5244f8d51ffe85e0cfdaab5180dd Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Sat, 8 Feb 2025 18:07:59 -0500 Subject: [PATCH 07/31] chore: adaptations --- Batteries/Data/Fin/Basic.lean | 16 ---------- Batteries/Data/Fin/Coding.lean | 57 ++++++++++++++++++---------------- Batteries/Data/Fin/Lemmas.lean | 20 ------------ 3 files changed, 30 insertions(+), 63 deletions(-) diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean index c392051297..da0f20ba32 100644 --- a/Batteries/Data/Fin/Basic.lean +++ b/Batteries/Data/Fin/Basic.lean @@ -107,19 +107,3 @@ protected def count (P : Fin n → Prop) [DecidablePred P] : Nat := /-- Find the first true value of a decidable predicate on `Fin n`, if there is one. -/ protected def find? (P : Fin n → Prop) [DecidablePred P] : Option (Fin n) := foldr n (fun i v => if P i then some i else v) none - -/-- Custom recursor for `Fin (n+1)`. -/ -def recZeroSuccOn {motive : Fin (n+1) → Sort _} (x : Fin (n+1)) - (zero : motive 0) (succ : (x : Fin n) → motive x.castSucc → motive x.succ) : motive x := - match x with - | 0 => zero - | ⟨x+1, hx⟩ => - let x : Fin n := ⟨x, Nat.lt_of_succ_lt_succ hx⟩ - succ x <| recZeroSuccOn x.castSucc zero succ - -/-- Custom recursor for `Fin (n+1)`. -/ -def casesZeroSuccOn {motive : Fin (n+1) → Sort _} (x : Fin (n+1)) - (zero : motive 0) (succ : (x : Fin n) → motive x.succ) : motive x := - match x with - | 0 => zero - | ⟨x+1, hx⟩ => succ ⟨x, Nat.lt_of_succ_lt_succ hx⟩ diff --git a/Batteries/Data/Fin/Coding.lean b/Batteries/Data/Fin/Coding.lean index 6facb49006..ec8dd5cacb 100644 --- a/Batteries/Data/Fin/Coding.lean +++ b/Batteries/Data/Fin/Coding.lean @@ -193,10 +193,10 @@ where /-- Encode a dependent sum of `Fin` types. -/ def encodeSigma (f : Fin n → Nat) (x : (i : Fin n) × Fin (f i)) : Fin (Fin.sum f) := match n, f, x with - | _+1, _, ⟨⟨0, _⟩, ⟨j, hj⟩⟩ => - ⟨j, Nat.lt_of_lt_of_le hj (sum_succ .. ▸ Nat.le_add_right ..)⟩ - | _+1, f, ⟨⟨i+1, hi⟩, ⟨j, hj⟩⟩ => - match encodeSigma ((f ∘ succ)) ⟨⟨i, Nat.lt_of_succ_lt_succ hi⟩, ⟨j, hj⟩⟩ with + | _+1, _, ⟨0, j⟩ => + ⟨j, Nat.lt_of_lt_of_le j.is_lt (sum_succ .. ▸ Nat.le_add_right ..)⟩ + | _+1, f, ⟨⟨i+1, hi⟩, j⟩ => + match encodeSigma ((f ∘ succ)) ⟨⟨i, Nat.lt_of_succ_lt_succ hi⟩, j⟩ with | ⟨k, hk⟩ => ⟨f 0 + k, sum_succ .. ▸ Nat.add_lt_add_left hk ..⟩ /-- Decode a dependent sum of `Fin` types. -/ @@ -221,7 +221,7 @@ def encodeSigma (f : Fin n → Nat) (x : (i : Fin n) × Fin (f i)) : Fin (Fin.su | succ n ih => simp only [decodeSigma] split - · simp [encodeSigma] + · rfl · next h1 => have h2 : x - f 0 < Fin.sum (f ∘ succ) := by apply Nat.sub_lt_left_of_lt_add @@ -240,7 +240,10 @@ def encodeSigma (f : Fin n → Nat) (x : (i : Fin n) × Fin (f i)) : Fin (Fin.su | succ n ih => simp only [decodeSigma] match x with - | ⟨0, x⟩ => simp [encodeSigma] + | ⟨0, x⟩ => + split + · rfl + · sorry | ⟨⟨i+1, hi⟩, ⟨x, hx⟩⟩ => have : ¬ encodeSigma f ⟨⟨i+1, hi⟩, ⟨x, hx⟩⟩ < f 0 := by simp [encodeSigma] rw [dif_neg this] @@ -350,12 +353,12 @@ def decodePi (f : Fin n → Nat) (x : Fin (Fin.prod f)) : (i : Fin n) → Fin (f funext i simp only [decodePi] split - · simp [Nat.mul_add_mod, Nat.mod_eq_of_lt (x 0).is_lt] + · simp [encodePi, Nat.mul_add_mod, Nat.mod_eq_of_lt (x 0).is_lt] · next i hi => have h : decodePi (f ∘ succ) (encodePi (f ∘ succ) fun i => x i.succ) ⟨i, Nat.lt_of_succ_lt_succ hi⟩ = x ⟨i+1, hi⟩ := by rw [ih]; rfl conv => rhs; rw [← h] - congr; simp [Nat.mul_add_div h0, Nat.div_eq_of_lt (x 0).is_lt]; rfl + congr; simp [encodePi, Nat.mul_add_div h0, Nat.div_eq_of_lt (x 0).is_lt]; rfl /-- Encode a decidable subtype of a `Fin` type. -/ def encodeSubtype (P : Fin n → Prop) [inst : DecidablePred P] (i : { i // P i }) : @@ -368,12 +371,12 @@ def encodeSubtype (P : Fin n → Prop) [inst : DecidablePred P] (i : { i // P i match encodeSubtype (fun i => P i.succ) ⟨⟨i, Nat.lt_of_succ_lt_succ hi⟩, hp⟩ with | ⟨k, hk⟩ => if h0 : P 0 then - have : Fin.count P = (Fin.count fun i => P i.succ) + 1 := by + have : (Fin.count fun i => P i.succ) + 1 = Fin.count P := by simp_arith only [count_succ, Function.comp_def, if_pos h0] - this ▸ ⟨k+1, Nat.succ_lt_succ hk⟩ + Fin.cast this ⟨k+1, Nat.succ_lt_succ hk⟩ else - have : Fin.count P = Fin.count fun i => P i.succ := by simp [count_succ, h0] - this ▸ ⟨k, hk⟩ + have : (Fin.count fun i => P i.succ) = Fin.count P := by simp [count_succ, h0] + Fin.cast this ⟨k, hk⟩ /-- Decode a decidable subtype of a `Fin` type. -/ def decodeSubtype (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (Fin.count p)) : @@ -393,29 +396,29 @@ def decodeSubtype (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (Fin.co match decodeSubtype (fun i => p (succ i)) ⟨k, this ▸ hk⟩ with | ⟨⟨i, hi⟩, hp⟩ => ⟨⟨i+1, Nat.succ_lt_succ hi⟩, hp⟩ -@[simp] theorem encodeSubtype_decodeSubtype (P : Fin n → Prop) [DecidablePred P] - (x : Fin (Fin.count P)) : encodeSubtype P (decodeSubtype P x) = x := by - induction n with - | zero => absurd x.is_lt; simp - | succ n ih => - simp only [decodeSubtype] - split - · ext; split <;> simp [encodeSubtype, count_succ, *] - · ext; simp [encodeSubtype, count_succ, *] - theorem encodeSubtype_zero_pos {P : Fin (n+1) → Prop} [DecidablePred P] (h₀ : P 0) : encodeSubtype P ⟨0, h₀⟩ = ⟨0, by simp [count_succ, *]⟩ := by - ext; simp [encodeSubtype] + ext; rw [encodeSubtype.eq_def]; rfl theorem encodeSubtype_succ_pos {P : Fin (n+1) → Prop} [DecidablePred P] (h₀ : P 0) {i : Fin n} (h : P i.succ) : encodeSubtype P ⟨i.succ, h⟩ = (encodeSubtype (fun i => P i.succ) ⟨i, h⟩).succ.cast (by simp [count_succ, *]) := by - ext; simp [encodeSubtype, count_succ, *] + ext; rw [encodeSubtype.eq_def]; simp [Fin.succ, *] theorem encodeSubtype_succ_neg {P : Fin (n+1) → Prop} [DecidablePred P] (h₀ : ¬ P 0) {i : Fin n} (h : P i.succ) : encodeSubtype P ⟨i.succ, h⟩ = (encodeSubtype (fun i => P i.succ) ⟨i, h⟩).cast (by simp [count_succ, *]) := by - ext; simp [encodeSubtype, count_succ, *] + ext; rw [encodeSubtype.eq_def]; simp [Fin.succ, *] + +@[simp] theorem encodeSubtype_decodeSubtype (P : Fin n → Prop) [DecidablePred P] + (x : Fin (Fin.count P)) : encodeSubtype P (decodeSubtype P x) = x := by + induction n with + | zero => absurd x.is_lt; simp + | succ n ih => + simp only [decodeSubtype] + split + · ext; split <;> simp [encodeSubtype_zero_pos, encodeSubtype, *]; done + · ext; simp [encodeSubtype, count_succ, *] @[simp] theorem decodeSubtype_encodeSubtype (P : Fin n → Prop) [DecidablePred P] (x : { x // P x}) : decodeSubtype P (encodeSubtype P x) = x := by @@ -426,7 +429,7 @@ theorem encodeSubtype_succ_neg {P : Fin (n+1) → Prop} [DecidablePred P] (h₀ | succ n ih => if h₀ : P 0 then simp only [decodeSubtype, dif_pos h₀] - cases i using Fin.casesZeroSuccOn with + cases i using Fin.cases with | zero => rw [encodeSubtype_zero_pos h₀] | succ i => rw [encodeSubtype_succ_pos h₀] @@ -435,7 +438,7 @@ theorem encodeSubtype_succ_neg {P : Fin (n+1) → Prop} [DecidablePred P] (h₀ rw [ih (fun i => P i.succ) ⟨i, h⟩] else simp only [decodeSubtype, dif_neg h₀] - cases i using Fin.casesZeroSuccOn with + cases i using Fin.cases with | zero => contradiction | succ i => rw [encodeSubtype_succ_neg h₀] diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean index 699d1ba925..7b667492c1 100644 --- a/Batteries/Data/Fin/Lemmas.lean +++ b/Batteries/Data/Fin/Lemmas.lean @@ -114,23 +114,3 @@ theorem find?_isSome_iff_exists {P : Fin n → Prop} [DecidablePred P] : | none => rw [heq] at h; contradiction · intro ⟨_, h⟩ exact find?_isSome_of_prop h - -/-! ### recZeroSuccOn -/ - -unseal Fin.recZeroSuccOn in -@[simp] theorem recZeroSuccOn_zero {motive : Fin (n+1) → Sort _} (zero : motive 0) - (succ : (x : Fin n) → motive x.castSucc → motive x.succ) : - Fin.recZeroSuccOn 0 zero succ = zero := rfl - -unseal Fin.recZeroSuccOn in -theorem recZeroSuccOn_succ {motive : Fin (n+1) → Sort _} (x : Fin n) (zero : motive 0) - (succ : (x : Fin n) → motive x.castSucc → motive x.succ) : - Fin.recZeroSuccOn x.succ zero succ = succ x (Fin.recZeroSuccOn x.castSucc zero succ) := rfl - -/-! ### casesZeroSuccOn -/ - -@[simp] theorem casesZeroSuccOn_zero {motive : Fin (n+1) → Sort _} (zero : motive 0) - (succ : (x : Fin n) → motive x.succ) : Fin.casesZeroSuccOn 0 zero succ = zero := rfl - -@[simp] theorem casesZeroSuccOn_succ {motive : Fin (n+1) → Sort _} (x : Fin n) (zero : motive 0) - (succ : (x : Fin n) → motive x.succ) : Fin.casesZeroSuccOn x.succ zero succ = succ x := rfl From 7e1c1a8fd92848c7679e7c05c1891fa1c6dc5157 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Sat, 31 May 2025 16:48:07 -0400 Subject: [PATCH 08/31] feat: add `Char` lemma --- Batteries/Data/Char.lean | 7 ++++++- Batteries/Data/Fin/Coding.lean | 4 +--- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/Batteries/Data/Char.lean b/Batteries/Data/Char.lean index 760e134273..d623e2117c 100644 --- a/Batteries/Data/Char.lean +++ b/Batteries/Data/Char.lean @@ -6,8 +6,13 @@ Authors: Jannis Limperg import Batteries.Data.UInt import Batteries.Tactic.Alias -theorem Char.le_antisymm_iff {x y : Char} : x = y ↔ x ≤ y ∧ y ≤ x := +namespace Char + +theorem le_antisymm_iff {x y : Char} : x = y ↔ x ≤ y ∧ y ≤ x := Char.ext_iff.trans UInt32.le_antisymm_iff instance : Batteries.LawfulOrd Char := .compareOfLessAndEq (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt Char.le_antisymm + +@[simp] theorem toNat_ofNatAux (n : Nat) (h : n.isValidChar) : + (Char.ofNatAux n h).toNat = n := rfl diff --git a/Batteries/Data/Fin/Coding.lean b/Batteries/Data/Fin/Coding.lean index 445e80e607..08ed3bc728 100644 --- a/Batteries/Data/Fin/Coding.lean +++ b/Batteries/Data/Fin/Coding.lean @@ -3,14 +3,12 @@ Copyright (c) 2024 François G. Dorais. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: François G. Dorais -/ +import Batteries.Data.Char import Batteries.Data.Fin.Lemmas import Batteries.Tactic.Basic import Batteries.Tactic.Trans import Batteries.Tactic.Lint -@[simp] theorem Char.toNat_ofNatAux (n : Nat) (h : n.isValidChar) : - (Char.ofNatAux n h).toNat = n := rfl - namespace Fin /-- Encode a unit value as a `Fin` type. -/ From b6f1ca284012a584e3db9851070f36f29709023c Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Sat, 19 Jul 2025 05:16:43 -0400 Subject: [PATCH 09/31] chore: delete `Fin.Enum` --- Batteries/Data/Fin.lean | 1 - Batteries/Data/Fin/Enum.lean | 193 --------------------------------- Batteries/Data/Fin/Lemmas.lean | 8 -- 3 files changed, 202 deletions(-) delete mode 100644 Batteries/Data/Fin/Enum.lean diff --git a/Batteries/Data/Fin.lean b/Batteries/Data/Fin.lean index ea2d8113d9..b08f5c7cea 100644 --- a/Batteries/Data/Fin.lean +++ b/Batteries/Data/Fin.lean @@ -1,6 +1,5 @@ import Batteries.Data.Fin.Basic import Batteries.Data.Fin.Coding -import Batteries.Data.Fin.Enum import Batteries.Data.Fin.Fold import Batteries.Data.Fin.Lemmas import Batteries.Data.Fin.OfBits diff --git a/Batteries/Data/Fin/Enum.lean b/Batteries/Data/Fin/Enum.lean deleted file mode 100644 index 07b28a2eac..0000000000 --- a/Batteries/Data/Fin/Enum.lean +++ /dev/null @@ -1,193 +0,0 @@ -/- -Copyright (c) 2024 François G. Dorais. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: François G. Dorais --/ -import Batteries.Data.Fin.Coding - -namespace Fin - -/-- Class of types that are in bijection with a `Fin` type. -/ -protected class Enum (α : Type _) where - /-- Size of type. -/ - size : Nat - /-- Enumeration of the type elements. -/ - decode : Fin size → α - /-- Find the index of a type element. -/ - encode : α → Fin size - /-- Inverse relation for `decode` and `encode`. -/ - decode_encode (x) : decode (encode x) = x - /-- Inverse relation for `decode` and `encode`. -/ - encode_decode (i) : encode (decode i) = i - -attribute [simp] Enum.decode_encode Enum.encode_decode - -namespace Enum - -instance : Fin.Enum Empty where - size := 0 - decode := nofun - encode := nofun - decode_encode := nofun - encode_decode := nofun - -instance : Fin.Enum PUnit where - size := 1 - decode := decodePUnit - encode := encodePUnit - decode_encode := decodePUnit_encodePUnit - encode_decode := encodePUnit_decodePUnit - -instance : Fin.Enum Bool where - size := 2 - decode := decodeBool - encode := encodeBool - 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 - encode x := encodeOption <| x.map encode - decode_encode := by simp [Function.comp_def] - encode_decode := by simp [Function.comp_def] - -instance [Fin.Enum α] [Fin.Enum β] : Fin.Enum (α ⊕ β) where - size := size α + size β - decode i := - match decodeSum i with - | .inl i => .inl <| decode i - | .inr i => .inr <| decode i - encode x := - match x with - | .inl x => encodeSum <| .inl (encode x) - | .inr x => encodeSum <| .inr (encode x) - decode_encode _ := by - split - · next h => - split at h; - · simp at h; cases h; simp - · simp at h - · next h => - split at h; - · simp at h - · simp at h; cases h; simp - encode_decode _ := by - split - · next h => - split at h - · next h' => cases h; simp [← h'] - · simp at h - · next h => - split at h - · simp at h - · next h' => cases h; simp [← h'] - -instance [Fin.Enum α] [Fin.Enum β] : Fin.Enum (α × β) where - size := size α * size β - decode i := (decode (decodeProd i).fst, decode (decodeProd i).snd) - encode x := encodeProd (encode x.fst, encode x.snd) - encode_decode := by simp [Prod.eta] - decode_encode := by simp - -instance [Fin.Enum α] [Fin.Enum β] : Fin.Enum (β → α) where - size := size α ^ size β - decode i x := decode (decodeFun i (encode x)) - encode f := encodeFun fun x => encode (f (decode x)) - encode_decode := by simp - decode_encode := by simp - -instance (β : α → Type _) [Fin.Enum α] [(x : α) → Fin.Enum (β x)] : Fin.Enum ((x : α) × β x) where - size := Fin.sum fun i => size (β (decode i)) - decode i := - match decodeSigma _ i with - | ⟨i, j⟩ => ⟨decode i, decode j⟩ - encode | ⟨x, y⟩ => encodeSigma _ ⟨encode x, encode (_root_.cast (by simp) y)⟩ - encode_decode i := by - simp only [] - conv => rhs; rw [← encodeSigma_decodeSigma _ i] - congr 1 - ext - · simp - · simp only [] - conv => rhs; rw [← encode_decode (decodeSigma _ i).snd] - congr <;> simp - decode_encode - | ⟨x, y⟩ => by - ext - simp only [cast, decodeSigma_encodeSigma, decode_encode] - simp [] - rw [decodeSigma_encodeSigma] - simp - -instance (β : α → Type _) [Fin.Enum α] [(x : α) → Fin.Enum (β x)] : Fin.Enum ((x : α) → β x) where - size := Fin.prod fun i => size (β (decode i)) - decode i x := decode <| (decodePi _ i (encode x)).cast (by rw [decode_encode]) - encode f := encodePi _ fun i => encode (f (decode i)) - encode_decode i := by - simp only [encode_decode] - conv => rhs; rw [← encodePi_decodePi _ i] - congr - ext - simp only [coe_cast] - rw [encode_decode] - decode_encode f := by - funext x - conv => rhs; rw [← decode_encode (f x)] - congr 1 - ext - simp only [decodePi_encodePi, coe_cast] - rw [decode_encode] - -instance (P : α → Prop) [DecidablePred P] [Fin.Enum α] : Fin.Enum { x // P x} where - size := Fin.count fun i => P (decode i) - decode i := ⟨decode (decodeSubtype _ i).val, (decodeSubtype _ i).property⟩ - encode x := encodeSubtype _ ⟨encode x.val, (decode_encode x.val).symm ▸ x.property⟩ - encode_decode i := by simp [Subtype.eta] - decode_encode := by simp - -private def decodeSetoid (s : Setoid α) [DecidableRel s.r] [Fin.Enum α] : - Setoid (Fin (size α)) where - r i j := s.r (decode i) (decode j) - iseqv := { - refl := fun i => Setoid.refl (decode i) - symm := Setoid.symm - trans := Setoid.trans - } - -private instance (s : Setoid α) [DecidableRel s.r] [Fin.Enum α] : DecidableRel (decodeSetoid s).r := - fun _ _ => inferInstanceAs (Decidable (s.r _ _)) - -instance (s : Setoid α) [DecidableRel s.r] [Fin.Enum α] : Fin.Enum (Quotient s) where - size := Fin.count fun i => getRepr (decodeSetoid s) i = i - decode i := Quotient.liftOn (decodeQuotient (decodeSetoid s) i) - (fun i => Quotient.mk s (decode i)) (fun _ _ h => Quotient.sound h) - encode x := Quotient.liftOn x - (fun x => encodeQuotient (decodeSetoid s) (Quotient.mk _ (encode x))) <| by - intro _ _ h - simp only [] - congr 1 - apply Quotient.sound - simp only [HasEquiv.Equiv, decodeSetoid, decode_encode] - exact h - decode_encode x := by - induction x using Quotient.inductionOn with - | _ x => - simp only [decodeQuotient, encodeQuotient, decodeSubtype_encodeSubtype, Quotient.liftOn, - Quotient.mk, Quot.liftOn] - apply Quot.sound - conv => rhs; rw [← decode_encode x] - exact getRepr_equiv (decodeSetoid s) .. - encode_decode i := by - conv => rhs; rw [← encodeSubtype_decodeSubtype _ i] - simp only [Quotient.liftOn, Quot.liftOn, encodeQuotient, Quotient.mk, decodeQuotient, - encode_decode] - congr - rw [(decodeSubtype _ i).property] diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean index 21df01787a..bccc6eadf9 100644 --- a/Batteries/Data/Fin/Lemmas.lean +++ b/Batteries/Data/Fin/Lemmas.lean @@ -15,14 +15,6 @@ attribute [norm_cast] val_last @[simp] theorem coe_clamp (n m : Nat) : (clamp n m : Nat) = min n m := rfl -/-! ### foldr -/ - -theorem map_foldr {g : α → β} {f : Fin n → α → α} {f' : Fin n → β → β} - (h : ∀ i x, g (f i x) = f' i (g x)) (x) : g (foldr n f x) = foldr n f' (g x) := by - induction n generalizing x with - | zero => simp - | succ n ih => simp [foldr_succ, ih, h] - /-! ### sum -/ @[simp] theorem sum_zero [OfNat α (nat_lit 0)] [Add α] (x : Fin 0 → α) : From b3c4434395fe670809bc5b6d5c2b33a80d197808 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Mon, 21 Jul 2025 10:59:18 -0400 Subject: [PATCH 10/31] chore: delete empty file (#1336) --- Batteries/Data/Array.lean | 1 - Batteries/Data/Array/OfFn.lean | 14 -------------- 2 files changed, 15 deletions(-) delete mode 100644 Batteries/Data/Array/OfFn.lean diff --git a/Batteries/Data/Array.lean b/Batteries/Data/Array.lean index 1f500b700a..4d41e75755 100644 --- a/Batteries/Data/Array.lean +++ b/Batteries/Data/Array.lean @@ -4,5 +4,4 @@ import Batteries.Data.Array.Lemmas import Batteries.Data.Array.Match import Batteries.Data.Array.Merge import Batteries.Data.Array.Monadic -import Batteries.Data.Array.OfFn import Batteries.Data.Array.Pairwise diff --git a/Batteries/Data/Array/OfFn.lean b/Batteries/Data/Array/OfFn.lean deleted file mode 100644 index 5233fd1f96..0000000000 --- a/Batteries/Data/Array/OfFn.lean +++ /dev/null @@ -1,14 +0,0 @@ -/- -Copyright (c) 2024 Lean FRO. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Kim Morrison --/ -import Batteries.Data.List.OfFn - -open List - -namespace Array - -/-! ### ofFn -/ - -end Array From 5f622f129f81993dc1f7385c4b70a71f00dc9dea Mon Sep 17 00:00:00 2001 From: Devon Tuma Date: Wed, 23 Jul 2025 03:14:18 -0700 Subject: [PATCH 11/31] feat: Laws for `MonadStateOf` instances (#1313) --- Batteries.lean | 1 + Batteries/Control/LawfulMonadState.lean | 221 ++++++++++++++++++++++++ Batteries/Control/OptionT.lean | 10 ++ 3 files changed, 232 insertions(+) create mode 100644 Batteries/Control/LawfulMonadState.lean diff --git a/Batteries.lean b/Batteries.lean index 597b2d8c9f..ca2738c094 100644 --- a/Batteries.lean +++ b/Batteries.lean @@ -11,6 +11,7 @@ import Batteries.Control.AlternativeMonad import Batteries.Control.ForInStep import Batteries.Control.ForInStep.Basic import Batteries.Control.ForInStep.Lemmas +import Batteries.Control.LawfulMonadState import Batteries.Control.Lemmas import Batteries.Control.Monad import Batteries.Control.Nondet.Basic diff --git a/Batteries/Control/LawfulMonadState.lean b/Batteries/Control/LawfulMonadState.lean new file mode 100644 index 0000000000..355681fc69 --- /dev/null +++ b/Batteries/Control/LawfulMonadState.lean @@ -0,0 +1,221 @@ +/- +Copyright (c) 2025 Devon Tuma. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma, Quang Dao +-/ + +/-! +# Laws for Monads with State + +This file defines a typeclass for `MonadStateOf` with compatible `get` and `set` operations. + +Note that we use `MonadStateOf` over `MonadState` as the first induces the second, +but we phrase things using `MonadStateOf.set` and `MonadState.get` as those are the +versions that are available at the top level namespace. +-/ + +/-- The namespaced `MonadStateOf.get` is equal to the `MonadState` provided `get`. -/ +@[simp] theorem monadStateOf_get_eq_get [MonadStateOf σ m] : + (MonadStateOf.get : m σ) = get := rfl + +/-- The namespaced `MonadStateOf.modifyGet` is equal to the `MonadState` provided `modifyGet`. -/ +@[simp] theorem monadStateOf_modifyGet_eq_modifyGet [MonadStateOf σ m] + (f : σ → α × σ) : (MonadStateOf.modifyGet f : m α) = modifyGet f := rfl + +@[simp] theorem liftM_get {m n} [MonadStateOf σ m] [MonadLift m n] : + (liftM (get (m := m)) : n _) = get := rfl + +@[simp] theorem liftM_set {m n} [MonadStateOf σ m] [MonadLift m n] + (s : σ) : (liftM (set (m := m) s) : n _) = set s := rfl + +@[simp] theorem liftM_modify {m n} [MonadStateOf σ m] [MonadLift m n] + (f : σ → σ) : (liftM (modify (m := m) f) : n _) = modify f := rfl + +@[simp] theorem liftM_modifyGet {m n} [MonadStateOf σ m] [MonadLift m n] + (f : σ → α × σ) : (liftM (modifyGet (m := m) f) : n _) = modifyGet f := rfl + +@[simp] theorem liftM_getModify {m n} [MonadStateOf σ m] [MonadLift m n] + (f : σ → σ) : (liftM (getModify (m := m) f) : n _) = getModify f := rfl + +/-- Class for well behaved state monads, extending the base `MonadState` type. +Requires that `modifyGet` is equal to the same definition with only `get` and `set`, +that `get` is idempotent if the result isn't used, and that `get` after `set` returns +exactly the value that was previously `set`. -/ +class LawfulMonadStateOf (σ : Type _) (m : Type _ → Type _) + [Monad m] [MonadStateOf σ m] extends LawfulMonad m where + /-- `modifyGet f` is equal to getting the state, modifying it, and returning a result. -/ + modifyGet_eq {α} (f : σ → α × σ) : + modifyGet (m := m) f = do let z ← f <$> get; set z.2; return z.1 + /-- Discarding the result of `get` is the same as never getting the state. -/ + get_bind_const {α} (mx : m α) : (do let _ ← get; mx) = mx + /-- Calling `get` twice is the same as just using the first retreived state value. -/ + get_bind_get_bind {α} (mx : σ → σ → m α) : + (do let s ← get; let s' ← get; mx s s') = (do let s ← get; mx s s) + /-- Setting the monad state to its current value has no effect. -/ + get_bind_set_bind {α} (mx : σ → PUnit → m α) : + (do let s ← get; let u ← set s; mx s u) = (do let s ← get; mx s PUnit.unit) + /-- Setting and then returning the monad state is the same as returning the set value. -/ + set_bind_get (s : σ) : (do set (m := m) s; get) = (do set s; return s) + /-- Setting the monad twice is the same as just setting to the final state. -/ + set_bind_set (s s' : σ) : (do set (m := m) s; set s') = set s' + +namespace LawfulMonadStateOf + +variable {σ : Type _} {m : Type _ → Type _} [Monad m] + [MonadStateOf σ m] [LawfulMonadStateOf σ m] + +attribute [simp] get_bind_const get_bind_get_bind get_bind_set_bind set_bind_get set_bind_set + +@[simp] theorem get_seqRight (mx : m α) : get *> mx = mx := by + rw [seqRight_eq_bind, get_bind_const] + +@[simp] theorem seqLeft_get (mx : m α) : mx <* get = mx := by + simp only [seqLeft_eq_bind, get_bind_const, bind_pure] + +@[simp] theorem get_map_const (x : α) : + (fun _ => x) <$> get (m := m) = pure x := by + rw [map_eq_pure_bind, get_bind_const] + +theorem get_bind_get : (do let _ ← get (m := m); get) = get := get_bind_const get + +@[simp] theorem get_bind_set : + (do let s ← get (m := m); set s) = return PUnit.unit := by + simpa only [bind_pure_comp, id_map', get_map_const] using + get_bind_set_bind (σ := σ) (m := m) (fun _ _ => return PUnit.unit) + +@[simp] theorem get_bind_map_set (f : σ → PUnit → α) : + (do let s ← get (m := m); f s <$> set s) = (do return f (← get) PUnit.unit) := by + simp [map_eq_pure_bind, bind_assoc, -bind_pure_comp] + +@[simp] theorem set_bind_get_bind (s : σ) (f : σ → m α) : + (do set s; let s' ← get; f s') = (do set s; f s) := by + rw [← bind_assoc, set_bind_get, bind_assoc, pure_bind] + +@[simp] theorem set_bind_map_get (f : σ → α) (s : σ) : + (do set (m := m) s; f <$> get) = (do set (m := m) s; pure (f s)) := by + simp [map_eq_pure_bind, -bind_pure_comp] + +@[simp] theorem set_bind_set_bind (s s' : σ) (mx : m α) : + (do set s; set s'; mx) = (do set s'; mx) := by + rw [← bind_assoc, set_bind_set] + +@[simp] theorem set_bind_map_set (s s' : σ) (f : PUnit → α) : + (do set (m := m) s; f <$> set s') = (do f <$> set s') := by + simp [map_eq_pure_bind, ← bind_assoc, -bind_pure_comp] + +section modify + +theorem modifyGetThe_eq (f : σ → α × σ) : + modifyGetThe σ (m := m) f = do let z ← f <$> get; set z.2; return z.1 := modifyGet_eq f + +theorem modify_eq (f : σ → σ) : + modify (m := m) f = (do set (f (← get))) := by simp [modify, modifyGet_eq] + +theorem modifyThe_eq (f : σ → σ) : + modifyThe σ (m := m) f = (do set (f (← get))) := modify_eq f + +theorem getModify_eq (f : σ → σ) : + getModify (m := m) f = do let s ← get; set (f s); return s := by + rw [getModify, modifyGet_eq, bind_map_left] + +/-- Version of `modifyGet_eq` that preserves an call to `modify`. -/ +theorem modifyGet_eq' (f : σ → α × σ) : + modifyGet (m := m) f = do let s ← get; modify (Prod.snd ∘ f); return (f s).fst := by + simp [modify_eq, modifyGet_eq] + +@[simp] theorem modify_id : modify (m := m) id = pure PUnit.unit := by + simp [modify_eq] + +@[simp] theorem getModify_id : getModify (m := m) id = get := by + simp [getModify_eq] + +@[simp] theorem set_bind_modify (s : σ) (f : σ → σ) : + (do set (m := m) s; modify f) = set (f s) := by simp [modify_eq] + +@[simp] theorem set_bind_modify_bind (s : σ) (f : σ → σ) (mx : PUnit → m α) : + (do set s; let u ← modify f; mx u) = (do set (f s); mx PUnit.unit) := by + simp [modify_eq, ← bind_assoc] + +@[simp] theorem set_bind_modifyGet (s : σ) (f : σ → α × σ) : + (do set (m := m) s; modifyGet f) = (do set (f s).2; return (f s).1) := by simp [modifyGet_eq] + +@[simp] theorem set_bind_modifyGet_bind (s : σ) (f : σ → α × σ) (mx : α → m β) : + (do set s; let x ← modifyGet f; mx x) = (do set (f s).2; mx (f s).1) := by simp [modifyGet_eq] + +@[simp] theorem set_bind_getModify (s : σ) (f : σ → σ) : + (do set (m := m) s; getModify f) = (do set (f s); return s) := by simp [getModify_eq] + +@[simp] theorem set_bind_getModify_bind (s : σ) (f : σ → σ) (mx : σ → m α) : + (do set s; let x ← getModify f; mx x) = (do set (f s); mx s) := by + simp [getModify_eq, ← bind_assoc] + +@[simp] theorem modify_bind_modify (f g : σ → σ) : + (do modify (m := m) f; modify g) = modify (g ∘ f) := by simp [modify_eq] + +@[simp] theorem modify_bind_modifyGet (f : σ → σ) (g : σ → α × σ) : + (do modify (m := m) f; modifyGet g) = modifyGet (g ∘ f) := by + simp [modify_eq, modifyGet_eq] + +@[simp] theorem getModify_bind_modify (f : σ → σ) (g : σ → σ → σ) : + (do let s ← getModify (m := m) f; modify (g s)) = + (do let s ← get; modify (g s ∘ f)) := by + simp [modify_eq, getModify_eq] + +theorem modify_comm_of_comp_comm {f g : σ → σ} (h : f ∘ g = g ∘ f) : + (do modify (m := m) f; modify g) = (do modify (m := m) g; modify f) := by + simp [modify_bind_modify, h] + +theorem modify_bind_get (f : σ → σ) : + (do modify (m := m) f; get) = (do let s ← get; modify f; return (f s)) := by + simp [modify_eq] + +end modify + +/-- `StateT` has lawful state operations if the underlying monad is lawful. +This is applied for `StateM` as well due to the reducibility of that definition. -/ +instance {m σ} [Monad m] [LawfulMonad m] : LawfulMonadStateOf σ (StateT σ m) where + modifyGet_eq f := StateT.ext fun s => by simp + get_bind_const mx := StateT.ext fun s => by simp + get_bind_get_bind mx := StateT.ext fun s => by simp + get_bind_set_bind mx := StateT.ext fun s => by simp + set_bind_get s := StateT.ext fun s => by simp + set_bind_set s s' := StateT.ext fun s => by simp + +/-- The continuation passing state monad variant `StateCpsT` always has lawful state instance. -/ +instance {σ m} : LawfulMonadStateOf σ (StateCpsT σ m) where + modifyGet_eq _ := rfl + get_bind_const _ := rfl + get_bind_get_bind _ := rfl + get_bind_set_bind _ := rfl + set_bind_get _ := rfl + set_bind_set _ _ := rfl + +/-- The `EStateM` monad always has a lawful state instance. -/ +instance {σ ε} : LawfulMonadStateOf σ (EStateM ε σ) where + modifyGet_eq _ := rfl + get_bind_const _ := rfl + get_bind_get_bind _ := rfl + get_bind_set_bind _ := rfl + set_bind_get _ := rfl + set_bind_set _ _ := rfl + +/-- If the underlying monad `m` has a lawful state instance, then the induced state instance on +`ReaderT ρ m` will also be lawful. -/ +instance {m σ ρ} [Monad m] [LawfulMonad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] : + LawfulMonadStateOf σ (ReaderT ρ m) where + modifyGet_eq f := ReaderT.ext fun ctx => by + simp [← liftM_modifyGet, LawfulMonadStateOf.modifyGet_eq, ← liftM_get] + get_bind_const mx := ReaderT.ext fun ctx => by + simp [← liftM_modifyGet, ← liftM_get] + get_bind_get_bind mx := ReaderT.ext fun ctx => by + simp [← liftM_modifyGet, ← liftM_get] + get_bind_set_bind mx := ReaderT.ext fun ctx => by + simp [← liftM_modifyGet, ← liftM_get, ← liftM_set] + set_bind_get s := ReaderT.ext fun ctx => by + simp [← liftM_modifyGet, ← liftM_get, ← liftM_set] + set_bind_set s s' := ReaderT.ext fun ctx => by + simp [← liftM_modifyGet, ← liftM_get, ← liftM_set] + +instance {m ω σ} [Monad m] [LawfulMonad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] : + LawfulMonadStateOf σ (StateRefT' ω σ m) := + inferInstanceAs (LawfulMonadStateOf σ (ReaderT _ _)) diff --git a/Batteries/Control/OptionT.lean b/Batteries/Control/OptionT.lean index 7654c2dc47..f2aa125a8b 100644 --- a/Batteries/Control/OptionT.lean +++ b/Batteries/Control/OptionT.lean @@ -5,6 +5,7 @@ Authors: Sebastian Ullrich -/ import Batteries.Control.Lemmas +import Batteries.Control.LawfulMonadState /-! # Lemmas About Option Monad Transformer @@ -74,4 +75,13 @@ instance (m) [Monad m] [LawfulMonad m] : LawfulMonad (OptionT m) := @[simp] theorem run_monadMap {n} [MonadFunctorT n m] (f : ∀ {α}, n α → n α) : (monadMap (@f) x : OptionT m α).run = monadMap (@f) x.run := rfl +instance [Monad m] [LawfulMonad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] : + LawfulMonadStateOf σ (OptionT m) where + modifyGet_eq f := by simp [← liftM_modifyGet, ← liftM_get, LawfulMonadStateOf.modifyGet_eq] + get_bind_const mx := OptionT.ext (by simp [← liftM_get]) + get_bind_get_bind mx := OptionT.ext (by simp [← liftM_get]) + get_bind_set_bind mx := OptionT.ext (by simp [← liftM_get, ← liftM_set]) + set_bind_get s := OptionT.ext (by simp [← liftM_get, ← liftM_set]) + set_bind_set s s' := OptionT.ext (by simp [← liftM_get, ← liftM_set]) + end OptionT From 1ea61e713d5fac9c33b019d4e3612a86c6b4b48b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Wed, 23 Jul 2025 06:19:49 -0400 Subject: [PATCH 12/31] feat: add ASCII character casing lemmas (#1333) --- Batteries/Data/Char.lean | 148 +++++++++++++++++++++++++++++++++++++-- 1 file changed, 144 insertions(+), 4 deletions(-) diff --git a/Batteries/Data/Char.lean b/Batteries/Data/Char.lean index d623e2117c..d48151b11c 100644 --- a/Batteries/Data/Char.lean +++ b/Batteries/Data/Char.lean @@ -1,10 +1,10 @@ /- Copyright (c) 2022 Jannis Limperg. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jannis Limperg +Authors: Jannis Limperg, François G. Dorais -/ import Batteries.Data.UInt -import Batteries.Tactic.Alias +import Batteries.Tactic.Basic namespace Char @@ -14,5 +14,145 @@ theorem le_antisymm_iff {x y : Char} : x = y ↔ x ≤ y ∧ y ≤ x := instance : Batteries.LawfulOrd Char := .compareOfLessAndEq (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt Char.le_antisymm -@[simp] theorem toNat_ofNatAux (n : Nat) (h : n.isValidChar) : - (Char.ofNatAux n h).toNat = n := rfl +@[simp] theorem toNat_val (c : Char) : c.val.toNat = c.toNat := rfl + +@[simp] theorem toNat_ofNatAux {n : Nat} (h : n.isValidChar) : toNat (ofNatAux n h) = n := by + simp [ofNatAux, toNat] + +theorem toNat_ofNat (n : Nat) : toNat (ofNat n) = if n.isValidChar then n else 0 := by + split + · simp [ofNat, *] + · simp [ofNat, toNat, *] + +/-! ## Lemmas for ASCII-casing + +These facts apply for ASCII characters only. Recall that `isAlpha`, `isLower`, `isUpper`, `toLower`, +`toUpper` do not consider characters outside the ASCII character range (code points less than 128). +-/ + +theorem not_isLower_of_isUpper {c : Char} : c.isUpper → ¬ c.isLower := by + simp only [isUpper, ge_iff_le, UInt32.le_iff_toNat_le, UInt32.reduceToNat, toNat_val, + Bool.and_eq_true, decide_eq_true_eq, isLower, not_and, Nat.not_le, and_imp] + omega + +theorem not_isUpper_of_isLower {c : Char} : c.isLower → ¬ c.isUpper := by + simp only [isUpper, ge_iff_le, UInt32.le_iff_toNat_le, UInt32.reduceToNat, toNat_val, + Bool.and_eq_true, decide_eq_true_eq, isLower, not_and, Nat.not_le, and_imp] + omega + +theorem toLower_eq_of_not_isUpper {c : Char} (h : ¬ c.isUpper) : c.toLower = c := by + simp only [isUpper, ge_iff_le, Bool.and_eq_true, decide_eq_true_eq, not_and] at h + simp only [toLower, ge_iff_le, ite_eq_right_iff, and_imp] + intro h65 h90 + absurd h h65 + exact h90 + +theorem toLower_eq_of_isUpper {c : Char} (h : c.isUpper) : c.toLower = ofNat (c.toNat + 32) := by + simp only [isUpper, ge_iff_le, Bool.and_eq_true, decide_eq_true_eq] at h + simp only [toLower, ge_iff_le, ite_eq_left_iff] + intro; contradiction + +theorem toUpper_eq_of_not_isLower {c : Char} (h : ¬ c.isLower) : c.toUpper = c := by + simp only [isLower, ge_iff_le, Bool.and_eq_true, decide_eq_true_eq, not_and] at h + simp only [toUpper, ge_iff_le, ite_eq_right_iff, and_imp] + intro h97 h122 + absurd h h97 + exact h122 + +theorem toUpper_eq_of_isLower {c : Char} (h : c.isLower) : c.toUpper = ofNat (c.toNat - 32) := by + simp only [isLower, ge_iff_le, Bool.and_eq_true, decide_eq_true_eq] at h + simp only [toUpper, ge_iff_le, ite_eq_left_iff] + intro; contradiction + +@[simp] theorem isUpper_toLower_eq_false (c : Char) : c.toLower.isUpper = false := by + simp only [isUpper, toLower, ge_iff_le, UInt32.le_iff_toNat_le, UInt32.reduceToNat, toNat_val, + Bool.and_eq_false_imp, decide_eq_true_eq, decide_eq_false_iff_not, Nat.not_le] + intro h + split at h + · next h' => + rw [if_pos h'] + have : (c.toNat + 32).isValidChar := by omega + simp only [toNat_ofNat, ↓reduceIte, gt_iff_lt, *] + omega + · next h' => + rw [if_neg h'] + omega + +@[simp] theorem isLower_toUpper_eq_false (c : Char) : c.toUpper.isLower = false := by + simp only [isLower, toUpper, ge_iff_le, UInt32.le_iff_toNat_le, UInt32.reduceToNat, toNat_val, + Bool.and_eq_false_imp, decide_eq_true_eq, decide_eq_false_iff_not, Nat.not_le] + intro h + split at h + · next h' => + rw [if_pos h'] + have : (c.toNat - 32).isValidChar := by omega + simp [toNat_ofNat, *] at h ⊢ + omega + · next h' => + rw [if_neg h'] + omega + +@[simp] theorem isLower_toLower_eq_isAlpha (c : Char) : c.toLower.isLower = c.isAlpha := by + rw [Bool.eq_iff_iff] + by_cases h : c.isUpper + · simp only [isLower, h, toLower_eq_of_isUpper, ge_iff_le, UInt32.le_iff_toNat_le, + UInt32.reduceToNat, toNat_val, Bool.and_eq_true, decide_eq_true_eq, isAlpha, Bool.true_or, + iff_true] + simp only [isUpper, ge_iff_le, UInt32.le_iff_toNat_le, UInt32.reduceToNat, toNat_val, + Bool.and_eq_true, decide_eq_true_eq] at h + have : (c.toNat + 32).isValidChar := by omega + simp [toNat_ofNat, *] + · simp [toLower_eq_of_not_isUpper, isAlpha, h] + +@[simp] theorem isUpper_toUpper_eq_isAlpha (c : Char) : c.toUpper.isUpper = c.isAlpha := by + rw [Bool.eq_iff_iff] + by_cases h : c.isLower + · simp only [isUpper, h, toUpper_eq_of_isLower, ge_iff_le, UInt32.le_iff_toNat_le, + UInt32.reduceToNat, toNat_val, Bool.and_eq_true, decide_eq_true_eq, isAlpha, Bool.or_true, + iff_true] + simp only [isLower, ge_iff_le, UInt32.le_iff_toNat_le, UInt32.reduceToNat, toNat_val, + Bool.and_eq_true, decide_eq_true_eq] at h + have : (c.toNat - 32).isValidChar := by omega + have : 32 ≤ c.toNat := by omega + simp [toNat_ofNat, Nat.le_sub_iff_add_le, *] + · simp [toUpper_eq_of_not_isLower, isAlpha, h] + +@[simp] theorem isAlpha_toLower_eq_isAlpha (c : Char) : c.toLower.isAlpha = c.isAlpha := by + simp [isAlpha] + +@[simp] theorem isAlpha_toUpper_eq_isAlpha (c : Char) : c.toUpper.isAlpha = c.isAlpha := by + simp [isAlpha] + +@[simp] theorem toLower_toLower_eq_toLower (c : Char) : c.toLower.toLower = c.toLower := by + simp [toLower_eq_of_not_isUpper] + +@[simp] theorem toLower_toUpper_eq_toLower (c : Char) : c.toUpper.toLower = c.toLower := by + by_cases hl : c.isLower + · have hu : ¬ c.isUpper := not_isUpper_of_isLower hl + have hu' : c.toUpper.isUpper := by simp [isAlpha, hl] + have hv : (c.toNat - 32).isValidChar := by + simp only [isLower, ge_iff_le, UInt32.le_iff_toNat_le, UInt32.reduceToNat, toNat_val, + Bool.and_eq_true, decide_eq_true_eq, isUpper, not_and, Nat.not_le] at hl hu + omega + have h : 32 ≤ c.toNat := by + simp only [isLower, ge_iff_le, UInt32.le_iff_toNat_le, UInt32.reduceToNat, toNat_val, + Bool.and_eq_true, decide_eq_true_eq, isUpper, not_and, Nat.not_le] at hl hu + omega + rw [toLower_eq_of_isUpper hu', toUpper_eq_of_isLower hl, toLower_eq_of_not_isUpper hu, + toNat_ofNat, if_pos hv, Nat.sub_add_cancel h, ofNat_toNat] + · rw [toUpper_eq_of_not_isLower hl] + +@[simp] theorem toUpper_toUpper_eq_toUpper (c : Char) : c.toUpper.toUpper = c.toUpper := by + simp [toUpper_eq_of_not_isLower] + +@[simp] theorem toUpper_toLower_eq_toUpper (c : Char) : c.toLower.toUpper = c.toUpper := by + by_cases hu : c.isUpper + · have hl : ¬ c.isLower := not_isLower_of_isUpper hu + have hl' : c.toLower.isLower := by simp [isAlpha, hu] + have hv : (c.toNat + 32).isValidChar := by + simp only [isUpper, ge_iff_le, UInt32.le_iff_toNat_le, UInt32.reduceToNat, toNat_val, + Bool.and_eq_true, decide_eq_true_eq, isLower, not_and, Nat.not_le] at hu hl + omega + rw [toUpper_eq_of_isLower hl', toLower_eq_of_isUpper hu, toUpper_eq_of_not_isLower hl, + toNat_ofNat, if_pos hv, Nat.add_sub_cancel, ofNat_toNat] + · rw [toLower_eq_of_not_isUpper hu] From 0ffd63586aef157af6707bbfa77491db45e461fa Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Fri, 8 Aug 2025 20:12:49 -0400 Subject: [PATCH 13/31] fix: review comments --- Batteries/Data/Fin/Basic.lean | 8 ++++---- Batteries/Data/Fin/Coding.lean | 37 +++++++++++++++++++++------------- Batteries/Data/Fin/Lemmas.lean | 16 +++++++-------- 3 files changed, 35 insertions(+), 26 deletions(-) diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean index 0d22555f47..7cdbbd12ca 100644 --- a/Batteries/Data/Fin/Basic.lean +++ b/Batteries/Data/Fin/Basic.lean @@ -87,16 +87,16 @@ This is the dependent version of `Fin.foldl`. -/ dfoldlM (m := Id) n α f init /-- Sum of a list indexed by `Fin n`. -/ -protected def sum [OfNat α (nat_lit 0)] [Add α] (x : Fin n → α) : α := +protected def sum [Zero α] [Add α] (x : Fin n → α) : α := foldr n (x · + ·) 0 /-- Product of a list indexed by `Fin n`. -/ -protected def prod [OfNat α (nat_lit 1)] [Mul α] (x : Fin n → α) : α := +protected def prod [One α] [Mul α] (x : Fin n → α) : α := foldr n (x · * ·) 1 /-- Count the number of true values of a decidable predicate on `Fin n`. -/ -protected def count (P : Fin n → Prop) [DecidablePred P] : Nat := - Fin.sum (if P · then 1 else 0) +protected def count (p : Fin n → Bool) : Nat := + Fin.sum (Bool.toNat ∘ p) /-- `findSome? f` returns `f i` for the first `i` for which `f i` is `some _`, or `none` if no such diff --git a/Batteries/Data/Fin/Coding.lean b/Batteries/Data/Fin/Coding.lean index 08ed3bc728..f65b54a57b 100644 --- a/Batteries/Data/Fin/Coding.lean +++ b/Batteries/Data/Fin/Coding.lean @@ -50,8 +50,13 @@ def encodeBool : Bool → Fin 2 | false => rfl | true => rfl -/-- Encode a character value as a `Fin` type. -/ +/-- Encode a character value as a `Fin` type. + +Valid character code points range from 0 to 1114112 (U+10FFFF) excluding the surrogate range from +55296 (U+D800) to 57343 (U+DFFF). This results in 1112064 valid code points. +-/ def encodeChar (c : Char) : Fin 1112064 := + /- -/ have : c.toNat < 1114112 := match c.valid with | .inl h => Nat.lt_trans h (by decide) @@ -61,7 +66,11 @@ def encodeChar (c : Char) : Fin 1112064 := else ⟨c.toNat - 2048, by omega⟩ -/-- Decode a character value as a `Fin` type. -/ +/-- Decode a character value as a `Fin` type. + +Valid character code points range from 0 to 1114112 (U+10FFFF) excluding the surrogate range from +55296 (U+D800) to 57343 (U+DFFF). This results in 1112064 valid code points. +-/ @[pp_nodot] def decodeChar (i : Fin 1112064) : Char := if h : i.val < 55296 then Char.ofNatAux i.val (by omega) @@ -194,11 +203,11 @@ where /-- Encode a dependent sum of `Fin` types. -/ def encodeSigma (f : Fin n → Nat) (x : (i : Fin n) × Fin (f i)) : Fin (Fin.sum f) := match n, f, x with - | _+1, _, ⟨0, j⟩ => - ⟨j, Nat.lt_of_lt_of_le j.is_lt (sum_succ .. ▸ Nat.le_add_right ..)⟩ + | _+1, f, ⟨0, j⟩ => + ⟨j, Nat.lt_of_lt_of_le j.is_lt (sum_succ f .. ▸ Nat.le_add_right ..)⟩ | _+1, f, ⟨⟨i+1, hi⟩, j⟩ => match encodeSigma ((f ∘ succ)) ⟨⟨i, Nat.lt_of_succ_lt_succ hi⟩, j⟩ with - | ⟨k, hk⟩ => ⟨f 0 + k, sum_succ .. ▸ Nat.add_lt_add_left hk ..⟩ + | ⟨k, hk⟩ => ⟨f 0 + k, sum_succ f .. ▸ Nat.add_lt_add_left hk ..⟩ /-- Decode a dependent sum of `Fin` types. -/ @[pp_nodot] def decodeSigma (f : Fin n → Nat) (x : Fin (Fin.sum f)) : (i : Fin n) × Fin (f i) := @@ -366,37 +375,37 @@ def decodePi (f : Fin n → Nat) (x : Fin (Fin.prod f)) : (i : Fin n) → Fin (f /-- Encode a decidable subtype of a `Fin` type. -/ def encodeSubtype (P : Fin n → Prop) [inst : DecidablePred P] (i : { i // P i }) : - Fin (Fin.count P) := + Fin (Fin.count (P ·)) := match n, P, inst, i with | n+1, P, inst, ⟨0, hp⟩ => - have : Fin.count P > 0 := by simp [count_succ, hp] + have : Fin.count (P ·) > 0 := by simp [count_succ, hp] ⟨0, this⟩ | n+1, P, inst, ⟨⟨i+1, hi⟩, hp⟩ => match encodeSubtype (fun i => P i.succ) ⟨⟨i, Nat.lt_of_succ_lt_succ hi⟩, hp⟩ with | ⟨k, hk⟩ => if h0 : P 0 then - have : (Fin.count fun i => P i.succ) + 1 = Fin.count P := by - simp +arith only [count_succ, Function.comp_def, if_pos h0] + have : (Fin.count fun i => P i.succ) + 1 = Fin.count (P ·) := by + simp +arith only [count_succ, Function.comp_def, if_pos (decide_eq_true h0)] Fin.cast this ⟨k+1, Nat.succ_lt_succ hk⟩ else - have : (Fin.count fun i => P i.succ) = Fin.count P := by simp [count_succ, h0] + have : (Fin.count fun i => P i.succ) = Fin.count (P ·) := by simp [count_succ, h0] Fin.cast this ⟨k, hk⟩ /-- Decode a decidable subtype of a `Fin` type. -/ -def decodeSubtype (P : Fin n → Prop) [inst : DecidablePred P] (k : Fin (Fin.count P)) : +def decodeSubtype (P : Fin n → Prop) [inst : DecidablePred P] (k : Fin (Fin.count (P ·))) : { i // P i } := match n, P, inst, k with | 0, _, _, ⟨_, h⟩ => False.elim (by simp at h) | n+1, P, inst, ⟨k, hk⟩ => if h0 : P 0 then - have : Fin.count P = (Fin.count fun i => P i.succ) + 1 := by simp [count_succ, h0] + have : Fin.count (P ·) = (Fin.count fun i => P i.succ) + 1 := by simp [count_succ, h0] match k with | 0 => ⟨0, h0⟩ | k + 1 => match decodeSubtype (fun i => P i.succ) ⟨k, Nat.lt_of_add_lt_add_right (this ▸ hk)⟩ with | ⟨⟨i, hi⟩, hp⟩ => ⟨⟨i+1, Nat.succ_lt_succ hi⟩, hp⟩ else - have : Fin.count P = Fin.count fun i => P i.succ := by simp [count_succ, h0] + have : Fin.count (P ·) = Fin.count fun i => P i.succ := by simp [count_succ, h0] match decodeSubtype (fun i => P (succ i)) ⟨k, this ▸ hk⟩ with | ⟨⟨i, hi⟩, hp⟩ => ⟨⟨i+1, Nat.succ_lt_succ hi⟩, hp⟩ @@ -415,7 +424,7 @@ theorem encodeSubtype_succ_neg {P : Fin (n+1) → Prop} [DecidablePred P] (h₀ ext; rw [encodeSubtype.eq_def]; simp [Fin.succ, *] @[simp] theorem encodeSubtype_decodeSubtype (P : Fin n → Prop) [DecidablePred P] - (x : Fin (Fin.count P)) : encodeSubtype P (decodeSubtype P x) = x := by + (x : Fin (Fin.count (P ·))) : encodeSubtype P (decodeSubtype P x) = x := by induction n with | zero => absurd x.is_lt; simp | succ n ih => diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean index bccc6eadf9..9cabc4da9a 100644 --- a/Batteries/Data/Fin/Lemmas.lean +++ b/Batteries/Data/Fin/Lemmas.lean @@ -17,34 +17,34 @@ attribute [norm_cast] val_last /-! ### sum -/ -@[simp] theorem sum_zero [OfNat α (nat_lit 0)] [Add α] (x : Fin 0 → α) : +@[simp] theorem sum_zero [Zero α] [Add α] (x : Fin 0 → α) : Fin.sum x = 0 := by simp [Fin.sum] -theorem sum_succ [OfNat α (nat_lit 0)] [Add α] (x : Fin (n + 1) → α) : +theorem sum_succ [Zero α] [Add α] (x : Fin (n + 1) → α) : Fin.sum x = x 0 + Fin.sum (x ∘ Fin.succ) := by simp [Fin.sum, foldr_succ] /-! ### prod -/ -@[simp] theorem prod_zero [OfNat α (nat_lit 1)] [Mul α] (x : Fin 0 → α) : +@[simp] theorem prod_zero [One α] [Mul α] (x : Fin 0 → α) : Fin.prod x = 1 := by simp [Fin.prod] -theorem prod_succ [OfNat α (nat_lit 1)] [Mul α] (x : Fin (n + 1) → α) : +theorem prod_succ [One α] [Mul α] (x : Fin (n + 1) → α) : Fin.prod x = x 0 * Fin.prod (x ∘ Fin.succ) := by simp [Fin.prod, foldr_succ] /-! ### count -/ -@[simp] theorem count_zero (P : Fin 0 → Prop) [DecidablePred P] : Fin.count P = 0 := by +@[simp] theorem count_zero (p : Fin 0 → Bool) : Fin.count p = 0 := by simp [Fin.count] -theorem count_succ (P : Fin (n + 1) → Prop) [DecidablePred P] : Fin.count P = - if P 0 then Fin.count (fun i => P i.succ) + 1 else Fin.count (fun i => P i.succ) := by +theorem count_succ (p : Fin (n + 1) → Bool) : Fin.count p = + if p 0 then Fin.count (fun i => p i.succ) + 1 else Fin.count (fun i => p i.succ) := by split <;> simp [Fin.count, Fin.sum_succ, Nat.one_add, Function.comp_def, *] -theorem count_le (P : Fin n → Prop) [DecidablePred P] : Fin.count P ≤ n := by +theorem count_le (p : Fin n → Bool) : Fin.count p ≤ n := by induction n with | zero => simp | succ n ih => From d751a0aa7fbe698480a4473515a127ba81fdee3a Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Fri, 8 Aug 2025 20:30:30 -0400 Subject: [PATCH 14/31] chore: cleanup simps --- Batteries/Data/Fin/Coding.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Batteries/Data/Fin/Coding.lean b/Batteries/Data/Fin/Coding.lean index f65b54a57b..02b4361dad 100644 --- a/Batteries/Data/Fin/Coding.lean +++ b/Batteries/Data/Fin/Coding.lean @@ -198,7 +198,7 @@ where @[simp] theorem decodeProd_encodeProd (x : Fin m × Fin n) : decodeProd (encodeProd x) = x := by match x with | ⟨⟨_, _⟩, ⟨_, h⟩⟩ => simp [encodeProd, decodeProd, decodeProd.left, decodeProd.right, - Nat.mul_add_div (Nat.zero_lt_of_lt h), Nat.div_eq_of_lt h, Nat.mul_add_mod, Nat.mod_eq_of_lt h] + Nat.mul_add_div (Nat.zero_lt_of_lt h), Nat.div_eq_of_lt h, Nat.mod_eq_of_lt h] /-- Encode a dependent sum of `Fin` types. -/ def encodeSigma (f : Fin n → Nat) (x : (i : Fin n) × Fin (f i)) : Fin (Fin.sum f) := @@ -308,7 +308,7 @@ def encodeFun : {m : Nat} → (Fin m → Fin n) → Fin (n ^ m) | succ m ih => have hn : 0 < n := Nat.zero_lt_of_lt (x 0).is_lt split - · ext; simp [Nat.mul_add_mod, Nat.mod_eq_of_lt] + · ext; simp [Nat.mod_eq_of_lt] · next i hi => have : decodeFun (encodeFun fun k => x k.succ) ⟨i, Nat.lt_of_succ_lt_succ hi⟩ = x ⟨i+1, hi⟩ := by rw [ih]; rfl @@ -366,7 +366,7 @@ def decodePi (f : Fin n → Nat) (x : Fin (Fin.prod f)) : (i : Fin n) → Fin (f funext i simp only [decodePi] split - · simp [encodePi, Nat.mul_add_mod, Nat.mod_eq_of_lt (x 0).is_lt] + · simp [encodePi, Nat.mod_eq_of_lt (x 0).is_lt] · next i hi => have h : decodePi (f ∘ succ) (encodePi (f ∘ succ) fun i => x i.succ) ⟨i, Nat.lt_of_succ_lt_succ hi⟩ = x ⟨i+1, hi⟩ := by rw [ih]; rfl @@ -385,7 +385,7 @@ def encodeSubtype (P : Fin n → Prop) [inst : DecidablePred P] (i : { i // P i | ⟨k, hk⟩ => if h0 : P 0 then have : (Fin.count fun i => P i.succ) + 1 = Fin.count (P ·) := by - simp +arith only [count_succ, Function.comp_def, if_pos (decide_eq_true h0)] + simp +arith only [count_succ, if_pos (decide_eq_true h0)] Fin.cast this ⟨k+1, Nat.succ_lt_succ hk⟩ else have : (Fin.count fun i => P i.succ) = Fin.count (P ·) := by simp [count_succ, h0] @@ -431,7 +431,7 @@ theorem encodeSubtype_succ_neg {P : Fin (n+1) → Prop} [DecidablePred P] (h₀ simp only [decodeSubtype] split · ext; split <;> simp [encodeSubtype_zero_pos, encodeSubtype, *]; done - · ext; simp [encodeSubtype, count_succ, *] + · ext; simp [encodeSubtype, *] @[simp] theorem decodeSubtype_encodeSubtype (P : Fin n → Prop) [DecidablePred P] (x : { x // P x}) : decodeSubtype P (encodeSubtype P x) = x := by From 7ecf87d634350c377e00886a87fa7de97a151970 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Sat, 9 Aug 2025 08:19:13 -0400 Subject: [PATCH 15/31] chore: cleanup --- Batteries/Data/Fin/Coding.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Batteries/Data/Fin/Coding.lean b/Batteries/Data/Fin/Coding.lean index 02b4361dad..2d99df694d 100644 --- a/Batteries/Data/Fin/Coding.lean +++ b/Batteries/Data/Fin/Coding.lean @@ -56,7 +56,6 @@ Valid character code points range from 0 to 1114112 (U+10FFFF) excluding the sur 55296 (U+D800) to 57343 (U+DFFF). This results in 1112064 valid code points. -/ def encodeChar (c : Char) : Fin 1112064 := - /- -/ have : c.toNat < 1114112 := match c.valid with | .inl h => Nat.lt_trans h (by decide) From a610da85c9356ecb5362c21d7bae54b241691d50 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Sun, 7 Sep 2025 22:21:13 -0400 Subject: [PATCH 16/31] fix: code review suggestions Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> --- Batteries/Data/Fin/Coding.lean | 71 +++++++++++++++------------------- Batteries/Data/Fin/Lemmas.lean | 17 ++++---- 2 files changed, 41 insertions(+), 47 deletions(-) diff --git a/Batteries/Data/Fin/Coding.lean b/Batteries/Data/Fin/Coding.lean index 2d99df694d..3a05ead519 100644 --- a/Batteries/Data/Fin/Coding.lean +++ b/Batteries/Data/Fin/Coding.lean @@ -9,6 +9,14 @@ import Batteries.Tactic.Basic import Batteries.Tactic.Trans import Batteries.Tactic.Lint +/-! # Coding recipes for `Fin` types + +This module collects encoding/decoding bijections to represent basic type constructors of `Fin` +types as `Fin` types. These functions implement the isomorphism `Option (Fin n) ≃ Fin (n+1)`, +`Fin m ⊕ Fin n ≃ Fin (m + n)`, `Fin m × Fin n ≃ Fin (m * n)`, ..., including, dependent sums, +dependent products, decidable subtypes and decidable quotients. +-/ + namespace Fin /-- Encode a unit value as a `Fin` type. -/ @@ -54,6 +62,7 @@ def encodeBool : Bool → Fin 2 Valid character code points range from 0 to 1114112 (U+10FFFF) excluding the surrogate range from 55296 (U+D800) to 57343 (U+DFFF). This results in 1112064 valid code points. +(See [unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).) -/ def encodeChar (c : Char) : Fin 1112064 := have : c.toNat < 1114112 := @@ -61,26 +70,27 @@ def encodeChar (c : Char) : Fin 1112064 := | .inl h => Nat.lt_trans h (by decide) | .inr h => h.right if _ : c.toNat < 55296 then - ⟨c.toNat, by omega⟩ + ⟨c.toNat, by grind⟩ else - ⟨c.toNat - 2048, by omega⟩ + ⟨c.toNat - 2048, by grind⟩ /-- Decode a character value as a `Fin` type. Valid character code points range from 0 to 1114112 (U+10FFFF) excluding the surrogate range from 55296 (U+D800) to 57343 (U+DFFF). This results in 1112064 valid code points. +(See [unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).) -/ @[pp_nodot] def decodeChar (i : Fin 1112064) : Char := if h : i.val < 55296 then - Char.ofNatAux i.val (by omega) + Char.ofNatAux i.val (by grind) else - Char.ofNatAux (i.val + 2048) (by omega) + Char.ofNatAux (i.val + 2048) (by grind) @[simp] theorem encodeChar_decodeChar (x) : encodeChar (decodeChar x) = x := by simp only [decodeChar, encodeChar] split · simp [*] - · have : ¬ x.val + 2048 < 55296 := by omega + · have : ¬ x.val + 2048 < 55296 := by grind simp [*] @[simp] theorem decodeChar_encodeChar (x) : decodeChar (encodeChar x) = x := by @@ -94,16 +104,16 @@ Valid character code points range from 0 to 1114112 (U+10FFFF) excluding the sur 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 + have h1 : ¬ x.toNat - 2048 < 55296 := by grind + have h2 : 2048 ≤ x.toNat := by grind simp only [dif_neg h1, Char.ofNatAux, Nat.sub_add_cancel h2]; rfl -/-- Decode an optional `Fin` types. -/ +/-- Decode an optional `Fin` type. -/ def encodeOption : Option (Fin n) → Fin (n+1) | none => 0 | some ⟨i, h⟩ => ⟨i+1, Nat.succ_lt_succ h⟩ -/-- Decode an optional `Fin` types. -/ +/-- Decode an optional `Fin` type. -/ @[pp_nodot] def decodeOption : Fin (n+1) → Option (Fin n) | 0 => none | ⟨i+1, h⟩ => some ⟨i, Nat.lt_of_succ_lt_succ h⟩ @@ -143,7 +153,7 @@ def encodeSum : Sum (Fin n) (Fin m) → Fin (n + m) if h : x < n then .inl ⟨x, h⟩ else - .inr ⟨x - n, by omega⟩ + .inr ⟨x - n, by grind⟩ @[simp] theorem encodeSum_decodeSum (x : Fin (n + m)) : encodeSum (decodeSum x) = x := by simp only [encodeSum, decodeSum] @@ -157,17 +167,17 @@ def encodeSum : Sum (Fin n) (Fin m) → Fin (n + m) · contradiction · next he => cases x; cases hd - simp at he ⊢; omega + simp at he ⊢; grind @[simp] theorem decodeSum_encodeSum (x : Sum (Fin n) (Fin m)) : decodeSum (encodeSum x) = x := by simp only [encodeSum, decodeSum] split · split · simp - · next h => simp only [coe_castLE] at h; omega + · next h => simp only [coe_castLE] at h; grind · split - · next h => simp only [coe_natAdd] at h; omega - · next x _ => cases x; simp only [natAdd_mk, Sum.inr.injEq, mk.injEq]; omega + · next h => simp only [coe_natAdd] at h; grind + · next x _ => cases x; simp only [natAdd_mk, Sum.inr.injEq, mk.injEq]; grind /-- Encode a product of `Fin` types. -/ def encodeProd : Fin m × Fin n → Fin (m * n) @@ -216,10 +226,7 @@ def encodeSigma (f : Fin n → Nat) (x : (i : Fin n) × Fin (f i)) : Fin (Fin.su if hx0 : x < f 0 then ⟨0, ⟨x, hx0⟩⟩ else - have hxf : x - f 0 < Fin.sum (f ∘ succ) := by - apply Nat.sub_lt_left_of_lt_add - · exact Nat.le_of_not_gt hx0 - · rw [← sum_succ]; exact hx + have hxf : x - f 0 < Fin.sum (f ∘ succ) := by grind [sum_succ] match decodeSigma ((f ∘ succ)) ⟨x - f 0, hxf⟩ with | ⟨⟨i, hi⟩, y⟩ => ⟨⟨i+1, Nat.succ_lt_succ hi⟩, y⟩ @@ -232,10 +239,7 @@ def encodeSigma (f : Fin n → Nat) (x : (i : Fin n) × Fin (f i)) : Fin (Fin.su split · rfl · next h1 => - have h2 : x - f 0 < Fin.sum (f ∘ succ) := by - apply Nat.sub_lt_left_of_lt_add - · exact Nat.le_of_not_gt h1 - · rw [← sum_succ]; exact x.is_lt + have h2 : x - f 0 < Fin.sum (f ∘ succ) := by grind [sum_succ] have : encodeSigma (f ∘ succ) (decodeSigma (f ∘ succ) ⟨x - f 0, h2⟩) = ↑x - f 0 := by rw [ih] ext; simp only [encodeSigma] @@ -252,10 +256,7 @@ def encodeSigma (f : Fin n → Nat) (x : (i : Fin n) × Fin (f i)) : Fin (Fin.su | ⟨⟨0, _⟩, x, hx⟩ => split · rfl - · next h => - absurd h - simp only [encodeSigma] - exact hx + · grind [encodeSigma] | ⟨⟨i+1, hi⟩, ⟨x, hx⟩⟩ => have : ¬ encodeSigma f ⟨⟨i+1, hi⟩, ⟨x, hx⟩⟩ < f 0 := by simp [encodeSigma] rw [dif_neg this] @@ -285,11 +286,7 @@ def encodeFun : {m : Nat} → (Fin m → Fin n) → Fin (n ^ m) @[pp_nodot] def decodeFun : {m : Nat} → Fin (n ^ m) → Fin m → Fin n | 0, _ => (nomatch .) | m+1, ⟨k, hk⟩ => - have hn : n > 0 := by - apply Nat.zero_lt_of_ne_zero - intro h - rw [h, Nat.pow_succ, Nat.mul_zero] at hk - contradiction + have hn : n > 0 := by grind fun | 0 => ⟨k % n, Nat.mod_lt k hn⟩ | ⟨i+1, hi⟩ => @@ -298,7 +295,7 @@ def encodeFun : {m : Nat} → (Fin m → Fin n) → Fin (n ^ m) @[simp] theorem encodeFun_decodeFun (x : Fin (n ^ m)) : encodeFun (decodeFun x) = x := by induction m with simp only [encodeFun, decodeFun, Fin.succ] - | zero => simp; omega + | zero => grind | succ m ih => cases x; simp [ih]; rw [← Fin.zero_eta, Nat.div_add_mod] @[simp] theorem decodeFun_encodeFun (x : Fin m → Fin n) : decodeFun (encodeFun x) = x := by @@ -320,8 +317,8 @@ def encodePi (f : Fin n → Nat) (x : (i : Fin n) → Fin (f i)) : Fin (Fin.prod | _+1, f, x => match encodePi ((f ∘ succ)) (fun ⟨i, hi⟩ => x ⟨i+1, Nat.succ_lt_succ hi⟩) with | ⟨k, hk⟩ => Fin.mk (f 0 * k + (x 0).val) $ calc - _ < f 0 * k + f 0 := Nat.add_lt_add_left (x 0).isLt .. - _ = f 0 * (k + 1) := Nat.mul_succ .. + _ < f 0 * k + f 0 := by grind + _ = f 0 * (k + 1) := by grind _ ≤ f 0 * Fin.prod (f ∘ succ) := Nat.mul_le_mul_left _ (Nat.succ_le_of_lt hk) _ = Fin.prod f := Eq.symm <| prod_succ .. @@ -330,11 +327,7 @@ def decodePi (f : Fin n → Nat) (x : Fin (Fin.prod f)) : (i : Fin n) → Fin (f match n, f, x with | 0, _, _ => (nomatch ·) | n+1, f, ⟨x, hx⟩ => - have h : f 0 > 0 := by - apply Nat.zero_lt_of_ne_zero - intro h - rw [prod_succ, h, Nat.zero_mul] at hx - contradiction + have h : f 0 > 0 := by grind [prod_succ] have : x / f 0 < Fin.prod (f ∘ succ) := by rw [Nat.div_lt_iff_lt_mul h, Nat.mul_comm, ← prod_succ] exact hx diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean index 267be9302e..a074095ed9 100644 --- a/Batteries/Data/Fin/Lemmas.lean +++ b/Batteries/Data/Fin/Lemmas.lean @@ -24,6 +24,12 @@ theorem sum_succ [Zero α] [Add α] (x : Fin (n + 1) → α) : Fin.sum x = x 0 + Fin.sum (x ∘ Fin.succ) := by simp [Fin.sum, foldr_succ] +theorem sum_eq_sum_map_finRange [Zero α] [Add α] (x : Fin n → α) : + Fin.sum x = (List.finRange n |>.map x).sum := by + simp [Fin.sum, List.sum] + rw [Fin.foldr_eq_finRange_foldr] + rw [List.foldr_map] + /-! ### prod -/ @[simp] theorem prod_zero [One α] [Mul α] (x : Fin 0 → α) : @@ -36,21 +42,16 @@ theorem prod_succ [One α] [Mul α] (x : Fin (n + 1) → α) : /-! ### count -/ -@[simp] theorem count_zero (p : Fin 0 → Bool) : Fin.count p = 0 := by +@[simp, grind =] theorem count_zero (p : Fin 0 → Bool) : Fin.count p = 0 := by simp [Fin.count] theorem count_succ (p : Fin (n + 1) → Bool) : Fin.count p = if p 0 then Fin.count (fun i => p i.succ) + 1 else Fin.count (fun i => p i.succ) := by split <;> simp [Fin.count, Fin.sum_succ, Nat.one_add, Function.comp_def, *] +@[grind] theorem count_le (p : Fin n → Bool) : Fin.count p ≤ n := by - induction n with - | zero => simp - | succ n ih => - rw [count_succ] - split - · simp [ih] - · apply Nat.le_trans _ (Nat.le_succ n); simp [ih] + induction n with grind [count_succ] /-! ### findSome? -/ From cde1e230e70ef6c6eacf571ecf50abf1b7e135f3 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Mon, 8 Sep 2025 06:48:10 -0400 Subject: [PATCH 17/31] chore: cleanup docs --- Batteries/Data/Fin/Coding.lean | 121 ++++++++++++++++++++------------- 1 file changed, 74 insertions(+), 47 deletions(-) diff --git a/Batteries/Data/Fin/Coding.lean b/Batteries/Data/Fin/Coding.lean index 3a05ead519..6eabd310d3 100644 --- a/Batteries/Data/Fin/Coding.lean +++ b/Batteries/Data/Fin/Coding.lean @@ -9,7 +9,7 @@ import Batteries.Tactic.Basic import Batteries.Tactic.Trans import Batteries.Tactic.Lint -/-! # Coding recipes for `Fin` types +/-! # Low-level coding recipes for `Fin` types This module collects encoding/decoding bijections to represent basic type constructors of `Fin` types as `Fin` types. These functions implement the isomorphism `Option (Fin n) ≃ Fin (n+1)`, @@ -19,101 +19,128 @@ dependent products, decidable subtypes and decidable quotients. namespace Fin -/-- Encode a unit value as a `Fin` type. -/ -@[nolint unusedArguments] +/-- Encode `Empty` into `Fin 0`. -/ +def encodeEmpty : Empty → Fin 0 := (nomatch ·) + +/-- Decode `Empty` from `Fin 0`. -/ +def decodeEmpty : Fin 0 → Empty := (nomatch ·) + +@[simp] theorem encodeEmpty_decodeEmpty (x : Fin 0) : encodeEmpty (decodeEmpty x) = x := nomatch x + +@[simp] theorem decodeEmpty_encodeEmpty (x : Empty) : decodeEmpty (encodeEmpty x) = x := nomatch x + +/-- Encode `PUnit` into `Fin 1`. -/ +@[simp, nolint unusedArguments] def encodePUnit : PUnit → Fin 1 | .unit => 0 -/-- Decode a unit value as a `Fin` type. -/ -@[pp_nodot] def decodePUnit : Fin 1 → PUnit +/-- Decode `PUnit` from `Fin 1`. -/ +@[simp, pp_nodot] def decodePUnit : Fin 1 → PUnit | 0 => .unit -/-- Encode a unit value as a `Fin` type. -/ +/-- Encode `Unit` into `Fin 1`. -/ abbrev encodeUnit : Unit → Fin 1 := encodePUnit -/-- Decode a unit value as a `Fin` type. -/ +/-- Decode `Unit` from `Fin 1`. -/ @[pp_nodot] abbrev decodeUnit : Fin 1 → Unit := decodePUnit -@[simp] theorem encodePUnit_decodePUnit : (x : Fin 1) → encodePUnit (decodePUnit x) = x +theorem encodePUnit_decodePUnit : (x : Fin 1) → encodePUnit (decodePUnit x) = x | 0 => rfl -@[simp] theorem decodePUnit_encodePUnit : (x : PUnit) → decodePUnit (encodePUnit x) = x +theorem decodePUnit_encodePUnit : (x : PUnit) → decodePUnit (encodePUnit x) = x | .unit => rfl -/-- Encode a boolean value as a `Fin` type. -/ -def encodeBool : Bool → Fin 2 +/-- Encode `Bool` into `Fin 2`. -/ +@[simp] def encodeBool : Bool → Fin 2 | false => 0 | true => 1 -/-- Decode a boolean value as a `Fin` type. -/ -@[pp_nodot] def decodeBool : Fin 2 → Bool +/-- Decode `Bool` from `Fin 2`. -/ +@[simp, pp_nodot] def decodeBool : Fin 2 → Bool | 0 => false | 1 => true -@[simp] theorem encodeBool_decodeBool : (x : Fin 2) → encodeBool (decodeBool x) = x - | 0 => rfl - | 1 => rfl +theorem encodeBool_decodeBool : (x : Fin 2) → encodeBool (decodeBool x) = x + | 0 | 1 => rfl -@[simp] theorem decodeBool_encodeBool : (x : Bool) → decodeBool (encodeBool x) = x - | false => rfl - | true => rfl +theorem decodeBool_encodeBool : (x : Bool) → decodeBool (encodeBool x) = x + | false| true => rfl -/-- Encode a character value as a `Fin` type. +/-- Encode `Ordering` into `Fin 3`. -/ +@[simp] def encodeOrdering : Ordering → Fin 3 + | .eq => 0 + | .lt => 1 + | .gt => 2 -Valid character code points range from 0 to 1114112 (U+10FFFF) excluding the surrogate range from +/-- Decode `Ordering` from `Fin 3`. -/ +@[simp, pp_nodot] def decodeOrdering : Fin 3 → Ordering + | 0 => .eq + | 1 => .lt + | 2 => .gt + +theorem encodeOrdering_decodeOrdering : (x : Fin 3) → encodeOrdering (decodeOrdering x) = x + | 0 | 1 | 2 => rfl + +theorem decodeOrdering_encodeOrdering : + (x : Ordering) → decodeOrdering (encodeOrdering x) = x + | .eq | .lt | .gt => rfl + +/-- Encode `Char` into `Fin 1112064`. + +Valid character code points range from 0 to 1114111 (U+10FFFF) excluding the surrogate range from 55296 (U+D800) to 57343 (U+DFFF). This results in 1112064 valid code points. (See [unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).) -/ def encodeChar (c : Char) : Fin 1112064 := - have : c.toNat < 1114112 := + have : c.toNat < 0x110000 := match c.valid with | .inl h => Nat.lt_trans h (by decide) | .inr h => h.right - if _ : c.toNat < 55296 then + if _ : c.toNat < 0xD800 then ⟨c.toNat, by grind⟩ else - ⟨c.toNat - 2048, by grind⟩ + ⟨c.toNat - (0xE000 - 0xD800), by grind⟩ -/-- Decode a character value as a `Fin` type. +/-- Decode `Char` from `Fin 1112064`. Valid character code points range from 0 to 1114112 (U+10FFFF) excluding the surrogate range from 55296 (U+D800) to 57343 (U+DFFF). This results in 1112064 valid code points. (See [unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).) -/ @[pp_nodot] def decodeChar (i : Fin 1112064) : Char := - if h : i.val < 55296 then + if h : i.val < 0xD800 then Char.ofNatAux i.val (by grind) else - Char.ofNatAux (i.val + 2048) (by grind) + Char.ofNatAux (i.val + (0xE000 - 0xD800)) (by grind) @[simp] theorem encodeChar_decodeChar (x) : encodeChar (decodeChar x) = x := by simp only [decodeChar, encodeChar] split · simp [*] - · have : ¬ x.val + 2048 < 55296 := by grind + · have : ¬ x.val + (0xE000 - 0xD800) < 0xD800 := by grind simp [*] @[simp] theorem decodeChar_encodeChar (x) : decodeChar (encodeChar x) = x := by ext; simp only [decodeChar, encodeChar] split · simp only [Char.ofNatAux, Char.toNat]; rfl - · have h0 : 57344 ≤ x.toNat ∧ x.toNat < 1114112 := by + · have h0 : 0xE000 ≤ x.toNat ∧ x.toNat < 0x110000 := 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 grind - have h2 : 2048 ≤ x.toNat := by grind + have h1 : ¬ x.toNat - (0xE000 - 0xD800) < 0xD800 := by grind + have h2 : (0xE000 - 0xD800) ≤ x.toNat := by grind simp only [dif_neg h1, Char.ofNatAux, Nat.sub_add_cancel h2]; rfl -/-- Decode an optional `Fin` type. -/ +/-- Encode `Option (Fin n)` into `Fin (n+1)`. -/ def encodeOption : Option (Fin n) → Fin (n+1) | none => 0 | some ⟨i, h⟩ => ⟨i+1, Nat.succ_lt_succ h⟩ -/-- Decode an optional `Fin` type. -/ +/-- Decode `Option (Fin n)` from `Fin (n+1)`. -/ @[pp_nodot] def decodeOption : Fin (n+1) → Option (Fin n) | 0 => none | ⟨i+1, h⟩ => some ⟨i, Nat.lt_of_succ_lt_succ h⟩ @@ -143,12 +170,12 @@ def encodeOption : Option (Fin n) → Fin (n+1) · cases he · cases he; rfl -/-- Encode a sum of `Fin` types. -/ +/-- Encode `Fin n ⊕ Fin m` into `Fin (n + m)`. -/ def encodeSum : Sum (Fin n) (Fin m) → Fin (n + m) | .inl x => x.castLE (Nat.le_add_right _ _) | .inr x => x.natAdd n -/-- Decode a sum of `Fin` types. -/ +/-- Decode `Fin n ⊕ Fin m` from `Fin (n + m)`. -/ @[pp_nodot] def decodeSum (x : Fin (n + m)) : Sum (Fin n) (Fin m) := if h : x < n then .inl ⟨x, h⟩ @@ -179,7 +206,7 @@ def encodeSum : Sum (Fin n) (Fin m) → Fin (n + m) · next h => simp only [coe_natAdd] at h; grind · next x _ => cases x; simp only [natAdd_mk, Sum.inr.injEq, mk.injEq]; grind -/-- Encode a product of `Fin` types. -/ +/-- Encode `Fin m × Fin n` into `Fin (m * n)`. -/ def encodeProd : Fin m × Fin n → Fin (m * n) | (⟨i, hi⟩, ⟨j, hj⟩) => Fin.mk (n * i + j) <| calc _ < n * i + n := Nat.add_lt_add_left hj .. @@ -187,7 +214,7 @@ def encodeProd : Fin m × Fin n → Fin (m * n) _ ≤ n * m := Nat.mul_le_mul_left n (Nat.succ_le_of_lt hi) _ = m * n := Nat.mul_comm .. -/-- Decode a product of `Fin` types. -/ +/-- Decode `Fin m × Fin n` from `Fin (m * n)`. -/ @[pp_nodot] def decodeProd (z : Fin (m * n)) : Fin m × Fin n := ⟨left, right⟩ where @@ -209,7 +236,7 @@ where | ⟨⟨_, _⟩, ⟨_, h⟩⟩ => simp [encodeProd, decodeProd, decodeProd.left, decodeProd.right, Nat.mul_add_div (Nat.zero_lt_of_lt h), Nat.div_eq_of_lt h, Nat.mod_eq_of_lt h] -/-- Encode a dependent sum of `Fin` types. -/ +/-- Encode `(i : Fin n) × Fin (f i)` into `Fin (Fin.sum f)`. -/ def encodeSigma (f : Fin n → Nat) (x : (i : Fin n) × Fin (f i)) : Fin (Fin.sum f) := match n, f, x with | _+1, f, ⟨0, j⟩ => @@ -218,7 +245,7 @@ def encodeSigma (f : Fin n → Nat) (x : (i : Fin n) × Fin (f i)) : Fin (Fin.su match encodeSigma ((f ∘ succ)) ⟨⟨i, Nat.lt_of_succ_lt_succ hi⟩, j⟩ with | ⟨k, hk⟩ => ⟨f 0 + k, sum_succ f .. ▸ Nat.add_lt_add_left hk ..⟩ -/-- Decode a dependent sum of `Fin` types. -/ +/-- Decode `(i : Fin n) × Fin (f i)` from `Fin (Fin.sum f)`. -/ @[pp_nodot] def decodeSigma (f : Fin n → Nat) (x : Fin (Fin.sum f)) : (i : Fin n) × Fin (f i) := match n, f, x with | 0, _, ⟨_, h⟩ => False.elim (by simp at h) @@ -272,7 +299,7 @@ def encodeSigma (f : Fin n → Nat) (x : (i : Fin n) × Fin (f i)) : Fin (Fin.su congr · apply HEq.trans _ h.2; congr -/-- Encode a function between `Fin` types. -/ +/-- Encode `Fin m → Fin n` into `Fin (n ^ m)`. -/ def encodeFun : {m : Nat} → (Fin m → Fin n) → Fin (n ^ m) | 0, _ => ⟨0, by simp⟩ | m+1, f => Fin.mk (n * (encodeFun fun k => f k.succ).val + (f 0).val) <| calc @@ -282,7 +309,7 @@ def encodeFun : {m : Nat} → (Fin m → Fin n) → Fin (n ^ m) _ = n ^ m * n := Nat.mul_comm .. _ = n ^ (m+1) := Nat.pow_succ .. -/-- Decode a function between `Fin` types. -/ +/-- Decode `Fin m → Fin n` from `Fin (n ^ m)`. -/ @[pp_nodot] def decodeFun : {m : Nat} → Fin (n ^ m) → Fin m → Fin n | 0, _ => (nomatch .) | m+1, ⟨k, hk⟩ => @@ -310,7 +337,7 @@ def encodeFun : {m : Nat} → (Fin m → Fin n) → Fin (n ^ m) = x ⟨i+1, hi⟩ := by rw [ih]; rfl simp [← this, Nat.mul_add_div hn, Nat.div_eq_of_lt] -/-- Encode a dependent product of `Fin` types. -/ +/-- Encode `(i : Fin n) → Fin (f i)` into `Fin (Fin.prod f)`. -/ def encodePi (f : Fin n → Nat) (x : (i : Fin n) → Fin (f i)) : Fin (Fin.prod f) := match n, f, x with | 0, _, _ => ⟨0, by simp [Fin.prod]⟩ @@ -322,7 +349,7 @@ def encodePi (f : Fin n → Nat) (x : (i : Fin n) → Fin (f i)) : Fin (Fin.prod _ ≤ f 0 * Fin.prod (f ∘ succ) := Nat.mul_le_mul_left _ (Nat.succ_le_of_lt hk) _ = Fin.prod f := Eq.symm <| prod_succ .. -/-- Decode a dependent product of `Fin` types. -/ +/-- Decode `(i : Fin n) → Fin (f i)` from `Fin (Fin.prod f)`. -/ def decodePi (f : Fin n → Nat) (x : Fin (Fin.prod f)) : (i : Fin n) → Fin (f i) := match n, f, x with | 0, _, _ => (nomatch ·) @@ -365,7 +392,7 @@ def decodePi (f : Fin n → Nat) (x : Fin (Fin.prod f)) : (i : Fin n) → Fin (f conv => rhs; rw [← h] congr; simp [encodePi, Nat.mul_add_div h0, Nat.div_eq_of_lt (x 0).is_lt]; rfl -/-- Encode a decidable subtype of a `Fin` type. -/ +/-- Encode `{ i : Fin n // P i }` into `Fin (Fin.count P)` where `P` is a decidable predicate. -/ def encodeSubtype (P : Fin n → Prop) [inst : DecidablePred P] (i : { i // P i }) : Fin (Fin.count (P ·)) := match n, P, inst, i with @@ -383,7 +410,7 @@ def encodeSubtype (P : Fin n → Prop) [inst : DecidablePred P] (i : { i // P i have : (Fin.count fun i => P i.succ) = Fin.count (P ·) := by simp [count_succ, h0] Fin.cast this ⟨k, hk⟩ -/-- Decode a decidable subtype of a `Fin` type. -/ +/-- Decode `{ i : Fin n // P i }` from `Fin (Fin.count P)` where `P` is a decidable predicate. -/ def decodeSubtype (P : Fin n → Prop) [inst : DecidablePred P] (k : Fin (Fin.count (P ·))) : { i // P i } := match n, P, inst, k with @@ -510,7 +537,7 @@ theorem getRepr_eq_getRepr_of_equiv (s : Setoid (Fin n)) [DecidableRel s.r] (h : apply getRepr_eq_getRepr_of_equiv exact getRepr_equiv .. -/-- Encode decidable quotient of a `Fin` type. -/ +/-- Encode `Quotient s` into `Fin m` where `s` is a decidable setoid on `Fin n`. -/ def encodeQuotient (s : Setoid (Fin n)) [DecidableRel s.r] (x : Quotient s) : Fin (Fin.count fun i => getRepr s i = i) := encodeSubtype _ <| Quotient.liftOn x (fun i => ⟨getRepr s i, getRepr_getRepr s i⟩) <| by @@ -518,7 +545,7 @@ def encodeQuotient (s : Setoid (Fin n)) [DecidableRel s.r] (x : Quotient s) : simp only [Subtype.mk.injEq] exact getRepr_eq_getRepr_of_equiv s h -/-- Decode decidable quotient of a `Fin ` type. -/ +/-- Decode `Quotient s` from `Fin m` where `s` is a decidable setoid on `Fin n`. -/ def decodeQuotient (s : Setoid (Fin n)) [DecidableRel s.r] (i : Fin (Fin.count fun i => getRepr s i = i)) : Quotient s := Quotient.mk s (decodeSubtype _ i) From bb51c090de69534ed959585f4c134699c0e5dcf0 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Tue, 9 Sep 2025 09:54:53 -0400 Subject: [PATCH 18/31] feat: add `Char` constants --- Batteries/Data/Char/Basic.lean | 35 ++++++++++++++++++++++++++++++++ Batteries/Data/Fin/Coding.lean | 37 ++++++++-------------------------- 2 files changed, 43 insertions(+), 29 deletions(-) diff --git a/Batteries/Data/Char/Basic.lean b/Batteries/Data/Char/Basic.lean index d3e1a5acac..7dd762a202 100644 --- a/Batteries/Data/Char/Basic.lean +++ b/Batteries/Data/Char/Basic.lean @@ -23,3 +23,38 @@ theorem toNat_ofNat (n : Nat) : toNat (ofNat n) = if n.isValidChar then n else 0 split · simp [ofNat, *] · simp [ofNat, toNat, *] + +/-- +Maximum character code point. +(See [unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).) +-/ +protected abbrev max := 0x10FFFF + +/-- +Maximum surrogate code point. +(See [unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).) +-/ +protected abbrev maxSurrogate := 0xDFFF + +/-- +Minimum surrogate code point. +(See [unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).) +-/ +protected abbrev minSurrogate := 0xD800 + +/-- +Number of valid character code points. +(See [unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).) +-/ +protected abbrev count := Char.max - Char.maxSurrogate + Char.minSurrogate + +@[grind] theorem toNat_le_max (c : Char) : c.toNat ≤ Char.max := by + match c.valid with + | .inl h => simp only [toNat_val] at h; grind + | .inr ⟨_, h⟩ => simp only [toNat_val] at h; grind + +@[grind] theorem toNat_not_surrogate (c : Char) : + ¬(Char.minSurrogate ≤ c.toNat ∧ c.toNat ≤ Char.maxSurrogate) := by + match c.valid with + | .inl h => simp only [toNat_val] at h; grind + | .inr ⟨h, _⟩ => simp only [toNat_val] at h; grind diff --git a/Batteries/Data/Fin/Coding.lean b/Batteries/Data/Fin/Coding.lean index 6eabd310d3..cf23ed9480 100644 --- a/Batteries/Data/Fin/Coding.lean +++ b/Batteries/Data/Fin/Coding.lean @@ -85,30 +85,16 @@ theorem decodeOrdering_encodeOrdering : (x : Ordering) → decodeOrdering (encodeOrdering x) = x | .eq | .lt | .gt => rfl -/-- Encode `Char` into `Fin 1112064`. - -Valid character code points range from 0 to 1114111 (U+10FFFF) excluding the surrogate range from -55296 (U+D800) to 57343 (U+DFFF). This results in 1112064 valid code points. -(See [unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).) --/ -def encodeChar (c : Char) : Fin 1112064 := - have : c.toNat < 0x110000 := - match c.valid with - | .inl h => Nat.lt_trans h (by decide) - | .inr h => h.right +/-- Encode `Char` into `Fin Char.count`. -/ +def encodeChar (c : Char) : Fin Char.count := if _ : c.toNat < 0xD800 then ⟨c.toNat, by grind⟩ else ⟨c.toNat - (0xE000 - 0xD800), by grind⟩ -/-- Decode `Char` from `Fin 1112064`. - -Valid character code points range from 0 to 1114112 (U+10FFFF) excluding the surrogate range from -55296 (U+D800) to 57343 (U+DFFF). This results in 1112064 valid code points. -(See [unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).) --/ -@[pp_nodot] def decodeChar (i : Fin 1112064) : Char := - if h : i.val < 0xD800 then +/-- Decode `Char` from `Fin Char.count`. -/ +@[pp_nodot] def decodeChar (i : Fin Char.count) : Char := + if _ : i.val < 0xD800 then Char.ofNatAux i.val (by grind) else Char.ofNatAux (i.val + (0xE000 - 0xD800)) (by grind) @@ -124,16 +110,9 @@ Valid character code points range from 0 to 1114112 (U+10FFFF) excluding the sur ext; simp only [decodeChar, encodeChar] split · simp only [Char.ofNatAux, Char.toNat]; rfl - · have h0 : 0xE000 ≤ x.toNat ∧ x.toNat < 0x110000 := 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 - (0xE000 - 0xD800) < 0xD800 := by grind - have h2 : (0xE000 - 0xD800) ≤ x.toNat := by grind - simp only [dif_neg h1, Char.ofNatAux, Nat.sub_add_cancel h2]; rfl + · have : ¬ x.toNat - (0xE000 - 0xD800) < 0xD800 := by grind + have : (0xE000 - 0xD800) ≤ x.toNat := by grind + simp [Char.ofNatAux, *]; rfl /-- Encode `Option (Fin n)` into `Fin (n+1)`. -/ def encodeOption : Option (Fin n) → Fin (n+1) From 20b995d3afda30b8abfa0cec7228a459adaa79ef Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Tue, 9 Sep 2025 10:02:49 -0400 Subject: [PATCH 19/31] chore: adjust simps --- Batteries/Data/Fin/Coding.lean | 29 ++++++++++++++++------------- 1 file changed, 16 insertions(+), 13 deletions(-) diff --git a/Batteries/Data/Fin/Coding.lean b/Batteries/Data/Fin/Coding.lean index cf23ed9480..0b7dfa534e 100644 --- a/Batteries/Data/Fin/Coding.lean +++ b/Batteries/Data/Fin/Coding.lean @@ -15,6 +15,9 @@ This module collects encoding/decoding bijections to represent basic type constr types as `Fin` types. These functions implement the isomorphism `Option (Fin n) ≃ Fin (n+1)`, `Fin m ⊕ Fin n ≃ Fin (m + n)`, `Fin m × Fin n ≃ Fin (m * n)`, ..., including, dependent sums, dependent products, decidable subtypes and decidable quotients. + +Only a minimal API is provided. These utility functions are intended for use in other constructions. +Such constructions should avoid exposing these functions as they are not meant for public use. -/ namespace Fin @@ -30,12 +33,12 @@ def decodeEmpty : Fin 0 → Empty := (nomatch ·) @[simp] theorem decodeEmpty_encodeEmpty (x : Empty) : decodeEmpty (encodeEmpty x) = x := nomatch x /-- Encode `PUnit` into `Fin 1`. -/ -@[simp, nolint unusedArguments] +@[nolint unusedArguments] def encodePUnit : PUnit → Fin 1 | .unit => 0 /-- Decode `PUnit` from `Fin 1`. -/ -@[simp, pp_nodot] def decodePUnit : Fin 1 → PUnit +@[pp_nodot] def decodePUnit : Fin 1 → PUnit | 0 => .unit /-- Encode `Unit` into `Fin 1`. -/ @@ -44,44 +47,44 @@ abbrev encodeUnit : Unit → Fin 1 := encodePUnit /-- Decode `Unit` from `Fin 1`. -/ @[pp_nodot] abbrev decodeUnit : Fin 1 → Unit := decodePUnit -theorem encodePUnit_decodePUnit : (x : Fin 1) → encodePUnit (decodePUnit x) = x +@[simp] theorem encodePUnit_decodePUnit : (x : Fin 1) → encodePUnit (decodePUnit x) = x | 0 => rfl -theorem decodePUnit_encodePUnit : (x : PUnit) → decodePUnit (encodePUnit x) = x +@[simp] theorem decodePUnit_encodePUnit : (x : PUnit) → decodePUnit (encodePUnit x) = x | .unit => rfl /-- Encode `Bool` into `Fin 2`. -/ -@[simp] def encodeBool : Bool → Fin 2 +def encodeBool : Bool → Fin 2 | false => 0 | true => 1 /-- Decode `Bool` from `Fin 2`. -/ -@[simp, pp_nodot] def decodeBool : Fin 2 → Bool +@[pp_nodot] def decodeBool : Fin 2 → Bool | 0 => false | 1 => true -theorem encodeBool_decodeBool : (x : Fin 2) → encodeBool (decodeBool x) = x +@[simp] theorem encodeBool_decodeBool : (x : Fin 2) → encodeBool (decodeBool x) = x | 0 | 1 => rfl -theorem decodeBool_encodeBool : (x : Bool) → decodeBool (encodeBool x) = x - | false| true => rfl +@[simp] theorem decodeBool_encodeBool : (x : Bool) → decodeBool (encodeBool x) = x + | false | true => rfl /-- Encode `Ordering` into `Fin 3`. -/ -@[simp] def encodeOrdering : Ordering → Fin 3 +def encodeOrdering : Ordering → Fin 3 | .eq => 0 | .lt => 1 | .gt => 2 /-- Decode `Ordering` from `Fin 3`. -/ -@[simp, pp_nodot] def decodeOrdering : Fin 3 → Ordering +@[pp_nodot] def decodeOrdering : Fin 3 → Ordering | 0 => .eq | 1 => .lt | 2 => .gt -theorem encodeOrdering_decodeOrdering : (x : Fin 3) → encodeOrdering (decodeOrdering x) = x +@[simp] theorem encodeOrdering_decodeOrdering : (x : Fin 3) → encodeOrdering (decodeOrdering x) = x | 0 | 1 | 2 => rfl -theorem decodeOrdering_encodeOrdering : +@[simp] theorem decodeOrdering_encodeOrdering : (x : Ordering) → decodeOrdering (encodeOrdering x) = x | .eq | .lt | .gt => rfl From d66b5bc796bc9d8e1b663e896dd6de900211c3dc Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Tue, 30 Sep 2025 07:15:15 -0400 Subject: [PATCH 20/31] docs: fix docstrings --- Batteries/Data/Fin/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean index 9a87a6eb75..1d209740e3 100644 --- a/Batteries/Data/Fin/Basic.lean +++ b/Batteries/Data/Fin/Basic.lean @@ -83,11 +83,11 @@ This is the dependent version of `Fin.foldl`. -/ (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (init : α 0) : α (last n) := dfoldlM (m := Id) n α f init -/-- Sum of a list indexed by `Fin n`. -/ +/-- Sum of a tuple indexed by `Fin n`. -/ protected def sum [Zero α] [Add α] (x : Fin n → α) : α := foldr n (x · + ·) 0 -/-- Product of a list indexed by `Fin n`. -/ +/-- Product of a tuple indexed by `Fin n`. -/ protected def prod [One α] [Mul α] (x : Fin n → α) : α := foldr n (x · * ·) 1 From 3719930b5364175bfdc7fc647412d0f5557d3339 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Thu, 2 Oct 2025 09:59:04 -0400 Subject: [PATCH 21/31] fix: deprecated --- Batteries/Data/Fin/Coding.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Batteries/Data/Fin/Coding.lean b/Batteries/Data/Fin/Coding.lean index 0b7dfa534e..b32d81cf78 100644 --- a/Batteries/Data/Fin/Coding.lean +++ b/Batteries/Data/Fin/Coding.lean @@ -466,7 +466,7 @@ abbrev getRepr (s : Setoid (Fin n)) [DecidableRel s.r] (x : Fin n) : Fin n := | some y => y | none => False.elim <| by have : Fin.find? (fun y => s.r x y) |>.isSome := by - rw [find?_isSome_iff] + rw [isSome_find?_iff] exists x apply decide_eq_true exact Setoid.refl x From b01c77ac8d8943919aa8d63e953cbbf23db9962f Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Fri, 10 Oct 2025 23:10:30 -0400 Subject: [PATCH 22/31] chore: remove empty file --- Batteries/Data/List.lean | 1 - Batteries/Data/List/OfFn.lean | 15 --------------- 2 files changed, 16 deletions(-) delete mode 100644 Batteries/Data/List/OfFn.lean diff --git a/Batteries/Data/List.lean b/Batteries/Data/List.lean index 3104e7096f..796d55a260 100644 --- a/Batteries/Data/List.lean +++ b/Batteries/Data/List.lean @@ -5,6 +5,5 @@ import Batteries.Data.List.Init.Lemmas import Batteries.Data.List.Lemmas import Batteries.Data.List.Matcher import Batteries.Data.List.Monadic -import Batteries.Data.List.OfFn import Batteries.Data.List.Pairwise import Batteries.Data.List.Perm diff --git a/Batteries/Data/List/OfFn.lean b/Batteries/Data/List/OfFn.lean deleted file mode 100644 index c66846e61a..0000000000 --- a/Batteries/Data/List/OfFn.lean +++ /dev/null @@ -1,15 +0,0 @@ -/- -Copyright (c) 2024 Lean FRO. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Kim Morrison --/ -import Batteries.Data.List.Lemmas -import Batteries.Data.Fin.Lemmas - -/-! -# Theorems about `List.ofFn` --/ - -namespace List - -end List From 30493d6df7d94b4fb4344b5144d42dc10b83dafa Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Fri, 10 Oct 2025 22:55:00 -0400 Subject: [PATCH 23/31] feat: add `Fin.divNat`, `Fin.modNat`, `Fin.mkDivMod` --- Batteries/Data/Fin/Basic.lean | 16 ++++++++++++++++ Batteries/Data/Fin/Lemmas.lean | 18 ++++++++++++++++++ Batteries/Data/Nat/Lemmas.lean | 14 ++++++++++++++ 3 files changed, 48 insertions(+) diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean index 9d34c899ec..262fabee65 100644 --- a/Batteries/Data/Fin/Basic.lean +++ b/Batteries/Data/Fin/Basic.lean @@ -3,6 +3,7 @@ Copyright (c) 2017 Robert Y. Lewis. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Robert Y. Lewis, Keeley Hoek, Mario Carneiro, François G. Dorais, Quang Dao -/ +import Batteries.Data.Nat.Lemmas namespace Fin @@ -96,3 +97,18 @@ The function `p` is not evaluated on further inputs after the first `i` is found -/ @[inline] def find? (p : Fin n → Bool) : Option (Fin n) := findSome? <| Option.guard fun i => p i + +/-- Compute `i / n`, where `n` is a `Nat` and inferred the type of `i`. -/ +def divNat (i : Fin (m * n)) : Fin m := + ⟨i / n, Nat.div_lt_of_lt_mul <| Nat.mul_comm m n ▸ i.is_lt⟩ + +/-- Compute `i % n`, where `n` is a `Nat` and inferred the type of `i`. -/ +def modNat (i : Fin (m * n)) : Fin n := + ⟨i % n, Nat.mod_lt _ <| Nat.pos_of_mul_pos_left i.pos⟩ + +/-- +Compute the element of `Fin (m * n)` with quotient `i : Fin m` and remainder `j : Fin n` +when divided by `n`. +-/ +def mkDivMod (i : Fin m) (j : Fin n) : Fin (m * n) := + ⟨n * i + j, Nat.mul_add_lt_mul_of_lt_of_lt i.is_lt j.is_lt⟩ diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean index 7183e0820c..c53f0d8a80 100644 --- a/Batteries/Data/Fin/Lemmas.lean +++ b/Batteries/Data/Fin/Lemmas.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ import Batteries.Data.Fin.Basic +import Batteries.Data.Nat.Lemmas import Batteries.Util.ProofWanted import Batteries.Tactic.Alias @@ -201,3 +202,20 @@ theorem exists_iff_exists_minimal (p : Fin n → Prop) [DecidablePred p] : (∃ i, p i) ↔ ∃ i, p i ∧ ∀ j < i, ¬ p j := by simpa only [decide_eq_true_iff, decide_eq_false_iff_not] using exists_eq_true_iff_exists_minimal_eq_true (p ·) + +/-! ### divNat / modNat / mkDivMod -/ + +@[simp] theorem coe_divNat (i : Fin (m * n)) : (i.divNat : Nat) = i / n := rfl + +@[simp] theorem coe_modNat (i : Fin (m * n)) : (i.modNat : Nat) = i % n := rfl + +@[simp] theorem coe_mkDivMod (i : Fin m) (j : Fin n) : (mkDivMod i j : Nat) = n * i + j := rfl + +@[simp] theorem divNat_mkDivMod (i : Fin m) (j : Fin n) : (mkDivMod i j).divNat = i := by + ext; simp [mkDivMod, Nat.mul_add_div (Nat.zero_lt_of_lt j.is_lt)] + +@[simp] theorem modNat_mkDivMod (i : Fin m) (j : Fin n) : (mkDivMod i j).modNat = j := by + ext; simp [mkDivMod, Nat.mod_eq_of_lt] + +@[simp] theorem divNat_mkDivMod_modNat (k : Fin (m * n)) : + mkDivMod k.divNat k.modNat = k := by ext; simp [mkDivMod, Nat.div_add_mod] diff --git a/Batteries/Data/Nat/Lemmas.lean b/Batteries/Data/Nat/Lemmas.lean index ca1d2b956d..126cd67103 100644 --- a/Batteries/Data/Nat/Lemmas.lean +++ b/Batteries/Data/Nat/Lemmas.lean @@ -203,3 +203,17 @@ theorem testBit_ofBits (f : Fin n → Bool) : cases Nat.lt_or_ge i n with | inl h => simp [h] | inr h => simp [h, Nat.not_lt_of_ge h] + +/-! ### Misc -/ + +theorem mul_add_lt_mul_of_lt_of_lt {m n x y : Nat} (hx : x < m) (hy : y < n) : + n * x + y < m * n := calc + _ < n * x + n := Nat.add_lt_add_left hy _ + _ = n * (x + 1) := Nat.mul_add_one .. |>.symm + _ ≤ n * m := Nat.mul_le_mul_left _ hx + _ = m * n := Nat.mul_comm .. + +theorem add_mul_lt_mul_of_lt_of_lt {m n x y : Nat} (hx : x < m) (hy : y < n) : + x + m * y < m * n := by + rw [Nat.add_comm, Nat.mul_comm _ n] + exact mul_add_lt_mul_of_lt_of_lt hy hx From 293658e975e88b724c48acf5fa34ca605dea42e3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Sat, 11 Oct 2025 17:33:40 -0400 Subject: [PATCH 24/31] fix: use `divNat` and `modNat` --- Batteries/Data/Fin/Coding.lean | 24 ++++-------------------- 1 file changed, 4 insertions(+), 20 deletions(-) diff --git a/Batteries/Data/Fin/Coding.lean b/Batteries/Data/Fin/Coding.lean index b32d81cf78..6ad7078d4e 100644 --- a/Batteries/Data/Fin/Coding.lean +++ b/Batteries/Data/Fin/Coding.lean @@ -190,33 +190,17 @@ def encodeSum : Sum (Fin n) (Fin m) → Fin (n + m) /-- Encode `Fin m × Fin n` into `Fin (m * n)`. -/ def encodeProd : Fin m × Fin n → Fin (m * n) - | (⟨i, hi⟩, ⟨j, hj⟩) => Fin.mk (n * i + j) <| calc - _ < n * i + n := Nat.add_lt_add_left hj .. - _ = n * (i + 1) := Nat.mul_succ .. - _ ≤ n * m := Nat.mul_le_mul_left n (Nat.succ_le_of_lt hi) - _ = m * n := Nat.mul_comm .. + | (i, j) => mkDivMod i j /-- Decode `Fin m × Fin n` from `Fin (m * n)`. -/ @[pp_nodot] def decodeProd (z : Fin (m * n)) : Fin m × Fin n := - ⟨left, right⟩ -where - hn : 0 < n := by - apply Nat.zero_lt_of_ne_zero - intro h - absurd z.is_lt - simp [h] - /-- Left case of `decodeProd`. -/ - left := ⟨z / n, by rw [Nat.div_lt_iff_lt_mul hn]; exact z.is_lt⟩ - /-- Right case of `decodeProd`. -/ - right := ⟨z % n, Nat.mod_lt _ hn⟩ + (z.divNat, z.modNat) @[simp] theorem encodeProd_decodeProd (x : Fin (m * n)) : encodeProd (decodeProd x) = x := by - simp [encodeProd, decodeProd, decodeProd.left, decodeProd.right, Nat.div_add_mod] + simp [encodeProd, decodeProd] @[simp] theorem decodeProd_encodeProd (x : Fin m × Fin n) : decodeProd (encodeProd x) = x := by - match x with - | ⟨⟨_, _⟩, ⟨_, h⟩⟩ => simp [encodeProd, decodeProd, decodeProd.left, decodeProd.right, - Nat.mul_add_div (Nat.zero_lt_of_lt h), Nat.div_eq_of_lt h, Nat.mod_eq_of_lt h] + simp [encodeProd, decodeProd] /-- Encode `(i : Fin n) × Fin (f i)` into `Fin (Fin.sum f)`. -/ def encodeSigma (f : Fin n → Nat) (x : (i : Fin n) × Fin (f i)) : Fin (Fin.sum f) := From ae1cc665a769138be4031d442c1fe1f12ed1d232 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Sun, 12 Oct 2025 02:43:23 -0400 Subject: [PATCH 25/31] feat: add `Fin.sum`, `Fin.prod`, `Fin.count` --- Batteries/Data/Fin/Basic.lean | 12 +++++++++++ Batteries/Data/Fin/Lemmas.lean | 39 ++++++++++++++++++++++++++++++++++ 2 files changed, 51 insertions(+) diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean index 262fabee65..b9f7950ed1 100644 --- a/Batteries/Data/Fin/Basic.lean +++ b/Batteries/Data/Fin/Basic.lean @@ -84,6 +84,18 @@ This is the dependent version of `Fin.foldl`. -/ (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (init : α 0) : α (last n) := dfoldlM (m := Id) n α f init +/-- Sum of a tuple indexed by `Fin n`. -/ +protected def sum [Zero α] [Add α] (x : Fin n → α) : α := + foldr n (x · + ·) 0 + +/-- Product of a tuple indexed by `Fin n`. -/ +protected def prod [One α] [Mul α] (x : Fin n → α) : α := + foldr n (x · * ·) 1 + +/-- Count the number of true values of a decidable predicate on `Fin n`. -/ +protected def count (p : Fin n → Bool) : Nat := + Fin.sum (Bool.toNat ∘ p) + /-- `findSome? f` returns `f i` for the first `i` for which `f i` is `some _`, or `none` if no such element is found. The function `f` is not evaluated on further inputs after the first `i` is found. diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean index c53f0d8a80..3b657fee44 100644 --- a/Batteries/Data/Fin/Lemmas.lean +++ b/Batteries/Data/Fin/Lemmas.lean @@ -40,6 +40,45 @@ theorem foldr_assoc {op : α → α → α} [ha : Std.Associative op] {f : Fin n @[simp] theorem coe_clamp (n m : Nat) : (clamp n m : Nat) = min n m := rfl +/-! ### sum -/ + +@[simp] theorem sum_zero [Zero α] [Add α] (x : Fin 0 → α) : + Fin.sum x = 0 := by + simp [Fin.sum] + +theorem sum_succ [Zero α] [Add α] (x : Fin (n + 1) → α) : + Fin.sum x = x 0 + Fin.sum (x ∘ Fin.succ) := by + simp [Fin.sum, foldr_succ] + +theorem sum_eq_sum_map_finRange [Zero α] [Add α] (x : Fin n → α) : + Fin.sum x = (List.finRange n |>.map x).sum := by + simp [Fin.sum, List.sum] + rw [Fin.foldr_eq_finRange_foldr] + rw [List.foldr_map] + +/-! ### prod -/ + +@[simp] theorem prod_zero [One α] [Mul α] (x : Fin 0 → α) : + Fin.prod x = 1 := by + simp [Fin.prod] + +theorem prod_succ [One α] [Mul α] (x : Fin (n + 1) → α) : + Fin.prod x = x 0 * Fin.prod (x ∘ Fin.succ) := by + simp [Fin.prod, foldr_succ] + +/-! ### count -/ + +@[simp, grind =] theorem count_zero (p : Fin 0 → Bool) : Fin.count p = 0 := by + simp [Fin.count] + +theorem count_succ (p : Fin (n + 1) → Bool) : Fin.count p = + if p 0 then Fin.count (fun i => p i.succ) + 1 else Fin.count (fun i => p i.succ) := by + split <;> simp [Fin.count, Fin.sum_succ, Nat.one_add, Function.comp_def, *] + +@[grind] +theorem count_le (p : Fin n → Bool) : Fin.count p ≤ n := by + induction n with grind [count_succ] + /-! ### findSome? -/ @[simp] theorem findSome?_zero {f : Fin 0 → Option α} : findSome? f = none := rfl From 15b43d04787e26b8608592f378bc012928b47e42 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Sun, 12 Oct 2025 03:02:27 -0400 Subject: [PATCH 26/31] chore: cleanup --- Batteries/Data/Fin/Basic.lean | 2 +- Batteries/Data/Fin/Lemmas.lean | 23 ++++++++++++++++------- 2 files changed, 17 insertions(+), 8 deletions(-) diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean index b9f7950ed1..36ef5a5635 100644 --- a/Batteries/Data/Fin/Basic.lean +++ b/Batteries/Data/Fin/Basic.lean @@ -94,7 +94,7 @@ protected def prod [One α] [Mul α] (x : Fin n → α) : α := /-- Count the number of true values of a decidable predicate on `Fin n`. -/ protected def count (p : Fin n → Bool) : Nat := - Fin.sum (Bool.toNat ∘ p) + Fin.sum (p · |>.toNat) /-- `findSome? f` returns `f i` for the first `i` for which `f i` is `some _`, or `none` if no such diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean index 3b657fee44..87b65b90f9 100644 --- a/Batteries/Data/Fin/Lemmas.lean +++ b/Batteries/Data/Fin/Lemmas.lean @@ -42,12 +42,13 @@ theorem foldr_assoc {op : α → α → α} [ha : Std.Associative op] {f : Fin n /-! ### sum -/ -@[simp] theorem sum_zero [Zero α] [Add α] (x : Fin 0 → α) : +@[simp, grind =] +theorem sum_zero [Zero α] [Add α] (x : Fin 0 → α) : Fin.sum x = 0 := by simp [Fin.sum] theorem sum_succ [Zero α] [Add α] (x : Fin (n + 1) → α) : - Fin.sum x = x 0 + Fin.sum (x ∘ Fin.succ) := by + Fin.sum x = x 0 + Fin.sum (x ·.succ) := by simp [Fin.sum, foldr_succ] theorem sum_eq_sum_map_finRange [Zero α] [Add α] (x : Fin n → α) : @@ -63,7 +64,7 @@ theorem sum_eq_sum_map_finRange [Zero α] [Add α] (x : Fin n → α) : simp [Fin.prod] theorem prod_succ [One α] [Mul α] (x : Fin (n + 1) → α) : - Fin.prod x = x 0 * Fin.prod (x ∘ Fin.succ) := by + Fin.prod x = x 0 * Fin.prod (x ·.succ) := by simp [Fin.prod, foldr_succ] /-! ### count -/ @@ -71,13 +72,21 @@ theorem prod_succ [One α] [Mul α] (x : Fin (n + 1) → α) : @[simp, grind =] theorem count_zero (p : Fin 0 → Bool) : Fin.count p = 0 := by simp [Fin.count] -theorem count_succ (p : Fin (n + 1) → Bool) : Fin.count p = - if p 0 then Fin.count (fun i => p i.succ) + 1 else Fin.count (fun i => p i.succ) := by - split <;> simp [Fin.count, Fin.sum_succ, Nat.one_add, Function.comp_def, *] +@[simp, grind =] theorem count_one (p : Fin 1 → Bool) : Fin.count p = (p 0).toNat := by + simp [Fin.count, Fin.sum_succ] + +theorem count_succ (p : Fin (n + 1) → Bool) : + Fin.count p = (p 0).toNat + Fin.count (p ·.succ) := by + simp [Fin.count, Fin.sum_succ] @[grind] theorem count_le (p : Fin n → Bool) : Fin.count p ≤ n := by - induction n with grind [count_succ] + induction n with simp only [count_zero, count_succ, Nat.le_refl] + | succ _ ih => + rw [Nat.add_comm] + apply Nat.add_le_add + · exact ih .. + · exact Bool.toNat_le .. /-! ### findSome? -/ From c4c8781fbaf0bd23cf3a6e084e3f9c402b5fdc93 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Sun, 12 Oct 2025 17:30:33 -0400 Subject: [PATCH 27/31] fix: use `Char` constants --- Batteries/Data/Fin/Coding.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Batteries/Data/Fin/Coding.lean b/Batteries/Data/Fin/Coding.lean index 8418348abf..9bb86ad889 100644 --- a/Batteries/Data/Fin/Coding.lean +++ b/Batteries/Data/Fin/Coding.lean @@ -90,31 +90,31 @@ def encodeOrdering : Ordering → Fin 3 /-- Encode `Char` into `Fin Char.count`. -/ def encodeChar (c : Char) : Fin Char.count := - if _ : c.toNat < 0xD800 then + if _ : c.toNat < Char.minSurrogate then ⟨c.toNat, by grind⟩ else - ⟨c.toNat - (0xE000 - 0xD800), by grind⟩ + ⟨c.toNat - (Char.maxSurrogate + 1 - Char.minSurrogate), by grind⟩ /-- Decode `Char` from `Fin Char.count`. -/ @[pp_nodot] def decodeChar (i : Fin Char.count) : Char := if _ : i.val < 0xD800 then Char.ofNatAux i.val (by grind) else - Char.ofNatAux (i.val + (0xE000 - 0xD800)) (by grind) + Char.ofNatAux (i.val + (Char.maxSurrogate + 1 - Char.minSurrogate)) (by grind) @[simp] theorem encodeChar_decodeChar (x) : encodeChar (decodeChar x) = x := by simp only [decodeChar, encodeChar] split · simp [*] - · have : ¬ x.val + (0xE000 - 0xD800) < 0xD800 := by grind + · have : ¬ x.val + (Char.maxSurrogate + 1 - Char.minSurrogate) < Char.minSurrogate := by grind simp [*] @[simp] theorem decodeChar_encodeChar (x) : decodeChar (encodeChar x) = x := by ext; simp only [decodeChar, encodeChar] split · simp only [Char.ofNatAux, Char.toNat]; rfl - · have : ¬ x.toNat - (0xE000 - 0xD800) < 0xD800 := by grind - have : (0xE000 - 0xD800) ≤ x.toNat := by grind + · have : ¬ x.toNat - (Char.maxSurrogate + 1 - Char.minSurrogate) < Char.minSurrogate := by grind + have : Char.maxSurrogate + 1 - Char.minSurrogate ≤ x.toNat := by grind simp [Char.ofNatAux, *]; rfl /-- Encode `Option (Fin n)` into `Fin (n+1)`. -/ From 08950cf6a30725961cd99f4b143f7bb195a45290 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Thu, 30 Oct 2025 12:02:18 -0400 Subject: [PATCH 28/31] fix: use Fin.addCases --- Batteries/Data/Fin/Coding.lean | 35 +++++++++------------------------- 1 file changed, 9 insertions(+), 26 deletions(-) diff --git a/Batteries/Data/Fin/Coding.lean b/Batteries/Data/Fin/Coding.lean index 9bb86ad889..424330b1bd 100644 --- a/Batteries/Data/Fin/Coding.lean +++ b/Batteries/Data/Fin/Coding.lean @@ -154,39 +154,22 @@ def encodeOption : Option (Fin n) → Fin (n+1) /-- Encode `Fin n ⊕ Fin m` into `Fin (n + m)`. -/ def encodeSum : Sum (Fin n) (Fin m) → Fin (n + m) - | .inl x => x.castLE (Nat.le_add_right _ _) - | .inr x => x.natAdd n + | .inl x => x.castAdd _ + | .inr x => x.natAdd _ /-- Decode `Fin n ⊕ Fin m` from `Fin (n + m)`. -/ @[pp_nodot] def decodeSum (x : Fin (n + m)) : Sum (Fin n) (Fin m) := - if h : x < n then - .inl ⟨x, h⟩ - else - .inr ⟨x - n, by grind⟩ + x.addCases .inl .inr -@[simp] theorem encodeSum_decodeSum (x : Fin (n + m)) : encodeSum (decodeSum x) = x := by +@[simp] theorem encodeSum_decodeSum (x : Fin (n + m)) : + encodeSum (decodeSum x) = x := by simp only [encodeSum, decodeSum] - split - · next hd => - split at hd - · cases hd; rfl - · contradiction - · next hd => - split at hd - · contradiction - · next he => - cases x; cases hd - simp at he ⊢; grind + cases x using addCases <;> simp -@[simp] theorem decodeSum_encodeSum (x : Sum (Fin n) (Fin m)) : decodeSum (encodeSum x) = x := by +@[simp] theorem decodeSum_encodeSum (x : Sum (Fin n) (Fin m)) : + decodeSum (encodeSum x) = x := by simp only [encodeSum, decodeSum] - split - · split - · simp - · next h => simp only [coe_castLE] at h; grind - · split - · next h => simp only [coe_natAdd] at h; grind - · next x _ => cases x; simp only [natAdd_mk, Sum.inr.injEq, mk.injEq]; grind + cases x <;> simp /-- Encode `Fin m × Fin n` into `Fin (m * n)`. -/ def encodeProd : Fin m × Fin n → Fin (m * n) From b06a514e73a6608ad62a96abf56e792c85feb973 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Thu, 30 Oct 2025 12:26:23 -0400 Subject: [PATCH 29/31] chore: use module --- Batteries/Data/Fin/Coding.lean | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/Batteries/Data/Fin/Coding.lean b/Batteries/Data/Fin/Coding.lean index 424330b1bd..45da2391b5 100644 --- a/Batteries/Data/Fin/Coding.lean +++ b/Batteries/Data/Fin/Coding.lean @@ -3,11 +3,15 @@ Copyright (c) 2024 François G. Dorais. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: François G. Dorais -/ -import Batteries.Data.Char -import Batteries.Data.Fin.Lemmas -import Batteries.Tactic.Basic -import Batteries.Tactic.Trans -import Batteries.Tactic.Lint +module + +public import Batteries.Data.Char +public import Batteries.Data.Fin.Lemmas +public import Batteries.Tactic.Basic +public import Batteries.Tactic.Trans +public import Batteries.Tactic.Lint + +@[expose] public section /-! # Low-level coding recipes for `Fin` types From 9057e9a51c99c4e135ada80afb80982099b8f67a Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Thu, 30 Oct 2025 18:39:40 -0400 Subject: [PATCH 30/31] fix: grind proofs --- Batteries/Data/Fin/Coding.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Batteries/Data/Fin/Coding.lean b/Batteries/Data/Fin/Coding.lean index 45da2391b5..e725d7a2b2 100644 --- a/Batteries/Data/Fin/Coding.lean +++ b/Batteries/Data/Fin/Coding.lean @@ -97,7 +97,7 @@ def encodeChar (c : Char) : Fin Char.count := if _ : c.toNat < Char.minSurrogate then ⟨c.toNat, by grind⟩ else - ⟨c.toNat - (Char.maxSurrogate + 1 - Char.minSurrogate), by grind⟩ + ⟨c.toNat - (Char.maxSurrogate + 1 - Char.minSurrogate), by cases c; grind [Char.toNat]⟩ /-- Decode `Char` from `Fin Char.count`. -/ @[pp_nodot] def decodeChar (i : Fin Char.count) : Char := @@ -117,7 +117,8 @@ def encodeChar (c : Char) : Fin Char.count := ext; simp only [decodeChar, encodeChar] split · simp only [Char.ofNatAux, Char.toNat]; rfl - · have : ¬ x.toNat - (Char.maxSurrogate + 1 - Char.minSurrogate) < Char.minSurrogate := by grind + · have : ¬ x.toNat - (Char.maxSurrogate + 1 - Char.minSurrogate) < Char.minSurrogate := by + cases x; grind [Char.toNat] have : Char.maxSurrogate + 1 - Char.minSurrogate ≤ x.toNat := by grind simp [Char.ofNatAux, *]; rfl From 629f6e443a14b5a25e0f87427043dff9b940bc93 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Sun, 18 Jan 2026 08:54:24 -0500 Subject: [PATCH 31/31] fixes --- Batteries/Data/Fin/Coding.lean | 47 ++++++++++++++++++---------------- 1 file changed, 25 insertions(+), 22 deletions(-) diff --git a/Batteries/Data/Fin/Coding.lean b/Batteries/Data/Fin/Coding.lean index e725d7a2b2..f6bb96093e 100644 --- a/Batteries/Data/Fin/Coding.lean +++ b/Batteries/Data/Fin/Coding.lean @@ -75,14 +75,14 @@ def encodeBool : Bool → Fin 2 /-- Encode `Ordering` into `Fin 3`. -/ def encodeOrdering : Ordering → Fin 3 - | .eq => 0 - | .lt => 1 + | .lt => 0 + | .eq => 1 | .gt => 2 /-- Decode `Ordering` from `Fin 3`. -/ @[pp_nodot] def decodeOrdering : Fin 3 → Ordering - | 0 => .eq - | 1 => .lt + | 0 => .lt + | 1 => .eq | 2 => .gt @[simp] theorem encodeOrdering_decodeOrdering : (x : Fin 3) → encodeOrdering (decodeOrdering x) = x @@ -346,58 +346,61 @@ def decodePi (f : Fin n → Nat) (x : Fin (Fin.prod f)) : (i : Fin n) → Fin (f conv => rhs; rw [← h] congr; simp [encodePi, Nat.mul_add_div h0, Nat.div_eq_of_lt (x 0).is_lt]; rfl -/-- Encode `{ i : Fin n // P i }` into `Fin (Fin.count P)` where `P` is a decidable predicate. -/ +/-- Encode `{ i : Fin n // P i }` into `Fin (Fin.countP P)` where `P` is a decidable predicate. -/ def encodeSubtype (P : Fin n → Prop) [inst : DecidablePred P] (i : { i // P i }) : - Fin (Fin.count (P ·)) := + Fin (Fin.countP (P ·)) := match n, P, inst, i with | n+1, P, inst, ⟨0, hp⟩ => - have : Fin.count (P ·) > 0 := by grind [count_succ] + have : Fin.countP (P ·) > 0 := by grind [countP_succ] ⟨0, this⟩ | n+1, P, inst, ⟨⟨i+1, hi⟩, hp⟩ => match encodeSubtype (fun i => P i.succ) ⟨⟨i, Nat.lt_of_succ_lt_succ hi⟩, hp⟩ with | ⟨k, hk⟩ => if h0 : P 0 then - have : (Fin.count fun i => P i.succ) + 1 = Fin.count (P ·) := by - grind [count_succ] + have : (Fin.countP fun i => P i.succ) + 1 = Fin.countP (P ·) := by + grind [countP_succ] Fin.cast this ⟨k+1, Nat.succ_lt_succ hk⟩ else - have : (Fin.count fun i => P i.succ) = Fin.count (P ·) := by simp [count_succ, h0] + have : (Fin.countP fun i => P i.succ) = Fin.countP (P ·) := by + simp [-countP_eq_countP_map_finRange, countP_succ, h0] Fin.cast this ⟨k, hk⟩ -/-- Decode `{ i : Fin n // P i }` from `Fin (Fin.count P)` where `P` is a decidable predicate. -/ -def decodeSubtype (P : Fin n → Prop) [inst : DecidablePred P] (k : Fin (Fin.count (P ·))) : +/-- Decode `{ i : Fin n // P i }` from `Fin (Fin.countP P)` where `P` is a decidable predicate. -/ +def decodeSubtype (P : Fin n → Prop) [inst : DecidablePred P] (k : Fin (Fin.countP (P ·))) : { i // P i } := match n, P, inst, k with | 0, _, _, ⟨_, h⟩ => False.elim (by simp at h) | n+1, P, inst, ⟨k, hk⟩ => if h0 : P 0 then - have : Fin.count (P ·) = (Fin.count fun i => P i.succ) + 1 := by grind [count_succ] + have : Fin.countP (P ·) = (Fin.countP fun i => P i.succ) + 1 := by grind [countP_succ] match k with | 0 => ⟨0, h0⟩ | k + 1 => match decodeSubtype (fun i => P i.succ) ⟨k, Nat.lt_of_add_lt_add_right (this ▸ hk)⟩ with | ⟨⟨i, hi⟩, hp⟩ => ⟨⟨i+1, Nat.succ_lt_succ hi⟩, hp⟩ else - have : Fin.count (P ·) = Fin.count fun i => P i.succ := by simp [count_succ, h0] + have : Fin.countP (P ·) = Fin.countP fun i => P i.succ := by + simp [-countP_eq_countP_map_finRange, countP_succ, h0] match decodeSubtype (fun i => P (succ i)) ⟨k, this ▸ hk⟩ with | ⟨⟨i, hi⟩, hp⟩ => ⟨⟨i+1, Nat.succ_lt_succ hi⟩, hp⟩ theorem encodeSubtype_zero_pos {P : Fin (n+1) → Prop} [DecidablePred P] (h₀ : P 0) : - encodeSubtype P ⟨0, h₀⟩ = ⟨0, by grind [count_succ]⟩ := by + encodeSubtype P ⟨0, h₀⟩ = ⟨0, by grind [countP_succ]⟩ := by ext; rw [encodeSubtype.eq_def]; rfl theorem encodeSubtype_succ_pos {P : Fin (n+1) → Prop} [DecidablePred P] (h₀ : P 0) {i : Fin n} (h : P i.succ) : encodeSubtype P ⟨i.succ, h⟩ = - (encodeSubtype (fun i => P i.succ) ⟨i, h⟩).succ.cast (by grind [count_succ]) := by + (encodeSubtype (fun i => P i.succ) ⟨i, h⟩).succ.cast (by grind [countP_succ]) := by ext; rw [encodeSubtype.eq_def]; simp [Fin.succ, *] theorem encodeSubtype_succ_neg {P : Fin (n+1) → Prop} [DecidablePred P] (h₀ : ¬ P 0) {i : Fin n} (h : P i.succ) : encodeSubtype P ⟨i.succ, h⟩ = - (encodeSubtype (fun i => P i.succ) ⟨i, h⟩).cast (by simp [count_succ, *]) := by + (encodeSubtype (fun i => P i.succ) ⟨i, h⟩).cast + (by simp [-countP_eq_countP_map_finRange, countP_succ, *]) := by ext; rw [encodeSubtype.eq_def]; simp [Fin.succ, *] @[simp] theorem encodeSubtype_decodeSubtype (P : Fin n → Prop) [DecidablePred P] - (x : Fin (Fin.count (P ·))) : encodeSubtype P (decodeSubtype P x) = x := by + (x : Fin (Fin.countP (P ·))) : encodeSubtype P (decodeSubtype P x) = x := by induction n with | zero => absurd x.is_lt; simp | succ n ih => @@ -419,7 +422,7 @@ theorem encodeSubtype_succ_neg {P : Fin (n+1) → Prop} [DecidablePred P] (h₀ | zero => rw [encodeSubtype_zero_pos h₀] | succ i => rw [encodeSubtype_succ_pos h₀] - simp only [coe_cast, val_succ, Subtype.mk.injEq] + simp only [val_cast, val_succ, Fin.eta, Subtype.mk.injEq] congr rw [ih (fun i => P i.succ) ⟨i, h⟩] else @@ -428,7 +431,7 @@ theorem encodeSubtype_succ_neg {P : Fin (n+1) → Prop} [DecidablePred P] (h₀ | zero => contradiction | succ i => rw [encodeSubtype_succ_neg h₀] - simp only [coe_cast, Subtype.mk.injEq] + simp only [val_cast, Fin.eta, Subtype.mk.injEq] congr rw [ih (fun i => P i.succ) ⟨i, h⟩] @@ -493,7 +496,7 @@ theorem getRepr_eq_getRepr_of_equiv (s : Setoid (Fin n)) [DecidableRel s.r] (h : /-- Encode `Quotient s` into `Fin m` where `s` is a decidable setoid on `Fin n`. -/ def encodeQuotient (s : Setoid (Fin n)) [DecidableRel s.r] (x : Quotient s) : - Fin (Fin.count fun i => getRepr s i = i) := + Fin (Fin.countP fun i => getRepr s i = i) := encodeSubtype _ <| Quotient.liftOn x (fun i => ⟨getRepr s i, getRepr_getRepr s i⟩) <| by intro _ _ h simp only [Subtype.mk.injEq] @@ -501,7 +504,7 @@ def encodeQuotient (s : Setoid (Fin n)) [DecidableRel s.r] (x : Quotient s) : /-- Decode `Quotient s` from `Fin m` where `s` is a decidable setoid on `Fin n`. -/ def decodeQuotient (s : Setoid (Fin n)) [DecidableRel s.r] - (i : Fin (Fin.count fun i => getRepr s i = i)) : Quotient s := + (i : Fin (Fin.countP fun i => getRepr s i = i)) : Quotient s := Quotient.mk s (decodeSubtype _ i) @[simp] theorem encodeQuotient_decodeQuotient (s : Setoid (Fin n)) [DecidableRel s.r] (x) :