From ebc02fc6e8801db1cb80290c18c039e35b8ebe5c Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 7 Nov 2024 14:30:11 +1100 Subject: [PATCH] feat: lemmas relating Array.findX and List.findX (#5985) This PR relates the operations `findSomeM?`, `findM?`, `findSome?`, and `find?` on `Array` with the corresponding operations on `List`, and also provides simp lemmas for the `Array` operations `findSomeRevM?`, `findRevM?`, `findSomeRev?`, `findRev?` (in terms of `reverse` and the usual forward find operations). --- src/Init/Data/Array/Lemmas.lean | 100 ++++++++++++++++++++++++++++++++ src/Init/Data/List/Control.lean | 34 +++++++++++ 2 files changed, 134 insertions(+) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index e4ec396ffa06..b4c1ef87d4d4 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -197,6 +197,58 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) : @[simp] theorem foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by induction l generalizing as <;> simp [*] +@[simp] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) : + l.toArray.findSomeM? f = l.findSomeM? f := by + rw [Array.findSomeM?] + simp only [bind_pure_comp, map_pure, forIn_toArray] + induction l with + | nil => simp + | cons a l ih => + simp only [forIn_cons, LawfulMonad.bind_assoc, findSomeM?] + congr + ext1 (_|_) <;> simp [ih] + +theorem findSomeRevM?_find_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) + (i : Nat) (h) : + findSomeRevM?.find l.toArray f i h = (l.take i).reverse.findSomeM? f := by + induction i generalizing l with + | zero => simp [Array.findSomeRevM?.find.eq_def] + | succ i ih => + rw [size_toArray] at h + rw [Array.findSomeRevM?.find, take_succ, getElem?_eq_getElem (by omega)] + simp only [ih, reverse_append] + congr + ext1 (_|_) <;> simp + +-- This is not marked as `@[simp]` as later we simplify all occurrences of `findSomeRevM?`. +theorem findSomeRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) : + l.toArray.findSomeRevM? f = l.reverse.findSomeM? f := by + simp [Array.findSomeRevM?, findSomeRevM?_find_toArray] + +-- This is not marked as `@[simp]` as later we simplify all occurrences of `findRevM?`. +theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) : + l.toArray.findRevM? f = l.reverse.findM? f := by + rw [Array.findRevM?, findSomeRevM?_toArray, findM?_eq_findSomeM?] + +@[simp] theorem findM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) : + l.toArray.findM? f = l.findM? f := by + rw [Array.findM?] + simp only [bind_pure_comp, map_pure, forIn_toArray] + induction l with + | nil => simp + | cons a l ih => + simp only [forIn_cons, LawfulMonad.bind_assoc, findM?] + congr + ext1 (_|_) <;> simp [ih] + +@[simp] theorem findSome?_toArray (f : α → Option β) (l : List α) : + l.toArray.findSome? f = l.findSome? f := by + rw [Array.findSome?, ← findSomeM?_id, findSomeM?_toArray, Id.run] + +@[simp] theorem find?_toArray (f : α → Bool) (l : List α) : + l.toArray.find? f = l.find? f := by + rw [Array.find?, ← findM?_id, findM?_toArray, Id.run] + theorem isPrefixOfAux_toArray_succ [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) : Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) = Array.isPrefixOfAux l₁.tail.toArray l₂.tail.toArray (by simp; omega) i := by @@ -1569,6 +1621,28 @@ theorem feraseIdx_eq_eraseIdx {a : Array α} {i : Fin a.size} : (Array.zip as bs).toList = List.zip as.toList bs.toList := by simp [zip, toList_zipWith, List.zip] +/-! ### findSomeM?, findM?, findSome?, find? -/ + +@[simp] theorem findSomeM?_toList [Monad m] [LawfulMonad m] (p : α → m (Option β)) (as : Array α) : + as.toList.findSomeM? p = as.findSomeM? p := by + cases as + simp + +@[simp] theorem findM?_toList [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) : + as.toList.findM? p = as.findM? p := by + cases as + simp + +@[simp] theorem findSome?_toList (p : α → Option β) (as : Array α) : + as.toList.findSome? p = as.findSome? p := by + cases as + simp + +@[simp] theorem find?_toList (p : α → Bool) (as : Array α) : + as.toList.find? p = as.find? p := by + cases as + simp + end Array open Array @@ -1805,6 +1879,32 @@ namespace Array induction as simp +/-! ### findSomeRevM?, findRevM?, findSomeRev?, findRev? -/ + +@[simp] theorem findSomeRevM?_eq_findSomeM?_reverse + [Monad m] [LawfulMonad m] (f : α → m (Option β)) (as : Array α) : + as.findSomeRevM? f = as.reverse.findSomeM? f := by + cases as + rw [List.findSomeRevM?_toArray] + simp + +@[simp] theorem findRevM?_eq_findM?_reverse + [Monad m] [LawfulMonad m] (f : α → m Bool) (as : Array α) : + as.findRevM? f = as.reverse.findM? f := by + cases as + rw [List.findRevM?_toArray] + simp + +@[simp] theorem findSomeRev?_eq_findSome?_reverse (f : α → Option β) (as : Array α) : + as.findSomeRev? f = as.reverse.findSome? f := by + cases as + simp [findSomeRev?, Id.run] + +@[simp] theorem findRev?_eq_find?_reverse (f : α → Bool) (as : Array α) : + as.findRev? f = as.reverse.find? f := by + cases as + simp [findRev?, Id.run] + /-! ### unzip -/ @[simp] theorem fst_unzip (as : Array (α × β)) : (Array.unzip as).fst = as.map Prod.fst := by diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean index dd17b841671b..9febda857009 100644 --- a/src/Init/Data/List/Control.lean +++ b/src/Init/Data/List/Control.lean @@ -5,6 +5,8 @@ Author: Leonardo de Moura -/ prelude import Init.Control.Basic +import Init.Control.Id +import Init.Control.Lawful import Init.Data.List.Basic namespace List @@ -207,6 +209,16 @@ def findM? {m : Type → Type u} [Monad m] {α : Type} (p : α → m Bool) : Lis | true => pure (some a) | false => findM? p as +@[simp] +theorem findM?_id (p : α → Bool) (as : List α) : findM? (m := Id) p as = as.find? p := by + induction as with + | nil => rfl + | cons a as ih => + simp only [findM?, find?] + cases p a with + | true => rfl + | false => rw [ih]; rfl + @[specialize] def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) : List α → m (Option β) | [] => pure none @@ -215,6 +227,28 @@ def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f | some b => pure (some b) | none => findSomeM? f as +@[simp] +theorem findSomeM?_id (f : α → Option β) (as : List α) : findSomeM? (m := Id) f as = as.findSome? f := by + induction as with + | nil => rfl + | cons a as ih => + simp only [findSomeM?, findSome?] + cases f a with + | some b => rfl + | none => rw [ih]; rfl + +theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] (p : α → m Bool) (as : List α) : + as.findM? p = as.findSomeM? fun a => return if (← p a) then some a else none := by + induction as with + | nil => rfl + | cons a as ih => + simp only [findM?, findSomeM?] + simp [ih] + congr + apply funext + intro b + cases b <;> simp + @[inline] protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β := let rec @[specialize] loop : (as' : List α) → (b : β) → Exists (fun bs => bs ++ as' = as) → m β | [], b, _ => pure b