From 2e31efe2f1d57a0ad616f54e0220b7a6e4cde48c Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Mon, 25 Mar 2024 09:15:15 +0000 Subject: [PATCH 01/27] chore: bump to nightly-2024-03-25 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index ca08d93846..f55067a5b4 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-03-24 +leanprover/lean4:nightly-2024-03-25 From 6921c4b225a2a135bb0b0018ba52eb4c66404955 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 26 Mar 2024 16:28:45 +1100 Subject: [PATCH 02/27] chore: remove some already upstreamed tactics (#713) --- Std/Tactic/Init.lean | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/Std/Tactic/Init.lean b/Std/Tactic/Init.lean index c0ff004e6d..326d11aab5 100644 --- a/Std/Tactic/Init.lean +++ b/Std/Tactic/Init.lean @@ -14,9 +14,6 @@ import Lean.Elab.Tactic.BuiltinTactic namespace Std.Tactic open Lean Parser.Tactic Elab Command Elab.Tactic Meta -/-- `exfalso` converts a goal `⊢ tgt` into `⊢ False` by applying `False.elim`. -/ -macro "exfalso" : tactic => `(tactic| refine False.elim ?_) - /-- `_` in tactic position acts like the `done` tactic: it fails and gives the list of goals if there are any. It is useful as a placeholder after starting a tactic block @@ -24,15 +21,6 @@ such as `by _` to make it syntactically correct and show the current goal. -/ macro "_" : tactic => `(tactic| {}) -@[inherit_doc failIfSuccess] -syntax (name := failIfSuccessConv) "fail_if_success " Conv.convSeq : conv - -attribute [tactic failIfSuccessConv] evalFailIfSuccess - -/-- `rwa` calls `rw`, then closes any remaining goals using `assumption`. -/ -macro "rwa " rws:rwRuleSeq loc:(location)? : tactic => - `(tactic| (rw $rws:rwRuleSeq $[$loc:location]?; assumption)) - /-- Like `exact`, but takes a list of terms and checks that all goals are discharged after the tactic. -/ From f9dbfb5e057b18ae588202e945d17826fc929e92 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 26 Mar 2024 19:15:06 +1100 Subject: [PATCH 03/27] bump --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index f55067a5b4..379f4bc3c7 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-03-25 +leanprover/lean4:nightly-2024-03-26 From a17d191b45af7755a1824781e33798b2be128c8e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Tue, 26 Mar 2024 19:51:11 -0400 Subject: [PATCH 04/27] feat: better `List.take_drop` and `List.drop_take` (#710) * feat: better `List.take_drop` and `List.drop_take` * fix: use simpa * fix: remove stray edit --- Std/Data/List/Lemmas.lean | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean index 873829249c..6021e8bf9d 100644 --- a/Std/Data/List/Lemmas.lean +++ b/Std/Data/List/Lemmas.lean @@ -1108,12 +1108,16 @@ theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j) _ = drop (n + m) l := drop_drop n m l _ = drop (n + (m + 1)) (a :: l) := rfl -theorem drop_take : ∀ (m n : Nat) (l : List α), drop m (take (m + n) l) = take n (drop m l) - | 0, n, _ => by simp - | m + 1, n, nil => by simp - | m + 1, n, _ :: l => by - have h : m + 1 + n = m + n + 1 := by rw [Nat.add_assoc, Nat.add_comm 1 n, ← Nat.add_assoc] - simpa [take_cons_succ, h] using drop_take m n l +theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (take (m + n) l) + | 0, _, _ => by simp + | _, _, [] => by simp + | _+1, _, _ :: _ => by simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop .. + +theorem drop_take : ∀ (m n : Nat) (l : List α), drop n (take m l) = take (m - n) (drop n l) + | 0, _, _ => by simp + | _, 0, _ => by simp + | _, _, [] => by simp + | _+1, _+1, _ :: _ => by simpa [take_succ_cons, drop_succ_cons] using drop_take .. theorem map_drop (f : α → β) : ∀ (L : List α) (i : Nat), (L.drop i).map f = (L.map f).drop i From e0ab3b19dc0338aec7d5405b476faf8aa89db2ef Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Wed, 27 Mar 2024 09:15:58 +0000 Subject: [PATCH 05/27] chore: bump to nightly-2024-03-27 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 379f4bc3c7..c6306360b3 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-03-26 +leanprover/lean4:nightly-2024-03-27 From 74f80f5289aef638ef2dd7a10ae683fffba1fb90 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Thu, 28 Mar 2024 09:15:35 +0000 Subject: [PATCH 06/27] chore: bump to nightly-2024-03-28 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index c6306360b3..2f33486949 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-03-27 +leanprover/lean4:nightly-2024-03-28 From 406fe30baf9887a5cbc9cb3471d6d84fd29bfc52 Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Thu, 28 Mar 2024 16:24:29 -0700 Subject: [PATCH 07/27] fix: remove upstreamed defs and fix some proofs --- Std/Data/Array/Lemmas.lean | 24 ++-- Std/Data/List/Basic.lean | 244 ------------------------------------- Std/Data/List/Lemmas.lean | 2 +- 3 files changed, 13 insertions(+), 257 deletions(-) diff --git a/Std/Data/Array/Lemmas.lean b/Std/Data/Array/Lemmas.lean index 199f1a3036..536f5071f4 100644 --- a/Std/Data/Array/Lemmas.lean +++ b/Std/Data/Array/Lemmas.lean @@ -20,12 +20,6 @@ local macro_rules | `($x[$i]'$h) => `(getElem $x $i $h) @[simp] theorem getElem!_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) [Decidable (Dom a i)] [Inhabited Elem] : a[i]! = a[i.1]! := rfl -theorem getElem?_pos [GetElem Cont Idx Elem Dom] - (a : Cont) (i : Idx) (h : Dom a i) [Decidable (Dom a i)] : a[i]? = a[i] := dif_pos h - -theorem getElem?_neg [GetElem Cont Idx Elem Dom] - (a : Cont) (i : Idx) (h : ¬Dom a i) [Decidable (Dom a i)] : a[i]? = none := dif_neg h - @[simp] theorem mkArray_data (n : Nat) (v : α) : (mkArray n v).data = List.replicate n v := rfl @[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) : @@ -93,13 +87,19 @@ theorem get?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x := b rw [getElem?_pos, get_push_eq] theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]? := by - split - . next heq => rw [heq, getElem?_pos, get_push_eq] - · next hne => + match Nat.lt_trichotomy i a.size with + | Or.inl g => + have h1 : i < a.size + 1 := by omega + have h2 : i ≠ a.size := by omega + simp [getElem?, size_push, g, h1, h2, get_push_lt] + | Or.inr (Or.inl heq) => + simp [heq, getElem?_pos, get_push_eq] + | Or.inr (Or.inr g) => simp only [getElem?, size_push] - split <;> split <;> try simp only [*, get_push_lt] - · next p q => exact Or.elim (Nat.eq_or_lt_of_le (Nat.le_of_lt_succ p)) hne q - · next p q => exact p (Nat.lt.step q) + have h1 : ¬ (i < a.size ) := by omega + have h2 : ¬ (i < a.size + 1) := by omega + have h3 : i ≠ a.size := by omega + simp [h1, h2, h3] @[simp] theorem get?_size {a : Array α} : a[a.size]? = none := by simp only [getElem?, Nat.lt_irrefl, dite_false] diff --git a/Std/Data/List/Basic.lean b/Std/Data/List/Basic.lean index 7774294973..86afb0187b 100644 --- a/Std/Data/List/Basic.lean +++ b/Std/Data/List/Basic.lean @@ -6,250 +6,6 @@ Authors: Leonardo de Moura namespace List -/-! ## Tail recursive implementations for definitions from core -/ - -/-- Tail recursive version of `erase`. -/ -@[inline] def setTR (l : List α) (n : Nat) (a : α) : List α := go l n #[] where - /-- Auxiliary for `setTR`: `setTR.go l a xs n acc = acc.toList ++ set xs a`, - unless `n ≥ l.length` in which case it returns `l` -/ - go : List α → Nat → Array α → List α - | [], _, _ => l - | _::xs, 0, acc => acc.toListAppend (a::xs) - | x::xs, n+1, acc => go xs n (acc.push x) - -@[csimp] theorem set_eq_setTR : @set = @setTR := by - funext α l n a; simp [setTR] - let rec go (acc) : ∀ xs n, l = acc.data ++ xs → - setTR.go l a xs n acc = acc.data ++ xs.set n a - | [], _ => fun h => by simp [setTR.go, set, h] - | x::xs, 0 => by simp [setTR.go, set] - | x::xs, n+1 => fun h => by simp [setTR.go, set]; rw [go _ xs]; {simp}; simp [h] - exact (go #[] _ _ rfl).symm - -/-- Tail recursive version of `erase`. -/ -@[inline] def eraseTR [BEq α] (l : List α) (a : α) : List α := go l #[] where - /-- Auxiliary for `eraseTR`: `eraseTR.go l a xs acc = acc.toList ++ erase xs a`, - unless `a` is not present in which case it returns `l` -/ - go : List α → Array α → List α - | [], _ => l - | x::xs, acc => bif x == a then acc.toListAppend xs else go xs (acc.push x) - -@[csimp] theorem erase_eq_eraseTR : @List.erase = @eraseTR := by - funext α _ l a; simp [eraseTR] - suffices ∀ xs acc, l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ xs.erase a from - (this l #[] (by simp)).symm - intro xs; induction xs with intro acc h - | nil => simp [List.erase, eraseTR.go, h] - | cons x xs IH => - simp [List.erase, eraseTR.go] - cases x == a <;> simp - · rw [IH]; simp; simp; exact h - -/-- Tail recursive version of `eraseIdx`. -/ -@[inline] def eraseIdxTR (l : List α) (n : Nat) : List α := go l n #[] where - /-- Auxiliary for `eraseIdxTR`: `eraseIdxTR.go l n xs acc = acc.toList ++ eraseIdx xs a`, - unless `a` is not present in which case it returns `l` -/ - go : List α → Nat → Array α → List α - | [], _, _ => l - | _::as, 0, acc => acc.toListAppend as - | a::as, n+1, acc => go as n (acc.push a) - -@[csimp] theorem eraseIdx_eq_eraseIdxTR : @eraseIdx = @eraseIdxTR := by - funext α l n; simp [eraseIdxTR] - suffices ∀ xs acc, l = acc.data ++ xs → eraseIdxTR.go l xs n acc = acc.data ++ xs.eraseIdx n from - (this l #[] (by simp)).symm - intro xs; induction xs generalizing n with intro acc h - | nil => simp [eraseIdx, eraseIdxTR.go, h] - | cons x xs IH => - match n with - | 0 => simp [eraseIdx, eraseIdxTR.go] - | n+1 => - simp [eraseIdx, eraseIdxTR.go] - rw [IH]; simp; simp; exact h - -/-- Tail recursive version of `bind`. -/ -@[inline] def bindTR (as : List α) (f : α → List β) : List β := go as #[] where - /-- Auxiliary for `bind`: `bind.go f as = acc.toList ++ bind f as` -/ - @[specialize] go : List α → Array β → List β - | [], acc => acc.toList - | x::xs, acc => go xs (acc ++ f x) - -@[csimp] theorem bind_eq_bindTR : @List.bind = @bindTR := by - funext α β as f - let rec go : ∀ as acc, bindTR.go f as acc = acc.data ++ as.bind f - | [], acc => by simp [bindTR.go, bind] - | x::xs, acc => by simp [bindTR.go, bind, go xs] - exact (go as #[]).symm - -/-- Tail recursive version of `join`. -/ -@[inline] def joinTR (l : List (List α)) : List α := bindTR l id - -@[csimp] theorem join_eq_joinTR : @join = @joinTR := by - funext α l; rw [← List.bind_id, List.bind_eq_bindTR]; rfl - -/-- Tail recursive version of `filterMap`. -/ -@[inline] def filterMapTR (f : α → Option β) (l : List α) : List β := go l #[] where - /-- Auxiliary for `filterMap`: `filterMap.go f l = acc.toList ++ filterMap f l` -/ - @[specialize] go : List α → Array β → List β - | [], acc => acc.toList - | a::as, acc => match f a with - | none => go as acc - | some b => go as (acc.push b) - -@[csimp] theorem filterMap_eq_filterMapTR : @List.filterMap = @filterMapTR := by - funext α β f l - let rec go : ∀ as acc, filterMapTR.go f as acc = acc.data ++ as.filterMap f - | [], acc => by simp [filterMapTR.go, filterMap] - | a::as, acc => by simp [filterMapTR.go, filterMap, go as]; split <;> simp [*] - exact (go l #[]).symm - -/-- Tail recursive version of `replace`. -/ -@[inline] def replaceTR [BEq α] (l : List α) (b c : α) : List α := go l #[] where - /-- Auxiliary for `replace`: `replace.go l b c xs acc = acc.toList ++ replace xs b c`, - unless `b` is not found in `xs` in which case it returns `l`. -/ - @[specialize] go : List α → Array α → List α - | [], _ => l - | a::as, acc => bif a == b then acc.toListAppend (c::as) else go as (acc.push a) - -@[csimp] theorem replace_eq_replaceTR : @List.replace = @replaceTR := by - funext α _ l b c; simp [replaceTR] - suffices ∀ xs acc, l = acc.data ++ xs → - replaceTR.go l b c xs acc = acc.data ++ xs.replace b c from - (this l #[] (by simp)).symm - intro xs; induction xs with intro acc - | nil => simp [replace, replaceTR.go] - | cons x xs IH => - simp [replace, replaceTR.go]; split <;> simp [*] - · intro h; rw [IH]; simp; simp; exact h - -/-- Tail recursive version of `take`. -/ -@[inline] def takeTR (n : Nat) (l : List α) : List α := go l n #[] where - /-- Auxiliary for `take`: `take.go l xs n acc = acc.toList ++ take n xs`, - unless `n ≥ xs.length` in which case it returns `l`. -/ - @[specialize] go : List α → Nat → Array α → List α - | [], _, _ => l - | _::_, 0, acc => acc.toList - | a::as, n+1, acc => go as n (acc.push a) - -@[csimp] theorem take_eq_takeTR : @take = @takeTR := by - funext α n l; simp [takeTR] - suffices ∀ xs acc, l = acc.data ++ xs → takeTR.go l xs n acc = acc.data ++ xs.take n from - (this l #[] (by simp)).symm - intro xs; induction xs generalizing n with intro acc - | nil => cases n <;> simp [take, takeTR.go] - | cons x xs IH => - cases n with simp [take, takeTR.go] - | succ n => intro h; rw [IH]; simp; simp; exact h - -/-- Tail recursive version of `takeWhile`. -/ -@[inline] def takeWhileTR (p : α → Bool) (l : List α) : List α := go l #[] where - /-- Auxiliary for `takeWhile`: `takeWhile.go p l xs acc = acc.toList ++ takeWhile p xs`, - unless no element satisfying `p` is found in `xs` in which case it returns `l`. -/ - @[specialize] go : List α → Array α → List α - | [], _ => l - | a::as, acc => bif p a then go as (acc.push a) else acc.toList - -@[csimp] theorem takeWhile_eq_takeWhileTR : @takeWhile = @takeWhileTR := by - funext α p l; simp [takeWhileTR] - suffices ∀ xs acc, l = acc.data ++ xs → - takeWhileTR.go p l xs acc = acc.data ++ xs.takeWhile p from - (this l #[] (by simp)).symm - intro xs; induction xs with intro acc - | nil => simp [takeWhile, takeWhileTR.go] - | cons x xs IH => - simp [takeWhile, takeWhileTR.go]; split <;> simp [*] - · intro h; rw [IH]; simp; simp; exact h - -/-- Tail recursive version of `foldr`. -/ -@[specialize] def foldrTR (f : α → β → β) (init : β) (l : List α) : β := l.toArray.foldr f init - -@[csimp] theorem foldr_eq_foldrTR : @foldr = @foldrTR := by - funext α β f init l; simp [foldrTR, Array.foldr_eq_foldr_data, -Array.size_toArray] - -/-- Tail recursive version of `zipWith`. -/ -@[inline] def zipWithTR (f : α → β → γ) (as : List α) (bs : List β) : List γ := go as bs #[] where - /-- Auxiliary for `zipWith`: `zipWith.go f as bs acc = acc.toList ++ zipWith f as bs` -/ - go : List α → List β → Array γ → List γ - | a::as, b::bs, acc => go as bs (acc.push (f a b)) - | _, _, acc => acc.toList - -@[csimp] theorem zipWith_eq_zipWithTR : @zipWith = @zipWithTR := by - funext α β γ f as bs - let rec go : ∀ as bs acc, zipWithTR.go f as bs acc = acc.data ++ as.zipWith f bs - | [], _, acc | _::_, [], acc => by simp [zipWithTR.go, zipWith] - | a::as, b::bs, acc => by simp [zipWithTR.go, zipWith, go as bs] - exact (go as bs #[]).symm - -/-- Tail recursive version of `unzip`. -/ -def unzipTR (l : List (α × β)) : List α × List β := - l.foldr (fun (a, b) (al, bl) => (a::al, b::bl)) ([], []) - -@[csimp] theorem unzip_eq_unzipTR : @unzip = @unzipTR := by - funext α β l; simp [unzipTR]; induction l <;> simp [*] - -/-- Tail recursive version of `enumFrom`. -/ -def enumFromTR (n : Nat) (l : List α) : List (Nat × α) := - let arr := l.toArray - (arr.foldr (fun a (n, acc) => (n-1, (n-1, a) :: acc)) (n + arr.size, [])).2 - -@[csimp] theorem enumFrom_eq_enumFromTR : @enumFrom = @enumFromTR := by - funext α n l; simp [enumFromTR, -Array.size_toArray] - let f := fun (a : α) (n, acc) => (n-1, (n-1, a) :: acc) - let rec go : ∀ l n, l.foldr f (n + l.length, []) = (n, enumFrom n l) - | [], n => rfl - | a::as, n => by - rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as] - simp [enumFrom, f] - rw [Array.foldr_eq_foldr_data] - simp [go] - -theorem replicateTR_loop_eq : ∀ n, replicateTR.loop a n acc = replicate n a ++ acc - | 0 => rfl - | n+1 => by rw [← replicateTR_loop_replicate_eq _ 1 n, replicate, replicate, - replicateTR.loop, replicateTR_loop_eq n, replicateTR_loop_eq n, append_assoc]; rfl - -/-- Tail recursive version of `dropLast`. -/ -@[inline] def dropLastTR (l : List α) : List α := l.toArray.pop.toList - -@[csimp] theorem dropLast_eq_dropLastTR : @dropLast = @dropLastTR := by - funext α l; simp [dropLastTR] - -/-- Tail recursive version of `intersperse`. -/ -def intersperseTR (sep : α) : List α → List α - | [] => [] - | [x] => [x] - | x::y::xs => x :: sep :: y :: xs.foldr (fun a r => sep :: a :: r) [] - -@[csimp] theorem intersperse_eq_intersperseTR : @intersperse = @intersperseTR := by - funext α sep l; simp [intersperseTR] - match l with - | [] | [_] => rfl - | x::y::xs => simp [intersperse]; induction xs generalizing y <;> simp [*] - -/-- Tail recursive version of `intercalate`. -/ -def intercalateTR (sep : List α) : List (List α) → List α - | [] => [] - | [x] => x - | x::xs => go sep.toArray x xs #[] -where - /-- Auxiliary for `intercalateTR`: - `intercalateTR.go sep x xs acc = acc.toList ++ intercalate sep.toList (x::xs)` -/ - go (sep : Array α) : List α → List (List α) → Array α → List α - | x, [], acc => acc.toListAppend x - | x, y::xs, acc => go sep y xs (acc ++ x ++ sep) - -@[csimp] theorem intercalate_eq_intercalateTR : @intercalate = @intercalateTR := by - funext α sep l; simp [intercalate, intercalateTR] - match l with - | [] => rfl - | [_] => simp - | x::y::xs => - let rec go {acc x} : ∀ xs, - intercalateTR.go sep.toArray x xs acc = acc.data ++ join (intersperse sep (x::xs)) - | [] => by simp [intercalateTR.go] - | _::_ => by simp [intercalateTR.go, go] - simp [intersperse, go] - /-! ## New definitions -/ /-- diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean index 4c80ce5e1d..da5a56601b 100644 --- a/Std/Data/List/Lemmas.lean +++ b/Std/Data/List/Lemmas.lean @@ -754,7 +754,7 @@ theorem get?_zero (l : List α) : l.get? 0 = l.head? := by cases l <;> rfl @[simp] theorem getElem_eq_get (l : List α) (i : Nat) (h) : l[i]'h = l.get ⟨i, h⟩ := rfl @[simp] theorem getElem?_eq_get? (l : List α) (i : Nat) : l[i]? = l.get? i := by - unfold getElem?; split + simp only [getElem?]; split · exact (get?_eq_get ‹_›).symm · exact (get?_eq_none.2 <| Nat.not_lt.1 ‹_›).symm From 1c9e0fb121384f9ea89c54295301556082370256 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Fri, 29 Mar 2024 09:14:31 +0000 Subject: [PATCH 08/27] chore: bump to nightly-2024-03-29 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 2f33486949..7268b6fc68 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-03-28 +leanprover/lean4:nightly-2024-03-29 From 084ff980820c328380edf42714368f51b4802cf0 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sat, 30 Mar 2024 09:18:35 +1100 Subject: [PATCH 09/27] chore: removed unnecessary array indexing proofs (#701) --- Std/CodeAction/Deprecated.lean | 2 +- Std/Data/Array/Lemmas.lean | 29 ++++++++++++++--------------- Std/Data/Array/Monadic.lean | 8 ++++---- Std/Data/HashMap/WF.lean | 2 +- Std/Lean/Meta/AssertHypotheses.lean | 2 +- Std/Linter/UnnecessarySeqFocus.lean | 2 +- 6 files changed, 22 insertions(+), 23 deletions(-) diff --git a/Std/CodeAction/Deprecated.lean b/Std/CodeAction/Deprecated.lean index 132edd575b..47082f6e70 100644 --- a/Std/CodeAction/Deprecated.lean +++ b/Std/CodeAction/Deprecated.lean @@ -32,7 +32,7 @@ def deprecatedCodeActionProvider : CodeActionProvider := fun params snap => do for diag in snap.interactiveDiags do if let some #[.deprecated] := diag.tags? then if h : _ then - msgs := msgs.push (snap.cmdState.messages.msgs[i]'h) + msgs := msgs.push (snap.cmdState.messages.msgs[i]) i := i + 1 if msgs.isEmpty then return #[] let start := doc.meta.text.lspPosToUtf8Pos params.range.start diff --git a/Std/Data/Array/Lemmas.lean b/Std/Data/Array/Lemmas.lean index 2a37edf6d4..f2fef9000d 100644 --- a/Std/Data/Array/Lemmas.lean +++ b/Std/Data/Array/Lemmas.lean @@ -10,8 +10,6 @@ import Std.Data.Array.Basic import Std.Tactic.SeqFocus import Std.Util.ProofWanted -local macro_rules | `($x[$i]'$h) => `(getElem $x $i $h) - @[simp] theorem getElem_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) : a[i] = a[i.1] := rfl @@ -30,7 +28,7 @@ theorem getElem?_neg [GetElem Cont Idx Elem Dom] @[simp] theorem mkArray_data (n : Nat) (v : α) : (mkArray n v).data = List.replicate n v := rfl @[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) : - (mkArray n v)[i]'h = v := by simp [Array.getElem_eq_data_get] + (mkArray n v)[i] = v := by simp [Array.getElem_eq_data_get] namespace Array @@ -108,7 +106,7 @@ theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x el @[simp] theorem data_set (a : Array α) (i v) : (a.set i v).data = a.data.set i.1 v := rfl theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) : - (a.set i v)[i.1]'(by simp [i.2]) = v := by + (a.set i v)[i.1] = v := by simp only [set, getElem_eq_data_get, List.get_set_eq] theorem get?_set_eq (a : Array α) (i : Fin a.size) (v : α) : @@ -131,7 +129,7 @@ theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v : simp only [set, getElem_eq_data_get, List.get_set_ne _ h] theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) : - (setD a i v)[i]'h = v := by + (setD a i v)[i] = v := by simp at h simp only [setD, h, dite_true, get_set, ite_true] @@ -187,7 +185,7 @@ theorem eq_push_pop_back_of_size_ne_zero [Inhabited α] {as : Array α} (h : as. theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size ≠ 0) : ∃ (bs : Array α) (c : α), as = bs.push c := - let _ : Inhabited α := ⟨as[0]'(Nat.zero_lt_of_ne_zero h)⟩ + let _ : Inhabited α := ⟨as[0]⟩ ⟨as.pop, as.back, eq_push_pop_back_of_size_ne_zero h⟩ theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl @@ -429,9 +427,9 @@ theorem map_eq_foldl (as : Array α) (f : α → β) : theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h0 : motive 0) (p : Fin as.size → β → Prop) (hs : ∀ i, motive i.1 → p i (f as[i]) ∧ motive (i+1)) : motive as.size ∧ - ∃ eq : (as.map f).size = as.size, ∀ i h, p ⟨i, h⟩ ((as.map f)[i]'(eq ▸ h)) := by + ∃ eq : (as.map f).size = as.size, ∀ i h, p ⟨i, h⟩ ((as.map f)[i]) := by have t := foldl_induction (as := as) (β := Array β) - (motive := fun i arr => motive i ∧ arr.size = i ∧ ∀ i h2, p i (arr[i.1]'h2)) + (motive := fun i arr => motive i ∧ arr.size = i ∧ ∀ i h2, p i arr[i.1]) (init := #[]) (f := fun r a => r.push (f a)) ?_ ?_ obtain ⟨m, eq, w⟩ := t · refine ⟨m, by simpa [map_eq_foldl] using eq, ?_⟩ @@ -455,11 +453,11 @@ theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f as[i])) : - ∃ eq : (as.map f).size = as.size, ∀ i h, p ⟨i, h⟩ ((as.map f)[i]'(eq ▸ h)) := by + ∃ eq : (as.map f).size = as.size, ∀ i h, p ⟨i, h⟩ ((as.map f)[i]) := by simpa using map_induction as f (fun _ => True) trivial p (by simp_all) @[simp] theorem getElem_map (f : α → β) (as : Array α) (i : Nat) (h) : - ((as.map f)[i]'h) = f (as[i]'(size_map .. ▸ h)) := by + ((as.map f)[i]) = f (as[i]'(size_map .. ▸ h)) := by have := map_spec as f (fun i b => b = f (as[i])) simp only [implies_true, true_implies] at this obtain ⟨eq, w⟩ := this @@ -474,10 +472,10 @@ theorem mapIdx_induction (as : Array α) (f : Fin as.size → α → β) (p : Fin as.size → β → Prop) (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) : motive as.size ∧ ∃ eq : (Array.mapIdx as f).size = as.size, - ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]'(eq ▸ h)) := by + ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) := by let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p ⟨i, h⟩ bs[i]) (hm : motive j) : let arr : Array β := Array.mapIdxM.map (m := Id) as f i j h bs - motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ (arr[i]'(eq ▸ h)) := by + motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i] := by induction i generalizing j bs with simp [mapIdxM.map] | zero => have := (Nat.zero_add _).symm.trans h @@ -497,7 +495,7 @@ theorem mapIdx_induction (as : Array α) (f : Fin as.size → α → β) theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β) (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) : ∃ eq : (Array.mapIdx as f).size = as.size, - ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]'(eq ▸ h)) := + ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) := (mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2 @[simp] theorem size_mapIdx (a : Array α) (f : Fin a.size → α → β) : (a.mapIdx f).size = a.size := @@ -506,9 +504,10 @@ theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β) @[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size := Array.size_mapIdx _ _ -@[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) (h) : +@[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) + (h : i < (mapIdx a f).size) : haveI : i < a.size := by simp_all - (a.mapIdx f)[i]'h = f ⟨i, this⟩ a[i] := + (a.mapIdx f)[i] = f ⟨i, this⟩ a[i] := (mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _ /-! ### modify -/ diff --git a/Std/Data/Array/Monadic.lean b/Std/Data/Array/Monadic.lean index b6caa4becd..65b18c88d3 100644 --- a/Std/Data/Array/Monadic.lean +++ b/Std/Data/Array/Monadic.lean @@ -34,7 +34,7 @@ theorem SatisfiesM_mapM [Monad m] [LawfulMonad m] (as : Array α) (f : α → m (p : Fin as.size → β → Prop) (hs : ∀ i, motive i.1 → SatisfiesM (p i · ∧ motive (i + 1)) (f as[i])) : SatisfiesM - (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ (arr[i]'(eq ▸ h))) + (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i]) (Array.mapM f as) := by rw [mapM_eq_foldlM] refine SatisfiesM_foldlM (m := m) (β := Array β) @@ -51,7 +51,7 @@ theorem SatisfiesM_mapM' [Monad m] [LawfulMonad m] (as : Array α) (f : α → m (p : Fin as.size → β → Prop) (hs : ∀ i, SatisfiesM (p i) (f as[i])) : SatisfiesM - (fun arr => ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ (arr[i]'(eq ▸ h))) + (fun arr => ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i]) (Array.mapM f as) := (SatisfiesM_mapM _ _ (fun _ => True) trivial _ (fun _ h => (hs _).imp (⟨·, h⟩))).imp (·.2) @@ -130,11 +130,11 @@ theorem SatisfiesM_mapIdxM [Monad m] [LawfulMonad m] (as : Array α) (f : Fin as (p : Fin as.size → β → Prop) (hs : ∀ i, motive i.1 → SatisfiesM (p i · ∧ motive (i + 1)) (f i as[i])) : SatisfiesM - (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ (arr[i]'(eq ▸ h))) + (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i]) (Array.mapIdxM as f) := by let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p ⟨i, h⟩ bs[i]) (hm : motive j) : SatisfiesM - (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ (arr[i]'(eq ▸ h))) + (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i]) (Array.mapIdxM.map as f i j h bs) := by induction i generalizing j bs with simp [mapIdxM.map] | zero => diff --git a/Std/Data/HashMap/WF.lean b/Std/Data/HashMap/WF.lean index 025f31252b..d1a4385786 100644 --- a/Std/Data/HashMap/WF.lean +++ b/Std/Data/HashMap/WF.lean @@ -69,7 +69,7 @@ theorem reinsertAux_size [Hashable α] (data : Buckets α β) (a : α) (b : β) theorem reinsertAux_WF [BEq α] [Hashable α] {data : Buckets α β} {a : α} {b : β} (H : data.WF) (h₁ : ∀ [PartialEquivBEq α] [LawfulHashable α], haveI := mkIdx data.2 (hash a).toUSize - (data.val[this.1]'this.2).All fun x _ => ¬(a == x)) : + data.val[this.1].All fun x _ => ¬(a == x)) : (reinsertAux data a b).WF := H.update (.cons h₁) fun | _, _, .head .. => rfl diff --git a/Std/Lean/Meta/AssertHypotheses.lean b/Std/Lean/Meta/AssertHypotheses.lean index f237e09ee4..908e990486 100644 --- a/Std/Lean/Meta/AssertHypotheses.lean +++ b/Std/Lean/Meta/AssertHypotheses.lean @@ -29,7 +29,7 @@ def _root_.Lean.MVarId.assertHypotheses' (mvarId : MVarId) mvarId.modifyLCtx fun lctx => Id.run do let mut lctx := lctx for h : i in [:hs.size] do - let h := hs[i]'h.2 + let h := hs[i] if h.kind != .default then lctx := lctx.setKind fvarIds[i]! h.kind if h.binderInfo != .default then diff --git a/Std/Linter/UnnecessarySeqFocus.lean b/Std/Linter/UnnecessarySeqFocus.lean index 9070d3c816..29ee10d210 100644 --- a/Std/Linter/UnnecessarySeqFocus.lean +++ b/Std/Linter/UnnecessarySeqFocus.lean @@ -106,7 +106,7 @@ def getPath : Info → PersistentArray InfoTree → List ((n : Nat) × Fin n) | i, _, [] => some i | _, c, ⟨n, i, h⟩::ns => if e : c.size = n then - if let .node i c' := c[i]'(e ▸ h) then getPath i c' ns else none + if let .node i c' := c[i] then getPath i c' ns else none else none mutual From cb411baa424e7938b3b8feb7d9453c0fbd3d0f11 Mon Sep 17 00:00:00 2001 From: Seppel3210 <34406239+Seppel3210@users.noreply.github.com> Date: Fri, 29 Mar 2024 23:19:27 +0100 Subject: [PATCH 10/27] =?UTF-8?q?feat:=20add=20Decidable=20instance=20for?= =?UTF-8?q?=20List.Forall=E2=82=82=20(#687)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Std/Data/List/Basic.lean | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/Std/Data/List/Basic.lean b/Std/Data/List/Basic.lean index 7774294973..c29dc224e9 100644 --- a/Std/Data/List/Basic.lean +++ b/Std/Data/List/Basic.lean @@ -823,6 +823,35 @@ inductive Forall₂ (R : α → β → Prop) : List α → List β → Prop attribute [simp] Forall₂.nil +@[simp] theorem forall₂_cons {R : α → β → Prop} {a b l₁ l₂} : + Forall₂ R (a :: l₁) (b :: l₂) ↔ R a b ∧ Forall₂ R l₁ l₂ := + ⟨fun | .cons h tail => ⟨h, tail⟩, fun ⟨head, tail⟩ => .cons head tail⟩ + +/-- +Check for all elements `a`, `b`, where `a` and `b` are the nth element of the first and second +List respectively, that `r a b = true`. +-/ +def all₂ (r : α → β → Bool) : List α → List β → Bool + | [], [] => true + | a::as, b::bs => + if r a b then + all₂ r as bs + else false + | _, _ => false + +@[simp] theorem all₂_eq_true {r : α → β → Bool} : + ∀ l₁ l₂, all₂ r l₁ l₂ ↔ Forall₂ (r · ·) l₁ l₂ + | [], [] => by simp [all₂] + | a::as, b::bs => by + by_cases h : r a b + <;> simp [all₂, h, all₂_eq_true, forall₂_cons] + | _::_, [] | [], _::_ => by + simp [all₂] + exact nofun + +instance {R : α → β → Prop} [∀ a b, Decidable (R a b)] : ∀ l₁ l₂, Decidable (Forall₂ R l₁ l₂) := + fun l₁ l₂ => decidable_of_iff (all₂ (R · ·) l₁ l₂) (by simp [all₂_eq_true]) + end Forall₂ /-- From aec0741522b0a23f1ed7051a936cf43f76a907ae Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Sat, 30 Mar 2024 09:13:18 +0000 Subject: [PATCH 11/27] chore: bump to nightly-2024-03-30 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 7268b6fc68..ba450671c4 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-03-29 +leanprover/lean4:nightly-2024-03-30 From 06f06f9267718090265dd1e38c0bbe0300dc2db5 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Mon, 1 Apr 2024 09:16:56 +0000 Subject: [PATCH 12/27] chore: bump to nightly-2024-04-01 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index ba450671c4..4610193327 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-03-30 +leanprover/lean4:nightly-2024-04-01 From 9d227cb9d5b7df6c061c15b6cf05a00654bcb8b4 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Tue, 2 Apr 2024 04:24:45 +0900 Subject: [PATCH 13/27] chore: golf proof (#718) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: François G. Dorais --- Std/Data/List/Lemmas.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean index 6021e8bf9d..7a03e8ee6e 100644 --- a/Std/Data/List/Lemmas.lean +++ b/Std/Data/List/Lemmas.lean @@ -646,7 +646,6 @@ theorem head!_of_head? [Inhabited α] : ∀ {l : List α}, head? l = some a → | _a::_l, rfl => rfl theorem head?_eq_head : ∀ l h, @head? α l = some (head l h) - | [], h => nomatch h rfl | _::_, _ => rfl /-! ### tail -/ From 09ff09778635a4a545717d044b9b1353e401a6d1 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Tue, 2 Apr 2024 05:08:29 +0900 Subject: [PATCH 14/27] doc: add section title (#720) --- Std/Data/List/Lemmas.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean index 7a03e8ee6e..cdb3566899 100644 --- a/Std/Data/List/Lemmas.lean +++ b/Std/Data/List/Lemmas.lean @@ -2332,6 +2332,8 @@ theorem IsInfix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ 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) From 67c40f89be2c17c6f4b0b6056d2de8591c0f92d3 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 2 Apr 2024 07:45:32 +1100 Subject: [PATCH 15/27] chore: remove triv tactic (#712) --- Std/Tactic/Init.lean | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/Std/Tactic/Init.lean b/Std/Tactic/Init.lean index 326d11aab5..19593a2e40 100644 --- a/Std/Tactic/Init.lean +++ b/Std/Tactic/Init.lean @@ -80,12 +80,8 @@ example (h : ∀ x : Nat, x = x → True) : True := by elab "eapply " e:term : tactic => evalApplyLikeTactic (·.apply (cfg := {newGoals := .nonDependentOnly})) e -/-- -Tries to solve the goal using a canonical proof of `True`, or the `rfl` tactic. -Unlike `trivial` or `trivial'`, does not use the `contradiction` tactic. --/ -macro (name := triv) "triv" : tactic => - `(tactic| first | exact trivial | rfl | fail "triv tactic failed") +/-- Deprecated variant of `trivial`. -/ +elab (name := triv) "triv" : tactic => throwError "`triv` has been removed; use `trivial` instead" /-- `conv` tactic to close a goal using an equality theorem. -/ macro (name := Conv.exact) "exact " t:term : conv => `(conv| tactic => exact $t) From d4161291e2a4c1c92d710bf670570aa79bf0d6ef Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Mon, 1 Apr 2024 16:00:02 -0700 Subject: [PATCH 16/27] chore: use BEq instead of DecidableEq in List additional ops (#716) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: François G. Dorais --- Std/Data/List/Basic.lean | 14 +++++++------- Std/Data/List/Lemmas.lean | 32 ++++++++++++++++++-------------- Std/Data/List/Perm.lean | 33 ++++++++++++--------------------- 3 files changed, 37 insertions(+), 42 deletions(-) diff --git a/Std/Data/List/Basic.lean b/Std/Data/List/Basic.lean index c29dc224e9..74eeb5e87d 100644 --- a/Std/Data/List/Basic.lean +++ b/Std/Data/List/Basic.lean @@ -391,17 +391,17 @@ Constructs the union of two lists, by inserting the elements of `l₁` in revers As a result, `l₂` will always be a suffix, but only the last occurrence of each element in `l₁` will be retained (but order will otherwise be preserved). -/ -@[inline] protected def union [DecidableEq α] (l₁ l₂ : List α) : List α := foldr .insert l₂ l₁ +@[inline] protected def union [BEq α] (l₁ l₂ : List α) : List α := foldr .insert l₂ l₁ -instance [DecidableEq α] : Union (List α) := ⟨List.union⟩ +instance [BEq α] : Union (List α) := ⟨List.union⟩ /-- Constructs the intersection of two lists, by filtering the elements of `l₁` that are in `l₂`. Unlike `bagInter` this does not preserve multiplicity: `[1, 1].inter [1]` is `[1, 1]`. -/ -@[inline] protected def inter [DecidableEq α] (l₁ l₂ : List α) : List α := filter (· ∈ l₂) l₁ +@[inline] protected def inter [BEq α] (l₁ l₂ : List α) : List α := filter (elem · l₂) l₁ -instance [DecidableEq α] : Inter (List α) := ⟨List.inter⟩ +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 @@ -415,11 +415,11 @@ inductive Sublist {α} : List α → List α → Prop @[inherit_doc] scoped infixl:50 " <+ " => Sublist /-- True if the first list is a potentially non-contiguous sub-sequence of the second list. -/ -def isSublist [DecidableEq α] : List α → List α → Bool +def isSublist [BEq α] : List α → List α → Bool | [], _ => true | _, [] => false | l₁@(hd₁::tl₁), hd₂::tl₂ => - if hd₁ = hd₂ + if hd₁ == hd₂ then tl₁.isSublist tl₂ else l₁.isSublist tl₂ @@ -1129,7 +1129,7 @@ instance nodupDecidable [DecidableEq α] : ∀ l : List α, Decidable (Nodup l) Defined as `pwFilter (≠)`. eraseDup [1, 0, 2, 2, 1] = [0, 2, 1] -/ -@[inline] def eraseDup [DecidableEq α] : List α → List α := pwFilter (· ≠ ·) +@[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`. -/ diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean index cdb3566899..fd749e4554 100644 --- a/Std/Data/List/Lemmas.lean +++ b/Std/Data/List/Lemmas.lean @@ -94,8 +94,11 @@ theorem append_of_mem {a : α} {l : List α} : a ∈ l → ∃ s t : List α, l | .head l => ⟨[], l, rfl⟩ | .tail b h => let ⟨s, t, h'⟩ := append_of_mem h; ⟨b::s, t, by rw [h', cons_append]⟩ -@[simp] theorem elem_iff {_ : DecidableEq α} {a : α} {as : List α} : - elem a as ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩ +theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {as : List α} : + elem a as = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩ + +@[simp] theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) : + elem a as = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff] theorem mem_of_ne_of_mem {a y : α} {l : List α} (h₁ : a ≠ y) (h₂ : a ∈ y :: l) : a ∈ l := Or.elim (mem_cons.mp h₂) (absurd · h₁) (·) @@ -619,13 +622,14 @@ theorem Sublist.eq_of_length_le (s : l₁ <+ l₂) (h : length l₂ ≤ length l | refl => apply Sublist.refl | step => simp [*, replicate, Sublist.cons] -theorem isSublist_iff_sublist [DecidableEq α] {l₁ l₂ : List α} : l₁.isSublist l₂ ↔ l₁ <+ l₂ := by +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 [h_eq] + simp only [beq_iff_eq, h_eq] constructor · intro h_sub apply Sublist.cons @@ -1369,13 +1373,13 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (! /-! ### insert -/ section insert -variable [DecidableEq α] +variable [BEq α] [LawfulBEq α] @[simp] theorem insert_of_mem {l : List α} (h : a ∈ l) : l.insert a = l := by - simp only [List.insert, elem_iff, if_pos h] + simp [List.insert, h] @[simp] theorem insert_of_not_mem {l : List α} (h : a ∉ l) : l.insert a = a :: l := by - simp only [List.insert, elem_iff, if_neg h] + simp [List.insert, h] @[simp] theorem mem_insert_iff {l : List α} : a ∈ l.insert b ↔ a = b ∨ a ∈ l := by if h : b ∈ l then @@ -2001,25 +2005,25 @@ theorem foldr_hom (f : β₁ → β₂) (g₁ : α → β₁ → β₁) (g₂ : section union -variable [DecidableEq α] +variable [BEq α] -theorem union_def [DecidableEq α] (l₁ l₂ : List α) : l₁ ∪ l₂ = foldr .insert l₂ l₁ := rfl +theorem union_def [BEq α] (l₁ l₂ : List α) : l₁ ∪ l₂ = foldr .insert l₂ l₁ := rfl @[simp] theorem nil_union (l : List α) : nil ∪ l = l := by simp [List.union_def, foldr] @[simp] theorem cons_union (a : α) (l₁ l₂ : List α) : (a :: l₁) ∪ l₂ = (l₁ ∪ l₂).insert a := by simp [List.union_def, foldr] -@[simp] theorem mem_union_iff {_ : DecidableEq α} {x : α} {l₁ l₂ : List α} : +@[simp] theorem mem_union_iff [LawfulBEq α] {x : α} {l₁ l₂ : List α} : x ∈ l₁ ∪ l₂ ↔ x ∈ l₁ ∨ x ∈ l₂ := by induction l₁ <;> simp [*, or_assoc] end union /-! ### inter -/ -theorem inter_def [DecidableEq α] (l₁ l₂ : List α) : l₁ ∩ l₂ = filter (· ∈ l₂) l₁ := rfl +theorem inter_def [BEq α] (l₁ l₂ : List α) : l₁ ∩ l₂ = filter (elem · l₂) l₁ := rfl -@[simp] theorem mem_inter_iff {_ : DecidableEq α} {x : α} {l₁ l₂ : List α} : +@[simp] theorem mem_inter_iff [BEq α] [LawfulBEq α] {x : α} {l₁ l₂ : List α} : x ∈ l₁ ∩ l₂ ↔ x ∈ l₁ ∧ x ∈ l₂ := by cases l₁ <;> simp [List.inter_def, mem_filter] @@ -2065,8 +2069,8 @@ theorem forIn_eq_bindList [Monad m] [LawfulMonad m] /-! ### diff -/ section Diff --- TODO: theorems about `BEq` -variable [DecidableEq α] +variable [BEq α] +variable [LawfulBEq α] @[simp] theorem diff_nil (l : List α) : l.diff [] = l := rfl diff --git a/Std/Data/List/Perm.lean b/Std/Data/List/Perm.lean index ec36d6b15c..15e11373cb 100644 --- a/Std/Data/List/Perm.lean +++ b/Std/Data/List/Perm.lean @@ -476,13 +476,10 @@ theorem Perm.diff_right {l₁ l₂ : List α} (t : List α) (h : l₁ ~ l₂) : induction t generalizing l₁ l₂ h with simp only [List.diff] | nil => exact h | cons x t ih => - split <;> rename_i hx - · simp [elem_eq_true_of_mem (h.subset (mem_of_elem_eq_true hx))] - exact ih (h.erase _) - · have : ¬elem x l₂ = true := fun contra => - hx <| elem_eq_true_of_mem <| h.symm.subset <| mem_of_elem_eq_true contra - simp [this] - exact ih h + simp only [elem_eq_mem, decide_eq_true_eq, Perm.mem_iff h] + split + · exact ih (h.erase _) + · exact ih h theorem Perm.diff_left (l : List α) {t₁ t₂ : List α} (h : t₁ ~ t₂) : l.diff t₁ = l.diff t₂ := by induction h generalizing l with try simp [List.diff] @@ -500,21 +497,15 @@ theorem Perm.diff {l₁ l₂ t₁ t₂ : List α} (hl : l₁ ~ l₂) (ht : t₁ theorem Subperm.diff_right {l₁ l₂ : List α} (h : l₁ <+~ l₂) (t : List α) : l₁.diff t <+~ l₂.diff t := by - induction t generalizing l₁ l₂ h with - | nil => simp only [List.diff]; exact h + induction t generalizing l₁ l₂ h with simp [List.diff, elem_eq_mem, *] | cons x t ih => - simp only [List.diff]; split <;> rename_i hx1 - · have : elem x l₂ = true := by - apply elem_eq_true_of_mem - apply h.subset (mem_of_elem_eq_true hx1) - simp [this] - apply ih - apply h.erase - · split <;> rename_i hx2 - · apply ih - have := h.erase x - simpa [erase_of_not_mem (hx1 ∘ elem_eq_true_of_mem)] using this - · apply ih h + split <;> rename_i hx1 + · simp [h.subset hx1] + exact ih (h.erase _) + · split + · rw [← erase_of_not_mem hx1] + exact ih (h.erase _) + · exact ih h theorem erase_cons_subperm_cons_erase (a b : α) (l : List α) : (a :: l).erase b <+~ a :: l.erase b := by From fac121c5b5b97f61c0bea495105e3da41eebd8a4 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Tue, 2 Apr 2024 09:15:46 +0000 Subject: [PATCH 17/27] chore: bump to nightly-2024-04-02 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 4610193327..39301b0434 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-04-01 +leanprover/lean4:nightly-2024-04-02 From 0af134abc3d7433de13467d9dc4281e155c1fbfd Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 2 Apr 2024 20:25:54 +1100 Subject: [PATCH 18/27] fixes --- Std/Lean/PersistentHashMap.lean | 6 ------ Std/Tactic/SqueezeScope.lean | 2 +- 2 files changed, 1 insertion(+), 7 deletions(-) diff --git a/Std/Lean/PersistentHashMap.lean b/Std/Lean/PersistentHashMap.lean index 4122f193b4..5054e15758 100644 --- a/Std/Lean/PersistentHashMap.lean +++ b/Std/Lean/PersistentHashMap.lean @@ -19,12 +19,6 @@ def insert' (m : PersistentHashMap α β) (a : α) (b : β) : PersistentHashMap let m := m.insert a b (m, m.size == oldSize) -/-- -Turns a `PersistentHashMap` into an array of key-value pairs. --/ -def toArray (m : PersistentHashMap α β) : Array (α × β) := - m.foldl (init := Array.mkEmpty m.size) fun xs k v => xs.push (k, v) - /-- Builds a `PersistentHashMap` from a list of key-value pairs. Values of duplicated keys are replaced by their respective last occurrences. diff --git a/Std/Tactic/SqueezeScope.lean b/Std/Tactic/SqueezeScope.lean index 39fad08cfc..cfb0476a57 100644 --- a/Std/Tactic/SqueezeScope.lean +++ b/Std/Tactic/SqueezeScope.lean @@ -85,7 +85,7 @@ elab_rules : tactic throw e if let some new := new then for (_, stx, usedSimps) in new do - let usedSimps := usedSimps.foldl (fun s usedSimps => usedSimps.fold .insert s) {} + let usedSimps := usedSimps.foldl (fun s usedSimps => usedSimps.foldl .insert s) {} let stx' ← mkSimpCallStx stx usedSimps TryThis.addSuggestion stx[0] stx' (origSpan? := stx) From 32983874c1b897d78f20d620fe92fc8fd3f06c3a Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 3 Apr 2024 10:07:02 +0200 Subject: [PATCH 19/27] chore: bump toolchain to v4.7.0 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index e35881ce7c..9ad304042c 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.7.0-rc2 +leanprover/lean4:v4.7.0 From 8ac01e7a007d637647af9350b39f6ba6b8cdb2bf Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Wed, 3 Apr 2024 09:15:52 +0000 Subject: [PATCH 20/27] chore: bump to nightly-2024-04-03 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 39301b0434..430ebaa8ea 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-04-02 +leanprover/lean4:nightly-2024-04-03 From e0eb3090ec2e5044c92e9bba9c269c91375f8d5e Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Thu, 4 Apr 2024 09:15:41 +0000 Subject: [PATCH 21/27] chore: bump to nightly-2024-04-04 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 430ebaa8ea..a6455ebdf6 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-04-03 +leanprover/lean4:nightly-2024-04-04 From 4d33b75d6944068d84f27cd43942deb75471724a Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Fri, 5 Apr 2024 09:14:50 +0000 Subject: [PATCH 22/27] chore: bump to nightly-2024-04-05 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index a6455ebdf6..7db3fefa0f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-04-04 +leanprover/lean4:nightly-2024-04-05 From 956e5c6c4f7b43f6468d90374dede5cf8fc89387 Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Fri, 29 Mar 2024 14:51:55 -0700 Subject: [PATCH 23/27] wip: list migration --- Std/Data/List/Count.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Std/Data/List/Count.lean b/Std/Data/List/Count.lean index 4458c457dc..6611d032f6 100644 --- a/Std/Data/List/Count.lean +++ b/Std/Data/List/Count.lean @@ -116,7 +116,6 @@ theorem countP_mono_left (h : ∀ x ∈ l, p x → q x) : countP p l ≤ countP apply Nat.le_trans ?_ (Nat.le_add_right _ _) apply ihl hl . simp [ha h] - apply Nat.succ_le_succ apply ihl hl theorem countP_congr (h : ∀ x ∈ l, p x ↔ q x) : countP p l = countP q l := From f47b0fbad62f1ffeb1f39bb85cbe4d763e86d7fd Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Sun, 7 Apr 2024 09:14:32 +0000 Subject: [PATCH 24/27] chore: bump to nightly-2024-04-07 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 7db3fefa0f..be51c72f93 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-04-05 +leanprover/lean4:nightly-2024-04-07 From 7514475571b81a3957e06555b968a099e658ec0d Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Mon, 8 Apr 2024 09:16:19 +0000 Subject: [PATCH 25/27] chore: bump to nightly-2024-04-08 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index be51c72f93..518ef00b94 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-04-07 +leanprover/lean4:nightly-2024-04-08 From 324d76c9d226ae84d37a66ad203dcd3bf417dc84 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Tue, 9 Apr 2024 09:16:00 +0000 Subject: [PATCH 26/27] chore: bump to nightly-2024-04-09 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 518ef00b94..16b2110185 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-04-08 +leanprover/lean4:nightly-2024-04-09 From 1352583e15fe7a6480eff3b856c1628064d3a453 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Thu, 11 Apr 2024 09:16:05 +0000 Subject: [PATCH 27/27] chore: bump to nightly-2024-04-11 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 16b2110185..ebbf7a5930 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-04-09 +leanprover/lean4:nightly-2024-04-11