From 021e272cb5cdcc82b7e1e760fe915ff2f64169ad Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 5 Aug 2024 12:16:22 +1000 Subject: [PATCH] chore: move to v4.11.0-rc1 (#907) --- Batteries.lean | 4 - Batteries/Classes/BEq.lean | 18 - Batteries/Data/Array/Basic.lean | 18 - Batteries/Data/Char.lean | 5 - Batteries/Data/HashMap/Basic.lean | 1 - Batteries/Data/HashMap/WF.lean | 10 +- Batteries/Data/List.lean | 1 - Batteries/Data/List/Basic.lean | 204 +----- Batteries/Data/List/Count.lean | 211 +----- Batteries/Data/List/EraseIdx.lean | 70 +- Batteries/Data/List/Init/Attach.lean | 44 -- Batteries/Data/List/Lemmas.lean | 985 +-------------------------- Batteries/Data/List/Pairwise.lean | 210 ------ Batteries/Data/List/Perm.lean | 17 +- Batteries/Data/Nat/Basic.lean | 3 - Batteries/Data/Nat/Lemmas.lean | 4 - Batteries/Data/RBMap/Lemmas.lean | 1 - Batteries/Data/Range/Lemmas.lean | 1 - Batteries/Data/String/Lemmas.lean | 15 +- Batteries/Data/UInt.lean | 10 - Batteries/Lean/SMap.lean | 17 - Batteries/Lean/Util/EnvSearch.lean | 3 +- Batteries/Lean/Util/Path.lean | 34 - Batteries/Logic.lean | 11 +- Batteries/StdDeprecations.lean | 1 - Batteries/Tactic/Lint/Basic.lean | 2 + Batteries/Util/CheckTactic.lean | 124 ---- lean-toolchain | 2 +- scripts/runLinter.lean | 2 +- test/array.lean | 1 - test/congr.lean | 2 - 31 files changed, 41 insertions(+), 1990 deletions(-) delete mode 100644 Batteries/Classes/BEq.lean delete mode 100644 Batteries/Data/List/Init/Attach.lean delete mode 100644 Batteries/Lean/SMap.lean delete mode 100644 Batteries/Lean/Util/Path.lean delete mode 100644 Batteries/Util/CheckTactic.lean diff --git a/Batteries.lean b/Batteries.lean index 2fac3bf121..8e1e6f1828 100644 --- a/Batteries.lean +++ b/Batteries.lean @@ -1,4 +1,3 @@ -import Batteries.Classes.BEq import Batteries.Classes.Cast import Batteries.Classes.Order import Batteries.Classes.RatCast @@ -64,12 +63,10 @@ import Batteries.Lean.NameMapAttribute import Batteries.Lean.PersistentHashMap import Batteries.Lean.PersistentHashSet import Batteries.Lean.Position -import Batteries.Lean.SMap import Batteries.Lean.Syntax import Batteries.Lean.System.IO import Batteries.Lean.TagAttribute import Batteries.Lean.Util.EnvSearch -import Batteries.Lean.Util.Path import Batteries.Linter import Batteries.Linter.UnnecessarySeqFocus import Batteries.Linter.UnreachableTactic @@ -101,7 +98,6 @@ import Batteries.Tactic.Unreachable import Batteries.Tactic.Where import Batteries.Test.Internal.DummyLabelAttr import Batteries.Util.Cache -import Batteries.Util.CheckTactic import Batteries.Util.ExtendedBinder import Batteries.Util.LibraryNote import Batteries.Util.Pickle diff --git a/Batteries/Classes/BEq.lean b/Batteries/Classes/BEq.lean deleted file mode 100644 index 98318f97c9..0000000000 --- a/Batteries/Classes/BEq.lean +++ /dev/null @@ -1,18 +0,0 @@ -/- -Copyright (c) 2022 Mario Carneiro. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Mario Carneiro --/ - -/-! ## Boolean equality -/ - -/-- `PartialEquivBEq α` says that the `BEq` implementation is a -partial equivalence relation, that is: -* it is symmetric: `a == b → b == a` -* it is transitive: `a == b → b == c → a == c`. --/ -class PartialEquivBEq (α) [BEq α] : Prop where - /-- Symmetry for `BEq`. If `a == b` then `b == a`. -/ - symm : (a : α) == b → b == a - /-- Transitivity for `BEq`. If `a == b` and `b == c` then `a == c`. -/ - trans : (a : α) == b → b == c → a == c diff --git a/Batteries/Data/Array/Basic.lean b/Batteries/Data/Array/Basic.lean index 1dddea3c14..ad6b8129e6 100644 --- a/Batteries/Data/Array/Basic.lean +++ b/Batteries/Data/Array/Basic.lean @@ -3,7 +3,6 @@ Copyright (c) 2021 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Arthur Paulino, Floris van Doorn, Jannis Limperg -/ -import Batteries.Data.List.Init.Attach import Batteries.Data.Array.Init.Lemmas /-! @@ -130,23 +129,6 @@ protected def maxI [ord : Ord α] [Inhabited α] (xs : Array α) (start := 0) (stop := xs.size) : α := xs.minI (ord := ord.opposite) start stop -/-- -Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of -`Array {x // P x}` is the same as the input `Array α`. --/ -@[inline] private unsafe def attachWithImpl - (xs : Array α) (P : α → Prop) (_ : ∀ x ∈ xs, P x) : Array {x // P x} := unsafeCast xs - -/-- `O(1)`. "Attach" a proof `P x` that holds for all the elements of `xs` to produce a new array - with the same elements but in the type `{x // P x}`. -/ -@[implemented_by attachWithImpl] def attachWith - (xs : Array α) (P : α → Prop) (H : ∀ x ∈ xs, P x) : Array {x // P x} := - ⟨xs.data.attachWith P fun x h => H x (Array.Mem.mk h)⟩ - -/-- `O(1)`. "Attach" the proof that the elements of `xs` are in `xs` to produce a new array - with the same elements but in the type `{x // x ∈ xs}`. -/ -@[inline] def attach (xs : Array α) : Array {x // x ∈ xs} := xs.attachWith _ fun _ => id - /-- `O(|join L|)`. `join L` concatenates all the arrays in `L` into one array. * `join #[#[a], #[], #[b, c], #[d, e, f]] = #[a, b, c, d, e, f]` diff --git a/Batteries/Data/Char.lean b/Batteries/Data/Char.lean index 5a9110ae12..4f3c59ef0b 100644 --- a/Batteries/Data/Char.lean +++ b/Batteries/Data/Char.lean @@ -6,11 +6,6 @@ Authors: Jannis Limperg import Batteries.Data.UInt import Batteries.Tactic.Alias -@[ext] theorem Char.ext : {a b : Char} → a.val = b.val → a = b - | ⟨_,_⟩, ⟨_,_⟩, rfl => rfl - -theorem Char.ext_iff {x y : Char} : x = y ↔ x.val = y.val := ⟨congrArg _, Char.ext⟩ - theorem Char.le_antisymm_iff {x y : Char} : x = y ↔ x ≤ y ∧ y ≤ x := Char.ext_iff.trans UInt32.le_antisymm_iff diff --git a/Batteries/Data/HashMap/Basic.lean b/Batteries/Data/HashMap/Basic.lean index 106fea1e4d..3419ba35ab 100644 --- a/Batteries/Data/HashMap/Basic.lean +++ b/Batteries/Data/HashMap/Basic.lean @@ -6,7 +6,6 @@ Authors: Leonardo de Moura, Mario Carneiro import Batteries.Data.AssocList import Batteries.Data.Nat.Basic import Batteries.Data.Array.Monadic -import Batteries.Classes.BEq namespace Batteries.HashMap diff --git a/Batteries/Data/HashMap/WF.lean b/Batteries/Data/HashMap/WF.lean index f6298d3322..e83e32e567 100644 --- a/Batteries/Data/HashMap/WF.lean +++ b/Batteries/Data/HashMap/WF.lean @@ -24,7 +24,7 @@ theorem exists_of_update (self : Buckets α β) (i d h) : ∃ l₁ l₂, self.1.data = l₁ ++ self.1[i] :: l₂ ∧ List.length l₁ = i.toNat ∧ (self.update i d h).1.data = l₁ ++ d :: l₂ := by simp only [Array.data_length, Array.ugetElem_eq_getElem, Array.getElem_eq_data_getElem] - exact List.exists_of_set' h + exact List.exists_of_set h theorem update_update (self : Buckets α β) (i d d' h h') : (self.update i d h).update i d' h' = self.update i d' h := by @@ -95,11 +95,11 @@ where · next H => refine (go (i+1) _ _ fun j hj => ?a).trans ?b <;> simp · case a => - simp [List.getD_eq_getElem?, List.getElem?_set, Option.map_eq_map]; split + simp [List.getD_eq_getElem?_getD, List.getElem?_set, Option.map_eq_map]; split · cases source.data[j]? <;> rfl · next H => exact hs _ (Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hj) (Ne.symm H)) · case b => - refine have ⟨l₁, l₂, h₁, _, eq⟩ := List.exists_of_set' H; eq ▸ ?_ + refine have ⟨l₁, l₂, h₁, _, eq⟩ := List.exists_of_set H; eq ▸ ?_ rw [h₁] simp only [Buckets.size_eq, List.map_append, List.map_cons, AssocList.toList, List.length_nil, Nat.sum_append, Nat.sum_cons, Nat.zero_add, Array.data_length] @@ -315,7 +315,7 @@ theorem WF.mapVal {α β γ} {f : α → β → γ} [BEq α] [Hashable α] have ⟨h₁, h₂⟩ := H.out simp only [Imp.mapVal, h₁, Buckets.mapVal, WF_iff]; refine ⟨?_, ?_, fun i h => ?_⟩ · simp only [Buckets.size, Array.map_data, List.map_map]; congr; funext l; simp - · simp only [Array.map_data, List.forall_mem_map_iff] + · simp only [Array.map_data, List.forall_mem_map] simp only [AssocList.toList_mapVal, List.pairwise_map] exact fun _ => h₂.1 _ · simp only [Array.size_map, AssocList.All, Array.getElem_map, AssocList.toList_mapVal, @@ -361,7 +361,7 @@ theorem WF.filterMap {α β γ} {f : α → β → Option γ} [BEq α] [Hashable simp only [Array.mapM_eq_mapM_data, bind, StateT.bind, H2, List.map_map, Nat.zero_add, g] intro bk sz h e'; cases e' refine .mk (by simp [Buckets.size]) ⟨?_, fun i h => ?_⟩ - · simp only [List.forall_mem_map_iff, List.toList_toAssocList] + · simp only [List.forall_mem_map, List.toList_toAssocList] refine fun l h => (List.pairwise_reverse.2 ?_).imp (mt PartialEquivBEq.symm) have := H.out.2.1 _ h rw [← List.pairwise_map (R := (¬ · == ·))] at this ⊢ diff --git a/Batteries/Data/List.lean b/Batteries/Data/List.lean index d060ba89c8..998160b904 100644 --- a/Batteries/Data/List.lean +++ b/Batteries/Data/List.lean @@ -1,7 +1,6 @@ import Batteries.Data.List.Basic import Batteries.Data.List.Count import Batteries.Data.List.EraseIdx -import Batteries.Data.List.Init.Attach import Batteries.Data.List.Init.Lemmas import Batteries.Data.List.Lemmas import Batteries.Data.List.Pairwise diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean index 2cff94c670..43915cd733 100644 --- a/Batteries/Data/List/Basic.lean +++ b/Batteries/Data/List/Basic.lean @@ -10,16 +10,6 @@ namespace List /-! ## New definitions -/ -/-- -`l₁ ⊆ l₂` means that every element of `l₁` is also an element of `l₂`, ignoring multiplicity. --/ -protected def Subset (l₁ l₂ : List α) := ∀ ⦃a : α⦄, a ∈ l₁ → a ∈ l₂ - -instance : HasSubset (List α) := ⟨List.Subset⟩ - -instance [DecidableEq α] : DecidableRel (Subset : List α → List α → Prop) := - fun _ _ => decidableBAll _ _ - /-- Computes the "bag intersection" of `l₁` and `l₂`, that is, the collection of elements of `l₁` which are also in `l₂`. As each element @@ -37,15 +27,6 @@ protected def diff {α} [BEq α] : List α → List α → List α open Option Nat -/-- Get the tail of a nonempty list, or return `[]` for `[]`. -/ -def tail : List α → List α - | [] => [] - | _::as => as - --- FIXME: `@[simp]` on the definition simplifies even `tail l` -@[simp] theorem tail_nil : @tail α [] = [] := rfl -@[simp] theorem tail_cons : @tail α (a::as) = as := rfl - /-- Get the head and tail of a list, if it is nonempty. -/ @[inline] def next? : List α → Option (α × List α) | [] => none @@ -83,16 +64,6 @@ drop_while (· != 1) [0, 1, 2, 3] = [1, 2, 3] | [] => [] | x :: xs => bif p x then xs else after p xs -/-- Returns the index of the first element satisfying `p`, or the length of the list otherwise. -/ -@[inline] def findIdx (p : α → Bool) (l : List α) : Nat := go l 0 where - /-- Auxiliary for `findIdx`: `findIdx.go p l n = findIdx p l + n` -/ - @[specialize] go : List α → Nat → Nat - | [], n => n - | a :: l, n => bif p a then n else go l (n + 1) - -/-- Returns the index of the first element equal to `a`, or the length of the list otherwise. -/ -def indexOf [BEq α] (a : α) : List α → Nat := findIdx (· == a) - @[deprecated (since := "2024-05-06")] alias removeNth := eraseIdx @[deprecated (since := "2024-05-06")] alias removeNthTR := eraseIdxTR @[deprecated (since := "2024-05-06")] alias removeNth_eq_removeNthTR := eraseIdx_eq_eraseIdxTR @@ -139,26 +110,6 @@ Unlike `bagInter` this does not preserve multiplicity: `[1, 1].inter [1]` is `[1 instance [BEq α] : Inter (List α) := ⟨List.inter⟩ -/-- `l₁ <+ l₂`, or `Sublist l₁ l₂`, says that `l₁` is a (non-contiguous) subsequence of `l₂`. -/ -inductive Sublist {α} : List α → List α → Prop - /-- the base case: `[]` is a sublist of `[]` -/ - | slnil : Sublist [] [] - /-- If `l₁` is a subsequence of `l₂`, then it is also a subsequence of `a :: l₂`. -/ - | cons a : Sublist l₁ l₂ → Sublist l₁ (a :: l₂) - /-- If `l₁` is a subsequence of `l₂`, then `a :: l₁` is a subsequence of `a :: l₂`. -/ - | cons₂ a : Sublist l₁ l₂ → Sublist (a :: l₁) (a :: l₂) - -@[inherit_doc] scoped infixl:50 " <+ " => Sublist - -/-- True if the first list is a potentially non-contiguous sub-sequence of the second list. -/ -def isSublist [BEq α] : List α → List α → Bool - | [], _ => true - | _, [] => false - | l₁@(hd₁::tl₁), hd₂::tl₂ => - if hd₁ == hd₂ - then tl₁.isSublist tl₂ - else l₁.isSublist tl₂ - /-- Split a list at an index. ``` @@ -299,7 +250,7 @@ theorem insertNthTR_go_eq : ∀ n l, insertNthTR.go a n l acc = acc.data ++ inse @[csimp] theorem insertNth_eq_insertNthTR : @insertNth = @insertNthTR := by funext α f n l; simp [insertNthTR, insertNthTR_go_eq] -@[simp] theorem headD_eq_head? (l) (a : α) : headD l a = (head? l).getD a := by cases l <;> rfl +theorem headD_eq_head? (l) (a : α) : headD l a = (head? l).getD a := by cases l <;> rfl /-- Take `n` elements from a list `l`. If `l` has less than `n` elements, append `n - length l` @@ -332,19 +283,6 @@ theorem takeDTR_go_eq : ∀ n l, takeDTR.go dflt n l acc = acc.data ++ takeD n l @[csimp] theorem takeD_eq_takeDTR : @takeD = @takeDTR := by funext α f n l; simp [takeDTR, takeDTR_go_eq] -/-- -Pads `l : List α` with repeated occurrences of `a : α` until it is of length `n`. -If `l` is initially larger than `n`, just return `l`. --/ -def leftpad (n : Nat) (a : α) (l : List α) : List α := replicate (n - length l) a ++ l - -/-- Optimized version of `leftpad`. -/ -@[inline] def leftpadTR (n : Nat) (a : α) (l : List α) : List α := - replicateTR.loop a (n - length l) l - -@[csimp] theorem leftpad_eq_leftpadTR : @leftpad = @leftpadTR := by - funext α n a l; simp [leftpad, leftpadTR, replicateTR_loop_eq] - /-- Fold a function `f` over the list from the left, returning the list of partial results. ``` @@ -416,14 +354,6 @@ indexesOf a [a, b, a, a] = [0, 2, 3] -/ @[inline] def indexesOf [BEq α] (a : α) : List α → List Nat := findIdxs (· == a) -/-- Return the index of the first occurrence of an element satisfying `p`. -/ -def findIdx? (p : α → Bool) : List α → (start : Nat := 0) → Option Nat -| [], _ => none -| a :: l, i => if p a then some i else findIdx? p l (i + 1) - -/-- Return the index of the first occurrence of `a` in the list. -/ -@[inline] def indexOf? [BEq α] (a : α) : List α → Option Nat := findIdx? (· == a) - /-- `lookmap` is a combination of `lookup` and `filterMap`. `lookmap f l` will apply `f : α → Option α` to each element of the list, @@ -437,40 +367,6 @@ replacing `a → b` at the first value `a` in the list such that `f a = some b`. | some b => acc.toListAppend (b :: l) | none => go l (acc.push a) -/-- `countP p l` is the number of elements of `l` that satisfy `p`. -/ -@[inline] def countP (p : α → Bool) (l : List α) : Nat := go l 0 where - /-- Auxiliary for `countP`: `countP.go p l acc = countP p l + acc`. -/ - @[specialize] go : List α → Nat → Nat - | [], acc => acc - | x :: xs, acc => bif p x then go xs (acc + 1) else go xs acc - -/-- `count a l` is the number of occurrences of `a` in `l`. -/ -@[inline] def count [BEq α] (a : α) : List α → Nat := countP (· == a) - -/-- -`IsPrefix l₁ l₂`, or `l₁ <+: l₂`, means that `l₁` is a prefix of `l₂`, -that is, `l₂` has the form `l₁ ++ t` for some `t`. --/ -def IsPrefix (l₁ : List α) (l₂ : List α) : Prop := ∃ t, l₁ ++ t = l₂ - -/-- -`IsSuffix l₁ l₂`, or `l₁ <:+ l₂`, means that `l₁` is a suffix of `l₂`, -that is, `l₂` has the form `t ++ l₁` for some `t`. --/ -def IsSuffix (l₁ : List α) (l₂ : List α) : Prop := ∃ t, t ++ l₁ = l₂ - -/-- -`IsInfix l₁ l₂`, or `l₁ <:+: l₂`, means that `l₁` is a contiguous -substring of `l₂`, that is, `l₂` has the form `s ++ l₁ ++ t` for some `s, t`. --/ -def IsInfix (l₁ : List α) (l₂ : List α) : Prop := ∃ s t, s ++ l₁ ++ t = l₂ - -@[inherit_doc] infixl:50 " <+: " => IsPrefix - -@[inherit_doc] infixl:50 " <:+ " => IsSuffix - -@[inherit_doc] infixl:50 " <:+: " => IsInfix - /-- `inits l` is the list of initial segments of `l`. ``` @@ -659,29 +555,6 @@ theorem sections_eq_nil_of_isEmpty : ∀ {L}, L.any isEmpty → @sections α L = rw [Array.foldl_eq_foldl_data, Array.foldl_data_eq_bind]; rfl intros; apply Array.foldl_data_eq_map -/-- `eraseP p l` removes the first element of `l` satisfying the predicate `p`. -/ -def eraseP (p : α → Bool) : List α → List α - | [] => [] - | a :: l => bif p a then l else a :: eraseP p l - -/-- Tail-recursive version of `eraseP`. -/ -@[inline] def erasePTR (p : α → Bool) (l : List α) : List α := go l #[] where - /-- Auxiliary for `erasePTR`: `erasePTR.go p l xs acc = acc.toList ++ eraseP p xs`, - unless `xs` does not contain any elements satisfying `p`, where it returns `l`. -/ - @[specialize] go : List α → Array α → List α - | [], _ => l - | a :: l, acc => bif p a then acc.toListAppend l else go l (acc.push a) - -@[csimp] theorem eraseP_eq_erasePTR : @eraseP = @erasePTR := by - funext α p l; simp [erasePTR] - let rec go (acc) : ∀ xs, l = acc.data ++ xs → - erasePTR.go p l xs acc = acc.data ++ xs.eraseP p - | [] => fun h => by simp [erasePTR.go, eraseP, h] - | x::xs => by - simp [erasePTR.go, eraseP]; cases p x <;> simp - · intro h; rw [go _ xs]; {simp}; simp [h] - exact (go #[] _ rfl).symm - /-- `extractP p l` returns a pair of an element `a` of `l` satisfying the predicate `p`, and `l`, with `a` removed. If there is no such element `a` it returns `(none, l)`. @@ -806,46 +679,6 @@ where rename_i a as b bs; unfold cond; cases R a b <;> simp [go as bs] exact (go as bs [] []).symm -section Pairwise - -variable (R : α → α → Prop) - -/-- -`Pairwise R l` means that all the elements with earlier indexes are -`R`-related to all the elements with later indexes. -``` -Pairwise R [1, 2, 3] ↔ R 1 2 ∧ R 1 3 ∧ R 2 3 -``` -For example if `R = (·≠·)` then it asserts `l` has no duplicates, -and if `R = (·<·)` then it asserts that `l` is (strictly) sorted. --/ -inductive Pairwise : List α → Prop - /-- All elements of the empty list are vacuously pairwise related. -/ - | nil : Pairwise [] - /-- `a :: l` is `Pairwise R` if `a` `R`-relates to every element of `l`, - and `l` is `Pairwise R`. -/ - | cons : ∀ {a : α} {l : List α}, (∀ a' ∈ l, R a a') → Pairwise l → Pairwise (a :: l) - -attribute [simp] Pairwise.nil - -variable {R} - -@[simp] theorem pairwise_cons : Pairwise R (a::l) ↔ (∀ a' ∈ l, R a a') ∧ Pairwise R l := - ⟨fun | .cons h₁ h₂ => ⟨h₁, h₂⟩, fun ⟨h₁, h₂⟩ => h₂.cons h₁⟩ - -instance instDecidablePairwise [DecidableRel R] : - (l : List α) → Decidable (Pairwise R l) - | [] => isTrue .nil - | hd :: tl => - match instDecidablePairwise tl with - | isTrue ht => - match decidableBAll (R hd) tl with - | isFalse hf => isFalse fun hf' => hf (pairwise_cons.1 hf').1 - | isTrue ht' => isTrue <| pairwise_cons.mpr (And.intro ht' ht) - | isFalse hf => isFalse fun | .cons _ ih => hf ih - -end Pairwise - /-- `pwFilter R l` is a maximal sublist of `l` which is `Pairwise R`. `pwFilter (·≠·)` is the erase duplicates function (cf. `eraseDup`), and `pwFilter (·<·)` finds @@ -881,47 +714,12 @@ def Chain' : List α → Prop end Chain -/-- `Nodup l` means that `l` has no duplicates, that is, any element appears at most - once in the List. It is defined as `Pairwise (≠)`. -/ -def Nodup : List α → Prop := Pairwise (· ≠ ·) - -instance nodupDecidable [DecidableEq α] : ∀ l : List α, Decidable (Nodup l) := - instDecidablePairwise - /-- `eraseDup l` removes duplicates from `l` (taking only the first occurrence). Defined as `pwFilter (≠)`. eraseDup [1, 0, 2, 2, 1] = [0, 2, 1] -/ @[inline] def eraseDup [BEq α] : List α → List α := pwFilter (· != ·) -/-- `range' start len step` is the list of numbers `[start, start+step, ..., start+(len-1)*step]`. - It is intended mainly for proving properties of `range` and `iota`. -/ -def range' : (start len : Nat) → (step : Nat := 1) → List Nat - | _, 0, _ => [] - | s, n+1, step => s :: range' (s+step) n step - -/-- Optimized version of `range'`. -/ -@[inline] def range'TR (s n : Nat) (step : Nat := 1) : List Nat := go n (s + step * n) [] where - /-- Auxiliary for `range'TR`: `range'TR.go n e = [e-n, ..., e-1] ++ acc`. -/ - go : Nat → Nat → List Nat → List Nat - | 0, _, acc => acc - | n+1, e, acc => go n (e-step) ((e-step) :: acc) - -@[csimp] theorem range'_eq_range'TR : @range' = @range'TR := by - funext s n step - let rec go (s) : ∀ n m, - range'TR.go step n (s + step * n) (range' (s + step * n) m step) = range' s (n + m) step - | 0, m => by simp [range'TR.go] - | n+1, m => by - simp [range'TR.go] - rw [Nat.mul_succ, ← Nat.add_assoc, Nat.add_sub_cancel, Nat.add_right_comm n] - exact go s n (m + 1) - exact (go s n 0).symm - -/-- Drop `none`s from a list, and replace each remaining `some a` with `a`. -/ -@[inline] def reduceOption {α} : List (Option α) → List α := - List.filterMap id - /-- `ilast' x xs` returns the last element of `xs` if `xs` is non-empty; it returns `x` otherwise. Use `List.getLastD` instead. diff --git a/Batteries/Data/List/Count.lean b/Batteries/Data/List/Count.lean index dfd1481052..036a76b4b8 100644 --- a/Batteries/Data/List/Count.lean +++ b/Batteries/Data/List/Count.lean @@ -19,111 +19,6 @@ open Nat namespace List -section countP - -variable (p q : α → Bool) - -@[simp] theorem countP_nil : countP p [] = 0 := rfl - -protected theorem countP_go_eq_add (l) : countP.go p l n = n + countP.go p l 0 := by - induction l generalizing n with - | nil => rfl - | cons head tail ih => - unfold countP.go - rw [ih (n := n + 1), ih (n := n), ih (n := 1)] - if h : p head then simp [h, Nat.add_assoc] else simp [h] - -@[simp] theorem countP_cons_of_pos (l) (pa : p a) : countP p (a :: l) = countP p l + 1 := by - have : countP.go p (a :: l) 0 = countP.go p l 1 := show cond .. = _ by rw [pa]; rfl - unfold countP - rw [this, Nat.add_comm, List.countP_go_eq_add] - -@[simp] theorem countP_cons_of_neg (l) (pa : ¬p a) : countP p (a :: l) = countP p l := by - simp [countP, countP.go, pa] - -theorem countP_cons (a : α) (l) : countP p (a :: l) = countP p l + if p a then 1 else 0 := by - by_cases h : p a <;> simp [h] - -theorem length_eq_countP_add_countP (l) : length l = countP p l + countP (fun a => ¬p a) l := by - induction l with - | nil => rfl - | cons x h ih => - if h : p x then - rw [countP_cons_of_pos _ _ h, countP_cons_of_neg _ _ _, length, ih] - · rw [Nat.add_assoc, Nat.add_comm _ 1, Nat.add_assoc] - · simp only [h, not_true_eq_false, decide_False, not_false_eq_true] - else - rw [countP_cons_of_pos (fun a => ¬p a) _ _, countP_cons_of_neg _ _ h, length, ih] - · rfl - · simp only [h, not_false_eq_true, decide_True] - -theorem countP_eq_length_filter (l) : countP p l = length (filter p l) := by - induction l with - | nil => rfl - | cons x l ih => - if h : p x - then rw [countP_cons_of_pos p l h, ih, filter_cons_of_pos l h, length] - else rw [countP_cons_of_neg p l h, ih, filter_cons_of_neg l h] - -theorem countP_le_length : countP p l ≤ l.length := by - simp only [countP_eq_length_filter] - apply length_filter_le - -@[simp] theorem countP_append (l₁ l₂) : countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂ := by - simp only [countP_eq_length_filter, filter_append, length_append] - -theorem countP_pos : 0 < countP p l ↔ ∃ a ∈ l, p a := by - simp only [countP_eq_length_filter, length_pos_iff_exists_mem, mem_filter, exists_prop] - -theorem countP_eq_zero : countP p l = 0 ↔ ∀ a ∈ l, ¬p a := by - simp only [countP_eq_length_filter, length_eq_zero, filter_eq_nil] - -theorem countP_eq_length : countP p l = l.length ↔ ∀ a ∈ l, p a := by - rw [countP_eq_length_filter, filter_length_eq_length] - -theorem Sublist.countP_le (s : l₁ <+ l₂) : countP p l₁ ≤ countP p l₂ := by - simp only [countP_eq_length_filter] - apply s.filter _ |>.length_le - -theorem countP_filter (l : List α) : - countP p (filter q l) = countP (fun a => p a ∧ q a) l := by - simp only [countP_eq_length_filter, filter_filter] - -@[simp] theorem countP_true {l : List α} : (l.countP fun _ => true) = l.length := by - rw [countP_eq_length] - simp - -@[simp] theorem countP_false {l : List α} : (l.countP fun _ => false) = 0 := by - rw [countP_eq_zero] - simp - -@[simp] theorem countP_map (p : β → Bool) (f : α → β) : - ∀ l, countP p (map f l) = countP (p ∘ f) l - | [] => rfl - | a :: l => by rw [map_cons, countP_cons, countP_cons, countP_map p f l]; rfl - -variable {p q} - -theorem countP_mono_left (h : ∀ x ∈ l, p x → q x) : countP p l ≤ countP q l := by - induction l with - | nil => apply Nat.le_refl - | cons a l ihl => - rw [forall_mem_cons] at h - have ⟨ha, hl⟩ := h - simp [countP_cons] - cases h : p a - . simp - apply Nat.le_trans ?_ (Nat.le_add_right _ _) - apply ihl hl - . simp [ha h] - apply ihl hl - -theorem countP_congr (h : ∀ x ∈ l, p x ↔ q x) : countP p l = countP q l := - Nat.le_antisymm - (countP_mono_left fun x hx => (h x hx).1) - (countP_mono_left fun x hx => (h x hx).2) - -end countP /-! ### count -/ @@ -131,71 +26,10 @@ section count variable [DecidableEq α] -@[simp] theorem count_nil (a : α) : count a [] = 0 := rfl - -theorem count_cons (a b : α) (l : List α) : - count a (b :: l) = count a l + if a = b then 1 else 0 := by - simp [count, countP_cons, eq_comm (a := a)] - -@[simp] theorem count_cons_self (a : α) (l : List α) : count a (a :: l) = count a l + 1 := by - simp [count_cons] - -@[simp] theorem count_cons_of_ne (h : a ≠ b) (l : List α) : count a (b :: l) = count a l := by - simp [count_cons, h] - -theorem count_tail : ∀ (l : List α) (a : α) (h : l ≠ []), - l.tail.count a = l.count a - if a = l.head h then 1 else 0 - | head :: tail, a, h => by simp [count_cons] - -theorem count_le_length (a : α) (l : List α) : count a l ≤ l.length := countP_le_length _ - -theorem Sublist.count_le (h : l₁ <+ l₂) (a : α) : count a l₁ ≤ count a l₂ := h.countP_le _ - -theorem count_le_count_cons (a b : α) (l : List α) : count a l ≤ count a (b :: l) := - (sublist_cons _ _).count_le _ - -theorem count_singleton (a : α) : count a [a] = 1 := by simp - -theorem count_singleton' (a b : α) : count a [b] = if a = b then 1 else 0 := by simp [count_cons] - -@[simp] theorem count_append (a : α) : ∀ l₁ l₂, count a (l₁ ++ l₂) = count a l₁ + count a l₂ := - countP_append _ +theorem count_singleton' (a b : α) : count a [b] = if b = a then 1 else 0 := by simp [count_cons] theorem count_concat (a : α) (l : List α) : count a (concat l a) = succ (count a l) := by simp -@[simp] -theorem count_pos_iff_mem {a : α} {l : List α} : 0 < count a l ↔ a ∈ l := by - simp only [count, countP_pos, beq_iff_eq, exists_eq_right] - -@[simp 900] theorem count_eq_zero_of_not_mem {a : α} {l : List α} (h : a ∉ l) : count a l = 0 := - Decidable.byContradiction fun h' => h <| count_pos_iff_mem.1 (Nat.pos_of_ne_zero h') - -theorem not_mem_of_count_eq_zero {a : α} {l : List α} (h : count a l = 0) : a ∉ l := - fun h' => Nat.ne_of_lt (count_pos_iff_mem.2 h') h.symm - -theorem count_eq_zero {l : List α} : count a l = 0 ↔ a ∉ l := - ⟨not_mem_of_count_eq_zero, count_eq_zero_of_not_mem⟩ - -theorem count_eq_length {l : List α} : count a l = l.length ↔ ∀ b ∈ l, a = b := by - rw [count, countP_eq_length] - refine ⟨fun h b hb => Eq.symm ?_, fun h b hb => ?_⟩ - · simpa using h b hb - · rw [h b hb, beq_self_eq_true] - -@[simp] theorem count_replicate_self (a : α) (n : Nat) : count a (replicate n a) = n := - (count_eq_length.2 <| fun _ h => (eq_of_mem_replicate h).symm).trans (length_replicate ..) - -theorem count_replicate (a b : α) (n : Nat) : count a (replicate n b) = if a = b then n else 0 := by - split - exacts [‹a = b› ▸ count_replicate_self .., count_eq_zero.2 <| mt eq_of_mem_replicate ‹a ≠ b›] - -theorem filter_beq (l : List α) (a : α) : l.filter (· == a) = replicate (count a l) a := by - simp only [count, countP_eq_length_filter, eq_replicate, mem_filter, beq_iff_eq] - exact ⟨trivial, fun _ h => h.2⟩ - -theorem filter_eq (l : List α) (a : α) : l.filter (· = a) = replicate (count a l) a := - filter_beq l a - @[deprecated filter_eq (since := "2023-12-14")] theorem filter_eq' (l : List α) (a : α) : l.filter (a = ·) = replicate (count a l) a := by simpa only [eq_comm] using filter_eq l a @@ -203,46 +37,3 @@ theorem filter_eq' (l : List α) (a : α) : l.filter (a = ·) = replicate (count @[deprecated filter_beq (since := "2023-12-14")] theorem filter_beq' (l : List α) (a : α) : l.filter (a == ·) = replicate (count a l) a := by simpa only [eq_comm (b := a)] using filter_eq l a - -theorem le_count_iff_replicate_sublist {l : List α} : n ≤ count a l ↔ replicate n a <+ l := by - refine ⟨fun h => ?_, fun h => ?_⟩ - · exact ((replicate_sublist_replicate a).2 h).trans <| filter_eq l a ▸ filter_sublist _ - · simpa only [count_replicate_self] using h.count_le a - -theorem replicate_count_eq_of_count_eq_length {l : List α} (h : count a l = length l) : - replicate (count a l) a = l := - (le_count_iff_replicate_sublist.mp (Nat.le_refl _)).eq_of_length <| - (length_replicate (count a l) a).trans h - -@[simp] theorem count_filter {l : List α} (h : p a) : count a (filter p l) = count a l := by - rw [count, countP_filter]; congr; funext b - rw [(by rfl : (b == a) = decide (b = a)), decide_eq_decide] - simp; rintro rfl; exact h - -theorem count_le_count_map [DecidableEq β] (l : List α) (f : α → β) (x : α) : - count x l ≤ count (f x) (map f l) := by - rw [count, count, countP_map] - apply countP_mono_left; simp (config := { contextual := true }) - -theorem count_erase (a b : α) : - ∀ l : List α, count a (l.erase b) = count a l - if a = b then 1 else 0 - | [] => by simp - | c :: l => by - rw [erase_cons] - if hc : c = b then - have hc_beq := (beq_iff_eq _ _).mpr hc - rw [if_pos hc_beq, hc, count_cons, Nat.add_sub_cancel] - else - have hc_beq := beq_false_of_ne hc - simp only [hc_beq, if_false, count_cons, count_cons, count_erase a b l] - if ha : a = b then - rw [← ha, eq_comm] at hc - rw [if_pos ha, if_neg hc, Nat.add_zero, Nat.add_zero] - else - rw [if_neg ha, Nat.sub_zero, Nat.sub_zero] - -@[simp] theorem count_erase_self (a : α) (l : List α) : - count a (List.erase l a) = count a l - 1 := by rw [count_erase, if_pos rfl] - -@[simp] theorem count_erase_of_ne (ab : a ≠ b) (l : List α) : count a (l.erase b) = count a l := by - rw [count_erase, if_neg ab, Nat.sub_zero] diff --git a/Batteries/Data/List/EraseIdx.lean b/Batteries/Data/List/EraseIdx.lean index ca3cf2e716..42b4bfacd1 100644 --- a/Batteries/Data/List/EraseIdx.lean +++ b/Batteries/Data/List/EraseIdx.lean @@ -17,75 +17,15 @@ namespace List universe u v variable {α : Type u} {β : Type v} -@[simp] theorem eraseIdx_zero (l : List α) : eraseIdx l 0 = tail l := by cases l <;> rfl - -theorem eraseIdx_eq_take_drop_succ : - ∀ (l : List α) (i : Nat), l.eraseIdx i = l.take i ++ l.drop (i + 1) - | nil, _ => by simp - | a::l, 0 => by simp - | a::l, i + 1 => by simp [eraseIdx_eq_take_drop_succ l i] - -theorem eraseIdx_sublist : ∀ (l : List α) (k : Nat), eraseIdx l k <+ l - | [], _ => by simp - | a::l, 0 => by simp - | a::l, k + 1 => by simp [eraseIdx_sublist l k] - -theorem eraseIdx_subset (l : List α) (k : Nat) : eraseIdx l k ⊆ l := (eraseIdx_sublist l k).subset - -@[simp] -theorem eraseIdx_eq_self : ∀ {l : List α} {k : Nat}, eraseIdx l k = l ↔ length l ≤ k - | [], _ => by simp - | a::l, 0 => by simp [(cons_ne_self _ _).symm] - | a::l, k + 1 => by simp [eraseIdx_eq_self] - -alias ⟨_, eraseIdx_of_length_le⟩ := eraseIdx_eq_self - -theorem eraseIdx_append_of_lt_length {l : List α} {k : Nat} (hk : k < length l) (l' : List α) : - eraseIdx (l ++ l') k = eraseIdx l k ++ l' := by - rw [eraseIdx_eq_take_drop_succ, take_append_of_le_length, drop_append_of_le_length, - eraseIdx_eq_take_drop_succ, append_assoc] - all_goals omega - -theorem eraseIdx_append_of_length_le {l : List α} {k : Nat} (hk : length l ≤ k) (l' : List α) : - eraseIdx (l ++ l') k = l ++ eraseIdx l' (k - length l) := by - rw [eraseIdx_eq_take_drop_succ, eraseIdx_eq_take_drop_succ, - take_append_eq_append_take, drop_append_eq_append_drop, - take_all_of_le hk, drop_eq_nil_of_le (by omega), nil_append, append_assoc] - congr - omega - -protected theorem IsPrefix.eraseIdx {l l' : List α} (h : l <+: l') (k : Nat) : - eraseIdx l k <+: eraseIdx l' k := by - rcases h with ⟨t, rfl⟩ - if hkl : k < length l then - simp [eraseIdx_append_of_lt_length hkl] - else - rw [Nat.not_lt] at hkl - simp [eraseIdx_append_of_length_le hkl, eraseIdx_of_length_le hkl] - -theorem mem_eraseIdx_iff_getElem {x : α} : - ∀ {l} {k}, x ∈ eraseIdx l k ↔ ∃ i : Fin l.length, ↑i ≠ k ∧ l[i.1] = x - | [], _ => by - simp only [eraseIdx, Fin.exists_iff, not_mem_nil, false_iff] - rintro ⟨i, h, -⟩ - exact Nat.not_lt_zero _ h - | a::l, 0 => by simp [Fin.exists_fin_succ, mem_iff_get] - | a::l, k+1 => by - simp [Fin.exists_fin_succ, mem_eraseIdx_iff_getElem, @eq_comm _ a, k.succ_ne_zero.symm] - @[deprecated mem_eraseIdx_iff_getElem (since := "2024-06-12")] theorem mem_eraseIdx_iff_get {x : α} {l} {k} : x ∈ eraseIdx l k ↔ ∃ i : Fin l.length, ↑i ≠ k ∧ l.get i = x := by - simp [mem_eraseIdx_iff_getElem] - -theorem mem_eraseIdx_iff_getElem? {x : α} {l} {k} : x ∈ eraseIdx l k ↔ ∃ i ≠ k, l[i]? = some x := by - simp only [mem_eraseIdx_iff_getElem, getElem_eq_iff, Fin.exists_iff, exists_and_left] - refine exists_congr fun i => and_congr_right' ?_ + simp only [mem_eraseIdx_iff_getElem, ne_eq, exists_and_left, get_eq_getElem] constructor - · rintro ⟨_, h⟩; exact h - · rintro h; - obtain ⟨h', -⟩ := getElem?_eq_some.1 h - exact ⟨h', h⟩ + · rintro ⟨i, h, w, rfl⟩ + exact ⟨⟨i, w⟩, h, rfl⟩ + · rintro ⟨i, h, rfl⟩ + exact ⟨i.1, h, i.2, rfl⟩ @[deprecated mem_eraseIdx_iff_getElem? (since := "2024-06-12")] theorem mem_eraseIdx_iff_get? {x : α} {l} {k} : x ∈ eraseIdx l k ↔ ∃ i ≠ k, l.get? i = x := by diff --git a/Batteries/Data/List/Init/Attach.lean b/Batteries/Data/List/Init/Attach.lean deleted file mode 100644 index d2b2bf0990..0000000000 --- a/Batteries/Data/List/Init/Attach.lean +++ /dev/null @@ -1,44 +0,0 @@ -/- -Copyright (c) 2023 Mario Carneiro. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Mario Carneiro --/ - -namespace List - -/-- `O(n)`. Partial map. If `f : Π a, P a → β` is a partial function defined on - `a : α` satisfying `P`, then `pmap f l h` is essentially the same as `map f l` - but is defined only when all members of `l` satisfy `P`, using the proof - to apply `f`. -/ -@[simp] def pmap {P : α → Prop} (f : ∀ a, P a → β) : ∀ l : List α, (H : ∀ a ∈ l, P a) → List β - | [], _ => [] - | a :: l, H => f a (forall_mem_cons.1 H).1 :: pmap f l (forall_mem_cons.1 H).2 - -/-- -Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of -`List {x // P x}` is the same as the input `List α`. -(Someday, the compiler might do this optimization automatically, but until then...) --/ -@[inline] private unsafe def attachWithImpl - (l : List α) (P : α → Prop) (_ : ∀ x ∈ l, P x) : List {x // P x} := unsafeCast l - -/-- `O(1)`. "Attach" a proof `P x` that holds for all the elements of `l` to produce a new list - with the same elements but in the type `{x // P x}`. -/ -@[implemented_by attachWithImpl] def attachWith - (l : List α) (P : α → Prop) (H : ∀ x ∈ l, P x) : List {x // P x} := pmap Subtype.mk l H - -/-- `O(1)`. "Attach" the proof that the elements of `l` are in `l` to produce a new list - with the same elements but in the type `{x // x ∈ l}`. -/ -@[inline] def attach (l : List α) : List {x // x ∈ l} := attachWith l _ fun _ => id - -/-- Implementation of `pmap` using the zero-copy version of `attach`. -/ -@[inline] private def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (l : List α) (H : ∀ a ∈ l, P a) : - List β := (l.attachWith _ H).map fun ⟨x, h'⟩ => f x h' - -@[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by - funext α β p f L h' - let rec go : ∀ L' (hL' : ∀ ⦃x⦄, x ∈ L' → p x), - pmap f L' hL' = map (fun ⟨x, hx⟩ => f x hx) (pmap Subtype.mk L' hL') - | nil, hL' => rfl - | cons _ L', hL' => congrArg _ <| go L' fun _ hx => hL' (.tail _ hx) - exact go L h' diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index 533a140f45..2e97cb5264 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -17,225 +17,6 @@ open Nat @[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by simp [Array.mem_def] -/-! ### drop -/ - -@[simp] -theorem drop_one : ∀ l : List α, drop 1 l = tail l - | [] | _ :: _ => rfl - -/-! ### zipWith -/ - -theorem zipWith_distrib_tail : (zipWith f l l').tail = zipWith f l.tail l'.tail := by - rw [← drop_one]; simp [zipWith_distrib_drop] - -/-! ### List subset -/ - -theorem subset_def {l₁ l₂ : List α} : l₁ ⊆ l₂ ↔ ∀ {a : α}, a ∈ l₁ → a ∈ l₂ := .rfl - -@[simp] theorem nil_subset (l : List α) : [] ⊆ l := nofun - -@[simp] theorem Subset.refl (l : List α) : l ⊆ l := fun _ i => i - -theorem Subset.trans {l₁ l₂ l₃ : List α} (h₁ : l₁ ⊆ l₂) (h₂ : l₂ ⊆ l₃) : l₁ ⊆ l₃ := - fun _ i => h₂ (h₁ i) - -instance : Trans (Membership.mem : α → List α → Prop) Subset Membership.mem := - ⟨fun h₁ h₂ => h₂ h₁⟩ - -instance : Trans (Subset : List α → List α → Prop) Subset Subset := - ⟨Subset.trans⟩ - -@[simp] theorem subset_cons (a : α) (l : List α) : l ⊆ a :: l := fun _ => Mem.tail _ - -theorem subset_of_cons_subset {a : α} {l₁ l₂ : List α} : a :: l₁ ⊆ l₂ → l₁ ⊆ l₂ := - fun s _ i => s (mem_cons_of_mem _ i) - -theorem subset_cons_of_subset (a : α) {l₁ l₂ : List α} : l₁ ⊆ l₂ → l₁ ⊆ a :: l₂ := - fun s _ i => .tail _ (s i) - -theorem cons_subset_cons {l₁ l₂ : List α} (a : α) (s : l₁ ⊆ l₂) : a :: l₁ ⊆ a :: l₂ := - fun _ => by simp only [mem_cons]; exact Or.imp_right (@s _) - -@[simp] theorem subset_append_left (l₁ l₂ : List α) : l₁ ⊆ l₁ ++ l₂ := fun _ => mem_append_left _ - -@[simp] theorem subset_append_right (l₁ l₂ : List α) : l₂ ⊆ l₁ ++ l₂ := fun _ => mem_append_right _ - -theorem subset_append_of_subset_left (l₂ : List α) : l ⊆ l₁ → l ⊆ l₁ ++ l₂ := -fun s => Subset.trans s <| subset_append_left _ _ - -theorem subset_append_of_subset_right (l₁ : List α) : l ⊆ l₂ → l ⊆ l₁ ++ l₂ := -fun s => Subset.trans s <| subset_append_right _ _ - -@[simp] theorem cons_subset : a :: l ⊆ m ↔ a ∈ m ∧ l ⊆ m := by - simp only [subset_def, mem_cons, or_imp, forall_and, forall_eq] - -@[simp] theorem append_subset {l₁ l₂ l : List α} : - l₁ ++ l₂ ⊆ l ↔ l₁ ⊆ l ∧ l₂ ⊆ l := by simp [subset_def, or_imp, forall_and] - -theorem subset_nil {l : List α} : l ⊆ [] ↔ l = [] := - ⟨fun h => match l with | [] => rfl | _::_ => (nomatch h (.head ..)), fun | rfl => Subset.refl _⟩ - -theorem map_subset {l₁ l₂ : List α} (f : α → β) (H : l₁ ⊆ l₂) : map f l₁ ⊆ map f l₂ := - fun x => by simp only [mem_map]; exact .imp fun a => .imp_left (@H _) - -/-! ### sublists -/ - -@[simp] theorem nil_sublist : ∀ l : List α, [] <+ l - | [] => .slnil - | a :: l => (nil_sublist l).cons a - -@[simp] theorem Sublist.refl : ∀ l : List α, l <+ l - | [] => .slnil - | a :: l => (Sublist.refl l).cons₂ a - -theorem Sublist.trans {l₁ l₂ l₃ : List α} (h₁ : l₁ <+ l₂) (h₂ : l₂ <+ l₃) : l₁ <+ l₃ := by - induction h₂ generalizing l₁ with - | slnil => exact h₁ - | cons _ _ IH => exact (IH h₁).cons _ - | @cons₂ l₂ _ a _ IH => - generalize e : a :: l₂ = l₂' - match e ▸ h₁ with - | .slnil => apply nil_sublist - | .cons a' h₁' => cases e; apply (IH h₁').cons - | .cons₂ a' h₁' => cases e; apply (IH h₁').cons₂ - -instance : Trans (@Sublist α) Sublist Sublist := ⟨Sublist.trans⟩ - -@[simp] theorem sublist_cons (a : α) (l : List α) : l <+ a :: l := (Sublist.refl l).cons _ - -theorem sublist_of_cons_sublist : a :: l₁ <+ l₂ → l₁ <+ l₂ := - (sublist_cons a l₁).trans - -@[simp] theorem sublist_append_left : ∀ l₁ l₂ : List α, l₁ <+ l₁ ++ l₂ - | [], _ => nil_sublist _ - | _ :: l₁, l₂ => (sublist_append_left l₁ l₂).cons₂ _ - -@[simp] theorem sublist_append_right : ∀ l₁ l₂ : List α, l₂ <+ l₁ ++ l₂ - | [], _ => Sublist.refl _ - | _ :: l₁, l₂ => (sublist_append_right l₁ l₂).cons _ - -theorem sublist_append_of_sublist_left (s : l <+ l₁) : l <+ l₁ ++ l₂ := - s.trans <| sublist_append_left .. - -theorem sublist_append_of_sublist_right (s : l <+ l₂) : l <+ l₁ ++ l₂ := - s.trans <| sublist_append_right .. - -@[simp] -theorem cons_sublist_cons : a :: l₁ <+ a :: l₂ ↔ l₁ <+ l₂ := - ⟨fun | .cons _ s => sublist_of_cons_sublist s | .cons₂ _ s => s, .cons₂ _⟩ - -@[simp] theorem append_sublist_append_left : ∀ l, l ++ l₁ <+ l ++ l₂ ↔ l₁ <+ l₂ - | [] => Iff.rfl - | _ :: l => cons_sublist_cons.trans (append_sublist_append_left l) - -theorem Sublist.append_left : l₁ <+ l₂ → ∀ l, l ++ l₁ <+ l ++ l₂ := - fun h l => (append_sublist_append_left l).mpr h - -theorem Sublist.append_right : l₁ <+ l₂ → ∀ l, l₁ ++ l <+ l₂ ++ l - | .slnil, _ => Sublist.refl _ - | .cons _ h, _ => (h.append_right _).cons _ - | .cons₂ _ h, _ => (h.append_right _).cons₂ _ - -theorem sublist_or_mem_of_sublist (h : l <+ l₁ ++ a :: l₂) : l <+ l₁ ++ l₂ ∨ a ∈ l := by - induction l₁ generalizing l with - | nil => match h with - | .cons _ h => exact .inl h - | .cons₂ _ h => exact .inr (.head ..) - | cons b l₁ IH => - match h with - | .cons _ h => exact (IH h).imp_left (Sublist.cons _) - | .cons₂ _ h => exact (IH h).imp (Sublist.cons₂ _) (.tail _) - -theorem Sublist.reverse : l₁ <+ l₂ → l₁.reverse <+ l₂.reverse - | .slnil => Sublist.refl _ - | .cons _ h => by rw [reverse_cons]; exact sublist_append_of_sublist_left h.reverse - | .cons₂ _ h => by rw [reverse_cons, reverse_cons]; exact h.reverse.append_right _ - -@[simp] theorem reverse_sublist : l₁.reverse <+ l₂.reverse ↔ l₁ <+ l₂ := - ⟨fun h => l₁.reverse_reverse ▸ l₂.reverse_reverse ▸ h.reverse, Sublist.reverse⟩ - -@[simp] theorem append_sublist_append_right (l) : l₁ ++ l <+ l₂ ++ l ↔ l₁ <+ l₂ := - ⟨fun h => by - have := h.reverse - simp only [reverse_append, append_sublist_append_left, reverse_sublist] at this - exact this, - fun h => h.append_right l⟩ - -theorem Sublist.append (hl : l₁ <+ l₂) (hr : r₁ <+ r₂) : l₁ ++ r₁ <+ l₂ ++ r₂ := - (hl.append_right _).trans ((append_sublist_append_left _).2 hr) - -theorem Sublist.subset : l₁ <+ l₂ → l₁ ⊆ l₂ - | .slnil, _, h => h - | .cons _ s, _, h => .tail _ (s.subset h) - | .cons₂ .., _, .head .. => .head .. - | .cons₂ _ s, _, .tail _ h => .tail _ (s.subset h) - -instance : Trans (@Sublist α) Subset Subset := - ⟨fun h₁ h₂ => trans h₁.subset h₂⟩ - -instance : Trans Subset (@Sublist α) Subset := - ⟨fun h₁ h₂ => trans h₁ h₂.subset⟩ - -instance : Trans (Membership.mem : α → List α → Prop) Sublist Membership.mem := - ⟨fun h₁ h₂ => h₂.subset h₁⟩ - -theorem Sublist.length_le : l₁ <+ l₂ → length l₁ ≤ length l₂ - | .slnil => Nat.le_refl 0 - | .cons _l s => le_succ_of_le (length_le s) - | .cons₂ _ s => succ_le_succ (length_le s) - -@[simp] theorem sublist_nil {l : List α} : l <+ [] ↔ l = [] := - ⟨fun s => subset_nil.1 s.subset, fun H => H ▸ Sublist.refl _⟩ - -theorem Sublist.eq_of_length : l₁ <+ l₂ → length l₁ = length l₂ → l₁ = l₂ - | .slnil, _ => rfl - | .cons a s, h => nomatch Nat.not_lt.2 s.length_le (h ▸ lt_succ_self _) - | .cons₂ a s, h => by rw [s.eq_of_length (succ.inj h)] - -theorem Sublist.eq_of_length_le (s : l₁ <+ l₂) (h : length l₂ ≤ length l₁) : l₁ = l₂ := - s.eq_of_length <| Nat.le_antisymm s.length_le h - -@[simp] theorem singleton_sublist {a : α} {l} : [a] <+ l ↔ a ∈ l := by - refine ⟨fun h => h.subset (mem_singleton_self _), fun h => ?_⟩ - obtain ⟨_, _, rfl⟩ := append_of_mem h - exact ((nil_sublist _).cons₂ _).trans (sublist_append_right ..) - -@[simp] theorem replicate_sublist_replicate {m n} (a : α) : - replicate m a <+ replicate n a ↔ m ≤ n := by - refine ⟨fun h => ?_, fun h => ?_⟩ - · have := h.length_le; simp only [length_replicate] at this ⊢; exact this - · induction h with - | refl => apply Sublist.refl - | step => simp [*, replicate, Sublist.cons] - -theorem isSublist_iff_sublist [BEq α] [LawfulBEq α] {l₁ l₂ : List α} : - l₁.isSublist l₂ ↔ l₁ <+ l₂ := by - cases l₁ <;> cases l₂ <;> simp [isSublist] - case cons.cons hd₁ tl₁ hd₂ tl₂ => - if h_eq : hd₁ = hd₂ then - simp [h_eq, cons_sublist_cons, isSublist_iff_sublist] - else - simp only [beq_iff_eq, h_eq] - constructor - · intro h_sub - apply Sublist.cons - exact isSublist_iff_sublist.mp h_sub - · intro h_sub - cases h_sub - case cons h_sub => - exact isSublist_iff_sublist.mpr h_sub - case cons₂ => - contradiction - -instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+ l₂) := - decidable_of_iff (l₁.isSublist l₂) isSublist_iff_sublist - -/-! ### tail -/ - -theorem tail_eq_tailD (l) : @tail α l = tailD l [] := by cases l <;> rfl - -theorem tail_eq_tail? (l) : @tail α l = (tail? l).getD [] := by simp [tail_eq_tailD] - /-! ### next? -/ @[simp] theorem next?_nil : @next? α [] = none := rfl @@ -243,51 +24,16 @@ theorem tail_eq_tail? (l) : @tail α l = (tail? l).getD [] := by simp [tail_eq_t /-! ### get? -/ -theorem getElem_eq_iff {l : List α} {n : Nat} {h : n < l.length} : l[n] = x ↔ l[n]? = some x := by - simp only [get_eq_getElem, get?_eq_getElem?, getElem?_eq_some] - exact ⟨fun w => ⟨h, w⟩, fun h => h.2⟩ - @[deprecated getElem_eq_iff (since := "2024-06-12")] theorem get_eq_iff : List.get l n = x ↔ l.get? n.1 = some x := by simp -theorem getElem?_inj - (h₀ : i < xs.length) (h₁ : Nodup xs) (h₂ : xs[i]? = xs[j]?) : i = j := by - induction xs generalizing i j with - | nil => cases h₀ - | cons x xs ih => - match i, j with - | 0, 0 => rfl - | i+1, j+1 => simp; cases h₁ with - | cons ha h₁ => - simp only [getElem?_cons_succ] at h₂ - exact ih (Nat.lt_of_succ_lt_succ h₀) h₁ h₂ - | i+1, 0 => ?_ - | 0, j+1 => ?_ - all_goals - simp only [get?_eq_getElem?, getElem?_cons_zero, getElem?_cons_succ] at h₂ - cases h₁; rename_i h' h - have := h x ?_ rfl; cases this - rw [mem_iff_get?] - simp only [get?_eq_getElem?] - exact ⟨_, h₂⟩; exact ⟨_ , h₂.symm⟩ - @[deprecated getElem?_inj (since := "2024-06-12")] theorem get?_inj (h₀ : i < xs.length) (h₁ : Nodup xs) (h₂ : xs.get? i = xs.get? j) : i = j := by apply getElem?_inj h₀ h₁ simp_all -/-! ### drop -/ - -theorem tail_drop (l : List α) (n : Nat) : (l.drop n).tail = l.drop (n + 1) := by - induction l generalizing n with - | nil => simp - | cons hd tl hl => - cases n - · simp - · simp [hl] - /-! ### modifyNth -/ @[simp] theorem modifyNth_nil (f : α → α) (n) : [].modifyNth f n = [] := by cases n <;> rfl @@ -405,18 +151,13 @@ theorem modifyNth_eq_set_get (f : α → α) {n} {l : List α} (h) : l.modifyNth f n = l.set n (f (l.get ⟨n, h⟩)) := by rw [modifyNth_eq_set_get?, get?_eq_get h]; rfl -theorem exists_of_set {l : List α} (h : n < l.length) : +-- The naming of `exists_of_set'` and `exists_of_set` have been swapped. +-- If no one complains, we will remove this version later. +@[deprecated exists_of_set (since := "2024-07-04")] +theorem exists_of_set' {l : List α} (h : n < l.length) : ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ l₁.length = n ∧ l.set n a' = l₁ ++ a' :: l₂ := by rw [set_eq_modifyNth]; exact exists_of_modifyNth _ h -theorem exists_of_set' {l : List α} (h : n < l.length) : - ∃ l₁ l₂, l = l₁ ++ l[n] :: l₂ ∧ l₁.length = n ∧ l.set n a' = l₁ ++ a' :: l₂ := - have ⟨_, _, _, h₁, h₂, h₃⟩ := exists_of_set h; ⟨_, _, getElem_of_append h₁ h₂ ▸ h₁, h₂, h₃⟩ - -@[simp] -theorem getElem?_set_eq' (a : α) (n) (l : List α) : (set l n a)[n]? = (fun _ => a) <$> l[n]? := by - simp only [set_eq_modifyNth, getElem?_modifyNth_eq] - @[deprecated getElem?_set_eq' (since := "2024-06-12")] theorem get?_set_eq (a : α) (n) (l : List α) : (set l n a).get? n = (fun _ => a) <$> l.get? n := by simp @@ -433,10 +174,6 @@ theorem get?_set_eq_of_lt (a : α) {n} {l : List α} (h : n < length l) : theorem get?_set_ne (a : α) {m n} (l : List α) (h : m ≠ n) : (set l m a).get? n = l.get? n := by simp [h] -theorem getElem?_set' (a : α) {m n} (l : List α) : - (set l m a)[n]? = if m = n then (fun _ => a) <$> l[n]? else l[n]? := by - by_cases m = n <;> simp [*] - @[deprecated getElem?_set (since := "2024-06-12")] theorem get?_set (a : α) {m n} (l : List α) : (set l m a).get? n = if m = n then (fun _ => a) <$> l.get? n else l.get? n := by @@ -450,123 +187,10 @@ theorem get?_set_of_lt' (a : α) {m n} (l : List α) (h : m < length l) : (set l m a).get? n = if m = n then some a else l.get? n := by simp [getElem?_set]; split <;> subst_vars <;> simp [*, getElem?_eq_getElem h] -theorem drop_set_of_lt (a : α) {n m : Nat} (l : List α) (h : n < m) : - (l.set n a).drop m = l.drop m := - List.ext_getElem? fun i => by rw [getElem?_drop, getElem?_drop, getElem?_set_ne (by omega)] - -theorem take_set_of_lt (a : α) {n m : Nat} (l : List α) (h : m < n) : - (l.set n a).take m = l.take m := - List.ext_getElem? fun i => by - rw [getElem?_take_eq_if, getElem?_take_eq_if] - split - · next h' => rw [getElem?_set_ne (by omega)] - · rfl - -/-! ### removeNth -/ - -theorem length_eraseIdx : ∀ {l i}, i < length l → length (@eraseIdx α l i) = length l - 1 - | [], _, _ => rfl - | _::_, 0, _ => by simp [eraseIdx] - | x::xs, i+1, h => by - have : i < length xs := Nat.lt_of_succ_lt_succ h - simp [eraseIdx, ← Nat.add_one] - rw [length_eraseIdx this, Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) this)] - @[deprecated (since := "2024-05-06")] alias length_removeNth := length_eraseIdx -/-! ### tail -/ - -@[simp] theorem length_tail (l : List α) : length (tail l) = length l - 1 := by cases l <;> rfl - /-! ### eraseP -/ -@[simp] theorem eraseP_nil : [].eraseP p = [] := rfl - -theorem eraseP_cons (a : α) (l : List α) : - (a :: l).eraseP p = bif p a then l else a :: l.eraseP p := rfl - -@[simp] theorem eraseP_cons_of_pos {l : List α} (p) (h : p a) : (a :: l).eraseP p = l := by - simp [eraseP_cons, h] - -@[simp] theorem eraseP_cons_of_neg {l : List α} (p) (h : ¬p a) : - (a :: l).eraseP p = a :: l.eraseP p := by simp [eraseP_cons, h] - -theorem eraseP_of_forall_not {l : List α} (h : ∀ a, a ∈ l → ¬p a) : l.eraseP p = l := by - induction l with - | nil => rfl - | cons _ _ ih => simp [h _ (.head ..), ih (forall_mem_cons.1 h).2] - -theorem exists_of_eraseP : ∀ {l : List α} {a} (al : a ∈ l) (pa : p a), - ∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b) ∧ p a ∧ l = l₁ ++ a :: l₂ ∧ l.eraseP p = l₁ ++ l₂ - | b :: l, a, al, pa => - if pb : p b then - ⟨b, [], l, forall_mem_nil _, pb, by simp [pb]⟩ - else - match al with - | .head .. => nomatch pb pa - | .tail _ al => - let ⟨c, l₁, l₂, h₁, h₂, h₃, h₄⟩ := exists_of_eraseP al pa - ⟨c, b::l₁, l₂, (forall_mem_cons ..).2 ⟨pb, h₁⟩, - h₂, by rw [h₃, cons_append], by simp [pb, h₄]⟩ - -theorem exists_or_eq_self_of_eraseP (p) (l : List α) : - l.eraseP p = l ∨ - ∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b) ∧ p a ∧ l = l₁ ++ a :: l₂ ∧ l.eraseP p = l₁ ++ l₂ := - if h : ∃ a ∈ l, p a then - let ⟨_, ha, pa⟩ := h - .inr (exists_of_eraseP ha pa) - else - .inl (eraseP_of_forall_not (h ⟨·, ·, ·⟩)) - -@[simp] theorem length_eraseP_of_mem (al : a ∈ l) (pa : p a) : - length (l.eraseP p) = Nat.pred (length l) := by - let ⟨_, l₁, l₂, _, _, e₁, e₂⟩ := exists_of_eraseP al pa - rw [e₂]; simp [length_append, e₁]; rfl - -theorem eraseP_append_left {a : α} (pa : p a) : - ∀ {l₁ : List α} l₂, a ∈ l₁ → (l₁++l₂).eraseP p = l₁.eraseP p ++ l₂ - | x :: xs, l₂, h => by - by_cases h' : p x <;> simp [h'] - rw [eraseP_append_left pa l₂ ((mem_cons.1 h).resolve_left (mt _ h'))] - intro | rfl => exact pa - -theorem eraseP_append_right : - ∀ {l₁ : List α} l₂, (∀ b ∈ l₁, ¬p b) → eraseP p (l₁++l₂) = l₁ ++ l₂.eraseP p - | [], l₂, _ => rfl - | x :: xs, l₂, h => by - simp [(forall_mem_cons.1 h).1, eraseP_append_right _ (forall_mem_cons.1 h).2] - -theorem eraseP_sublist (l : List α) : l.eraseP p <+ l := by - match exists_or_eq_self_of_eraseP p l with - | .inl h => rw [h]; apply Sublist.refl - | .inr ⟨c, l₁, l₂, _, _, h₃, h₄⟩ => rw [h₄, h₃]; simp - -theorem eraseP_subset (l : List α) : l.eraseP p ⊆ l := (eraseP_sublist l).subset - -protected theorem Sublist.eraseP : l₁ <+ l₂ → l₁.eraseP p <+ l₂.eraseP p - | .slnil => Sublist.refl _ - | .cons a s => by - by_cases h : p a <;> simp [h] - exacts [s.eraseP.trans (eraseP_sublist _), s.eraseP.cons _] - | .cons₂ a s => by - by_cases h : p a <;> simp [h] - exacts [s, s.eraseP] - -theorem mem_of_mem_eraseP {l : List α} : a ∈ l.eraseP p → a ∈ l := (eraseP_subset _ ·) - -@[simp] theorem mem_eraseP_of_neg {l : List α} (pa : ¬p a) : a ∈ l.eraseP p ↔ a ∈ l := by - refine ⟨mem_of_mem_eraseP, fun al => ?_⟩ - match exists_or_eq_self_of_eraseP p l with - | .inl h => rw [h]; assumption - | .inr ⟨c, l₁, l₂, h₁, h₂, h₃, h₄⟩ => - rw [h₄]; rw [h₃] at al - have : a ≠ c := fun h => (h ▸ pa).elim h₂ - simp [this] at al; simp [al] - -theorem eraseP_map (f : β → α) : ∀ (l : List β), (map f l).eraseP p = map f (l.eraseP (p ∘ f)) - | [] => rfl - | b::l => by by_cases h : p (f b) <;> simp [h, eraseP_map f l, eraseP_cons_of_pos] - @[simp] theorem extractP_eq_find?_eraseP (l : List α) : extractP p l = (find? p l, eraseP p l) := by let rec go (acc) : ∀ xs, l = acc.data ++ xs → @@ -579,216 +203,8 @@ theorem eraseP_map (f : β → α) : ∀ (l : List β), (map f l).eraseP p = map /-! ### erase -/ -section erase -variable [BEq α] - -theorem erase_eq_eraseP' (a : α) (l : List α) : l.erase a = l.eraseP (· == a) := by - induction l - · simp - · next b t ih => - rw [erase_cons, eraseP_cons, ih] - if h : b == a then simp [h] else simp [h] - -theorem erase_eq_eraseP [LawfulBEq α] (a : α) : ∀ l : List α, l.erase a = l.eraseP (a == ·) - | [] => rfl - | b :: l => by - if h : a = b then simp [h] else simp [h, Ne.symm h, erase_eq_eraseP a l] - -theorem exists_erase_eq [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) : - ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.erase a = l₁ ++ l₂ := by - let ⟨_, l₁, l₂, h₁, e, h₂, h₃⟩ := exists_of_eraseP h (beq_self_eq_true _) - rw [erase_eq_eraseP]; exact ⟨l₁, l₂, fun h => h₁ _ h (beq_self_eq_true _), eq_of_beq e ▸ h₂, h₃⟩ - -@[simp] theorem length_erase_of_mem [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) : - length (l.erase a) = Nat.pred (length l) := by - rw [erase_eq_eraseP]; exact length_eraseP_of_mem h (beq_self_eq_true a) - -theorem erase_append_left [LawfulBEq α] {l₁ : List α} (l₂) (h : a ∈ l₁) : - (l₁ ++ l₂).erase a = l₁.erase a ++ l₂ := by - simp [erase_eq_eraseP]; exact eraseP_append_left (beq_self_eq_true a) l₂ h - -theorem erase_append_right [LawfulBEq α] {a : α} {l₁ : List α} (l₂ : List α) (h : a ∉ l₁) : - (l₁ ++ l₂).erase a = (l₁ ++ l₂.erase a) := by - rw [erase_eq_eraseP, erase_eq_eraseP, eraseP_append_right] - intros b h' h''; rw [eq_of_beq h''] at h; exact h h' - -theorem erase_sublist (a : α) (l : List α) : l.erase a <+ l := - erase_eq_eraseP' a l ▸ eraseP_sublist l - -theorem erase_subset (a : α) (l : List α) : l.erase a ⊆ l := (erase_sublist a l).subset - -theorem Sublist.erase (a : α) {l₁ l₂ : List α} (h : l₁ <+ l₂) : l₁.erase a <+ l₂.erase a := by - simp only [erase_eq_eraseP']; exact h.eraseP @[deprecated (since := "2024-04-22")] alias sublist.erase := Sublist.erase -theorem mem_of_mem_erase {a b : α} {l : List α} (h : a ∈ l.erase b) : a ∈ l := erase_subset _ _ h - -@[simp] theorem mem_erase_of_ne [LawfulBEq α] {a b : α} {l : List α} (ab : a ≠ b) : - a ∈ l.erase b ↔ a ∈ l := - erase_eq_eraseP b l ▸ mem_eraseP_of_neg (mt eq_of_beq ab.symm) - -theorem erase_comm [LawfulBEq α] (a b : α) (l : List α) : - (l.erase a).erase b = (l.erase b).erase a := by - if ab : a == b then rw [eq_of_beq ab] else ?_ - if ha : a ∈ l then ?_ else - simp only [erase_of_not_mem ha, erase_of_not_mem (mt mem_of_mem_erase ha)] - if hb : b ∈ l then ?_ else - simp only [erase_of_not_mem hb, erase_of_not_mem (mt mem_of_mem_erase hb)] - match l, l.erase a, exists_erase_eq ha with - | _, _, ⟨l₁, l₂, ha', rfl, rfl⟩ => - if h₁ : b ∈ l₁ then - rw [erase_append_left _ h₁, erase_append_left _ h₁, - erase_append_right _ (mt mem_of_mem_erase ha'), erase_cons_head] - else - rw [erase_append_right _ h₁, erase_append_right _ h₁, erase_append_right _ ha', - erase_cons_tail _ ab, erase_cons_head] - -end erase - -/-! ### filter and partition -/ - -@[simp] theorem filter_sublist {p : α → Bool} : ∀ (l : List α), filter p l <+ l - | [] => .slnil - | a :: l => by rw [filter]; split <;> simp [Sublist.cons, Sublist.cons₂, filter_sublist l] - -/-! ### filterMap -/ - -protected theorem Sublist.filterMap (f : α → Option β) (s : l₁ <+ l₂) : - filterMap f l₁ <+ filterMap f l₂ := by - induction s <;> simp [filterMap_cons] <;> split <;> simp [*, cons, cons₂] - -theorem Sublist.filter (p : α → Bool) {l₁ l₂} (s : l₁ <+ l₂) : filter p l₁ <+ filter p l₂ := by - rw [← filterMap_eq_filter]; apply s.filterMap - -/-! ### findIdx -/ - -@[simp] theorem findIdx_nil {α : Type _} (p : α → Bool) : [].findIdx p = 0 := rfl - -theorem findIdx_cons (p : α → Bool) (b : α) (l : List α) : - (b :: l).findIdx p = bif p b then 0 else (l.findIdx p) + 1 := by - cases H : p b with - | true => simp [H, findIdx, findIdx.go] - | false => simp [H, findIdx, findIdx.go, findIdx_go_succ] -where - findIdx_go_succ (p : α → Bool) (l : List α) (n : Nat) : - List.findIdx.go p l (n + 1) = (findIdx.go p l n) + 1 := by - cases l with - | nil => unfold findIdx.go; exact Nat.succ_eq_add_one n - | cons head tail => - unfold findIdx.go - cases p head <;> simp only [cond_false, cond_true] - exact findIdx_go_succ p tail (n + 1) - -theorem findIdx_of_get?_eq_some {xs : List α} (w : xs.get? (xs.findIdx p) = some y) : p y := by - induction xs with - | nil => simp_all - | cons x xs ih => by_cases h : p x <;> simp_all [findIdx_cons] - -theorem findIdx_get {xs : List α} {w : xs.findIdx p < xs.length} : - p (xs.get ⟨xs.findIdx p, w⟩) := - xs.findIdx_of_get?_eq_some (get?_eq_get w) - -theorem findIdx_lt_length_of_exists {xs : List α} (h : ∃ x ∈ xs, p x) : - xs.findIdx p < xs.length := by - induction xs with - | nil => simp_all - | cons x xs ih => - by_cases p x - · simp_all only [forall_exists_index, and_imp, mem_cons, exists_eq_or_imp, true_or, - findIdx_cons, cond_true, length_cons] - apply Nat.succ_pos - · simp_all [findIdx_cons] - refine Nat.succ_lt_succ ?_ - obtain ⟨x', m', h'⟩ := h - exact ih x' m' h' - -theorem findIdx_get?_eq_get_of_exists {xs : List α} (h : ∃ x ∈ xs, p x) : - xs.get? (xs.findIdx p) = some (xs.get ⟨xs.findIdx p, xs.findIdx_lt_length_of_exists h⟩) := - get?_eq_get (findIdx_lt_length_of_exists h) - - /-! ### findIdx? -/ - -@[simp] theorem findIdx?_nil : ([] : List α).findIdx? p i = none := rfl - -@[simp] theorem findIdx?_cons : - (x :: xs).findIdx? p i = if p x then some i else findIdx? p xs (i + 1) := rfl - -@[simp] theorem findIdx?_succ : - (xs : List α).findIdx? p (i+1) = (xs.findIdx? p i).map fun i => i + 1 := by - induction xs generalizing i with simp - | cons _ _ _ => split <;> simp_all - -theorem findIdx?_eq_some_iff (xs : List α) (p : α → Bool) : - xs.findIdx? p = some i ↔ (xs.take (i + 1)).map p = replicate i false ++ [true] := by - induction xs generalizing i with - | nil => simp - | cons x xs ih => - simp only [findIdx?_cons, Nat.zero_add, findIdx?_succ, take_succ_cons, map_cons] - split <;> cases i <;> simp_all [replicate_succ] - -theorem findIdx?_of_eq_some {xs : List α} {p : α → Bool} (w : xs.findIdx? p = some i) : - match xs.get? i with | some a => p a | none => false := by - induction xs generalizing i with - | nil => simp_all - | cons x xs ih => - simp_all only [findIdx?_cons, Nat.zero_add, findIdx?_succ] - split at w <;> cases i <;> simp_all - -theorem findIdx?_of_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p = none) : - ∀ i, match xs.get? i with | some a => ¬ p a | none => true := by - intro i - induction xs generalizing i with - | nil => simp_all - | cons x xs ih => - simp_all only [Bool.not_eq_true, findIdx?_cons, Nat.zero_add, findIdx?_succ] - cases i with - | zero => - split at w <;> simp_all - | succ i => - simp only [get?_cons_succ] - apply ih - split at w <;> simp_all - -@[simp] theorem findIdx?_append : - (xs ++ ys : List α).findIdx? p = - (xs.findIdx? p <|> (ys.findIdx? p).map fun i => i + xs.length) := by - induction xs with simp - | cons _ _ _ => split <;> simp_all [Option.map_orElse, Option.map_map]; rfl - -@[simp] theorem findIdx?_replicate : - (replicate n a).findIdx? p = if 0 < n ∧ p a then some 0 else none := by - induction n with - | zero => simp - | succ n ih => - simp only [replicate, findIdx?_cons, Nat.zero_add, findIdx?_succ, Nat.zero_lt_succ, true_and] - split <;> simp_all - -/-! ### pairwise -/ - -theorem Pairwise.sublist : l₁ <+ l₂ → l₂.Pairwise R → l₁.Pairwise R - | .slnil, h => h - | .cons _ s, .cons _ h₂ => h₂.sublist s - | .cons₂ _ s, .cons h₁ h₂ => (h₂.sublist s).cons fun _ h => h₁ _ (s.subset h) - -theorem pairwise_map {l : List α} : - (l.map f).Pairwise R ↔ l.Pairwise fun a b => R (f a) (f b) := by - induction l - · simp - · simp only [map, pairwise_cons, forall_mem_map_iff, *] - -theorem pairwise_append {l₁ l₂ : List α} : - (l₁ ++ l₂).Pairwise R ↔ l₁.Pairwise R ∧ l₂.Pairwise R ∧ ∀ a ∈ l₁, ∀ b ∈ l₂, R a b := by - induction l₁ <;> simp [*, or_imp, forall_and, and_assoc, and_left_comm] - -theorem pairwise_reverse {l : List α} : - l.reverse.Pairwise R ↔ l.Pairwise (fun a b => R b a) := by - induction l <;> simp [*, pairwise_append, and_comm] - -theorem Pairwise.imp {α R S} (H : ∀ {a b}, R a b → S a b) : - ∀ {l : List α}, l.Pairwise R → l.Pairwise S - | _, .nil => .nil - | _, .cons h₁ h₂ => .cons (H ∘ h₁ ·) (h₂.imp H) - /-! ### replaceF -/ theorem replaceF_nil : [].replaceF p = [] := rfl @@ -857,10 +273,10 @@ theorem disjoint_of_subset_right (ss : l₂ ⊆ l) (d : Disjoint l₁ l) : Disjo fun _ m m₁ => d m (ss m₁) theorem disjoint_of_disjoint_cons_left {l₁ l₂} : Disjoint (a :: l₁) l₂ → Disjoint l₁ l₂ := -disjoint_of_subset_left (subset_cons _ _) + disjoint_of_subset_left (subset_cons_self _ _) theorem disjoint_of_disjoint_cons_right {l₁ l₂} : Disjoint l₁ (a :: l₂) → Disjoint l₁ l₂ := -disjoint_of_subset_right (subset_cons _ _) + disjoint_of_subset_right (subset_cons_self _ _) @[simp] theorem disjoint_nil_left (l : List α) : Disjoint [] l := fun a => (not_mem_nil a).elim @@ -896,16 +312,6 @@ theorem disjoint_of_disjoint_append_right_left (d : Disjoint l (l₁ ++ l₂)) : theorem disjoint_of_disjoint_append_right_right (d : Disjoint l (l₁ ++ l₂)) : Disjoint l l₂ := (disjoint_append_right.1 d).2 -/-! ### foldl / foldr -/ - -theorem foldl_hom (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂) (l : List β) (init : α₁) - (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by - induction l generalizing init <;> simp [*, H] - -theorem foldr_hom (f : β₁ → β₂) (g₁ : α → β₁ → β₁) (g₂ : α → β₂ → β₂) (l : List α) (init : β₁) - (H : ∀ x y, g₂ x (f y) = f (g₁ x y)) : l.foldr g₂ (f init) = f (l.foldr g₁ init) := by - induction l <;> simp [*, H] - /-! ### union -/ section union @@ -941,38 +347,14 @@ theorem pair_mem_product {xs : List α} {ys : List β} {x : α} {y : β} : simp only [product, and_imp, mem_map, Prod.mk.injEq, exists_eq_right_right, mem_bind, iff_self] -/-! ### leftpad -/ - -/-- The length of the List returned by `List.leftpad n a l` is equal - to the larger of `n` and `l.length` -/ -@[simp] -theorem leftpad_length (n : Nat) (a : α) (l : List α) : - (leftpad n a l).length = max n l.length := by - simp only [leftpad, length_append, length_replicate, Nat.sub_add_eq_max] - -theorem leftpad_prefix (n : Nat) (a : α) (l : List α) : - replicate (n - length l) a <+: leftpad n a l := by - simp only [IsPrefix, leftpad] - exact Exists.intro l rfl - -theorem leftpad_suffix (n : Nat) (a : α) (l : List α) : l <:+ (leftpad n a l) := by - simp only [IsSuffix, leftpad] - exact Exists.intro (replicate (n - length l) a) rfl - /-! ### monadic operations -/ --- we use ForIn.forIn as the simp normal form -@[simp] theorem forIn_eq_forIn [Monad m] : @List.forIn α β m _ = forIn := rfl - theorem forIn_eq_bindList [Monad m] [LawfulMonad m] (f : α → β → m (ForInStep β)) (l : List α) (init : β) : forIn l init f = ForInStep.run <$> (ForInStep.yield init).bindList f l := by induction l generalizing init <;> simp [*, map_eq_pure_bind] congr; ext (b | b) <;> simp -@[simp] theorem forM_append [Monad m] [LawfulMonad m] (l₁ l₂ : List α) (f : α → m PUnit) : - (l₁ ++ l₂).forM f = (do l₁.forM f; l₂.forM f) := by induction l₁ <;> simp [*] - /-! ### diff -/ section Diff @@ -1050,205 +432,8 @@ theorem Sublist.erase_diff_erase_sublist {a : α} : end Diff -/-! ### prefix, suffix, infix -/ - -@[simp] theorem prefix_append (l₁ l₂ : List α) : l₁ <+: l₁ ++ l₂ := ⟨l₂, rfl⟩ - -@[simp] theorem suffix_append (l₁ l₂ : List α) : l₂ <:+ l₁ ++ l₂ := ⟨l₁, rfl⟩ - -theorem infix_append (l₁ l₂ l₃ : List α) : l₂ <:+: l₁ ++ l₂ ++ l₃ := ⟨l₁, l₃, rfl⟩ - -@[simp] theorem infix_append' (l₁ l₂ l₃ : List α) : l₂ <:+: l₁ ++ (l₂ ++ l₃) := by - rw [← List.append_assoc]; apply infix_append - -theorem IsPrefix.isInfix : l₁ <+: l₂ → l₁ <:+: l₂ := fun ⟨t, h⟩ => ⟨[], t, h⟩ - -theorem IsSuffix.isInfix : l₁ <:+ l₂ → l₁ <:+: l₂ := fun ⟨t, h⟩ => ⟨t, [], by rw [h, append_nil]⟩ - -theorem nil_prefix (l : List α) : [] <+: l := ⟨l, rfl⟩ - -theorem nil_suffix (l : List α) : [] <:+ l := ⟨l, append_nil _⟩ - -theorem nil_infix (l : List α) : [] <:+: l := (nil_prefix _).isInfix - -theorem prefix_refl (l : List α) : l <+: l := ⟨[], append_nil _⟩ - -theorem suffix_refl (l : List α) : l <:+ l := ⟨[], rfl⟩ - -theorem infix_refl (l : List α) : l <:+: l := (prefix_refl l).isInfix - -@[simp] theorem suffix_cons (a : α) : ∀ l, l <:+ a :: l := suffix_append [a] - -theorem infix_cons : l₁ <:+: l₂ → l₁ <:+: a :: l₂ := fun ⟨L₁, L₂, h⟩ => ⟨a :: L₁, L₂, h ▸ rfl⟩ - -theorem infix_concat : l₁ <:+: l₂ → l₁ <:+: concat l₂ a := fun ⟨L₁, L₂, h⟩ => - ⟨L₁, concat L₂ a, by simp [← h, concat_eq_append, append_assoc]⟩ - -theorem IsPrefix.trans : ∀ {l₁ l₂ l₃ : List α}, l₁ <+: l₂ → l₂ <+: l₃ → l₁ <+: l₃ - | _, _, _, ⟨r₁, rfl⟩, ⟨r₂, rfl⟩ => ⟨r₁ ++ r₂, (append_assoc _ _ _).symm⟩ - -theorem IsSuffix.trans : ∀ {l₁ l₂ l₃ : List α}, l₁ <:+ l₂ → l₂ <:+ l₃ → l₁ <:+ l₃ - | _, _, _, ⟨l₁, rfl⟩, ⟨l₂, rfl⟩ => ⟨l₂ ++ l₁, append_assoc _ _ _⟩ - -theorem IsInfix.trans : ∀ {l₁ l₂ l₃ : List α}, l₁ <:+: l₂ → l₂ <:+: l₃ → l₁ <:+: l₃ - | l, _, _, ⟨l₁, r₁, rfl⟩, ⟨l₂, r₂, rfl⟩ => ⟨l₂ ++ l₁, r₁ ++ r₂, by simp only [append_assoc]⟩ - -protected theorem IsInfix.sublist : l₁ <:+: l₂ → l₁ <+ l₂ - | ⟨_, _, h⟩ => h ▸ (sublist_append_right ..).trans (sublist_append_left ..) - -protected theorem IsInfix.subset (hl : l₁ <:+: l₂) : l₁ ⊆ l₂ := - hl.sublist.subset - -protected theorem IsPrefix.sublist (h : l₁ <+: l₂) : l₁ <+ l₂ := - h.isInfix.sublist - -protected theorem IsPrefix.subset (hl : l₁ <+: l₂) : l₁ ⊆ l₂ := - hl.sublist.subset - -protected theorem IsSuffix.sublist (h : l₁ <:+ l₂) : l₁ <+ l₂ := - h.isInfix.sublist - -protected theorem IsSuffix.subset (hl : l₁ <:+ l₂) : l₁ ⊆ l₂ := - hl.sublist.subset - -@[simp] theorem reverse_suffix : reverse l₁ <:+ reverse l₂ ↔ l₁ <+: l₂ := - ⟨fun ⟨r, e⟩ => ⟨reverse r, by rw [← reverse_reverse l₁, ← reverse_append, e, reverse_reverse]⟩, - fun ⟨r, e⟩ => ⟨reverse r, by rw [← reverse_append, e]⟩⟩ - -@[simp] theorem reverse_prefix : reverse l₁ <+: reverse l₂ ↔ l₁ <:+ l₂ := by - rw [← reverse_suffix]; simp only [reverse_reverse] - -@[simp] theorem reverse_infix : reverse l₁ <:+: reverse l₂ ↔ l₁ <:+: l₂ := by - refine ⟨fun ⟨s, t, e⟩ => ⟨reverse t, reverse s, ?_⟩, fun ⟨s, t, e⟩ => ⟨reverse t, reverse s, ?_⟩⟩ - · rw [← reverse_reverse l₁, append_assoc, ← reverse_append, ← reverse_append, e, - reverse_reverse] - · rw [append_assoc, ← reverse_append, ← reverse_append, e] - -theorem IsInfix.length_le (h : l₁ <:+: l₂) : l₁.length ≤ l₂.length := - h.sublist.length_le - -theorem IsPrefix.length_le (h : l₁ <+: l₂) : l₁.length ≤ l₂.length := - h.sublist.length_le - -theorem IsSuffix.length_le (h : l₁ <:+ l₂) : l₁.length ≤ l₂.length := - h.sublist.length_le - -@[simp] theorem infix_nil : l <:+: [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ infix_refl _)⟩ - -@[simp] theorem prefix_nil : l <+: [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ prefix_refl _)⟩ - -@[simp] theorem suffix_nil : l <:+ [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ suffix_refl _)⟩ - -theorem infix_iff_prefix_suffix (l₁ l₂ : List α) : l₁ <:+: l₂ ↔ ∃ t, l₁ <+: t ∧ t <:+ l₂ := - ⟨fun ⟨_, t, e⟩ => ⟨l₁ ++ t, ⟨_, rfl⟩, e ▸ append_assoc .. ▸ ⟨_, rfl⟩⟩, - fun ⟨_, ⟨t, rfl⟩, s, e⟩ => ⟨s, t, append_assoc .. ▸ e⟩⟩ - -theorem IsInfix.eq_of_length (h : l₁ <:+: l₂) : l₁.length = l₂.length → l₁ = l₂ := - h.sublist.eq_of_length - -theorem IsPrefix.eq_of_length (h : l₁ <+: l₂) : l₁.length = l₂.length → l₁ = l₂ := - h.sublist.eq_of_length - -theorem IsSuffix.eq_of_length (h : l₁ <:+ l₂) : l₁.length = l₂.length → l₁ = l₂ := - h.sublist.eq_of_length - -theorem prefix_of_prefix_length_le : - ∀ {l₁ l₂ l₃ : List α}, l₁ <+: l₃ → l₂ <+: l₃ → length l₁ ≤ length l₂ → l₁ <+: l₂ - | [], l₂, _, _, _, _ => nil_prefix _ - | a :: l₁, b :: l₂, _, ⟨r₁, rfl⟩, ⟨r₂, e⟩, ll => by - injection e with _ e'; subst b - rcases prefix_of_prefix_length_le ⟨_, rfl⟩ ⟨_, e'⟩ (le_of_succ_le_succ ll) with ⟨r₃, rfl⟩ - exact ⟨r₃, rfl⟩ - -theorem prefix_or_prefix_of_prefix (h₁ : l₁ <+: l₃) (h₂ : l₂ <+: l₃) : l₁ <+: l₂ ∨ l₂ <+: l₁ := - (Nat.le_total (length l₁) (length l₂)).imp (prefix_of_prefix_length_le h₁ h₂) - (prefix_of_prefix_length_le h₂ h₁) - -theorem suffix_of_suffix_length_le - (h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) (ll : length l₁ ≤ length l₂) : l₁ <:+ l₂ := - reverse_prefix.1 <| - prefix_of_prefix_length_le (reverse_prefix.2 h₁) (reverse_prefix.2 h₂) (by simp [ll]) - -theorem suffix_or_suffix_of_suffix (h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) : l₁ <:+ l₂ ∨ l₂ <:+ l₁ := - (prefix_or_prefix_of_prefix (reverse_prefix.2 h₁) (reverse_prefix.2 h₂)).imp reverse_prefix.1 - reverse_prefix.1 - -theorem suffix_cons_iff : l₁ <:+ a :: l₂ ↔ l₁ = a :: l₂ ∨ l₁ <:+ l₂ := by - constructor - · rintro ⟨⟨hd, tl⟩, hl₃⟩ - · exact Or.inl hl₃ - · simp only [cons_append] at hl₃ - injection hl₃ with _ hl₄ - exact Or.inr ⟨_, hl₄⟩ - · rintro (rfl | hl₁) - · exact (a :: l₂).suffix_refl - · exact hl₁.trans (l₂.suffix_cons _) - -theorem infix_cons_iff : l₁ <:+: a :: l₂ ↔ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂ := by - constructor - · rintro ⟨⟨hd, tl⟩, t, hl₃⟩ - · exact Or.inl ⟨t, hl₃⟩ - · simp only [cons_append] at hl₃ - injection hl₃ with _ hl₄ - exact Or.inr ⟨_, t, hl₄⟩ - · rintro (h | hl₁) - · exact h.isInfix - · exact infix_cons hl₁ - -theorem infix_of_mem_join : ∀ {L : List (List α)}, l ∈ L → l <:+: join L - | l' :: _, h => - match h with - | List.Mem.head .. => infix_append [] _ _ - | List.Mem.tail _ hlMemL => - IsInfix.trans (infix_of_mem_join hlMemL) <| (suffix_append _ _).isInfix - -theorem prefix_append_right_inj (l) : l ++ l₁ <+: l ++ l₂ ↔ l₁ <+: l₂ := - exists_congr fun r => by rw [append_assoc, append_right_inj] - -@[simp] -theorem prefix_cons_inj (a) : a :: l₁ <+: a :: l₂ ↔ l₁ <+: l₂ := - prefix_append_right_inj [a] - -theorem take_prefix (n) (l : List α) : take n l <+: l := - ⟨_, take_append_drop _ _⟩ - -theorem drop_suffix (n) (l : List α) : drop n l <:+ l := - ⟨_, take_append_drop _ _⟩ - -theorem take_sublist (n) (l : List α) : take n l <+ l := - (take_prefix n l).sublist - -theorem drop_sublist (n) (l : List α) : drop n l <+ l := - (drop_suffix n l).sublist - -theorem take_subset (n) (l : List α) : take n l ⊆ l := - (take_sublist n l).subset - -theorem drop_subset (n) (l : List α) : drop n l ⊆ l := - (drop_sublist n l).subset - -theorem mem_of_mem_take {l : List α} (h : a ∈ l.take n) : a ∈ l := - take_subset n l h - -theorem IsPrefix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) : - l₁.filter p <+: l₂.filter p := by - obtain ⟨xs, rfl⟩ := h - rw [filter_append]; apply prefix_append - -theorem IsSuffix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) : - l₁.filter p <:+ l₂.filter p := by - obtain ⟨xs, rfl⟩ := h - rw [filter_append]; apply suffix_append - -theorem IsInfix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) : - l₁.filter p <:+: l₂.filter p := by - obtain ⟨xs, ys, rfl⟩ := h - rw [filter_append, filter_append]; apply infix_append _ - /-! ### drop -/ -theorem mem_of_mem_drop {n} {l : List α} (h : a ∈ l.drop n) : a ∈ l := drop_subset _ _ h - theorem disjoint_take_drop : ∀ {l : List α}, l.Nodup → m ≤ n → Disjoint (l.take m) (l.drop n) | [], _, _ => by simp | x :: xs, hl, h => by @@ -1297,39 +482,6 @@ protected theorem Pairwise.chain (p : Pairwise R (a :: l)) : Chain R a l := by /-! ### range', range -/ -theorem range'_succ (s n step) : range' s (n + 1) step = s :: range' (s + step) n step := by - simp [range', Nat.add_succ, Nat.mul_succ] - -@[simp] theorem length_range' (s step) : ∀ n : Nat, length (range' s n step) = n - | 0 => rfl - | _ + 1 => congrArg succ (length_range' _ _ _) - -@[simp] theorem range'_eq_nil : range' s n step = [] ↔ n = 0 := by - rw [← length_eq_zero, length_range'] - -theorem mem_range' : ∀{n}, m ∈ range' s n step ↔ ∃ i < n, m = s + step * i - | 0 => by simp [range', Nat.not_lt_zero] - | n + 1 => by - have h (i) : i ≤ n ↔ i = 0 ∨ ∃ j, i = succ j ∧ j < n := by cases i <;> simp [Nat.succ_le] - simp [range', mem_range', Nat.lt_succ, h]; simp only [← exists_and_right, and_assoc] - rw [exists_comm]; simp [Nat.mul_succ, Nat.add_assoc, Nat.add_comm] - -@[simp] theorem mem_range'_1 : m ∈ range' s n ↔ s ≤ m ∧ m < s + n := by - simp [mem_range']; exact ⟨ - fun ⟨i, h, e⟩ => e ▸ ⟨Nat.le_add_right .., Nat.add_lt_add_left h _⟩, - fun ⟨h₁, h₂⟩ => ⟨m - s, Nat.sub_lt_left_of_lt_add h₁ h₂, (Nat.add_sub_cancel' h₁).symm⟩⟩ - -@[simp] -theorem map_add_range' (a) : ∀ s n step, map (a + ·) (range' s n step) = range' (a + s) n step - | _, 0, _ => rfl - | s, n + 1, step => by simp [range', map_add_range' _ (s + step) n step, Nat.add_assoc] - -theorem map_sub_range' (a s n : Nat) (h : a ≤ s) : - map (· - a) (range' s n step) = range' (s - a) n step := by - conv => lhs; rw [← Nat.add_sub_cancel' h] - rw [← map_add_range', map_map, (?_ : _∘_ = _), map_id] - funext x; apply Nat.add_sub_cancel_left - theorem chain_succ_range' : ∀ s n step : Nat, Chain (fun a b => b = a + step) s (range' (s + step) n step) | _, 0, _ => Chain.nil @@ -1339,41 +491,6 @@ theorem chain_lt_range' (s n : Nat) {step} (h : 0 < step) : Chain (· < ·) s (range' (s + step) n step) := (chain_succ_range' s n step).imp fun _ _ e => e.symm ▸ Nat.lt_add_of_pos_right h -theorem range'_append : ∀ s m n step : Nat, - range' s m step ++ range' (s + step * m) n step = range' s (n + m) step - | s, 0, n, step => rfl - | s, m + 1, n, step => by - simpa [range', Nat.mul_succ, Nat.add_assoc, Nat.add_comm] - using range'_append (s + step) m n step - -@[simp] theorem range'_append_1 (s m n : Nat) : - range' s m ++ range' (s + m) n = range' s (n + m) := by simpa using range'_append s m n 1 - -theorem range'_sublist_right {s m n : Nat} : range' s m step <+ range' s n step ↔ m ≤ n := - ⟨fun h => by simpa only [length_range'] using h.length_le, - fun h => by rw [← Nat.sub_add_cancel h, ← range'_append]; apply sublist_append_left⟩ - -theorem range'_subset_right {s m n : Nat} (step0 : 0 < step) : - range' s m step ⊆ range' s n step ↔ m ≤ n := by - refine ⟨fun h => Nat.le_of_not_lt fun hn => ?_, fun h => (range'_sublist_right.2 h).subset⟩ - have ⟨i, h', e⟩ := mem_range'.1 <| h <| mem_range'.2 ⟨_, hn, rfl⟩ - exact Nat.ne_of_gt h' (Nat.eq_of_mul_eq_mul_left step0 (Nat.add_left_cancel e)) - -theorem range'_subset_right_1 {s m n : Nat} : range' s m ⊆ range' s n ↔ m ≤ n := - range'_subset_right (by decide) - -theorem getElem?_range' (s step) : - ∀ {m n : Nat}, m < n → (range' s n step)[m]? = some (s + step * m) - | 0, n + 1, _ => by simp [range'_succ] - | m + 1, n + 1, h => by - simp only [range'_succ, getElem?_cons_succ] - exact (getElem?_range' (s + step) step (Nat.lt_of_add_lt_add_right h)).trans <| by - simp [Nat.mul_succ, Nat.add_assoc, Nat.add_comm] - -@[simp] theorem getElem_range' {n m step} (i) (H : i < (range' n m step).length) : - (range' n m step)[i] = n + step * i := - (getElem?_eq_some.1 <| getElem?_range' n step (by simpa using H)).2 - @[deprecated getElem?_range' (since := "2024-06-12")] theorem get?_range' (s step) {m n : Nat} (h : m < n) : get? (range' s n step) m = some (s + step * m) := by @@ -1384,54 +501,6 @@ theorem get_range' {n m step} (i) (H : i < (range' n m step).length) : get (range' n m step) ⟨i, H⟩ = n + step * i := by simp -theorem range'_concat (s n : Nat) : range' s (n + 1) step = range' s n step ++ [s + step * n] := by - rw [Nat.add_comm n 1]; exact (range'_append s n 1 step).symm - -theorem range'_1_concat (s n : Nat) : range' s (n + 1) = range' s n ++ [s + n] := by - simp [range'_concat] - -theorem range_loop_range' : ∀ s n : Nat, range.loop s (range' s n) = range' 0 (n + s) - | 0, n => rfl - | s + 1, n => by rw [← Nat.add_assoc, Nat.add_right_comm n s 1]; exact range_loop_range' s (n + 1) - -theorem range_eq_range' (n : Nat) : range n = range' 0 n := - (range_loop_range' n 0).trans <| by rw [Nat.zero_add] - -theorem range_succ_eq_map (n : Nat) : range (n + 1) = 0 :: map succ (range n) := by - rw [range_eq_range', range_eq_range', range', Nat.add_comm, ← map_add_range'] - congr; exact funext one_add - -theorem range'_eq_map_range (s n : Nat) : range' s n = map (s + ·) (range n) := by - rw [range_eq_range', map_add_range']; rfl - -@[simp] theorem length_range (n : Nat) : length (range n) = n := by - simp only [range_eq_range', length_range'] - -@[simp] theorem range_eq_nil {n : Nat} : range n = [] ↔ n = 0 := by - rw [← length_eq_zero, length_range] - -@[simp] -theorem range_sublist {m n : Nat} : range m <+ range n ↔ m ≤ n := by - simp only [range_eq_range', range'_sublist_right] - -@[simp] -theorem range_subset {m n : Nat} : range m ⊆ range n ↔ m ≤ n := by - simp only [range_eq_range', range'_subset_right, lt_succ_self] - -@[simp] -theorem mem_range {m n : Nat} : m ∈ range n ↔ m < n := by - simp only [range_eq_range', mem_range'_1, Nat.zero_le, true_and, Nat.zero_add] - -theorem not_mem_range_self {n : Nat} : n ∉ range n := by simp - -theorem self_mem_range_succ (n : Nat) : n ∈ range (n + 1) := by simp - -theorem getElem?_range {m n : Nat} (h : m < n) : (range n)[m]? = some m := by - simp [range_eq_range', getElem?_range' _ _ h] - -@[simp] theorem getElem_range {n : Nat} (m) (h : m < (range n).length) : (range n)[m] = m := by - simp [range_eq_range'] - @[deprecated getElem?_range (since := "2024-06-12")] theorem get?_range {m n : Nat} (h : m < n) : get? (range n) m = some m := by simp [getElem?_range, h] @@ -1440,41 +509,6 @@ theorem get?_range {m n : Nat} (h : m < n) : get? (range n) m = some m := by theorem get_range {n} (i) (H : i < (range n).length) : get (range n) ⟨i, H⟩ = i := by simp -theorem range_succ (n : Nat) : range (succ n) = range n ++ [n] := by - simp only [range_eq_range', range'_1_concat, Nat.zero_add] - -theorem range_add (a b : Nat) : range (a + b) = range a ++ (range b).map (a + ·) := by - rw [← range'_eq_map_range] - simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 a b).symm - -theorem iota_eq_reverse_range' : ∀ n : Nat, iota n = reverse (range' 1 n) - | 0 => rfl - | n + 1 => by simp [iota, range'_concat, iota_eq_reverse_range' n, reverse_append, Nat.add_comm] - -@[simp] theorem length_iota (n : Nat) : length (iota n) = n := by simp [iota_eq_reverse_range'] - -@[simp] -theorem mem_iota {m n : Nat} : m ∈ iota n ↔ 1 ≤ m ∧ m ≤ n := by - simp [iota_eq_reverse_range', Nat.add_comm, Nat.lt_succ] - -theorem reverse_range' : ∀ s n : Nat, reverse (range' s n) = map (s + n - 1 - ·) (range n) - | s, 0 => rfl - | s, n + 1 => by - rw [range'_1_concat, reverse_append, range_succ_eq_map, - show s + (n + 1) - 1 = s + n from rfl, map, map_map] - simp [reverse_range', Nat.sub_right_comm, Nat.sub_sub] - - -/-! ### enum, enumFrom -/ - -@[simp] theorem enumFrom_map_fst (n) : - ∀ (l : List α), map Prod.fst (enumFrom n l) = range' n l.length - | [] => rfl - | _ :: _ => congrArg (cons _) (enumFrom_map_fst _ _) - -@[simp] theorem enum_map_fst (l : List α) : map Prod.fst (enum l) = range l.length := by - simp only [enum, enumFrom_map_fst, range_eq_range'] - /-! ### indexOf and indexesOf -/ theorem foldrIdx_start : @@ -1514,13 +548,6 @@ theorem indexesOf_cons [BEq α] : (x :: xs : List α).indexesOf y = bif x == y then 0 :: (xs.indexesOf y).map (· + 1) else (xs.indexesOf y).map (· + 1) := by simp [indexesOf, findIdxs_cons] -@[simp] theorem indexOf_nil [BEq α] : ([] : List α).indexOf x = 0 := rfl - -theorem indexOf_cons [BEq α] : - (x :: xs : List α).indexOf y = bif x == y then 0 else xs.indexOf y + 1 := by - dsimp [indexOf] - simp [findIdx_cons] - theorem indexOf_mem_indexesOf [BEq α] [LawfulBEq α] {xs : List α} (m : x ∈ xs) : xs.indexOf x ∈ xs.indexesOf x := by induction xs with diff --git a/Batteries/Data/List/Pairwise.lean b/Batteries/Data/List/Pairwise.lean index 83b935f8ae..dd94875ca9 100644 --- a/Batteries/Data/List/Pairwise.lean +++ b/Batteries/Data/List/Pairwise.lean @@ -30,164 +30,6 @@ namespace List /-! ### Pairwise -/ -theorem rel_of_pairwise_cons (p : (a :: l).Pairwise R) : ∀ {a'}, a' ∈ l → R a a' := - (pairwise_cons.1 p).1 _ - -theorem Pairwise.of_cons (p : (a :: l).Pairwise R) : Pairwise R l := - (pairwise_cons.1 p).2 - -theorem Pairwise.tail : ∀ {l : List α} (_p : Pairwise R l), Pairwise R l.tail - | [], h => h - | _ :: _, h => h.of_cons - -theorem Pairwise.drop : ∀ {l : List α} {n : Nat}, List.Pairwise R l → List.Pairwise R (l.drop n) - | _, 0, h => h - | [], _ + 1, _ => List.Pairwise.nil - | _ :: _, n + 1, h => Pairwise.drop (n := n) (pairwise_cons.mp h).right - -theorem Pairwise.imp_of_mem {S : α → α → Prop} - (H : ∀ {a b}, a ∈ l → b ∈ l → R a b → S a b) (p : Pairwise R l) : Pairwise S l := by - induction p with - | nil => constructor - | @cons a l r _ ih => - constructor - · exact fun x h => H (mem_cons_self ..) (mem_cons_of_mem _ h) <| r x h - · exact ih fun m m' => H (mem_cons_of_mem _ m) (mem_cons_of_mem _ m') - -theorem Pairwise.and (hR : Pairwise R l) (hS : Pairwise S l) : - l.Pairwise fun a b => R a b ∧ S a b := by - induction hR with - | nil => simp only [Pairwise.nil] - | cons R1 _ IH => - simp only [Pairwise.nil, pairwise_cons] at hS ⊢ - exact ⟨fun b bl => ⟨R1 b bl, hS.1 b bl⟩, IH hS.2⟩ - -theorem pairwise_and_iff : l.Pairwise (fun a b => R a b ∧ S a b) ↔ Pairwise R l ∧ Pairwise S l := - ⟨fun h => ⟨h.imp fun h => h.1, h.imp fun h => h.2⟩, fun ⟨hR, hS⟩ => hR.and hS⟩ - -theorem Pairwise.imp₂ (H : ∀ a b, R a b → S a b → T a b) - (hR : Pairwise R l) (hS : l.Pairwise S) : l.Pairwise T := - (hR.and hS).imp fun ⟨h₁, h₂⟩ => H _ _ h₁ h₂ - -theorem Pairwise.iff_of_mem {S : α → α → Prop} {l : List α} - (H : ∀ {a b}, a ∈ l → b ∈ l → (R a b ↔ S a b)) : Pairwise R l ↔ Pairwise S l := - ⟨Pairwise.imp_of_mem fun m m' => (H m m').1, Pairwise.imp_of_mem fun m m' => (H m m').2⟩ - -theorem Pairwise.iff {S : α → α → Prop} (H : ∀ a b, R a b ↔ S a b) {l : List α} : - Pairwise R l ↔ Pairwise S l := - Pairwise.iff_of_mem fun _ _ => H .. - -theorem pairwise_of_forall {l : List α} (H : ∀ x y, R x y) : Pairwise R l := by - induction l <;> simp [*] - -theorem Pairwise.and_mem {l : List α} : - Pairwise R l ↔ Pairwise (fun x y => x ∈ l ∧ y ∈ l ∧ R x y) l := - Pairwise.iff_of_mem <| by simp (config := { contextual := true }) - -theorem Pairwise.imp_mem {l : List α} : - Pairwise R l ↔ Pairwise (fun x y => x ∈ l → y ∈ l → R x y) l := - Pairwise.iff_of_mem <| by simp (config := { contextual := true }) - -theorem Pairwise.forall_of_forall_of_flip (h₁ : ∀ x ∈ l, R x x) (h₂ : Pairwise R l) - (h₃ : l.Pairwise (flip R)) : ∀ ⦃x⦄, x ∈ l → ∀ ⦃y⦄, y ∈ l → R x y := by - induction l with - | nil => exact forall_mem_nil _ - | cons a l ih => - rw [pairwise_cons] at h₂ h₃ - simp only [mem_cons] - rintro x (rfl | hx) y (rfl | hy) - · exact h₁ _ (l.mem_cons_self _) - · exact h₂.1 _ hy - · exact h₃.1 _ hx - · exact ih (fun x hx => h₁ _ <| mem_cons_of_mem _ hx) h₂.2 h₃.2 hx hy - -theorem pairwise_singleton (R) (a : α) : Pairwise R [a] := by simp - -theorem pairwise_pair {a b : α} : Pairwise R [a, b] ↔ R a b := by simp - -theorem pairwise_append_comm {R : α → α → Prop} (s : ∀ {x y}, R x y → R y x) {l₁ l₂ : List α} : - Pairwise R (l₁ ++ l₂) ↔ Pairwise R (l₂ ++ l₁) := by - have (l₁ l₂ : List α) (H : ∀ x : α, x ∈ l₁ → ∀ y : α, y ∈ l₂ → R x y) - (x : α) (xm : x ∈ l₂) (y : α) (ym : y ∈ l₁) : R x y := s (H y ym x xm) - simp only [pairwise_append, and_left_comm]; rw [Iff.intro (this l₁ l₂) (this l₂ l₁)] - -theorem pairwise_middle {R : α → α → Prop} (s : ∀ {x y}, R x y → R y x) {a : α} {l₁ l₂ : List α} : - Pairwise R (l₁ ++ a :: l₂) ↔ Pairwise R (a :: (l₁ ++ l₂)) := by - show Pairwise R (l₁ ++ ([a] ++ l₂)) ↔ Pairwise R ([a] ++ l₁ ++ l₂) - rw [← append_assoc, pairwise_append, @pairwise_append _ _ ([a] ++ l₁), pairwise_append_comm s] - simp only [mem_append, or_comm] - -theorem Pairwise.of_map {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, S (f a) (f b) → R a b) - (p : Pairwise S (map f l)) : Pairwise R l := - (pairwise_map.1 p).imp (H _ _) - -theorem Pairwise.map {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, R a b → S (f a) (f b)) - (p : Pairwise R l) : Pairwise S (map f l) := - pairwise_map.2 <| p.imp (H _ _) - -theorem pairwise_filterMap (f : β → Option α) {l : List β} : - Pairwise R (filterMap f l) ↔ Pairwise (fun a a' : β => ∀ b ∈ f a, ∀ b' ∈ f a', R b b') l := by - let _S (a a' : β) := ∀ b ∈ f a, ∀ b' ∈ f a', R b b' - simp only [Option.mem_def] - induction l with - | nil => simp only [filterMap, Pairwise.nil] - | cons a l IH => ?_ - match e : f a with - | none => - rw [filterMap_cons_none _ _ e, pairwise_cons] - simp only [e, false_implies, implies_true, true_and, IH] - | some b => - rw [filterMap_cons_some _ _ _ e] - simpa [IH, e] using fun _ => - ⟨fun h a ha b hab => h _ _ ha hab, fun h a b ha hab => h _ ha _ hab⟩ - -theorem Pairwise.filter_map {S : β → β → Prop} (f : α → Option β) - (H : ∀ a a' : α, R a a' → ∀ b ∈ f a, ∀ b' ∈ f a', S b b') {l : List α} (p : Pairwise R l) : - Pairwise S (filterMap f l) := - (pairwise_filterMap _).2 <| p.imp (H _ _) - -theorem pairwise_filter (p : α → Prop) [DecidablePred p] {l : List α} : - Pairwise R (filter p l) ↔ Pairwise (fun x y => p x → p y → R x y) l := by - rw [← filterMap_eq_filter, pairwise_filterMap] - simp - -theorem Pairwise.filter (p : α → Bool) : Pairwise R l → Pairwise R (filter p l) := - Pairwise.sublist (filter_sublist _) - -theorem pairwise_join {L : List (List α)} : - Pairwise R (join L) ↔ - (∀ l ∈ L, Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ x ∈ l₁, ∀ y ∈ l₂, R x y) L := by - induction L with - | nil => simp - | cons l L IH => - simp only [join, pairwise_append, IH, mem_join, exists_imp, and_imp, forall_mem_cons, - pairwise_cons, and_assoc, and_congr_right_iff] - rw [and_comm, and_congr_left_iff] - intros; exact ⟨fun h a b c d e => h c d e a b, fun h c d e a b => h a b c d e⟩ - -theorem pairwise_bind {R : β → β → Prop} {l : List α} {f : α → List β} : - List.Pairwise R (l.bind f) ↔ - (∀ a ∈ l, Pairwise R (f a)) ∧ Pairwise (fun a₁ a₂ => ∀ x ∈ f a₁, ∀ y ∈ f a₂, R x y) l := by - simp [List.bind, pairwise_join, pairwise_map] - -theorem pairwise_iff_forall_sublist : l.Pairwise R ↔ (∀ {a b}, [a,b] <+ l → R a b) := by - induction l with - | nil => simp - | cons hd tl IH => - rw [List.pairwise_cons] - constructor <;> intro h - · intro - | a, b, .cons _ hab => exact IH.mp h.2 hab - | _, b, .cons₂ _ hab => refine h.1 _ (hab.subset ?_); simp - · constructor - · intro x hx - apply h - rw [List.cons_sublist_cons, List.singleton_sublist] - exact hx - · apply IH.mpr - intro a b hab - apply h; exact hab.cons _ - @[deprecated pairwise_iff_forall_sublist (since := "2023-09-18")] theorem pairwise_of_reflexive_on_dupl_of_forall_ne [DecidableEq α] {l : List α} {r : α → α → Prop} (hr : ∀ a, 1 < count a l → r a a) (h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b) : l.Pairwise r := by @@ -200,53 +42,6 @@ theorem pairwise_of_reflexive_on_dupl_of_forall_ne [DecidableEq α] {l : List α apply h <;> try (apply hab.subset; simp) exact heq -/-- given a list `is` of monotonically increasing indices into `l`, getting each index - produces a sublist of `l`. -/ -theorem map_get_sublist {l : List α} {is : List (Fin l.length)} (h : is.Pairwise (·.val < ·.val)) : - is.map (get l) <+ l := by - suffices ∀ n l', l' = l.drop n → (∀ i ∈ is, n ≤ i) → map (get l) is <+ l' - from this 0 l (by simp) (by simp) - intro n l' hl' his - induction is generalizing n l' with - | nil => simp - | cons hd tl IH => - simp; cases hl' - have := IH h.of_cons (hd+1) _ rfl (pairwise_cons.mp h).1 - specialize his hd (.head _) - have := (drop_eq_getElem_cons ..).symm ▸ this.cons₂ (get l hd) - have := Sublist.append (nil_sublist (take hd l |>.drop n)) this - rwa [nil_append, ← (drop_append_of_le_length ?_), take_append_drop] at this - simp [Nat.min_eq_left (Nat.le_of_lt hd.isLt), his] - -/-- given a sublist `l' <+ l`, there exists a list of indices `is` such that - `l' = map (get l) is`. -/ -theorem sublist_eq_map_get (h : l' <+ l) : ∃ is : List (Fin l.length), - l' = map (get l) is ∧ is.Pairwise (· < ·) := by - induction h with - | slnil => exact ⟨[], by simp⟩ - | cons _ _ IH => - let ⟨is, IH⟩ := IH - refine ⟨is.map (·.succ), ?_⟩ - simp [comp, pairwise_map] - exact IH - | cons₂ _ _ IH => - rcases IH with ⟨is,IH⟩ - refine ⟨⟨0, by simp [Nat.zero_lt_succ]⟩ :: is.map (·.succ), ?_⟩ - simp [comp_def, pairwise_map, IH, ← get_eq_getElem] - -theorem pairwise_iff_getElem : Pairwise R l ↔ - ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j), R l[i] l[j] := by - rw [pairwise_iff_forall_sublist] - constructor <;> intro h - · intros i j hi hj h' - apply h - simpa [h'] using map_get_sublist (is := [⟨i, hi⟩, ⟨j, hj⟩]) - · intros a b h' - have ⟨is, h', hij⟩ := sublist_eq_map_get h' - rcases is with ⟨⟩ | ⟨a', ⟨⟩ | ⟨b', ⟨⟩⟩⟩ <;> simp at h' - rcases h' with ⟨rfl, rfl⟩ - apply h; simpa using hij - theorem pairwise_iff_get : Pairwise R l ↔ ∀ (i j) (_hij : i < j), R (get l i) (get l j) := by rw [pairwise_iff_getElem] constructor <;> intro h @@ -255,11 +50,6 @@ theorem pairwise_iff_get : Pairwise R l ↔ ∀ (i j) (_hij : i < j), R (get l i · intros i j hi hj h' exact h ⟨i, hi⟩ ⟨j, hj⟩ h' -theorem pairwise_replicate {α : Type _} {r : α → α → Prop} {x : α} (hx : r x x) : - ∀ n : Nat, Pairwise r (List.replicate n x) - | 0 => by simp - | n + 1 => by simp [mem_replicate, hx, pairwise_replicate hx n, replicate_succ] - /-! ### Pairwise filtering -/ @[simp] theorem pwFilter_nil [DecidableRel R] : pwFilter R [] = [] := rfl diff --git a/Batteries/Data/List/Perm.lean b/Batteries/Data/List/Perm.lean index ab12db10b1..5c31720c7c 100644 --- a/Batteries/Data/List/Perm.lean +++ b/Batteries/Data/List/Perm.lean @@ -4,10 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro -/ import Batteries.Tactic.Alias -import Batteries.Data.List.Init.Attach import Batteries.Data.List.Pairwise --- Adaptation note: nightly-2024-03-18. We should be able to remove this after nightly-2024-03-19. -import Lean.Elab.Tactic.Rfl /-! # List Permutations @@ -234,7 +231,7 @@ theorem Subperm.trans {l₁ l₂ l₃ : List α} (s₁₂ : l₁ <+~ l₂) (s₂ ⟨l₁', p₁, s₁.trans s₂⟩ theorem Subperm.cons_right {α : Type _} {l l' : List α} (x : α) (h : l <+~ l') : l <+~ x :: l' := - h.trans (sublist_cons x l').subperm + h.trans (sublist_cons_self x l').subperm theorem Subperm.length_le {l₁ l₂ : List α} : l₁ <+~ l₂ → length l₁ ≤ length l₂ | ⟨_l, p, s⟩ => p.length_eq ▸ s.length_le @@ -371,7 +368,7 @@ theorem perm_append_right_iff {l₁ l₂ : List α} (l) : l₁ ++ l ~ l₂ ++ l theorem subperm_cons (a : α) {l₁ l₂ : List α} : a :: l₁ <+~ a :: l₂ ↔ l₁ <+~ l₂ := by refine ⟨fun ⟨l, p, s⟩ => ?_, fun ⟨l, p, s⟩ => ⟨a :: l, p.cons a, s.cons₂ _⟩⟩ match s with - | .cons _ s' => exact (p.subperm_left.2 <| (sublist_cons _ _).subperm).trans s'.subperm + | .cons _ s' => exact (p.subperm_left.2 <| (sublist_cons_self _ _).subperm).trans s'.subperm | .cons₂ _ s' => exact ⟨_, p.cons_inv, s'⟩ /-- Weaker version of `Subperm.cons_left` -/ @@ -412,7 +409,7 @@ theorem Subperm.exists_of_length_lt {l₁ l₂ : List α} (s : l₁ <+~ l₂) (h | slnil => cases h | cons a s IH => match Nat.lt_or_eq_of_le (Nat.le_of_lt_succ h) with - | .inl h => exact (IH h).imp fun a s => s.trans (sublist_cons _ _).subperm + | .inl h => exact (IH h).imp fun a s => s.trans (sublist_cons_self _ _).subperm | .inr h => exact ⟨a, s.eq_of_length h ▸ .refl _⟩ | cons₂ b _ IH => exact (IH <| Nat.lt_of_succ_lt_succ h).imp fun a s => @@ -440,12 +437,12 @@ theorem Nodup.perm_iff_eq_of_sublist {l₁ l₂ l : List α} (d : Nodup l) | .cons _ s₁ => exact IH d.2 s₁ h | .cons₂ _ s₁ => have := Subperm.subset ⟨_, h.symm, s₂⟩ (.head _) - exact (d.1 _ this rfl).elim + exact (d.1 this).elim | cons₂ a _ IH => match s₁ with | .cons _ s₁ => have := Subperm.subset ⟨_, h, s₁⟩ (.head _) - exact (d.1 _ this rfl).elim + exact (d.1 this).elim | .cons₂ _ s₁ => rw [IH d.2 s₁ h.cons_inv] section DecidableEq @@ -464,7 +461,7 @@ theorem subperm_cons_erase (a : α) (l : List α) : l <+~ a :: l.erase a := if h : a ∈ l then (perm_cons_erase h).subperm else - (erase_of_not_mem h).symm ▸ (sublist_cons _ _).subperm + (erase_of_not_mem h).symm ▸ (sublist_cons_self _ _).subperm theorem erase_subperm (a : α) (l : List α) : l.erase a <+~ l := (erase_sublist _ _).subperm @@ -513,7 +510,7 @@ theorem erase_cons_subperm_cons_erase (a b : α) (l : List α) : rw [h, erase_cons_head]; apply subperm_cons_erase else have : ¬(a == b) = true := by simp only [beq_false_of_ne h, not_false_eq_true] - rw [erase_cons_tail _ this] + rw [erase_cons_tail this] theorem subperm_cons_diff {a : α} {l₁ l₂ : List α} : (a :: l₁).diff l₂ <+~ a :: l₁.diff l₂ := by induction l₂ with diff --git a/Batteries/Data/Nat/Basic.lean b/Batteries/Data/Nat/Basic.lean index a6e55a6ea2..1d9658f49e 100644 --- a/Batteries/Data/Nat/Basic.lean +++ b/Batteries/Data/Nat/Basic.lean @@ -94,9 +94,6 @@ protected def casesDiagOn {motive : Nat → Nat → Sort _} (m n : Nat) Nat.recDiag zero_zero (fun _ _ => zero_succ _) (fun _ _ => succ_zero _) (fun _ _ _ => succ_succ _ _) m n -/-- Sum of a list of natural numbers. -/ -protected def sum (l : List Nat) : Nat := l.foldr (·+·) 0 - /-- Integer square root function. Implemented via Newton's method. -/ diff --git a/Batteries/Data/Nat/Lemmas.lean b/Batteries/Data/Nat/Lemmas.lean index 842ca09e95..1c3edddeaf 100644 --- a/Batteries/Data/Nat/Lemmas.lean +++ b/Batteries/Data/Nat/Lemmas.lean @@ -177,10 +177,6 @@ protected alias le_of_le_of_sub_le_sub_left := Nat.le_of_sub_le_sub_left /-! ### sum -/ -@[simp] theorem sum_nil : Nat.sum [] = 0 := rfl - -@[simp] theorem sum_cons : Nat.sum (a :: l) = a + Nat.sum l := rfl - @[simp] theorem sum_append : Nat.sum (l₁ ++ l₂) = Nat.sum l₁ + Nat.sum l₂ := by induction l₁ <;> simp [*, Nat.add_assoc] diff --git a/Batteries/Data/RBMap/Lemmas.lean b/Batteries/Data/RBMap/Lemmas.lean index 37f24ebea9..5577b3a1a7 100644 --- a/Batteries/Data/RBMap/Lemmas.lean +++ b/Batteries/Data/RBMap/Lemmas.lean @@ -152,7 +152,6 @@ theorem min?_eq_toList_head? {t : RBNode α} : t.min? = t.toList.head? := by | nil => rfl | node _ l _ _ ih => cases l <;> simp [RBNode.min?, ih] - next ll _ _ => cases toList ll <;> rfl theorem max?_eq_toList_getLast? {t : RBNode α} : t.max? = t.toList.getLast? := by rw [← min?_reverse, min?_eq_toList_head?]; simp diff --git a/Batteries/Data/Range/Lemmas.lean b/Batteries/Data/Range/Lemmas.lean index 586f32a7e8..d71082848f 100644 --- a/Batteries/Data/Range/Lemmas.lean +++ b/Batteries/Data/Range/Lemmas.lean @@ -5,7 +5,6 @@ Authors: Mario Carneiro -/ import Batteries.Tactic.SeqFocus import Batteries.Data.List.Lemmas -import Batteries.Data.List.Init.Attach namespace Std.Range diff --git a/Batteries/Data/String/Lemmas.lean b/Batteries/Data/String/Lemmas.lean index e046783fee..9984d0fb52 100644 --- a/Batteries/Data/String/Lemmas.lean +++ b/Batteries/Data/String/Lemmas.lean @@ -12,7 +12,8 @@ import Batteries.Tactic.SqueezeScope namespace String -attribute [ext] ext +-- TODO(kmill): add `@[ext]` attribute to `String.ext` in core. +attribute [ext (iff := false)] ext theorem lt_trans {s₁ s₂ s₃ : String} : s₁ < s₂ → s₂ < s₃ → s₁ < s₃ := List.lt_trans' (α := Char) Nat.lt_trans @@ -87,7 +88,8 @@ end namespace Pos -attribute [ext] ext +-- TODO(kmill): add `@[ext]` attribute to `String.Pos.ext` in core. +attribute [ext (iff := false)] ext theorem lt_addChar (p : Pos) (c : Char) : p < p + c := Nat.lt_add_of_pos_right (Char.utf8Size_pos _) @@ -335,7 +337,7 @@ theorem firstDiffPos_loop_eq (l₁ l₂ r₁ r₂ stop p) · next h => rw [dif_neg] <;> simp [hstop, ← hl₁, ← hl₂, -Nat.not_lt, Nat.lt_min] intro h₁ h₂ - have : ∀ {cs}, p < p + utf8Len cs → cs ≠ [] := by rintro _ h rfl; simp at h + have : ∀ {cs}, 0 < utf8Len cs → cs ≠ [] := by rintro _ h rfl; simp at h obtain ⟨a, as, e₁⟩ := List.exists_cons_of_ne_nil (this h₁) obtain ⟨b, bs, e₂⟩ := List.exists_cons_of_ne_nil (this h₂) exact h _ _ _ _ e₁ e₂ @@ -420,8 +422,9 @@ theorem splitAux_of_valid (p l m r acc) : splitAux ⟨l ++ m ++ r⟩ p ⟨utf8Len l⟩ ⟨utf8Len l + utf8Len m⟩ acc = acc.reverse ++ (List.splitOnP.go p r m.reverse).map mk := by unfold splitAux - simp only [List.append_assoc, atEnd_iff, endPos_eq, utf8Len_append, Pos.mk_le_mk, by - simpa using atEnd_of_valid (l ++ m) r, List.reverse_cons, dite_eq_ite] + simp only [List.append_assoc, atEnd_iff, endPos_eq, utf8Len_append, Pos.mk_le_mk, + Nat.add_le_add_iff_left, by simpa using atEnd_of_valid (l ++ m) r, List.reverse_cons, + dite_eq_ite] split · subst r; simpa [List.splitOnP.go] using extract_of_valid l m [] · obtain ⟨c, r, rfl⟩ := r.exists_cons_of_ne_nil ‹_› @@ -674,7 +677,7 @@ theorem foldrAux_of_valid (f : Char → α → α) (l m r a) : rw [← m.reverse_reverse] induction m.reverse generalizing r a with (unfold foldrAux; simp) | cons c m IH => - rw [if_pos (by exact Nat.lt_add_of_pos_right add_utf8Size_pos)] + rw [if_pos add_utf8Size_pos] simp only [← Nat.add_assoc, by simpa using prev_of_valid (l ++ m.reverse) c r] simp only [by simpa using get_of_valid (l ++ m.reverse) (c :: r)] simpa using IH (c::r) (f c a) diff --git a/Batteries/Data/UInt.lean b/Batteries/Data/UInt.lean index a9ce1b561a..44ebfd9b80 100644 --- a/Batteries/Data/UInt.lean +++ b/Batteries/Data/UInt.lean @@ -10,8 +10,6 @@ import Batteries.Classes.Order @[ext] theorem UInt8.ext : {x y : UInt8} → x.toNat = y.toNat → x = y | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl -theorem UInt8.ext_iff {x y : UInt8} : x = y ↔ x.toNat = y.toNat := ⟨congrArg _, UInt8.ext⟩ - @[simp] theorem UInt8.val_val_eq_toNat (x : UInt8) : x.val.val = x.toNat := rfl @[simp] theorem UInt8.val_ofNat (n) : @@ -57,8 +55,6 @@ instance : Batteries.LawfulOrd UInt8 := .compareOfLessAndEq @[ext] theorem UInt16.ext : {x y : UInt16} → x.toNat = y.toNat → x = y | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl -theorem UInt16.ext_iff {x y : UInt16} : x = y ↔ x.toNat = y.toNat := ⟨congrArg _, UInt16.ext⟩ - @[simp] theorem UInt16.val_val_eq_toNat (x : UInt16) : x.val.val = x.toNat := rfl @[simp] theorem UInt16.val_ofNat (n) : @@ -104,8 +100,6 @@ instance : Batteries.LawfulOrd UInt16 := .compareOfLessAndEq @[ext] theorem UInt32.ext : {x y : UInt32} → x.toNat = y.toNat → x = y | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl -theorem UInt32.ext_iff {x y : UInt32} : x = y ↔ x.toNat = y.toNat := ⟨congrArg _, UInt32.ext⟩ - @[simp] theorem UInt32.val_val_eq_toNat (x : UInt32) : x.val.val = x.toNat := rfl @[simp] theorem UInt32.val_ofNat (n) : @@ -151,8 +145,6 @@ instance : Batteries.LawfulOrd UInt32 := .compareOfLessAndEq @[ext] theorem UInt64.ext : {x y : UInt64} → x.toNat = y.toNat → x = y | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl -theorem UInt64.ext_iff {x y : UInt64} : x = y ↔ x.toNat = y.toNat := ⟨congrArg _, UInt64.ext⟩ - @[simp] theorem UInt64.val_val_eq_toNat (x : UInt64) : x.val.val = x.toNat := rfl @[simp] theorem UInt64.val_ofNat (n) : @@ -198,8 +190,6 @@ instance : Batteries.LawfulOrd UInt64 := .compareOfLessAndEq @[ext] theorem USize.ext : {x y : USize} → x.toNat = y.toNat → x = y | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl -theorem USize.ext_iff {x y : USize} : x = y ↔ x.toNat = y.toNat := ⟨congrArg _, USize.ext⟩ - @[simp] theorem USize.val_val_eq_toNat (x : USize) : x.val.val = x.toNat := rfl @[simp] theorem USize.val_ofNat (n) : diff --git a/Batteries/Lean/SMap.lean b/Batteries/Lean/SMap.lean deleted file mode 100644 index 44a660e2e0..0000000000 --- a/Batteries/Lean/SMap.lean +++ /dev/null @@ -1,17 +0,0 @@ -/- -Copyright (c) 2023 Scott Morrison. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Scott Morrison --/ -import Lean.Data.SMap - -/-! -# Extra functions on Lean.SMap --/ - -set_option autoImplicit true - -/-- Monadic fold over a staged map. -/ -def Lean.SMap.foldM {m : Type w → Type w} [Monad m] [BEq α] [Hashable α] - (f : σ → α → β → m σ) (init : σ) (map : SMap α β) : m σ := do - map.map₂.foldlM f (← map.map₁.foldM f init) diff --git a/Batteries/Lean/Util/EnvSearch.lean b/Batteries/Lean/Util/EnvSearch.lean index 9143c89511..d9419b8cbf 100644 --- a/Batteries/Lean/Util/EnvSearch.lean +++ b/Batteries/Lean/Util/EnvSearch.lean @@ -24,8 +24,7 @@ where /-- Check constant should be returned -/ @[nolint unusedArguments] check matches_ (_name : Name) cinfo := do - let include ← p cinfo - if include then + if ← p cinfo then pure $ matches_.push cinfo else pure matches_ diff --git a/Batteries/Lean/Util/Path.lean b/Batteries/Lean/Util/Path.lean deleted file mode 100644 index d9488c0dc8..0000000000 --- a/Batteries/Lean/Util/Path.lean +++ /dev/null @@ -1,34 +0,0 @@ -/- -Copyright (c) 2022 Gabriel Ebner. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Gabriel Ebner --/ -import Lean.Elab.Term - -/-! -# `compile_time_search_path%` term elaborator. - -Use this as `searchPathRef.set compile_time_search_path%`. --/ - -open Lean System - --- Ideally this instance would be constructed simply by `deriving instance ToExpr for FilePath` --- but for now we have decided not to upstream the `ToExpr` derive handler from `Mathlib`. --- https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/ToExpr.20derive.20handler/near/386476438 -instance : ToExpr FilePath where - toTypeExpr := mkConst ``FilePath - toExpr path := mkApp (mkConst ``FilePath.mk) (toExpr path.1) - -/-- -Term elaborator that retrieves the current `SearchPath`. - -Typical usage is `searchPathRef.set compile_time_search_path%`. - -This must not be used in files that are potentially compiled on another machine and then -imported. -(That is, if used in an imported file it will embed the search path from whichever machine -compiled the `.olean`.) --/ -elab "compile_time_search_path%" : term => - return toExpr (← searchPathRef.get) diff --git a/Batteries/Logic.lean b/Batteries/Logic.lean index d0fd84e688..5c6efe108a 100644 --- a/Batteries/Logic.lean +++ b/Batteries/Logic.lean @@ -16,10 +16,6 @@ instance {f : α → β} [DecidablePred p] : DecidablePred (p ∘ f) := theorem Function.id_def : @id α = fun x => x := rfl -/-! ## exists and forall -/ - -alias ⟨forall_not_of_not_exists, not_exists_of_forall_not⟩ := not_exists - /-! ## decidable -/ protected alias ⟨Decidable.exists_not_of_not_forall, _⟩ := Decidable.not_forall @@ -60,8 +56,7 @@ theorem funext₃ {β : α → Sort _} {γ : ∀ a, β a → Sort _} {δ : ∀ a {f g : ∀ a b c, δ a b c} (h : ∀ a b c, f a b c = g a b c) : f = g := funext fun _ => funext₂ <| h _ -theorem Function.funext_iff {β : α → Sort u} {f₁ f₂ : ∀ x : α, β x} : f₁ = f₂ ↔ ∀ a, f₁ a = f₂ a := - ⟨congrFun, funext⟩ +protected alias Function.funext_iff := funext_iff theorem ne_of_apply_ne {α β : Sort _} (f : α → β) {x y : α} : f x ≠ f y → x ≠ y := mt <| congrArg _ @@ -128,9 +123,7 @@ end Mem -- instance (priority := 10) {α} [Subsingleton α] : DecidableEq α -- | a, b => isTrue (Subsingleton.elim a b) --- @[simp] -- TODO(Mario): profile -theorem eq_iff_true_of_subsingleton [Subsingleton α] (x y : α) : x = y ↔ True := - iff_true_intro (Subsingleton.elim ..) +-- TODO(Mario): profile adding `@[simp]` to `eq_iff_true_of_subsingleton` /-- If all points are equal to a given point `x`, then `α` is a subsingleton. -/ theorem subsingleton_of_forall_eq (x : α) (h : ∀ y, y = x) : Subsingleton α := diff --git a/Batteries/StdDeprecations.lean b/Batteries/StdDeprecations.lean index c705ee839d..f82b1739a7 100644 --- a/Batteries/StdDeprecations.lean +++ b/Batteries/StdDeprecations.lean @@ -22,7 +22,6 @@ Let's hope that people using the tactic implementations can work this out themse -/ @[deprecated (since := "2024-05-07")] alias Std.AssocList := Batteries.AssocList -@[deprecated (since := "2024-05-07")] alias Std.HashMap := Batteries.HashMap @[deprecated (since := "2024-05-07")] alias Std.mkHashMap := Batteries.mkHashMap @[deprecated (since := "2024-05-07")] alias Std.DList := Batteries.DList @[deprecated (since := "2024-05-07")] alias Std.PairingHeapImp.Heap := Batteries.PairingHeapImp.Heap diff --git a/Batteries/Tactic/Lint/Basic.lean b/Batteries/Tactic/Lint/Basic.lean index 87cc925a06..948bab5456 100644 --- a/Batteries/Tactic/Lint/Basic.lean +++ b/Batteries/Tactic/Lint/Basic.lean @@ -42,6 +42,8 @@ def isAutoDecl (decl : Name) : CoreM Bool := do if env.isConstructor n && ["injEq", "inj", "sizeOf_spec"].any (· == s) then return true if let ConstantInfo.inductInfo _ := (← getEnv).find? n then + if s.startsWith "brecOn_" || s.startsWith "below_" || s.startsWith "binductionOn_" + || s.startsWith "ibelow_" then return true if [casesOnSuffix, recOnSuffix, brecOnSuffix, binductionOnSuffix, belowSuffix, "ibelow", "ndrec", "ndrecOn", "noConfusionType", "noConfusion", "ofNat", "toCtorIdx" ].any (· == s) then diff --git a/Batteries/Util/CheckTactic.lean b/Batteries/Util/CheckTactic.lean deleted file mode 100644 index bc97e681cc..0000000000 --- a/Batteries/Util/CheckTactic.lean +++ /dev/null @@ -1,124 +0,0 @@ -/- -Copyright (c) 2024 Lean FRO. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joe Hendrix --/ -import Lean.Elab.Tactic.ElabTerm -import Lean.Elab.Term - -/- -This file is the home for commands to tactics behave as expected. - -It currently includes two tactics: - -#check_tactic t ~> res - - -only a #check_simp command that applies simp -IT --/ - -namespace Batteries.Tactic - -open Lean Elab Tactic -open Meta - -/-- -Type used to lift an arbitrary value into a type parameter so it can -appear in a proof goal. - -It is used by the #check_tactic command. --/ -private inductive CheckGoalType {α : Sort u} : (val : α) → Prop where -| intro : (val : α) → CheckGoalType val - -private def matchCheckGoalType (stx : Syntax) (goalType : Expr) : MetaM (Expr × Expr × Level) := do - let u ← mkFreshLevelMVar - let type ← mkFreshExprMVar (some (.sort u)) - let val ← mkFreshExprMVar (some type) - let extType := mkAppN (.const ``CheckGoalType [u]) #[type, val] - if !(← isDefEq goalType extType) then - throwErrorAt stx "Goal{indentExpr goalType}\nis expected to match {indentExpr extType}" - pure (val, type, u) - -/-- -`check_tactic_goal t` verifies that the goal has is equal to -`CheckGoalType t` with reducible transparency. It closes the goal if so -and otherwise reports an error. - -It is used by #check_tactic. --/ -local syntax (name := check_tactic_goal) "check_tactic_goal " term : tactic - -/-- -Implementation of `check_tactic_goal` --/ -@[tactic check_tactic_goal] private def evalCheckTacticGoal : Tactic := fun stx => - match stx with - | `(tactic| check_tactic_goal $exp) => - closeMainGoalUsing (checkUnassigned := false) fun goalType => do - let (val, type, u) ← matchCheckGoalType stx goalType - let expTerm ← elabTermEnsuringType exp type - if !(← Meta.withReducible <| isDefEq val expTerm) then - throwErrorAt stx - m!"Term reduces to{indentExpr val}\nbut is expected to reduce to {indentExpr expTerm}" - return mkAppN (.const ``CheckGoalType.intro [u]) #[type, val] - | _ => throwErrorAt stx "check_goal syntax error" - -/-- -`check_tactic_goal t` verifies that the goal has is equal to -`CheckGoalType t` with reducible transparency. It closes the goal if so -and otherwise reports an error. - -It is used by #check_tactic. --/ -local syntax (name := check_tactic_fails) "check_tactic_fails " tactic : tactic - -@[tactic check_tactic_fails] private def evalCheckTacticFails : Tactic := fun stx => do - let `(tactic| check_tactic_fails $tactic) := stx - | throwUnsupportedSyntax - closeMainGoalUsing (checkUnassigned := false) fun goalType => do - let (val, type, u) ← matchCheckGoalType stx goalType - Term.withoutErrToSorry <| withoutRecover do - match (← try (some <$> evalTactic tactic) catch _ => pure none) with - | none => - return mkAppN (.const ``CheckGoalType.intro [u]) #[type, val] - | some () => - let gls ← getGoals - let ppGoal (g : MVarId) := do - let (val, _type, _u) ← matchCheckGoalType stx (← g.getType) - pure m!"{indentExpr val}" - let msg ← - match gls with - | [] => pure m!"{tactic} expected to fail on {val}, but closed goal." - | [g] => - pure <| m!"{tactic} expected to fail on {val}, but returned: {←ppGoal g}" - | gls => - let app m g := do pure <| m ++ (←ppGoal g) - let init := m!"{tactic} expected to fail on {val}, but returned goals:" - gls.foldlM (init := init) app - throwErrorAt stx msg - -/-- -`#check_tactic t ~> r by commands` runs the tactic sequence `commands` -on a goal with t in the type and sees if the resulting expression has -reduced it to `r`. --/ -macro "#check_tactic " t:term "~>" result:term "by" tac:tactic : command => - `(command|example : CheckGoalType $t := by $tac; check_tactic_goal $result) - -/-- -`#check_simp t ~> r` checks `simp` reduces `t` to `r`. --/ -macro "#check_simp " t:term "~>" exp:term : command => - `(command|#check_tactic $t ~> $exp by simp) - -example (x : Nat) : CheckGoalType ((x + z) = x) := by - fail_if_success simp [] - exact (CheckGoalType.intro ((x + z) = x)) - -/-- -`#check_simp t !~>` checks `simp` fails to reduce `t`. --/ -macro "#check_simp " t:term "!~>" : command => - `(command|example : CheckGoalType $t := by check_tactic_fails simp) diff --git a/lean-toolchain b/lean-toolchain index 7f0ea50aaa..64981ae5f5 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.10.0 +leanprover/lean4:v4.11.0-rc1 diff --git a/scripts/runLinter.lean b/scripts/runLinter.lean index 3d98a1c902..4f18be6b50 100644 --- a/scripts/runLinter.lean +++ b/scripts/runLinter.lean @@ -1,6 +1,6 @@ +import Lean.Util.SearchPath import Batteries.Tactic.Lint import Batteries.Data.Array.Basic -import Batteries.Lean.Util.Path open Lean Core Elab Command Std.Tactic.Lint open System (FilePath) diff --git a/test/array.lean b/test/array.lean index 41338a8bd4..2ba3a29577 100644 --- a/test/array.lean +++ b/test/array.lean @@ -1,4 +1,3 @@ -import Batteries.Util.CheckTactic import Batteries.Data.Array section diff --git a/test/congr.lean b/test/congr.lean index a71aed0315..065a899f99 100644 --- a/test/congr.lean +++ b/test/congr.lean @@ -19,8 +19,6 @@ example {α β γ δ} {F : ∀ {α β}, (α → β) → γ → δ} {f g : α → -- apply_assumption -- FIXME apply h -attribute [ext] Subtype.eq - example {α β : Type _} {f : _ → β} {x y : { x : { x : α // x = x } // x = x }} (h : x.1 = y.1) : f x = f y := by congr with : 1