From 83ad82162fe18b49d87f31139c7a8684e0a284b3 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 29 Jul 2024 09:23:59 +1000 Subject: [PATCH] feat: upstream more List lemmas (#4856) --- src/Init/Core.lean | 1 + src/Init/Data.lean | 1 + src/Init/Data/List.lean | 2 + src/Init/Data/List/Attach.lean | 153 +++++ src/Init/Data/List/Basic.lean | 6 +- src/Init/Data/List/Control.lean | 2 + src/Init/Data/List/Lemmas.lean | 725 +++++++++++++++++++- src/Init/Data/List/Nat.lean | 93 +++ src/Init/Data/List/Range.lean | 387 +++++++++++ src/Init/Data/List/TakeDrop.lean | 126 ++-- src/Init/Data/Nat/Basic.lean | 6 +- src/Init/Data/Nat/Bitwise/Lemmas.lean | 4 +- src/Init/Data/Nat/Lemmas.lean | 17 +- src/Init/Data/Subtype.lean | 27 + tests/lean/run/1017.lean | 6 +- tests/lean/run/binop_binrel_perf_issue.lean | 3 - tests/lean/run/issue3175.lean | 4 +- tests/lean/run/simpArith1.lean | 10 - 18 files changed, 1441 insertions(+), 132 deletions(-) create mode 100644 src/Init/Data/List/Nat.lean create mode 100644 src/Init/Data/List/Range.lean create mode 100644 src/Init/Data/Subtype.lean diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 1a3b97213b39..9fc9cb01d870 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -1107,6 +1107,7 @@ inductive Relation.TransGen {α : Sort u} (r : α → α → Prop) : α → α /-! # Subtype -/ namespace Subtype + theorem existsOfSubtype {α : Type u} {p : α → Prop} : { x // p x } → Exists (fun x => p x) | ⟨a, h⟩ => ⟨a, h⟩ diff --git a/src/Init/Data.lean b/src/Init/Data.lean index 2f1a41173e7f..91938d7707e1 100644 --- a/src/Init/Data.lean +++ b/src/Init/Data.lean @@ -36,3 +36,4 @@ import Init.Data.Channel import Init.Data.Cast import Init.Data.Sum import Init.Data.BEq +import Init.Data.Subtype diff --git a/src/Init/Data/List.lean b/src/Init/Data/List.lean index e24079350935..6652b1a04cf8 100644 --- a/src/Init/Data/List.lean +++ b/src/Init/Data/List.lean @@ -12,3 +12,5 @@ import Init.Data.List.Attach import Init.Data.List.Impl import Init.Data.List.TakeDrop import Init.Data.List.Notation +import Init.Data.List.Range +import Init.Data.List.Nat diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean index 6e813182cc86..f4c075b7b8fe 100644 --- a/src/Init/Data/List/Attach.lean +++ b/src/Init/Data/List/Attach.lean @@ -5,6 +5,7 @@ Authors: Mario Carneiro -/ prelude import Init.Data.List.Lemmas +import Init.Data.Subtype namespace List @@ -44,3 +45,155 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep | nil, hL' => rfl | cons _ L', hL' => congrArg _ <| go L' fun _ hx => hL' (.tail _ hx) exact go L h' + +@[simp] theorem attach_nil : ([] : List α).attach = [] := rfl + +@[simp] +theorem pmap_eq_map (p : α → Prop) (f : α → β) (l : List α) (H) : + @pmap _ _ p (fun a _ => f a) l H = map f l := by + induction l + · rfl + · simp only [*, pmap, map] + +theorem pmap_congr {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (l : List α) {H₁ H₂} + (h : ∀ a ∈ l, ∀ (h₁ h₂), f a h₁ = g a h₂) : pmap f l H₁ = pmap g l H₂ := by + induction l with + | nil => rfl + | cons x l ih => rw [pmap, pmap, h _ (mem_cons_self _ _), ih fun a ha => h a (mem_cons_of_mem _ ha)] + +theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (l H) : + map g (pmap f l H) = pmap (fun a h => g (f a h)) l H := by + induction l + · rfl + · simp only [*, pmap, map] + +theorem pmap_map {p : β → Prop} (g : ∀ b, p b → γ) (f : α → β) (l H) : + pmap g (map f l) H = pmap (fun a h => g (f a) h) l fun a h => H _ (mem_map_of_mem _ h) := by + induction l + · rfl + · simp only [*, pmap, map] + +theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l H) : + pmap f l H = l.attach.map fun x => f x.1 (H _ x.2) := by + rw [attach, attachWith, map_pmap]; exact pmap_congr l fun _ _ _ _ => rfl + +theorem attach_map_coe (l : List α) (f : α → β) : + (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by + rw [attach, attachWith, map_pmap]; exact pmap_eq_map _ _ _ _ + +theorem attach_map_val (l : List α) (f : α → β) : (l.attach.map fun i => f i.val) = l.map f := + attach_map_coe _ _ + +@[simp] +theorem attach_map_subtype_val (l : List α) : l.attach.map Subtype.val = l := + (attach_map_coe _ _).trans l.map_id + +theorem countP_attach (l : List α) (p : α → Bool) : l.attach.countP (fun a : {x // x ∈ l} => p a) = l.countP p := by + simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attach_map_subtype_val] + +@[simp] +theorem count_attach [DecidableEq α] (l : List α) (a : {x // x ∈ l}) : l.attach.count a = l.count ↑a := + Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attach _ _ + +@[simp] +theorem mem_attach (l : List α) : ∀ x, x ∈ l.attach + | ⟨a, h⟩ => by + have := mem_map.1 (by rw [attach_map_subtype_val] <;> exact h) + rcases this with ⟨⟨_, _⟩, m, rfl⟩ + exact m + +@[simp] +theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H b} : + b ∈ pmap f l H ↔ ∃ (a : _) (h : a ∈ l), f a (H a h) = b := by + simp only [pmap_eq_map_attach, mem_map, mem_attach, true_and, Subtype.exists, eq_comm] + +@[simp] +theorem length_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H} : length (pmap f l H) = length l := by + induction l + · rfl + · simp only [*, pmap, length] + +@[simp] +theorem length_attach (L : List α) : L.attach.length = L.length := + length_pmap + +@[simp] +theorem pmap_eq_nil {p : α → Prop} {f : ∀ a, p a → β} {l H} : pmap f l H = [] ↔ l = [] := by + rw [← length_eq_zero, length_pmap, length_eq_zero] + +@[simp] +theorem attach_eq_nil (l : List α) : l.attach = [] ↔ l = [] := + pmap_eq_nil + +theorem getLast_pmap (p : α → Prop) (f : ∀ a, p a → β) (l : List α) + (hl₁ : ∀ a ∈ l, p a) (hl₂ : l ≠ []) : + (l.pmap f hl₁).getLast (mt List.pmap_eq_nil.1 hl₂) = + f (l.getLast hl₂) (hl₁ _ (List.getLast_mem hl₂)) := by + induction l with + | nil => apply (hl₂ rfl).elim + | cons l_hd l_tl l_ih => + by_cases hl_tl : l_tl = [] + · simp [hl_tl] + · simp only [pmap] + rw [getLast_cons, l_ih _ hl_tl] + simp only [getLast_cons hl_tl] + +theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) (n : Nat) : + (pmap f l h)[n]? = Option.pmap f l[n]? fun x H => h x (getElem?_mem H) := by + induction l generalizing n with + | nil => simp + | cons hd tl hl => + rcases n with ⟨n⟩ + · simp only [Option.pmap] + split <;> simp_all + · simp only [hl, pmap, Option.pmap, getElem?_cons_succ] + split <;> rename_i h₁ _ <;> split <;> rename_i h₂ _ + · simp_all + · simp at h₂ + simp_all + · simp_all + · simp_all + +theorem get?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) (n : Nat) : + get? (pmap f l h) n = Option.pmap f (get? l n) fun x H => h x (get?_mem H) := by + simp only [get?_eq_getElem?] + simp [getElem?_pmap, h] + +theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) {n : Nat} + (hn : n < (pmap f l h).length) : + (pmap f l h)[n] = + f (l[n]'(@length_pmap _ _ p f l h ▸ hn)) + (h _ (getElem_mem l n (@length_pmap _ _ p f l h ▸ hn))) := by + induction l generalizing n with + | nil => + simp only [length, pmap] at hn + exact absurd hn (Nat.not_lt_of_le n.zero_le) + | cons hd tl hl => + cases n + · simp + · simp [hl] + +theorem get_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) {n : Nat} + (hn : n < (pmap f l h).length) : + get (pmap f l h) ⟨n, hn⟩ = + f (get l ⟨n, @length_pmap _ _ p f l h ▸ hn⟩) + (h _ (get_mem l n (@length_pmap _ _ p f l h ▸ hn))) := by + simp only [get_eq_getElem] + simp [getElem_pmap] + +theorem pmap_append {p : ι → Prop} (f : ∀ a : ι, p a → α) (l₁ l₂ : List ι) + (h : ∀ a ∈ l₁ ++ l₂, p a) : + (l₁ ++ l₂).pmap f h = + (l₁.pmap f fun a ha => h a (mem_append_left l₂ ha)) ++ + l₂.pmap f fun a ha => h a (mem_append_right l₁ ha) := by + induction l₁ with + | nil => rfl + | cons _ _ ih => + dsimp only [pmap, cons_append] + rw [ih] + +theorem pmap_append' {p : α → Prop} (f : ∀ a : α, p a → β) (l₁ l₂ : List α) + (h₁ : ∀ a ∈ l₁, p a) (h₂ : ∀ a ∈ l₂, p a) : + ((l₁ ++ l₂).pmap f fun a ha => (List.mem_append.1 ha).elim (h₁ a) (h₂ a)) = + l₁.pmap f h₁ ++ l₂.pmap f h₂ := + pmap_append f l₁ l₂ _ diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index ba2985afdab3..98bb6f30d79a 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -611,7 +611,7 @@ If `l` is initially larger than `n`, just return `l`. -/ def rightpad (n : Nat) (a : α) (l : List α) : List α := l ++ replicate (n - length l) a -/-! ### reduceOption-/ +/-! ### reduceOption -/ /-- Drop `none`s from a list, and replace each remaining `some a` with `a`. -/ @[inline] def reduceOption {α} : List (Option α) → List α := @@ -1168,11 +1168,15 @@ theorem findSome?_cons {f : α → Option β} : | [], n => n | a :: l, n => bif p a then n else go l (n + 1) +@[simp] theorem findIdx_nil {α : Type _} (p : α → Bool) : [].findIdx p = 0 := rfl + /-! ### indexOf -/ /-- 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) +@[simp] theorem indexOf_nil [BEq α] : ([] : List α).indexOf x = 0 := rfl + /-! ### findIdx? -/ /-- Return the index of the first occurrence of an element satisfying `p`. -/ diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean index 69cbf2661503..7e6dc918c668 100644 --- a/src/Init/Data/List/Control.lean +++ b/src/Init/Data/List/Control.lean @@ -227,6 +227,8 @@ def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f instance : ForIn m (List α) α where forIn := List.forIn +@[simp] theorem forIn_eq_forIn [Monad m] : @List.forIn α β m _ = forIn := rfl + @[simp] theorem forIn_nil [Monad m] (f : α → β → m (ForInStep β)) (b : β) : forIn [] b f = pure b := rfl diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 2efb5b4c8e52..814e92395551 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -243,6 +243,14 @@ theorem getElem?_eq_some {l : List α} : l[n]? = some a ↔ ∃ h : n < l.length theorem getElem?_eq_none (h : length l ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h +theorem getElem_eq_iff {l : List α} {n : Nat} {h : n < l.length} : l[n] = x ↔ l[n]? = some x := by + simp only [getElem?_eq_some] + exact ⟨fun w => ⟨h, w⟩, fun h => h.2⟩ + +theorem getElem_eq_getElem? (l : List α) (i : Nat) (h : i < l.length) : + l[i] = l[i]?.get (by simp [getElem?_eq_getElem, h]) := by + simp [getElem_eq_iff] + @[simp] theorem getElem?_nil {n : Nat} : ([] : List α)[n]? = none := rfl theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by simp @@ -517,10 +525,17 @@ theorem get_set_eq {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) (l.set i a).get ⟨i, h⟩ = a := by simp -@[simp] theorem getElem?_set_eq {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) : +@[simp] theorem getElem?_set_eq {l : List α} {i : Nat} {a : α} (h : i < l.length) : (l.set i a)[i]? = some a := by simp_all [getElem?_eq_some] +@[simp] +theorem getElem?_set_eq' {l : List α} {i : Nat} {a : α} : (set l i a)[i]? = (fun _ => a) <$> l[i]? := by + by_cases h : i < l.length + · simp [getElem?_set_eq h, getElem?_eq_getElem h] + · simp only [Nat.not_lt] at h + simpa [getElem?_eq_none_iff.2 h] + @[simp] theorem getElem_set_ne {l : List α} {i j : Nat} (h : i ≠ j) {a : α} (hj : j < (l.set i a).length) : (l.set i a)[j] = l[j]'(by simp at hj; exact hj) := @@ -569,6 +584,12 @@ theorem getElem?_set {l : List α} {i j : Nat} {a : α} : else simp [h] +theorem getElem?_set' {l : List α} {i j : Nat} {a : α} : + (set l i a)[j]? = if i = j then (fun _ => a) <$> l[j]? else l[j]? := by + by_cases i = j + · simp only [getElem?_set_eq', Option.map_eq_map, ↓reduceIte, *] + · simp only [ne_eq, not_false_eq_true, getElem?_set_ne, ↓reduceIte, *] + theorem set_eq_of_length_le {l : List α} {n : Nat} (h : l.length ≤ n) {a : α} : l.set n a = l := by induction l generalizing n with @@ -703,6 +724,14 @@ theorem foldr_map' {α β : Type u} (g : α → β) (f : α → α → α) (f' : · simp · simp [*, h] +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] + /-! ### getLast -/ theorem getLast_eq_getElem : ∀ (l : List α) (h : l ≠ []), @@ -722,8 +751,8 @@ theorem getLast_eq_get (l : List α) (h : l ≠ []) : | a :: l => exact Nat.le_refl _⟩ := by simp [getLast_eq_getElem] -theorem getLast_cons' {a : α} {l : List α} : ∀ (h₁ : a :: l ≠ nil) (h₂ : l ≠ nil), - getLast (a :: l) h₁ = getLast l h₂ := by +theorem getLast_cons {a : α} {l : List α} : ∀ (h : l ≠ nil), + getLast (a :: l) (cons_ne_nil a l) = getLast l h := by induction l <;> intros; {contradiction}; rfl theorem getLast_eq_getLastD (a l h) : @getLast α (a::l) h = getLastD l a := by @@ -808,12 +837,20 @@ theorem head?_eq_getElem? : ∀ l : List α, head? l = l[0]? @[simp] theorem headD_eq_head?_getD {l : List α} : headD l a = (head? l).getD a := by cases l <;> simp [headD] -/-! ### tail -/ +/-! ### tailD -/ /-- `simp` unfolds `tailD` in terms of `tail?` and `Option.getD`. -/ @[simp] theorem tailD_eq_tail? (l l' : List α) : tailD l l' = (tail? l).getD l' := by cases l <;> rfl +/-! ### tail -/ + +@[simp] theorem length_tail (l : List α) : length (tail l) = length l - 1 := by cases l <;> rfl + +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] + /-! ## Basic operations -/ /-! ### map -/ @@ -1189,10 +1226,10 @@ theorem forall_none_of_filterMap_eq_nil (h : filterMap f xs = []) : ∀ x ∈ xs | cons y ys ih => simp only [filterMap_cons] at h split at h - . cases hx with + · cases hx with | head => assumption | tail _ hmem => exact ih h hmem - . contradiction + · contradiction theorem filterMap_eq_nil {l} : filterMap f l = [] ↔ ∀ a ∈ l, f a = none := by constructor @@ -1319,7 +1356,7 @@ theorem append_left_inj {s₁ s₂ : List α} (t) : s₁ ++ t = s₂ ++ t ↔ s @[simp] theorem getLast_concat {a : α} : ∀ (l : List α), getLast (l ++ [a]) (by simp) = a | [] => rfl | a::t => by - simp [getLast_cons' _ fun H => cons_ne_nil _ _ (append_eq_nil.1 H).2, getLast_concat t] + simp [getLast_cons _, getLast_concat t] theorem getElem_append : ∀ {l₁ l₂ : List α} (n : Nat) (h : n < l₁.length), (l₁ ++ l₂)[n]'(length_append .. ▸ Nat.lt_add_right _ h) = l₁[n] @@ -1930,7 +1967,7 @@ theorem reverseAux_eq (as bs : List α) : reverseAux as bs = reverse as ++ bs := simp by_cases h' : l = [] · simp_all - · rw [getLast_cons' _ h', head_append_of_ne_nil, ih] + · rw [getLast_cons, head_append_of_ne_nil, ih] simp_all theorem getLast_eq_head_reverse {l : List α} (h : l ≠ []) : @@ -1994,6 +2031,26 @@ theorem getLast?_replicate (a : α) (n : Nat) : (replicate n a).getLast? = if n @[simp] theorem getLast_replicate (w : replicate n a ≠ []) : (replicate n a).getLast w = a := by simp [getLast_eq_head_reverse] +/-! ## Additional operations -/ + +/-! ### 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 + /-! ## List membership -/ /-! ### elem / contains -/ @@ -2020,6 +2077,10 @@ Further results on `List.take` and `List.drop`, which rely on stronger automatio are given in `Init.Data.List.TakeDrop`. -/ +@[simp] +theorem drop_one : ∀ l : List α, drop 1 l = tail l + | [] | _ :: _ => rfl + @[simp] theorem take_append_drop : ∀ (n : Nat) (l : List α), take n l ++ drop n l = l | 0, _ => rfl | _+1, [] => rfl @@ -2090,6 +2151,14 @@ theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l. theorem getElem?_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1))[n]? = l[n]? := getElem?_take (Nat.lt_succ_self n) +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] + @[simp] theorem drop_eq_nil_iff_le {l : List α} {k : Nat} : l.drop k = [] ↔ l.length ≤ k := by refine' ⟨fun h => _, drop_eq_nil_of_le⟩ @@ -3208,6 +3277,9 @@ theorem drop_subset (n) (l : List α) : drop n l ⊆ l := theorem mem_of_mem_take {l : List α} (h : a ∈ l.take n) : a ∈ l := take_subset n l h +theorem mem_of_mem_drop {n} {l : List α} (h : a ∈ l.drop n) : a ∈ l := + drop_subset _ _ h + theorem IsPrefix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) : l₁.filter p <+: l₂.filter p := by obtain ⟨xs, rfl⟩ := h @@ -3914,6 +3986,16 @@ theorem Nodup.erase [BEq α] [LawfulBEq α] (a : α) : Nodup l → Nodup (l.eras end erase +/-! ### eraseIdx -/ + +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)] + /-! ### find? -/ @[simp] theorem find?_cons_of_pos (l) (h : p a) : find? p (a :: l) = some a := by @@ -4018,6 +4100,342 @@ theorem findSome?_isSome_of_sublist {l₁ l₂ : List α} (h : l₁ <+ l₂) : simp only [findSome?] split <;> simp_all +/-! ### findIdx -/ + +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, succ_inj'] + +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 [succ_inj'] + +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 + +/-! ### indexOf -/ + +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] + +/-! ### countP -/ +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 h, length] + else rw [countP_cons_of_neg p l h, ih, filter_cons_of_neg 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 only [Bool.false_eq_true, ↓reduceIte, Nat.add_zero] + apply Nat.le_trans ?_ (Nat.le_add_right _ _) + apply ihl hl + · simp only [↓reduceIte, ha h, succ_le_succ_iff] + 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 -/ + +section count + +variable [BEq α] + +@[simp] theorem count_nil (a : α) : count a [] = 0 := rfl + +theorem count_cons (a b : α) (l : List α) : + count a (b :: l) = count a l + if b == a then 1 else 0 := by + simp [count, countP_cons] + +theorem count_tail : ∀ (l : List α) (a : α) (h : l ≠ []), + l.tail.count a = l.count a - if l.head h == a then 1 else 0 + | head :: tail, a, _ => 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_self _ _).count_le _ + +theorem count_singleton (a b : α) : count a [b] = if b == a 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 _ + +variable [LawfulBEq α] + +@[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 only [count_cons, cond_eq_if, beq_iff_eq] + split <;> simp_all + +theorem count_singleton_self (a : α) : count a [a] = 1 := by simp + +theorem count_concat_self (a : α) (l : List α) : + count a (concat l a) = (count a l) + 1 := 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] + +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 b == a then n else 0 := by + split <;> (rename_i h; simp only [beq_iff_eq] at h) + · exact ‹b = a› ▸ count_replicate_self .. + · exact count_eq_zero.2 <| mt eq_of_mem_replicate (Ne.symm h) + +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 {α} [DecidableEq α] (l : List α) (a : α) : l.filter (· = a) = replicate (count a l) a := + filter_beq 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_beq 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 + 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 b == a 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 : b = a then + rw [ha, eq_comm] at hc + rw [if_pos ((beq_iff_eq _ _).2 ha), if_neg (by simpa using Ne.symm hc), Nat.add_zero, Nat.add_zero] + else + rw [if_neg (by simpa using 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 (by simp)] + +@[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 (by simpa using ab.symm), Nat.sub_zero] + +end count + /-! ### lookup -/ section lookup variable [BEq α] [LawfulBEq α] @@ -4216,6 +4634,8 @@ theorem of_mem_zip {a b} : ∀ {l₁ : List α} {l₂ : List β}, (a, b) ∈ zip · have := of_mem_zip h exact ⟨Mem.tail _ this.1, Mem.tail _ this.2⟩ +@[deprecated of_mem_zip (since := "2024-07-28")] abbrev mem_zip := @of_mem_zip + theorem map_fst_zip : ∀ (l₁ : List α) (l₂ : List β), l₁.length ≤ l₂.length → map Prod.fst (zip l₁ l₂) = l₁ | [], bs, _ => rfl @@ -4236,6 +4656,18 @@ theorem map_snd_zip : show _ :: map Prod.snd (zip as bs) = _ :: bs rw [map_snd_zip as bs h] +theorem map_prod_left_eq_zip {l : List α} (f : α → β) : + (l.map fun x => (x, f x)) = l.zip (l.map f) := by + rw [← zip_map'] + congr + exact map_id _ + +theorem map_prod_right_eq_zip {l : List α} (f : α → β) : + (l.map fun x => (f x, x)) = (l.map f).zip l := by + rw [← zip_map'] + congr + exact map_id _ + /-- See also `List.zip_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths. -/ @[simp] theorem zip_replicate' {a : α} {b : β} {n : Nat} : zip (replicate n a) (replicate n b) = replicate n (a, b) := by @@ -4245,6 +4677,26 @@ theorem map_snd_zip : /-! ### zipWith -/ +theorem zipWith_comm (f : α → β → γ) : + ∀ (la : List α) (lb : List β), zipWith f la lb = zipWith (fun b a => f a b) lb la + | [], _ => List.zipWith_nil_right.symm + | _ :: _, [] => rfl + | _ :: as, _ :: bs => congrArg _ (zipWith_comm f as bs) + +theorem zipWith_comm_of_comm (f : α → α → β) (comm : ∀ x y : α, f x y = f y x) (l l' : List α) : + zipWith f l l' = zipWith f l' l := by + rw [zipWith_comm] + simp only [comm] + +@[simp] +theorem zipWith_same (f : α → α → δ) : ∀ l : List α, zipWith f l l = l.map fun a => f a a + | [] => rfl + | _ :: xs => congrArg _ (zipWith_same f xs) + +/-- +See also `getElem?_zipWith'` for a variant +using `Option.map` and `Option.bind` rather than a `match`. +-/ theorem getElem?_zipWith {f : α → β → γ} {i : Nat} : (List.zipWith f as bs)[i]? = match as[i]?, bs[i]? with | some a, some b => some (f a b) | _, _ => none := by @@ -4256,6 +4708,32 @@ theorem getElem?_zipWith {f : α → β → γ} {i : Nat} : | nil => simp | cons b bs => cases i <;> simp_all +/-- Variant of `getElem?_zipWith` using `Option.map` and `Option.bind` rather than a `match`. -/ +theorem getElem?_zipWith' {f : α → β → γ} {i : Nat} : + (zipWith f l₁ l₂)[i]? = (l₁[i]?.map f).bind fun g => l₂[i]?.map g := by + induction l₁ generalizing l₂ i with + | nil => rw [zipWith] <;> simp + | cons head tail => + cases l₂ + · simp + · cases i <;> simp_all + +theorem getElem?_zipWith_eq_some (f : α → β → γ) (l₁ : List α) (l₂ : List β) (z : γ) (i : Nat) : + (zipWith f l₁ l₂)[i]? = some z ↔ + ∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z := by + induction l₁ generalizing l₂ i + · simp + · cases l₂ <;> cases i <;> simp_all + +theorem getElem?_zip_eq_some (l₁ : List α) (l₂ : List β) (z : α × β) (i : Nat) : + (zip l₁ l₂)[i]? = some z ↔ l₁[i]? = some z.1 ∧ l₂[i]? = some z.2 := by + cases z + rw [zip, getElem?_zipWith_eq_some]; constructor + · rintro ⟨x, y, h₀, h₁, h₂⟩ + simpa [h₀, h₁] using h₂ + · rintro ⟨h₀, h₁⟩ + exact ⟨_, _, h₀, h₁, rfl⟩ + @[deprecated getElem?_zipWith (since := "2024-06-12")] theorem get?_zipWith {f : α → β → γ} : (List.zipWith f as bs).get? i = match as.get? i, bs.get? i with @@ -4333,6 +4811,11 @@ theorem drop_zipWith : (zipWith f l l').drop n = zipWith f (l.drop n) (l'.drop n @[deprecated drop_zipWith (since := "2024-07-26")] abbrev zipWith_distrib_drop := @drop_zipWith +theorem tail_zipWith : (zipWith f l l').tail = zipWith f l.tail l'.tail := by + rw [← drop_one]; simp [drop_zipWith] + +@[deprecated tail_zipWith (since := "2024-07-28")] abbrev zipWith_distrib_tail := @tail_zipWith + theorem zipWith_append (f : α → β → γ) (l la : List α) (l' lb : List β) (h : l.length = l'.length) : zipWith f (l ++ la) (l' ++ lb) = zipWith f l l' ++ zipWith f la lb := by @@ -4422,31 +4905,44 @@ theorem map_zipWithAll {δ : Type _} (f : α → β) (g : Option γ → Option @[simp] theorem unzip_snd : (unzip l).snd = l.map Prod.snd := by induction l <;> simp_all -@[simp] theorem unzip_replicate {n : Nat} {a : α} {b : β} : - unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by - ext1 <;> simp - -/-! ## Ranges and enumeration -/ - -/-! ### enumFrom -/ +@[deprecated unzip_fst (since := "2024-07-28")] abbrev unzip_left := @unzip_fst +@[deprecated unzip_snd (since := "2024-07-28")] abbrev unzip_right := @unzip_snd -@[simp] theorem enumFrom_length : ∀ {n} {l : List α}, (enumFrom n l).length = l.length - | _, [] => rfl - | _, _ :: _ => congrArg Nat.succ enumFrom_length - -theorem map_enumFrom (f : α → β) (n : Nat) (l : List α) : - map (Prod.map id f) (enumFrom n l) = enumFrom n (map f l) := by - induction l generalizing n <;> simp_all - -/-! ### enum -/ - -@[simp] theorem enum_length : (enum l).length = l.length := - enumFrom_length +theorem unzip_eq_map : ∀ l : List (α × β), unzip l = (l.map Prod.fst, l.map Prod.snd) + | [] => rfl + | (a, b) :: l => by simp only [unzip_cons, map_cons, unzip_eq_map l] -theorem enum_cons : (a::as).enum = (0, a) :: as.enumFrom 1 := rfl +theorem zip_unzip : ∀ l : List (α × β), zip (unzip l).1 (unzip l).2 = l + | [] => rfl + | (a, b) :: l => by simp only [unzip_cons, zip_cons_cons, zip_unzip l] + +theorem unzip_zip_left : + ∀ {l₁ : List α} {l₂ : List β}, length l₁ ≤ length l₂ → (unzip (zip l₁ l₂)).1 = l₁ + | [], l₂, _ => rfl + | l₁, [], h => by rw [eq_nil_of_length_eq_zero (Nat.eq_zero_of_le_zero h)]; rfl + | a :: l₁, b :: l₂, h => by + simp only [zip_cons_cons, unzip_cons, unzip_zip_left (le_of_succ_le_succ h)] + +theorem unzip_zip_right : + ∀ {l₁ : List α} {l₂ : List β}, length l₂ ≤ length l₁ → (unzip (zip l₁ l₂)).2 = l₂ + | [], l₂, _ => by simp_all + | l₁, [], _ => by simp + | a :: l₁, b :: l₂, h => by + simp only [zip_cons_cons, unzip_cons, unzip_zip_right (le_of_succ_le_succ h)] + +theorem unzip_zip {l₁ : List α} {l₂ : List β} (h : length l₁ = length l₂) : + unzip (zip l₁ l₂) = (l₁, l₂) := by + ext + · rw [unzip_zip_left (Nat.le_of_eq h)] + · rw [unzip_zip_right (Nat.le_of_eq h.symm)] + +theorem zip_of_prod {l : List α} {l' : List β} {lp : List (α × β)} (hl : lp.map Prod.fst = l) + (hr : lp.map Prod.snd = l') : lp = l.zip l' := by + rw [← hl, ← hr, ← zip_unzip lp, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip] -theorem map_enum (f : α → β) (l : List α) : map (Prod.map id f) (enum l) = enum (map f l) := - map_enumFrom f 0 l +@[simp] theorem unzip_replicate {n : Nat} {a : α} {b : β} : + unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by + ext1 <;> simp /-! ## Minima and maxima -/ @@ -4619,4 +5115,173 @@ theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) (a::as).forM f = (f a >>= fun _ => as.forM f : m PUnit) := List.forM_cons _ _ _ +@[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 [*] + +end List + + +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 _ + end List diff --git a/src/Init/Data/List/Nat.lean b/src/Init/Data/List/Nat.lean new file mode 100644 index 000000000000..c9576f9a0576 --- /dev/null +++ b/src/Init/Data/List/Nat.lean @@ -0,0 +1,93 @@ +/- +Copyright (c) 2014 Parikshit Khanna. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro +-/ +prelude +import Init.Data.List.Lemmas +import Init.Data.Nat.Lemmas + +/-! +# Miscellaneous `List` lemmas, that require more `Nat` lemmas than are available in `Init.Data.List.Lemmas`. + +In particular, `omega` is available here. +-/ + +open Nat + +namespace List + +/-! ### filter -/ + +theorem length_filter_lt_length_iff_exists (l) : + length (filter p l) < length l ↔ ∃ x ∈ l, ¬p x := by + simpa [length_eq_countP_add_countP p l, countP_eq_length_filter] using + countP_pos (fun x => ¬p x) (l := l) + +/-! ### minimum? -/ + +-- A specialization of `minimum?_eq_some_iff` to Nat. +theorem minimum?_eq_some_iff' {xs : List Nat} : + xs.minimum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) := + minimum?_eq_some_iff + (le_refl := Nat.le_refl) + (min_eq_or := fun _ _ => by omega) + (le_min_iff := fun _ _ _ => by omega) + +-- This could be generalized, +-- but will first require further work on order typeclasses in the core repository. +theorem minimum?_cons' {a : Nat} {l : List Nat} : + (a :: l).minimum? = some (match l.minimum? with + | none => a + | some m => min a m) := by + rw [minimum?_eq_some_iff'] + split <;> rename_i h m + · simp_all + · rw [minimum?_eq_some_iff'] at m + obtain ⟨m, le⟩ := m + rw [Nat.min_def] + constructor + · split + · exact mem_cons_self a l + · exact mem_cons_of_mem a m + · intro b m + cases List.mem_cons.1 m with + | inl => split <;> omega + | inr h => + specialize le b h + split <;> omega + +/-! ### maximum? -/ + +-- A specialization of `maximum?_eq_some_iff` to Nat. +theorem maximum?_eq_some_iff' {xs : List Nat} : + xs.maximum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, b ≤ a) := + maximum?_eq_some_iff + (le_refl := Nat.le_refl) + (max_eq_or := fun _ _ => by omega) + (max_le_iff := fun _ _ _ => by omega) + +-- This could be generalized, +-- but will first require further work on order typeclasses in the core repository. +theorem maximum?_cons' {a : Nat} {l : List Nat} : + (a :: l).maximum? = some (match l.maximum? with + | none => a + | some m => max a m) := by + rw [maximum?_eq_some_iff'] + split <;> rename_i h m + · simp_all + · rw [maximum?_eq_some_iff'] at m + obtain ⟨m, le⟩ := m + rw [Nat.max_def] + constructor + · split + · exact mem_cons_of_mem a m + · exact mem_cons_self a l + · intro b m + cases List.mem_cons.1 m with + | inl => split <;> omega + | inr h => + specialize le b h + split <;> omega + +end List diff --git a/src/Init/Data/List/Range.lean b/src/Init/Data/List/Range.lean new file mode 100644 index 000000000000..4e94fabdd6ea --- /dev/null +++ b/src/Init/Data/List/Range.lean @@ -0,0 +1,387 @@ +/- +Copyright (c) 2014 Parikshit Khanna. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro +-/ +prelude +import Init.Data.List.TakeDrop +import Init.Data.Nat.Lemmas + +/-! +# Lemmas about `List.range` and `List.enum` +-/ + +namespace List + +open Nat + +/-! ## Ranges and enumeration -/ + +/-! ### 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 range'_one {s step : Nat} : range' s 1 step = [s] := rfl + +@[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, Nat.succ_inj'] + 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⟩⟩ + +theorem pairwise_lt_range' s n (step := 1) (pos : 0 < step := by simp) : + Pairwise (· < ·) (range' s n step) := + match s, n, step, pos with + | _, 0, _, _ => Pairwise.nil + | s, n + 1, step, pos => by + simp only [range'_succ, pairwise_cons] + constructor + · intros n m + rw [mem_range'] at m + omega + · exact pairwise_lt_range' (s + step) n step pos + +theorem pairwise_le_range' s n (step := 1) : + Pairwise (· ≤ ·) (range' s n step) := + match s, n, step with + | _, 0, _ => Pairwise.nil + | s, n + 1, step => by + simp only [range'_succ, pairwise_cons] + constructor + · intros n m + rw [mem_range'] at m + omega + · exact pairwise_le_range' (s + step) n step + +theorem nodup_range' (s n : Nat) (step := 1) (h : 0 < step := by simp) : Nodup (range' s n step) := + (pairwise_lt_range' s n step h).imp Nat.ne_of_lt + +@[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 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 + +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] + +/-! ### range -/ + +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 (Nat.add_comm 1) + +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] + +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 pairwise_lt_range (n : Nat) : Pairwise (· < ·) (range n) := by + simp (config := {decide := true}) only [range_eq_range', pairwise_lt_range'] + +theorem pairwise_le_range (n : Nat) : Pairwise (· ≤ ·) (range n) := + Pairwise.imp Nat.le_of_lt (pairwise_lt_range _) + +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'] + +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 take_range (m n : Nat) : take m (range n) = range (min m n) := by + apply List.ext_getElem + · simp + · simp (config := { contextual := true }) [← getElem_take, Nat.lt_min] + +theorem nodup_range (n : Nat) : Nodup (range n) := by + simp (config := {decide := true}) only [range_eq_range', nodup_range'] + +/-! ### iota -/ + +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 pairwise_gt_iota (n : Nat) : Pairwise (· > ·) (iota n) := by + simpa only [iota_eq_reverse_range', pairwise_reverse] using pairwise_lt_range' 1 n + +theorem nodup_iota (n : Nat) : Nodup (iota n) := + (pairwise_gt_iota n).imp Nat.ne_of_gt + +/-! ### enumFrom -/ + +@[simp] +theorem enumFrom_singleton (x : α) (n : Nat) : enumFrom n [x] = [(n, x)] := + rfl + +@[simp] +theorem enumFrom_eq_nil {n : Nat} {l : List α} : List.enumFrom n l = [] ↔ l = [] := by + cases l <;> simp + +@[simp] theorem enumFrom_length : ∀ {n} {l : List α}, (enumFrom n l).length = l.length + | _, [] => rfl + | _, _ :: _ => congrArg Nat.succ enumFrom_length + +@[simp] +theorem getElem?_enumFrom : + ∀ n (l : List α) m, (enumFrom n l)[m]? = l[m]?.map fun a => (n + m, a) + | n, [], m => rfl + | n, a :: l, 0 => by simp + | n, a :: l, m + 1 => by + simp only [enumFrom_cons, getElem?_cons_succ] + exact (getElem?_enumFrom (n + 1) l m).trans <| by rw [Nat.add_right_comm]; rfl + +@[simp] +theorem getElem_enumFrom (l : List α) (n) (i : Nat) (h : i < (l.enumFrom n).length) : + (l.enumFrom n)[i] = (n + i, l[i]'(by simpa [enumFrom_length] using h)) := by + simp only [enumFrom_length] at h + rw [getElem_eq_getElem?] + simp only [getElem?_enumFrom, getElem?_eq_getElem h] + simp + +theorem mk_add_mem_enumFrom_iff_getElem? {n i : Nat} {x : α} {l : List α} : + (n + i, x) ∈ enumFrom n l ↔ l[i]? = some x := by + simp [mem_iff_get?] + +theorem mk_mem_enumFrom_iff_le_and_getElem?_sub {n i : Nat} {x : α} {l : List α} : + (i, x) ∈ enumFrom n l ↔ n ≤ i ∧ l[i - n]? = x := by + if h : n ≤ i then + rcases Nat.exists_eq_add_of_le h with ⟨i, rfl⟩ + simp [mk_add_mem_enumFrom_iff_getElem?, Nat.add_sub_cancel_left] + else + have : ∀ k, n + k ≠ i := by rintro k rfl; simp at h + simp [h, mem_iff_get?, this] + +theorem le_fst_of_mem_enumFrom {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) : + n ≤ x.1 := + (mk_mem_enumFrom_iff_le_and_getElem?_sub.1 h).1 + +theorem fst_lt_add_of_mem_enumFrom {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) : + x.1 < n + length l := by + rcases mem_iff_get.1 h with ⟨i, rfl⟩ + simpa using i.isLt + +theorem map_enumFrom (f : α → β) (n : Nat) (l : List α) : + map (Prod.map id f) (enumFrom n l) = enumFrom n (map f l) := by + induction l generalizing n <;> simp_all + +@[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 enumFrom_map_snd : ∀ (n) (l : List α), map Prod.snd (enumFrom n l) = l + | _, [] => rfl + | _, _ :: _ => congrArg (cons _) (enumFrom_map_snd _ _) + +theorem snd_mem_of_mem_enumFrom {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) : x.2 ∈ l := + enumFrom_map_snd n l ▸ mem_map_of_mem _ h + +theorem mem_enumFrom {x : α} {i j : Nat} (xs : List α) (h : (i, x) ∈ xs.enumFrom j) : + j ≤ i ∧ i < j + xs.length ∧ x ∈ xs := + ⟨le_fst_of_mem_enumFrom h, fst_lt_add_of_mem_enumFrom h, snd_mem_of_mem_enumFrom h⟩ + +theorem map_fst_add_enumFrom_eq_enumFrom (l : List α) (n k : Nat) : + map (Prod.map (· + n) id) (enumFrom k l) = enumFrom (n + k) l := + ext_getElem? fun i ↦ by simp [(· ∘ ·), Nat.add_comm, Nat.add_left_comm]; rfl + +theorem map_fst_add_enum_eq_enumFrom (l : List α) (n : Nat) : + map (Prod.map (· + n) id) (enum l) = enumFrom n l := + map_fst_add_enumFrom_eq_enumFrom l _ _ + +theorem enumFrom_cons' (n : Nat) (x : α) (xs : List α) : + enumFrom n (x :: xs) = (n, x) :: (enumFrom n xs).map (Prod.map (· + 1) id) := by + rw [enumFrom_cons, Nat.add_comm, ← map_fst_add_enumFrom_eq_enumFrom] + +theorem enumFrom_map (n : Nat) (l : List α) (f : α → β) : + enumFrom n (l.map f) = (enumFrom n l).map (Prod.map id f) := by + induction l with + | nil => rfl + | cons hd tl IH => + rw [map_cons, enumFrom_cons', enumFrom_cons', map_cons, map_map, IH, map_map] + rfl + +theorem enumFrom_append (xs ys : List α) (n : Nat) : + enumFrom n (xs ++ ys) = enumFrom n xs ++ enumFrom (n + xs.length) ys := by + induction xs generalizing ys n with + | nil => simp + | cons x xs IH => + rw [cons_append, enumFrom_cons, IH, ← cons_append, ← enumFrom_cons, length, Nat.add_right_comm, + Nat.add_assoc] + +theorem enumFrom_eq_zip_range' (l : List α) {n : Nat} : l.enumFrom n = (range' n l.length).zip l := + zip_of_prod (enumFrom_map_fst _ _) (enumFrom_map_snd _ _) + +@[simp] +theorem unzip_enumFrom_eq_prod (l : List α) {n : Nat} : + (l.enumFrom n).unzip = (range' n l.length, l) := by + simp only [enumFrom_eq_zip_range', unzip_zip, length_range'] + +/-! ### enum -/ + +theorem enum_cons : (a::as).enum = (0, a) :: as.enumFrom 1 := rfl + +theorem enum_cons' (x : α) (xs : List α) : + enum (x :: xs) = (0, x) :: (enum xs).map (Prod.map (· + 1) id) := + enumFrom_cons' _ _ _ + +@[simp] +theorem enum_eq_nil {l : List α} : List.enum l = [] ↔ l = [] := enumFrom_eq_nil + +@[simp] theorem enum_singleton (x : α) : enum [x] = [(0, x)] := rfl + +@[simp] theorem enum_length : (enum l).length = l.length := + enumFrom_length + +@[simp] +theorem getElem?_enum (l : List α) (n : Nat) : (enum l)[n]? = l[n]?.map fun a => (n, a) := by + rw [enum, getElem?_enumFrom, Nat.zero_add] + +@[simp] +theorem getElem_enum (l : List α) (i : Nat) (h : i < l.enum.length) : + l.enum[i] = (i, l[i]'(by simpa [enum_length] using h)) := by + simp [enum] + +theorem mk_mem_enum_iff_getElem? {i : Nat} {x : α} {l : List α} : (i, x) ∈ enum l ↔ l[i]? = x := by + simp [enum, mk_mem_enumFrom_iff_le_and_getElem?_sub] + +theorem mem_enum_iff_getElem? {x : Nat × α} {l : List α} : x ∈ enum l ↔ l[x.1]? = some x.2 := + mk_mem_enum_iff_getElem? + +theorem fst_lt_of_mem_enum {x : Nat × α} {l : List α} (h : x ∈ enum l) : x.1 < length l := by + simpa using fst_lt_add_of_mem_enumFrom h + +theorem snd_mem_of_mem_enum {x : Nat × α} {l : List α} (h : x ∈ enum l) : x.2 ∈ l := + snd_mem_of_mem_enumFrom h + +theorem map_enum (f : α → β) (l : List α) : map (Prod.map id f) (enum l) = enum (map f l) := + map_enumFrom f 0 l + +@[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'] + +@[simp] +theorem enum_map_snd (l : List α) : map Prod.snd (enum l) = l := + enumFrom_map_snd _ _ + +theorem enum_map (l : List α) (f : α → β) : (l.map f).enum = l.enum.map (Prod.map id f) := + enumFrom_map _ _ _ + +theorem enum_append (xs ys : List α) : enum (xs ++ ys) = enum xs ++ enumFrom xs.length ys := by + simp [enum, enumFrom_append] + +theorem enum_eq_zip_range (l : List α) : l.enum = (range l.length).zip l := + zip_of_prod (enum_map_fst _) (enum_map_snd _) + +@[simp] +theorem unzip_enum_eq_prod (l : List α) : l.enum.unzip = (range l.length, l) := by + simp only [enum_eq_zip_range, unzip_zip, length_range] + +end List diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean index c49495f944b8..1116e157005e 100644 --- a/src/Init/Data/List/TakeDrop.lean +++ b/src/Init/Data/List/TakeDrop.lean @@ -124,6 +124,14 @@ theorem take_take : ∀ (n m) (l : List α), take n (take m l) = take (min n m) | succ n, succ m, a :: l => by simp only [take, succ_min_succ, take_take n m l] +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 + @[simp] theorem take_replicate (a : α) : ∀ n m : Nat, take n (replicate m a) = replicate (min n m) a | n, 0 => by simp [Nat.min_zero] | 0, m => by simp [Nat.zero_min] @@ -164,7 +172,7 @@ theorem take_eq_take : | _ :: xs, 0, 0 => by simp | x :: xs, m + 1, 0 => by simp [Nat.zero_min, succ_min_succ] | x :: xs, 0, n + 1 => by simp [Nat.zero_min, succ_min_succ] - | x :: xs, m + 1, n + 1 => by simp [succ_min_succ, take_eq_take]; omega + | x :: xs, m + 1, n + 1 => by simp [succ_min_succ, take_eq_take] theorem take_add (l : List α) (m n : Nat) : l.take (m + n) = l.take m ++ (l.drop m).take n := by suffices take (m + n) (take m l ++ drop m l) = take m l ++ take n (drop m l) by @@ -280,7 +288,7 @@ theorem drop_length_cons {l : List α} (h : l ≠ []) (a : α) : simp only [drop, length] by_cases h₁ : l = [] · simp [h₁] - rw [getLast_cons' _ h₁] + rw [getLast_cons h₁] exact ih h₁ y /-- Dropping the elements up to `n` in `l₁ ++ l₂` is the same as dropping the elements up to `n` @@ -299,7 +307,6 @@ theorem drop_append_of_le_length {l₁ l₂ : List α} {n : Nat} (h : n ≤ l₁ (l₁ ++ l₂).drop n = l₁.drop n ++ l₂ := by simp [drop_append_eq_append_drop, Nat.sub_eq_zero_of_le h] - /-- Dropping the elements up to `l₁.length + i` in `l₁ + l₂` is the same as dropping the elements up to `i` in `l₂`. -/ @[simp] @@ -316,7 +323,7 @@ theorem set_eq_take_append_cons_drop {l : List α} {n : Nat} {a : α} : getElem?_take h'] · by_cases h'' : m = n · subst h'' - rw [getElem?_set_eq (by simp; omega), getElem?_append_right, length_take, + rw [getElem?_set_eq ‹_›, getElem?_append_right, length_take, Nat.min_eq_left (by omega), Nat.sub_self, getElem?_cons_zero] rw [length_take] exact Nat.min_le_left m l.length @@ -420,12 +427,43 @@ theorem drop_reverse {α} {xs : List α} {n : Nat} (h : n ≤ xs.length) : induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all [succ_min_succ, Nat.zero_min, Nat.min_zero] +theorem lt_length_left_of_zipWith {f : α → β → γ} {i : Nat} {l : List α} {l' : List β} + (h : i < (zipWith f l l').length) : i < l.length := by rw [length_zipWith] at h; omega + +theorem lt_length_right_of_zipWith {f : α → β → γ} {i : Nat} {l : List α} {l' : List β} + (h : i < (zipWith f l l').length) : i < l'.length := by rw [length_zipWith] at h; omega + +@[simp] +theorem getElem_zipWith {f : α → β → γ} {l : List α} {l' : List β} + {i : Nat} {h : i < (zipWith f l l').length} : + (zipWith f l l')[i] = + f (l[i]'(lt_length_left_of_zipWith h)) + (l'[i]'(lt_length_right_of_zipWith h)) := by + rw [← Option.some_inj, ← getElem?_eq_getElem, getElem?_zipWith_eq_some] + exact + ⟨l[i]'(lt_length_left_of_zipWith h), l'[i]'(lt_length_right_of_zipWith h), + by rw [getElem?_eq_getElem], by rw [getElem?_eq_getElem]; exact ⟨rfl, rfl⟩⟩ + theorem zipWith_eq_zipWith_take_min : ∀ (l₁ : List α) (l₂ : List β), zipWith f l₁ l₂ = zipWith f (l₁.take (min l₁.length l₂.length)) (l₂.take (min l₁.length l₂.length)) | [], _ => by simp | _, [] => by simp | a :: l₁, b :: l₂ => by simp [succ_min_succ, zipWith_eq_zipWith_take_min l₁ l₂] +theorem reverse_zipWith (h : l.length = l'.length) : + (zipWith f l l').reverse = zipWith f l.reverse l'.reverse := by + induction l generalizing l' with + | nil => simp + | cons hd tl hl => + cases l' with + | nil => simp + | cons hd' tl' => + simp only [Nat.add_right_cancel_iff, length] at h + have : tl.reverse.length = tl'.reverse.length := by simp [h] + simp [hl h, zipWith_append _ _ _ _ _ this] + +@[deprecated reverse_zipWith (since := "2024-07-28")] abbrev zipWith_distrib_reverse := @reverse_zipWith + @[simp] theorem zipWith_replicate {a : α} {b : β} {m n : Nat} : zipWith f (replicate m a) (replicate n b) = replicate (min m n) (f a b) := by rw [zipWith_eq_zipWith_take_min] @@ -437,6 +475,20 @@ theorem zipWith_eq_zipWith_take_min : ∀ (l₁ : List α) (l₂ : List β), length (zip l₁ l₂) = min (length l₁) (length l₂) := by simp [zip] +theorem lt_length_left_of_zip {i : Nat} {l : List α} {l' : List β} (h : i < (zip l l').length) : + i < l.length := + lt_length_left_of_zipWith h + +theorem lt_length_right_of_zip {i : Nat} {l : List α} {l' : List β} (h : i < (zip l l').length) : + i < l'.length := + lt_length_right_of_zipWith h + +@[simp] +theorem getElem_zip {l : List α} {l' : List β} {i : Nat} {h : i < (zip l l').length} : + (zip l l')[i] = + (l[i]'(lt_length_left_of_zip h), l'[i]'(lt_length_right_of_zip h)) := + getElem_zipWith (h := h) + theorem zip_eq_zip_take_min : ∀ (l₁ : List α) (l₂ : List β), zip l₁ l₂ = zip (l₁.take (min l₁.length l₂.length)) (l₂.take (min l₁.length l₂.length)) | [], _ => by simp @@ -448,70 +500,4 @@ theorem zip_eq_zip_take_min : ∀ (l₁ : List α) (l₂ : List β), rw [zip_eq_zip_take_min] simp -/-! ### minimum? -/ - --- A specialization of `minimum?_eq_some_iff` to Nat. -theorem minimum?_eq_some_iff' {xs : List Nat} : - xs.minimum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) := - minimum?_eq_some_iff - (le_refl := Nat.le_refl) - (min_eq_or := fun _ _ => by omega) - (le_min_iff := fun _ _ _ => by omega) - --- This could be generalized, --- but will first require further work on order typeclasses in the core repository. -theorem minimum?_cons' {a : Nat} {l : List Nat} : - (a :: l).minimum? = some (match l.minimum? with - | none => a - | some m => min a m) := by - rw [minimum?_eq_some_iff'] - split <;> rename_i h m - · simp_all - · rw [minimum?_eq_some_iff'] at m - obtain ⟨m, le⟩ := m - rw [Nat.min_def] - constructor - · split - · exact mem_cons_self a l - · exact mem_cons_of_mem a m - · intro b m - cases List.mem_cons.1 m with - | inl => split <;> omega - | inr h => - specialize le b h - split <;> omega - -/-! ### maximum? -/ - --- A specialization of `maximum?_eq_some_iff` to Nat. -theorem maximum?_eq_some_iff' {xs : List Nat} : - xs.maximum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, b ≤ a) := - maximum?_eq_some_iff - (le_refl := Nat.le_refl) - (max_eq_or := fun _ _ => by omega) - (max_le_iff := fun _ _ _ => by omega) - --- This could be generalized, --- but will first require further work on order typeclasses in the core repository. -theorem maximum?_cons' {a : Nat} {l : List Nat} : - (a :: l).maximum? = some (match l.maximum? with - | none => a - | some m => max a m) := by - rw [maximum?_eq_some_iff'] - split <;> rename_i h m - · simp_all - · rw [maximum?_eq_some_iff'] at m - obtain ⟨m, le⟩ := m - rw [Nat.max_def] - constructor - · split - · exact mem_cons_of_mem a m - · exact mem_cons_self a l - · intro b m - cases List.mem_cons.1 m with - | inl => split <;> omega - | inr h => - specialize le b h - split <;> omega - end List diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index 967a7cd24d1f..4e9ae2eb9a47 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -388,11 +388,11 @@ theorem le_or_eq_of_le_succ {m n : Nat} (h : m ≤ succ n) : m ≤ n ∨ m = suc theorem le_or_eq_of_le_add_one {m n : Nat} (h : m ≤ n + 1) : m ≤ n ∨ m = n + 1 := le_or_eq_of_le_succ h -theorem le_add_right : ∀ (n k : Nat), n ≤ n + k +@[simp] theorem le_add_right : ∀ (n k : Nat), n ≤ n + k | n, 0 => Nat.le_refl n | n, k+1 => le_succ_of_le (le_add_right n k) -theorem le_add_left (n m : Nat): n ≤ m + n := +@[simp] theorem le_add_left (n m : Nat): n ≤ m + n := Nat.add_comm n m ▸ le_add_right n m theorem le_of_add_right_le {n m k : Nat} (h : n + k ≤ m) : n ≤ m := @@ -528,7 +528,7 @@ protected theorem le_of_add_le_add_right {a b c : Nat} : a + b ≤ c + b → a rw [Nat.add_comm _ b, Nat.add_comm _ b] apply Nat.le_of_add_le_add_left -protected theorem add_le_add_iff_right {n : Nat} : m + n ≤ k + n ↔ m ≤ k := +@[simp] protected theorem add_le_add_iff_right {n : Nat} : m + n ≤ k + n ↔ m ≤ k := ⟨Nat.le_of_add_le_add_right, fun h => Nat.add_le_add_right h _⟩ /-! ### le/lt -/ diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean index bed448fdee1c..442f792693fc 100644 --- a/src/Init/Data/Nat/Bitwise/Lemmas.lean +++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean @@ -265,8 +265,8 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) : have x_eq : x = y + 2^j := Nat.eq_add_of_sub_eq x_ge_j y_eq simp only [Nat.two_pow_pos, x_eq, Nat.le_add_left, true_and, ite_true] have y_lt_x : y < x := by - simp [x_eq] - exact Nat.lt_add_of_pos_right (Nat.two_pow_pos j) + simp only [x_eq, Nat.lt_add_right_iff_pos] + exact Nat.two_pow_pos j simp only [hyp y y_lt_x] if i_lt_j : i < j then rw [Nat.add_comm _ (2^_), testBit_two_pow_add_gt i_lt_j] diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean index 605c50255338..442d51f98f0c 100644 --- a/src/Init/Data/Nat/Lemmas.lean +++ b/src/Init/Data/Nat/Lemmas.lean @@ -19,6 +19,9 @@ and later these lemmas should be organised into other files more systematically. -/ namespace Nat + +attribute [simp] not_lt_zero + /-! ## add -/ protected theorem add_add_add_comm (a b c d : Nat) : (a + b) + (c + d) = (a + c) + (b + d) := by @@ -36,13 +39,13 @@ protected theorem eq_zero_of_add_eq_zero_right (h : n + m = 0) : n = 0 := protected theorem add_eq_zero_iff : n + m = 0 ↔ n = 0 ∧ m = 0 := ⟨Nat.eq_zero_of_add_eq_zero, fun ⟨h₁, h₂⟩ => h₂.symm ▸ h₁⟩ -protected theorem add_left_cancel_iff {n : Nat} : n + m = n + k ↔ m = k := +@[simp] protected theorem add_left_cancel_iff {n : Nat} : n + m = n + k ↔ m = k := ⟨Nat.add_left_cancel, fun | rfl => rfl⟩ -protected theorem add_right_cancel_iff {n : Nat} : m + n = k + n ↔ m = k := +@[simp] protected theorem add_right_cancel_iff {n : Nat} : m + n = k + n ↔ m = k := ⟨Nat.add_right_cancel, fun | rfl => rfl⟩ -protected theorem add_le_add_iff_left {n : Nat} : n + m ≤ n + k ↔ m ≤ k := +@[simp] protected theorem add_le_add_iff_left {n : Nat} : n + m ≤ n + k ↔ m ≤ k := ⟨Nat.le_of_add_le_add_left, fun h => Nat.add_le_add_left h _⟩ protected theorem lt_of_add_lt_add_right : ∀ {n : Nat}, k + n < m + n → k < m @@ -52,10 +55,10 @@ protected theorem lt_of_add_lt_add_right : ∀ {n : Nat}, k + n < m + n → k < protected theorem lt_of_add_lt_add_left {n : Nat} : n + k < n + m → k < m := by rw [Nat.add_comm n, Nat.add_comm n]; exact Nat.lt_of_add_lt_add_right -protected theorem add_lt_add_iff_left {k n m : Nat} : k + n < k + m ↔ n < m := +@[simp] protected theorem add_lt_add_iff_left {k n m : Nat} : k + n < k + m ↔ n < m := ⟨Nat.lt_of_add_lt_add_left, fun h => Nat.add_lt_add_left h _⟩ -protected theorem add_lt_add_iff_right {k n m : Nat} : n + k < m + k ↔ n < m := +@[simp] protected theorem add_lt_add_iff_right {k n m : Nat} : n + k < m + k ↔ n < m := ⟨Nat.lt_of_add_lt_add_right, fun h => Nat.add_lt_add_right h _⟩ protected theorem add_lt_add_of_le_of_lt {a b c d : Nat} (hle : a ≤ b) (hlt : c < d) : @@ -75,10 +78,10 @@ protected theorem pos_of_lt_add_right (h : n < n + k) : 0 < k := protected theorem pos_of_lt_add_left : n < k + n → 0 < k := by rw [Nat.add_comm]; exact Nat.pos_of_lt_add_right -protected theorem lt_add_right_iff_pos : n < n + k ↔ 0 < k := +@[simp] protected theorem lt_add_right_iff_pos : n < n + k ↔ 0 < k := ⟨Nat.pos_of_lt_add_right, Nat.lt_add_of_pos_right⟩ -protected theorem lt_add_left_iff_pos : n < k + n ↔ 0 < k := +@[simp] protected theorem lt_add_left_iff_pos : n < k + n ↔ 0 < k := ⟨Nat.pos_of_lt_add_left, Nat.lt_add_of_pos_left⟩ protected theorem add_pos_left (h : 0 < m) (n) : 0 < m + n := diff --git a/src/Init/Data/Subtype.lean b/src/Init/Data/Subtype.lean new file mode 100644 index 000000000000..d8be8da53a31 --- /dev/null +++ b/src/Init/Data/Subtype.lean @@ -0,0 +1,27 @@ +/- +Copyright (c) 2017 Johannes Hölzl. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johannes Hölzl +-/ +prelude +import Init.Ext + +namespace Subtype + +universe u +variable {α : Sort u} {p q : α → Prop} + +@[ext] +protected theorem ext : ∀ {a1 a2 : { x // p x }}, (a1 : α) = (a2 : α) → a1 = a2 + | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl + +@[simp] +protected theorem «forall» {q : { a // p a } → Prop} : (∀ x, q x) ↔ ∀ a b, q ⟨a, b⟩ := + ⟨fun h a b ↦ h ⟨a, b⟩, fun h ⟨a, b⟩ ↦ h a b⟩ + +@[simp] +protected theorem «exists» {q : { a // p a } → Prop} : + (Exists fun x => q x) ↔ Exists fun a => Exists fun b => q ⟨a, b⟩ := + ⟨fun ⟨⟨a, b⟩, h⟩ ↦ ⟨a, b, h⟩, fun ⟨a, b, h⟩ ↦ ⟨⟨a, b⟩, h⟩⟩ + +end Subtype diff --git a/tests/lean/run/1017.lean b/tests/lean/run/1017.lean index a01fd84fee8b..29b102d580e1 100644 --- a/tests/lean/run/1017.lean +++ b/tests/lean/run/1017.lean @@ -30,17 +30,17 @@ instance hasNextWF : WellFoundedRelation {s : ρ // isFinite s} where cases h; case intro w h => induction w generalizing s case zero => - intro ⟨s',h'⟩ h_next + intro s' h' h_next simp [hasNext] at h_next cases h_next; case intro x h_next => simp [lengthBoundedBy, isEmpty, Option.isNone, take, h_next] at h case succ n ih => - intro ⟨s',h'⟩ h_next + intro s' h' h_next simp [hasNext] at h_next cases h_next; case intro x h_next => simp [lengthBoundedBy, take, h_next] at h have := ih s' h - exact Acc.intro (⟨s',h'⟩ : {s : ρ // isFinite s}) this + exact Acc.intro (⟨s',h'⟩ : {s : ρ // isFinite s}) (by simpa) ⟩⟩ def mwe [Stream ρ τ] (acc : α) : {l : ρ // isFinite l} → α diff --git a/tests/lean/run/binop_binrel_perf_issue.lean b/tests/lean/run/binop_binrel_perf_issue.lean index fae2fac9841b..d426fec52e7c 100644 --- a/tests/lean/run/binop_binrel_perf_issue.lean +++ b/tests/lean/run/binop_binrel_perf_issue.lean @@ -58,9 +58,6 @@ section Mathlib.Data.Subtype variable {α : Sort _} {p : α → Prop} -protected theorem Subtype.ext : ∀ {a1 a2 : { x // p x }}, (a1 : α) = (a2 : α) → a1 = a2 - | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl - theorem Subtype.coe_injective : Function.Injective (fun (a : Subtype p) ↦ (a : α)) := fun _ _ ↦ Subtype.ext end Mathlib.Data.Subtype diff --git a/tests/lean/run/issue3175.lean b/tests/lean/run/issue3175.lean index 831aac668e59..42a906119955 100644 --- a/tests/lean/run/issue3175.lean +++ b/tests/lean/run/issue3175.lean @@ -2,11 +2,9 @@ def foo : (n : Nat) → (i : Fin n) → Bool | 0, _ => false | 1, _ => false | _+2, _ => foo 1 ⟨0, Nat.zero_lt_one⟩ -decreasing_by simp_wf; simp_arith def bar : (n : Nat) → (i : Fin n) → Bool | 0, _ => false | 1, _ => false | _+2, _ => bar 1 ⟨0, Nat.zero_lt_one⟩ -termination_by n i => n -decreasing_by simp_wf; simp_arith +termination_by n => n diff --git a/tests/lean/run/simpArith1.lean b/tests/lean/run/simpArith1.lean index 96e7a6bd635e..4d2a15ec5ca6 100644 --- a/tests/lean/run/simpArith1.lean +++ b/tests/lean/run/simpArith1.lean @@ -7,16 +7,6 @@ theorem ex2 : a + b < b + 1 + a + c := by theorem ex3 : a + (fun x => x) b < b + 1 + a + c := by simp_arith -/-- -info: a b c : Nat -⊢ (fun x => x) b ≤ b + c --/ -#guard_msgs in -theorem ex4 : a + (fun x => x) b < b + 1 + a + c := by - simp_arith (config := { beta := false }) - trace_state - simp_arith - theorem ex5 (h : a + d + b > b + 1 + (a + (c + c) + d)) : False := by simp_arith at h