chore: cleanup grind List tests (#11903)
Some of these tests were last investigated a long time ago: happily many of the failing tests now work due to subsequent improvements to grind.
This commit is contained in:
Kim Morrison
GitHub
parent
06b7b022b3
commit
8207919728
5 changed files with 479 additions and 649 deletions
|
|
@ -169,10 +169,10 @@ Examples:
|
|||
| a::as, b::bs, eqv => eqv a b && isEqv as bs eqv
|
||||
| _, _, _ => false
|
||||
|
||||
@[simp] theorem isEqv_nil_nil : isEqv ([] : List α) [] eqv = true := rfl
|
||||
@[simp] theorem isEqv_nil_cons : isEqv ([] : List α) (a::as) eqv = false := rfl
|
||||
@[simp] theorem isEqv_cons_nil : isEqv (a::as : List α) [] eqv = false := rfl
|
||||
theorem isEqv_cons₂ : isEqv (a::as) (b::bs) eqv = (eqv a b && isEqv as bs eqv) := rfl
|
||||
@[simp, grind =] theorem isEqv_nil_nil : isEqv ([] : List α) [] eqv = true := rfl
|
||||
@[simp, grind =] theorem isEqv_nil_cons : isEqv ([] : List α) (a::as) eqv = false := rfl
|
||||
@[simp, grind =] theorem isEqv_cons_nil : isEqv (a::as : List α) [] eqv = false := rfl
|
||||
@[grind =] theorem isEqv_cons₂ : isEqv (a::as) (b::bs) eqv = (eqv a b && isEqv as bs eqv) := rfl
|
||||
|
||||
|
||||
/-! ## Lexicographic ordering -/
|
||||
|
|
|
|||
|
|
@ -2,19 +2,15 @@
|
|||
-- involving `Nat` modulo and div with variable denominators.
|
||||
|
||||
example (a b n : Nat) (ha : a < n) : (n - a) * b % n = (n - a * b % n) % n := by
|
||||
rw [Nat.sub_mul]
|
||||
rw [Nat.mod_eq_mod_iff]
|
||||
rw [Nat.sub_mul, Nat.mod_eq_mod_iff]
|
||||
match b with
|
||||
| 0 => refine ⟨1, 0, by simp⟩
|
||||
| b+1 =>
|
||||
refine ⟨a*(b+1)/n, b, ?_⟩
|
||||
refine ⟨a * (b + 1) / n, b, ?_⟩
|
||||
rw [Nat.mod_def, Nat.mul_add_one, Nat.mul_comm _ n, Nat.mul_comm b n]
|
||||
have : n * (a * (b + 1) / n) ≤ a * (b + 1) := Nat.mul_div_le (a * (b + 1)) n
|
||||
have := Nat.lt_mul_div_succ (a * (b + 1)) (show 0 < n by omega)
|
||||
rw [Nat.mul_add_one n] at this
|
||||
have := Nat.lt_mul_div_succ (a * (b + 1)) (show 0 < n by grind)
|
||||
have : a * (b + 1) ≤ n * b + n := by
|
||||
rw [Nat.mul_add_one]
|
||||
have := Nat.mul_le_mul_right b ha
|
||||
rw [Nat.succ_mul] at this
|
||||
omega
|
||||
omega
|
||||
grind
|
||||
grind
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -9,7 +9,7 @@
|
|||
-- This file only contains those theorems that can be proved "effortlessly" with `grind`.
|
||||
-- `tests/lean/grind/experiments/list.lean` contains everything from `Data/List/Lemmas.lean`
|
||||
-- that still resists `grind`!
|
||||
@[expose] public section -- TODO: remove after congr_eq has been fixed
|
||||
|
||||
open List Nat
|
||||
|
||||
namespace Hidden
|
||||
|
|
@ -444,8 +444,6 @@ theorem map_singleton {f : α → β} {a : α} : map f [a] = [f a] := by grind
|
|||
theorem map_eq_nil_iff {f : α → β} {l : List α} : map f l = [] ↔ l = [] := by
|
||||
cases l with grind
|
||||
|
||||
-- FIXME
|
||||
attribute [local grind] List.map_inj_left in
|
||||
theorem map_inj_left {f g : α → β} : map f l = map g l ↔ ∀ a ∈ l, f a = g a := by
|
||||
induction l with grind
|
||||
|
||||
|
|
@ -457,8 +455,6 @@ theorem map_eq_singleton_iff {f : α → β} {l : List α} {b : β} :
|
|||
map f l = [b] ↔ ∃ a, l = [a] ∧ f a = b := by
|
||||
grind [cases List]
|
||||
|
||||
-- FIXME
|
||||
attribute [local grind] List.map_inj_left in
|
||||
theorem map_eq_map_iff : map f l = map g l ↔ ∀ a ∈ l, f a = g a := by
|
||||
induction l with grind
|
||||
|
||||
|
|
|
|||
432
tests/lean/run/grind_list3.lean
Normal file
432
tests/lean/run/grind_list3.lean
Normal file
|
|
@ -0,0 +1,432 @@
|
|||
-- Note that `grind_list.lean` uses `reset_grind_attrs%` to clear the grind attributes.
|
||||
-- This file does not: it is testing the grind attributes in the library.
|
||||
|
||||
-- This file follows `Data/List/Lemmas.lean`. Indeed, if we decided `grind` is allowed there,
|
||||
-- it should be possible to replace proofs there with these.
|
||||
-- (In some cases, the proofs here are now cheating and directly using the same result from the library,
|
||||
-- but initially I was avoiding this, but haven't bothered writing `grind [-X]` everywhere.)
|
||||
|
||||
open List Nat
|
||||
|
||||
namespace Hidden
|
||||
|
||||
|
||||
/-! ### getElem? and getElem -/
|
||||
|
||||
theorem getElem?_eq_some_iff {l : List α} : l[i]? = some a ↔ ∃ h : i < l.length, l[i] = a := by
|
||||
induction l with grind
|
||||
|
||||
theorem some_eq_getElem?_iff {l : List α} : some a = l[i]? ↔ ∃ h : i < l.length, l[i] = a := by
|
||||
grind
|
||||
|
||||
theorem some_getElem_eq_getElem?_iff {xs : List α} {i : Nat} (h : i < xs.length) :
|
||||
(some xs[i] = xs[i]?) ↔ True := by
|
||||
grind
|
||||
|
||||
theorem getElem?_eq_some_getElem_iff {xs : List α} {i : Nat} (h : i < xs.length) :
|
||||
(xs[i]? = some xs[i]) ↔ True := by
|
||||
grind
|
||||
|
||||
theorem getElem_eq_iff {l : List α} {i : Nat} (h : i < l.length) : l[i] = x ↔ l[i]? = some x := by
|
||||
grind
|
||||
|
||||
theorem getElem_eq_getElem?_get {l : List α} {i : Nat} (h : i < l.length) :
|
||||
l[i] = l[i]?.get (by simp [h]) := by
|
||||
grind
|
||||
|
||||
theorem getD_getElem? {l : List α} {i : Nat} {d : α} :
|
||||
l[i]?.getD d = if p : i < l.length then l[i]'p else d := by
|
||||
grind
|
||||
|
||||
theorem getElem_singleton {a : α} {i : Nat} (h : i < 1) : [a][i] = a := by grind
|
||||
|
||||
theorem getElem?_singleton {a : α} {i : Nat} : [a][i]? = if i = 0 then some a else none := by
|
||||
grind
|
||||
|
||||
theorem getElem_zero {l : List α} (h : 0 < l.length) : l[0] = l.head (length_pos_iff.mp h) := by
|
||||
grind
|
||||
|
||||
theorem ext_getElem {l₁ l₂ : List α} (hl : length l₁ = length l₂)
|
||||
(h : ∀ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length), l₁[i]'h₁ = l₂[i]'h₂) : l₁ = l₂ :=
|
||||
ext_getElem? (by grind)
|
||||
|
||||
theorem getElem_concat_length {l : List α} {a : α} {i : Nat} (h : i = l.length) (w) :
|
||||
(l ++ [a])[i]'w = a := by
|
||||
grind
|
||||
|
||||
/-! ### mem -/
|
||||
|
||||
theorem exists_mem_cons {p : α → Prop} {a : α} {l : List α} :
|
||||
(∃ x, ∃ _ : x ∈ a :: l, p x) ↔ p a ∨ ∃ x, ∃ _ : x ∈ l, p x := by grind
|
||||
|
||||
theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ i : Nat, l[i]? = some a := by
|
||||
let ⟨n, _, e⟩ := getElem_of_mem h
|
||||
exact ⟨n, by grind⟩
|
||||
|
||||
/-! ### any / all -/
|
||||
|
||||
theorem any_eq {l : List α} : l.any p = decide (∃ x, x ∈ l ∧ p x) := by grind
|
||||
|
||||
theorem all_eq {l : List α} : l.all p = decide (∀ x, x ∈ l → p x) := by grind
|
||||
|
||||
theorem decide_exists_mem {l : List α} {p : α → Prop} [DecidablePred p] :
|
||||
decide (∃ x, x ∈ l ∧ p x) = l.any p := by
|
||||
grind
|
||||
|
||||
theorem decide_forall_mem {l : List α} {p : α → Prop} [DecidablePred p] :
|
||||
decide (∀ x, x ∈ l → p x) = l.all p := by
|
||||
grind
|
||||
|
||||
theorem any_eq_true {l : List α} : l.any p = true ↔ ∃ x, x ∈ l ∧ p x := by
|
||||
grind
|
||||
|
||||
theorem all_eq_true {l : List α} : l.all p = true ↔ ∀ x, x ∈ l → p x := by
|
||||
grind
|
||||
|
||||
theorem any_eq_false {l : List α} : l.any p = false ↔ ∀ x, x ∈ l → ¬p x := by
|
||||
grind
|
||||
|
||||
theorem all_eq_false {l : List α} : l.all p = false ↔ ∃ x, x ∈ l ∧ ¬p x := by
|
||||
grind
|
||||
|
||||
/-! ### any / all -/
|
||||
|
||||
theorem all_bne [BEq α] {l : List α} : (l.all fun x => a != x) = !l.contains a := by
|
||||
induction l <;> grind [bne]
|
||||
|
||||
/-! ### set -/
|
||||
|
||||
theorem getElem?_set_self' {l : List α} {i : Nat} {a : α} :
|
||||
(set l i a)[i]? = Function.const _ a <$> l[i]? := by
|
||||
grind
|
||||
|
||||
theorem getElem?_set' {l : List α} {i j : Nat} {a : α} :
|
||||
(set l i a)[j]? = if i = j then Function.const _ a <$> l[j]? else l[j]? := by
|
||||
grind
|
||||
|
||||
/-! ### getLast -/
|
||||
|
||||
theorem _root_.List.length_pos_of_ne_nil {l : List α} (h : l ≠ []) : 0 < l.length := by
|
||||
grind
|
||||
|
||||
theorem getLast_eq_getLastD {a l} (h) : @getLast α (a::l) h = getLastD l a := by
|
||||
grind
|
||||
|
||||
theorem getLast!_cons_eq_getLastD [Inhabited α] : @getLast! α _ (a::l) = getLastD l a := by
|
||||
grind
|
||||
|
||||
theorem getElem_cons_length {x : α} {xs : List α} {i : Nat} (h : i = xs.length) :
|
||||
(x :: xs)[i]'(by simp [h]) = (x :: xs).getLast (cons_ne_nil x xs) := by
|
||||
grind
|
||||
|
||||
/-! ### getLast? -/
|
||||
|
||||
theorem getLast_eq_iff_getLast?_eq_some {xs : List α} (h) :
|
||||
xs.getLast h = a ↔ xs.getLast? = some a := by
|
||||
grind
|
||||
|
||||
/-! ### getLast! -/
|
||||
|
||||
theorem getLast!_nil [Inhabited α] : ([] : List α).getLast! = default := by grind
|
||||
|
||||
theorem getLast!_eq_getLast?_getD [Inhabited α] {l : List α} : getLast! l = (getLast? l).getD default := by
|
||||
cases l with grind
|
||||
|
||||
theorem getLast!_eq_getElem! [Inhabited α] {l : List α} : l.getLast! = l[l.length - 1]! := by
|
||||
cases l with grind
|
||||
|
||||
/-! ### map -/
|
||||
|
||||
theorem mem_map {f : α → β} {l : List α} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by
|
||||
induction l with grind
|
||||
|
||||
theorem forall_mem_map {f : α → β} {l : List α} {P : β → Prop} :
|
||||
(∀ (i) (_ : i ∈ l.map f), P i) ↔ ∀ (j) (_ : j ∈ l), P (f j) := by
|
||||
grind
|
||||
|
||||
example {f : α → β} (w : ∀ x y, f x = f y → x = y) (x y : α) (h : f x = f y) : x = y := by
|
||||
grind
|
||||
|
||||
theorem map_inj_right {f : α → β} (w : ∀ x y, f x = f y → x = y) : map f l = map f l' ↔ l = l' := by
|
||||
induction l generalizing l' with grind [cases List]
|
||||
|
||||
theorem map_eq_cons_iff {f : α → β} {l : List α} :
|
||||
map f l = b :: l₂ ↔ ∃ a l₁, l = a :: l₁ ∧ f a = b ∧ map f l₁ = l₂ := by
|
||||
cases l with grind
|
||||
|
||||
theorem getLast_map {f : α → β} {l : List α} (h) :
|
||||
getLast (map f l) h = f (getLast l (by simpa using h)) := by
|
||||
cases l with grind
|
||||
|
||||
theorem getLast?_map {f : α → β} {l : List α} : (map f l).getLast? = l.getLast?.map f := by
|
||||
cases l with grind
|
||||
|
||||
/-! ### filter -/
|
||||
|
||||
theorem length_filter_eq_length_iff {l} : (filter p l).length = l.length ↔ ∀ a ∈ l, p a := by
|
||||
induction l with grind
|
||||
|
||||
theorem filterMap_length_eq_length {l} :
|
||||
(filterMap f l).length = l.length ↔ ∀ a ∈ l, (f a).isSome := by
|
||||
induction l with grind
|
||||
|
||||
theorem filterMap_eq_filter {p : α → Bool} :
|
||||
filterMap (Option.guard (p ·)) = filter p := by
|
||||
funext l
|
||||
induction l with grind
|
||||
|
||||
theorem mem_filterMap {f : α → Option β} {l : List α} {b : β} :
|
||||
b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b := by
|
||||
induction l with grind
|
||||
|
||||
theorem filterMap_eq_nil_iff {l} : filterMap f l = [] ↔ ∀ a ∈ l, f a = none := by
|
||||
constructor
|
||||
· grind
|
||||
· induction l with grind
|
||||
|
||||
/-! ### append -/
|
||||
|
||||
theorem append_of_mem {a : α} {l : List α} : a ∈ l → ∃ s t : List α, l = s ++ a :: t
|
||||
| .head l => ⟨[], l, rfl⟩
|
||||
| .tail b h => let ⟨s, t, h'⟩ := append_of_mem h; ⟨b::s, t, by grind⟩
|
||||
|
||||
theorem mem_iff_append {a : α} {l : List α} : a ∈ l ↔ ∃ s t : List α, l = s ++ a :: t :=
|
||||
⟨append_of_mem, by grind⟩
|
||||
|
||||
theorem forall_mem_append {p : α → Prop} {l₁ l₂ : List α} :
|
||||
(∀ (x) (_ : x ∈ l₁ ++ l₂), p x) ↔ (∀ (x) (_ : x ∈ l₁), p x) ∧ (∀ (x) (_ : x ∈ l₂), p x) := by
|
||||
grind
|
||||
|
||||
theorem getElem_append_right' (l₁ : List α) {l₂ : List α} {i : Nat} (hi : i < l₂.length) :
|
||||
l₂[i] = (l₁ ++ l₂)[i + l₁.length]'(by grind) := by
|
||||
grind
|
||||
|
||||
theorem getElem_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = i) :
|
||||
l[i]'(by grind) = a := by
|
||||
grind
|
||||
|
||||
theorem append_eq_append_iff {ws xs ys zs : List α} :
|
||||
ws ++ xs = ys ++ zs ↔ (∃ as, ys = ws ++ as ∧ xs = as ++ zs) ∨ ∃ bs, ws = ys ++ bs ∧ zs = bs ++ xs := by
|
||||
induction ws generalizing ys with
|
||||
| nil => grind
|
||||
| cons a as ih => cases ys with grind
|
||||
|
||||
theorem concat_append {a : α} {l₁ l₂ : List α} : concat l₁ a ++ l₂ = l₁ ++ a :: l₂ := by grind
|
||||
|
||||
theorem append_concat {a : α} {l₁ l₂ : List α} : l₁ ++ concat l₂ a = concat (l₁ ++ l₂) a := by
|
||||
grind
|
||||
|
||||
theorem map_concat {f : α → β} {a : α} {l : List α} : map f (concat l a) = concat (map f l) (f a) := by
|
||||
induction l with grind
|
||||
|
||||
/-! ### flatMap -/
|
||||
|
||||
theorem flatMap_map (f : α → β) (g : β → List γ) (l : List α) :
|
||||
(map f l).flatMap g = l.flatMap (fun a => g (f a)) := by
|
||||
induction l with grind
|
||||
|
||||
theorem flatMap_eq_foldl {f : α → List β} {l : List α} :
|
||||
l.flatMap f = l.foldl (fun acc a => acc ++ f a) [] := by
|
||||
suffices ∀ l', l' ++ l.flatMap f = l.foldl (fun acc a => acc ++ f a) l' by grind
|
||||
intro l'
|
||||
induction l generalizing l' with grind
|
||||
|
||||
/-! ### replicate -/
|
||||
|
||||
theorem getElem?_replicate : (replicate n a)[i]? = if i < n then some a else none := by
|
||||
grind
|
||||
|
||||
theorem filter_replicate : (replicate n a).filter p = if p a then replicate n a else [] := by
|
||||
cases n with grind
|
||||
|
||||
theorem filterMap_replicate {f : α → Option β} :
|
||||
(replicate n a).filterMap f = match f a with | none => [] | .some b => replicate n b := by
|
||||
induction n with grind
|
||||
|
||||
theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
|
||||
induction n with grind
|
||||
|
||||
/-! ### reverse -/
|
||||
|
||||
theorem getElem?_reverse' : ∀ {l : List α} {i j}, i + j + 1 = length l →
|
||||
l.reverse[i]? = l[j]?
|
||||
| [], _, _, _ => by grind
|
||||
| a::l, i, 0, h => by grind
|
||||
| a::l, i, j+1, h => by grind
|
||||
|
||||
theorem getElem?_reverse {l : List α} {i} (h : i < length l) :
|
||||
l.reverse[i]? = l[l.length - 1 - i]? := by grind
|
||||
|
||||
theorem getElem_reverse {l : List α} {i} (h : i < l.reverse.length) :
|
||||
l.reverse[i] = l[l.length - 1 - i]'(by grind) := by
|
||||
grind
|
||||
|
||||
theorem getLast?_reverse {l : List α} : l.reverse.getLast? = l.head? := by
|
||||
cases l with grind
|
||||
|
||||
theorem head?_reverse {l : List α} : l.reverse.head? = l.getLast? := by
|
||||
grind
|
||||
|
||||
theorem mem_of_mem_getLast? {l : List α} {a : α} (h : a ∈ getLast? l) : a ∈ l := by
|
||||
grind
|
||||
|
||||
theorem filterMap_reverse {f : α → Option β} {l : List α} : (l.reverse.filterMap f) = (l.filterMap f).reverse := by
|
||||
induction l with grind
|
||||
|
||||
/-! ### foldlM and foldrM -/
|
||||
|
||||
theorem foldlM_pure [Monad m] [LawfulMonad m] {f : β → α → β} {b : β} {l : List α} :
|
||||
l.foldlM (m := m) (pure <| f · ·) b = pure (l.foldl f b) := by
|
||||
induction l generalizing b with grind
|
||||
|
||||
theorem foldrM_pure [Monad m] [LawfulMonad m] {f : α → β → β} {b : β} {l : List α} :
|
||||
l.foldrM (m := m) (pure <| f · ·) b = pure (l.foldr f b) := by
|
||||
induction l generalizing b with grind
|
||||
|
||||
/-! ### foldl and foldr -/
|
||||
|
||||
theorem foldl_eq_foldr_reverse {l : List α} {f : β → α → β} {b : β} :
|
||||
l.foldl f b = l.reverse.foldr (fun x y => f y x) b := by grind
|
||||
|
||||
theorem foldr_eq_foldl_reverse {l : List α} {f : α → β → β} {b : β} :
|
||||
l.foldr f b = l.reverse.foldl (fun x y => f y x) b := by grind
|
||||
|
||||
theorem foldl_assoc {op : α → α → α} [ha : Std.Associative op]
|
||||
{l : List α} {a₁ a₂} : l.foldl op (op a₁ a₂) = op a₁ (l.foldl op a₂) := by
|
||||
induction l generalizing a₁ a₂ with grind
|
||||
|
||||
theorem foldl_add_const {l : List α} {a b : Nat} :
|
||||
l.foldl (fun x _ => x + a) b = b + a * l.length := by
|
||||
induction l generalizing b with grind
|
||||
|
||||
theorem foldr_add_const {l : List α} {a b : Nat} :
|
||||
l.foldr (fun _ x => x + a) b = b + a * l.length := by
|
||||
induction l generalizing b with grind
|
||||
|
||||
/-! #### Further results about `getLast` and `getLast?` -/
|
||||
|
||||
theorem head_reverse {l : List α} (h : l.reverse ≠ []) :
|
||||
l.reverse.head h = getLast l (by simp_all) := by
|
||||
induction l with grind
|
||||
|
||||
theorem mem_of_getLast? {xs : List α} {a : α} (h : xs.getLast? = some a) : a ∈ xs := by
|
||||
grind
|
||||
|
||||
theorem getLast_reverse {l : List α} (h : l.reverse ≠ []) :
|
||||
l.reverse.getLast h = l.head (by simp_all) := by
|
||||
grind
|
||||
|
||||
theorem head_eq_getLast_reverse {l : List α} (h : l ≠ []) :
|
||||
l.head h = l.reverse.getLast (by simp_all) := by
|
||||
grind
|
||||
|
||||
theorem getLast_append_of_ne_nil {l : List α} (h₁) (h₂ : l' ≠ []) :
|
||||
(l ++ l').getLast h₁ = l'.getLast h₂ := by
|
||||
grind
|
||||
|
||||
theorem getLast?_append {l l' : List α} : (l ++ l').getLast? = l'.getLast?.or l.getLast? := by
|
||||
grind
|
||||
|
||||
/-! ### leftpad -/
|
||||
|
||||
theorem leftpad_prefix {n : Nat} {a : α} {l : List α} :
|
||||
replicate (n - length l) a <+: leftpad n a l := by
|
||||
grind
|
||||
|
||||
theorem leftpad_suffix {n : Nat} {a : α} {l : List α} : l <:+ (leftpad n a l) := by
|
||||
grind
|
||||
|
||||
/-! ### elem / contains -/
|
||||
|
||||
theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true := by grind
|
||||
|
||||
theorem contains_iff_exists_mem_beq [BEq α] {l : List α} {a : α} :
|
||||
l.contains a ↔ ∃ a' ∈ l, a == a' := by
|
||||
induction l with grind
|
||||
|
||||
/-! ### dropLast -/
|
||||
|
||||
theorem length_dropLast {xs : List α} : xs.dropLast.length = xs.length - 1 := by
|
||||
induction xs with grind
|
||||
|
||||
theorem getElem_dropLast : ∀ {xs : List α} {i : Nat} (h : i < xs.dropLast.length),
|
||||
xs.dropLast[i] = xs[i]'(by grind)
|
||||
| _ :: _ :: _, 0, _ => by grind
|
||||
| _ :: _ :: _, _ + 1, h => by grind
|
||||
|
||||
theorem head?_dropLast {xs : List α} : xs.dropLast.head? = if 1 < xs.length then xs.head? else none := by
|
||||
cases xs with
|
||||
| nil => grind
|
||||
| cons x xs => cases xs with grind
|
||||
|
||||
theorem getLast?_dropLast {xs : List α} :
|
||||
xs.dropLast.getLast? = if xs.length ≤ 1 then none else xs[xs.length - 2]? := by
|
||||
grind
|
||||
|
||||
/-! ### replace -/
|
||||
section replace
|
||||
variable [BEq α]
|
||||
|
||||
theorem getElem?_replace [LawfulBEq α] {l : List α} {i : Nat} :
|
||||
(l.replace a b)[i]? = if l[i]? == some a then if a ∈ l.take i then some a else some b else l[i]? := by
|
||||
induction l generalizing i with cases i with grind
|
||||
|
||||
theorem getElem_replace [LawfulBEq α] {l : List α} {i : Nat} (h : i < l.length) :
|
||||
(l.replace a b)[i]'(by grind) = if l[i] == a then if a ∈ l.take i then a else b else l[i] := by
|
||||
grind
|
||||
|
||||
theorem head?_replace {l : List α} {a b : α} :
|
||||
(l.replace a b).head? = match l.head? with
|
||||
| none => none
|
||||
| some x => some (if a == x then b else x) := by
|
||||
cases l with grind
|
||||
|
||||
theorem replace_take {l : List α} {i : Nat} :
|
||||
(l.take i).replace a b = (l.replace a b).take i := by
|
||||
induction l generalizing i with
|
||||
| nil => grind
|
||||
| cons x xs ih => cases i with grind
|
||||
|
||||
theorem replace_replicate_ne [LawfulBEq α] {a b c : α} (h : !b == a) :
|
||||
(replicate n a).replace b c = replicate n a := by
|
||||
grind [replace_of_not_mem]
|
||||
|
||||
end replace
|
||||
|
||||
/-! ### insert -/
|
||||
|
||||
section insert
|
||||
variable [BEq α]
|
||||
|
||||
variable [LawfulBEq α]
|
||||
|
||||
theorem getElem?_insert {l : List α} {a : α} {i : Nat} :
|
||||
(l.insert a)[i]? = if a ∈ l then l[i]? else if i = 0 then some a else l[i-1]? := by
|
||||
grind
|
||||
|
||||
theorem getElem_insert {l : List α} {a : α} {i : Nat} (h : i < l.length) :
|
||||
(l.insert a)[i]'(Nat.lt_of_lt_of_le h length_le_length_insert) =
|
||||
if a ∈ l then l[i] else if i = 0 then a else l[i-1]'(Nat.lt_of_le_of_lt (Nat.pred_le _) h) := by
|
||||
grind
|
||||
|
||||
end insert
|
||||
|
||||
/-! ### any / all -/
|
||||
|
||||
theorem any_replicate {n : Nat} {a : α} :
|
||||
(replicate n a).any f = if n = 0 then false else f a := by
|
||||
cases n with grind
|
||||
|
||||
theorem all_replicate {n : Nat} {a : α} :
|
||||
(replicate n a).all f = if n = 0 then true else f a := by
|
||||
cases n with grind
|
||||
|
||||
theorem any_insert [BEq α] [LawfulBEq α] {l : List α} {a : α} :
|
||||
(l.insert a).any f = (f a || l.any f) := by
|
||||
grind
|
||||
|
||||
theorem all_insert [BEq α] [LawfulBEq α] {l : List α} {a : α} :
|
||||
(l.insert a).all f = (f a && l.all f) := by
|
||||
grind
|
||||
|
||||
end Hidden
|
||||
Loading…
Add table
Reference in a new issue