more

Author: kim-em

src/Init/Data/Array/Count.lean

@@ -52,6 +52,7 @@ theorem countP_push {a : α} {xs : Array α} : countP p (xs.push a) = countP p x
   rcases xs with ⟨xs⟩
   simp_all
 
+@[grind =]
 theorem countP_singleton {a : α} : countP p #[a] = if p a then 1 else 0 := by
   simp
 
@@ -63,6 +64,8 @@ theorem countP_eq_size_filter {xs : Array α} : countP p xs = (filter p xs).size
   rcases xs with ⟨xs⟩
   simp [List.countP_eq_length_filter]
 
+grind_pattern countP_eq_size_filter => countP p xs, filter p xs
+
 theorem countP_eq_size_filter' : countP p = size ∘ filter p := by
   funext xs
   apply countP_eq_size_filter
@@ -189,13 +192,14 @@ theorem count_le_size {a : α} {xs : Array α} : count a xs ≤ xs.size := count
 theorem count_le_count_push {a b : α} {xs : Array α} : count a xs ≤ count a (xs.push b) := by
   simp [count_push]
 
+@[grind =]
 theorem count_singleton {a b : α} : count a #[b] = if b == a then 1 else 0 := by
   simp [count_eq_countP]
 
 @[simp, grind =] theorem count_append {a : α} {xs ys : Array α} : count a (xs ++ ys) = count a xs + count a ys :=
   countP_append
 
-@[simp] theorem count_flatten {a : α} {xss : Array (Array α)} :
+@[simp, grind =] theorem count_flatten {a : α} {xss : Array (Array α)} :
     count a xss.flatten = (xss.map (count a)).sum := by
   cases xss using array₂_induction
   simp [List.count_flatten, Function.comp_def]

src/Init/Data/Array/Perm.lean

@@ -91,17 +91,26 @@ theorem Perm.mem_iff {a : α} {xs ys : Array α} (p : xs ~ ys) : a ∈ xs ↔ a
   simp only [perm_iff_toList_perm] at p
   simpa using p.mem_iff
 
+grind_pattern Perm.mem_iff => xs ~ ys, a ∈ xs
+grind_pattern Perm.mem_iff => xs ~ ys, a ∈ ys
+
 theorem Perm.append {xs ys as bs : Array α} (p₁ : xs ~ ys) (p₂ : as ~ bs) :
     xs ++ as ~ ys ++ bs := by
   cases xs; cases ys; cases as; cases bs
   simp only [append_toArray, perm_iff_toList_perm] at p₁ p₂ ⊢
   exact p₁.append p₂
 
+grind_pattern Perm.append => xs ~ ys, as ~ bs, xs ++ as
+grind_pattern Perm.append => xs ~ ys, as ~ bs, ys ++ bs
+
 theorem Perm.push (x : α) {xs ys : Array α} (p : xs ~ ys) :
     xs.push x ~ ys.push x := by
   rw [push_eq_append_singleton]
   exact p.append .rfl
 
+grind_pattern Perm.push => xs ~ ys, xs.push x
+grind_pattern Perm.push => xs ~ ys, ys.push x
+
 theorem Perm.push_comm (x y : α) {xs ys : Array α} (p : xs ~ ys) :
     (xs.push x).push y ~ (ys.push y).push x := by
   cases xs; cases ys

src/Init/Data/Array/Range.lean

@@ -128,6 +128,16 @@ theorem erase_range' :
   simp only [← List.toArray_range', List.erase_toArray]
   simp [List.erase_range']
 
+@[simp, grind =]
+theorem count_range' {a s n step} (h : 0 < step := by simp) :
+    count a (range' s n step) = if ∃ i, i < n ∧ a = s + step * i then 1 else 0 := by
+  rw [← List.toArray_range', List.count_toArray, ← List.count_range' h]
+
+@[simp, grind =]
+theorem count_range_1' {a s n} :
+    count a (range' s n) = if s ≤ a ∧ a < s + n then 1 else 0 := by
+  rw [← List.toArray_range', List.count_toArray, ← List.count_range_1']
+
 /-! ### range -/
 
 @[grind _=_]
@@ -191,6 +201,10 @@ theorem self_mem_range_succ {n : Nat} : n ∈ range (n + 1) := by simp
 theorem erase_range : (range n).erase i = range (min n i) ++ range' (i + 1) (n - (i + 1)) := by
   simp [range_eq_range', erase_range']
 
+@[simp, grind =]
+theorem count_range {a n} :
+    count a (range n) = if a < n then 1 else 0 := by
+  rw [← List.toArray_range, List.count_toArray, ← List.count_range]
 
 /-! ### zipIdx -/
 

src/Init/Data/List/Perm.lean

@@ -108,9 +108,15 @@ theorem Perm.append_left {t₁ t₂ : List α} : ∀ l : List α, t₁ ~ t₂ 
 theorem Perm.append {l₁ l₂ t₁ t₂ : List α} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) : l₁ ++ t₁ ~ l₂ ++ t₂ :=
   (p₁.append_right t₁).trans (p₂.append_left l₂)
 
+grind_pattern Perm.append => l₁ ~ l₂, t₁ ~ t₂, l₁ ++ t₁
+grind_pattern Perm.append => l₁ ~ l₂, t₁ ~ t₂, l₂ ++ t₂
+
 theorem Perm.append_cons (a : α) {l₁ l₂ r₁ r₂ : List α} (p₁ : l₁ ~ l₂) (p₂ : r₁ ~ r₂) :
     l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂ := p₁.append (p₂.cons a)
 
+grind_pattern Perm.append_cons => l₁ ~ l₂, r₁ ~ r₂, l₁ ++ a :: r₁
+grind_pattern Perm.append_cons => l₁ ~ l₂, r₁ ~ r₂, l₂ ++ a :: r₂
+
 @[simp] theorem perm_middle {a : α} : ∀ {l₁ l₂ : List α}, l₁ ++ a :: l₂ ~ a :: (l₁ ++ l₂)
   | [], _ => .refl _
   | b :: _, _ => (Perm.cons _ perm_middle).trans (swap a b _)