simplifications of several problems

HumanEvalLean/HumanEval109.lean

@@ -5,16 +5,14 @@ section helper
 theorem Nat.lt_two_iff {n : Nat} : n < 2 ↔ n = 0 ∨ n = 1 := by
   omega
 
-theorem List.exists_mem_and {P : α → Prop} {l : List α} :
-    (∃ a, a ∈ l ∧ P a) ↔ (∃ (n : Nat), ∃ h, P (l[n]'h)) := by
-  refine ⟨fun ⟨a, h, h'⟩ => ?_, fun ⟨n, h, h'⟩ => ⟨l[n], by simp, h'⟩⟩
-  obtain ⟨i, h'', rfl⟩ := List.getElem_of_mem h
-  exact ⟨_, _, h'⟩
+theorem List.exists_mem_iff_exists_getElem (P : α → Prop) (l : List α) :
+    (∃ x ∈ l, P x) ↔ ∃ (i : Nat), ∃ hi, P (l[i]'hi) := by
+  grind [mem_iff_getElem]
 
 theorem List.sum_eq_zero {l : List Nat} : l.sum = 0 ↔
     ∀ (i : Nat) (hi : i < l.length), l[i]'hi = 0 := by
   rw [← Decidable.not_iff_not]
-  simp [← Nat.pos_iff_ne_zero, Nat.sum_pos_iff_exists_pos, List.exists_mem_and]
+  simp [← Nat.pos_iff_ne_zero, Nat.sum_pos_iff_exists_pos, List.exists_mem_iff_exists_getElem]
 
 theorem List.sum_eq_one_iff {l : List Nat} : l.sum = 1 ↔ ∃ (i : Nat) (hi : i < l.length),
     l[i] = 1 ∧ ∀ (j : Nat) (hj : j < l.length), i ≠ j → l[j] = 0 := by

HumanEvalLean/HumanEval110.lean

@@ -83,30 +83,11 @@ public theorem isExchangePossible_eq_yes_or_no {xs ys : Array Int} :
     isExchangePossible xs ys = "YES" ∨ isExchangePossible xs ys = "NO" := by
   grind [isExchangePossible]
 
-@[grind =]
-public theorem List.countP_add_countP_not {xs : List Int} P :
-    xs.countP P + xs.countP (! P ·) = xs.length := by
-  induction xs <;> grind
-
-@[grind =]
-public theorem Vector.countP_add_countP_not {xs : Vector Int m} {P} :
-    xs.countP P + xs.countP (! P ·) = m := by
-  simp only [← Vector.countP_toList]
-  grind
-
 public theorem VectorPair.countP_le_countP_iff_size_le_countP {p : VectorPair m n} :
     p.1.countP (· % 2 == 1) ≤ p.2.countP (· % 2 == 0) ↔
       m ≤ p.concat.countP (· %  2 == 0) := by
-  conv => rhs; lhs; rw [← Vector.countP_add_countP_not (xs := p.1) (P := (· % 2 == 1))]
-  have : ∀ x : Int, (x % 2 == 0) = (! x % 2 == 1) := by grind
-  simp only [this, VectorPair.concat, Vector.countP_append]
-  grind
-
-@[grind .]
-public theorem Vector.Perm.countP_eq {xs ys : Vector α n} {P}
-    (h : Vector.Perm xs ys) : xs.countP P = ys.countP P := by
-  simp only [Vector.countP, ← Array.countP_toList, Vector.toList_toArray]
-  grind [List.Perm.countP_eq, Array.Perm.toList, Vector.Perm.toArray]
+  simp only [Vector.size_eq_countP_add_countP (xs := p.1) (p := (· % 2 == 0))]
+  grind [VectorPair.concat]
 
 public theorem VectorPair.countP_le_countP_iff_exists {p : VectorPair m n} :
     p.1.countP (· % 2 == 1) ≤ p.2.countP (· % 2 == 0) ↔
@@ -142,7 +123,9 @@ public theorem VectorPair.countP_le_countP_iff_exists {p : VectorPair m n} :
       · simp only [Vector.all_eq_true, beq_iff_eq] at hes
         rw [Vector.forall_mem_iff_forall_getElem]
         grind
-    grind
+    -- Alternatively to the following, we could add `Vector.Perm.countP_eq` and use
+    -- `grind [Vector.Perm.countP_eq]`.
+    grind [List.Perm.countP_eq, Vector.Perm.toList, =_ Vector.countP_toList]
 
 public theorem isExchangePossible_correct {xs ys : Array Int} :
     isExchangePossible xs ys = "YES" ↔
@@ -151,9 +134,8 @@ public theorem isExchangePossible_correct {xs ys : Array Int} :
   generalize h : VectorPair.mk xs.toVector ys.toVector = p
   simp only [show xs = p.1.toArray by grind, show ys = p.2.toArray by grind]
   -- prove the actual statement
-  simp only [isExchangePossible, ← Std.Iter.length_toList_eq_count, Std.Iter.toList_filter,
-    Array.toList_iter, ← List.countP_eq_length_filter]
-  grind [VectorPair.countP_le_countP_iff_exists, List.countP_eq_length_filter]
+  simp [isExchangePossible, ← Std.Iter.length_toList_eq_count,
+    ← List.countP_eq_length_filter, VectorPair.countP_le_countP_iff_exists]
 
 /-!
 ## Prompt

HumanEvalLean/HumanEval114.lean

@@ -6,14 +6,6 @@ set_option mvcgen.warning false
 ## Implementation
 -/
 
-@[grind]
-def Array.minD [Min α] (xs : Array α) (fallback : α) : α :=
-  xs.toList.min?.getD fallback
-
-@[grind]
-def List.minD [Min α] (xs : List α) (fallback : α) : α :=
-  xs.min?.getD fallback
-
 def minSubarraySum (xs : Array Int) : Int := Id.run do
   let mut minSum := 0
   let mut s := 0
@@ -23,7 +15,7 @@ def minSubarraySum (xs : Array Int) : Int := Id.run do
   if minSum < 0 then
       return minSum
   else
-      return xs.minD 0
+      return xs.toList.min?.getD 0
 
 /-!
 ## Tests
@@ -56,16 +48,6 @@ example : minSubarraySum #[] = 0 := by decide
 attribute [grind =] List.toList_mkSlice_rco List.toList_mkSlice_rci List.le_min_iff
 attribute [grind →] List.mem_of_mem_take List.mem_of_mem_drop
 
-@[simp, grind =]
-theorem Array.minD_empty [Min α] {fallback : α} :
-    (#[] : Array α).minD fallback = fallback := by
-  simp [Array.minD]
-
-@[simp, grind =]
-theorem List.minD_nil [Min α] {fallback : α} :
-    ([] : List α).minD fallback = fallback := by
-  simp [List.minD]
-
 @[simp, grind =]
 theorem List.sum_append_int {l₁ l₂ : List Int} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
   induction l₁ generalizing l₂ <;> simp_all [Int.add_assoc]
@@ -205,23 +187,16 @@ theorem List.length_mul_le_sum {xs : List Int} {m : Int} (h : ∀ x, x ∈ xs 
     simp only [mem_cons, forall_eq_or_imp, length_cons] at *
     grind
 
-theorem this_should_not_be_so_hard (a : Int) (b : Nat) (h : 0 ≤ a) (h' : 0 < b) :
-    a ≤ b * a := by
-  match b with
-  | 0 => grind
-  | b + 1 =>
-    induction b <;> grind
-
 @[grind →, grind <=]
 theorem isMinSubarraySum_of_nonneg {xs : List Int} {minSum : Int}
     (h : IsMinSubarraySum₀ xs minSum)  (hs : minSum ≥ 0) :
-    IsMinSubarraySum xs (xs.minD 0) := by
+    IsMinSubarraySum xs (xs.min?.getD 0) := by
   rw [IsMinSubarraySum]
   split
   · simp [*]
   · have : minSum = 0 := by grind
     have := this
-    rw [List.minD, List.min?_eq_some_min (by grind), Option.getD_some]
+    rw [List.min?_eq_some_min (by grind), Option.getD_some]
     have hmin : xs.min (by grind) = xs.min (by grind) := rfl
     rw [List.min_eq_iff, List.mem_iff_getElem] at hmin
     have : 0 ≤ xs.min (by grind) := by
@@ -238,8 +213,8 @@ theorem isMinSubarraySum_of_nonneg {xs : List Int} {minSum : Int}
       have := List.length_mul_le_sum this
       simp only [List.toList_mkSlice_rco, *]
       refine Int.le_trans ?_ this
-      simp only [List.length_drop, List.length_take]
-      apply this_should_not_be_so_hard <;> grind
+      rw (occs := [1]) [show ∀ h, xs.min h = 1 * xs.min h by grind]
+      apply Int.mul_le_mul <;> grind
 
 /-!
 ### Final theorems

HumanEvalLean/HumanEval115.lean

@@ -58,23 +58,10 @@ theorem Nat.div_add_div_le_add_div (a b c : Nat) : a / c + b / c ≤ (a + b) / c
     · apply Nat.mod_le
   · grind
 
-theorem Nat.le_add_sub_one_div (a b : Nat) (hb : b > 0) :
-    a ≤ (a + b - 1) / b * b := by
-  have := Nat.div_add_mod' a b |>.symm
-  rw [this, Nat.add_sub_assoc hb, Nat.add_assoc]
-  refine Nat.le_trans (m := a / b * b / b * b + (a % b + (b - 1)) / b * b) ?_ ?_
-  · rw [Nat.mul_div_cancel _ hb, Nat.add_le_add_iff_left]
-    by_cases h : a % b = 0
-    · grind
-    · have : b ≤ a % b + (b - 1) := by grind
-      have : b ≤ (a % b + (b - 1)) / b * b := by
-        apply Nat.le_mul_of_pos_left
-        exact Nat.div_pos this hb
-      have : a % b < b := by exact Nat.mod_lt a hb
-      grind
-  · rw [← Nat.add_mul]
-    apply Nat.mul_le_mul_right
-    apply Nat.div_add_div_le_add_div
+theorem Nat.le_mul_iff_le_left (hc : 0 < z) :
+    x ≤ y * z ↔ (x + z - 1) / z ≤ y := by
+  rw [Nat.div_le_iff_le_mul hc]
+  omega
 
 @[simp, grind =]
 theorem Vector.sum_toList {xs : Vector Nat α} :
@@ -93,16 +80,14 @@ theorem Vector.toList_zip {as : Vector α n} {bs : Vector β n} :
   rcases bs with ⟨bs, h⟩
   simp
 
-theorem List.exists_mem_and {P : α → Prop} {l : List α} :
-    (∃ a, a ∈ l ∧ P a) ↔ (∃ (n : Nat), ∃ h, P (l[n]'h)) := by
-  refine ⟨fun ⟨a, h, h'⟩ => ?_, fun ⟨n, h, h'⟩ => ⟨l[n], by simp, h'⟩⟩
-  obtain ⟨i, h'', rfl⟩ := List.getElem_of_mem h
-  exact ⟨_, _, h'⟩
+theorem List.exists_mem_iff_exists_getElem (P : α → Prop) (l : List α) :
+    (∃ x ∈ l, P x) ↔ ∃ (i : Nat), ∃ hi, P (l[i]'hi) := by
+  grind [mem_iff_getElem]
 
 theorem List.sum_eq_zero {l : List Nat} : l.sum = 0 ↔
     ∀ (i : Nat) (hi : i < l.length), l[i] = 0 := by
   rw [← Decidable.not_iff_not]
-  simp [← Nat.pos_iff_ne_zero, Nat.sum_pos_iff_exists_pos, List.exists_mem_and]
+  simp [← Nat.pos_iff_ne_zero, Nat.sum_pos_iff_exists_pos, List.exists_mem_iff_exists_getElem]
 
 theorem Vector.sum_eq_zero {xs : Vector Nat n} : xs.sum = 0 ↔ ∀ (i : Nat) (hi : i < n), xs[i] = 0 := by
   rw [← Vector.sum_toList, List.sum_eq_zero]
@@ -350,8 +335,8 @@ theorem isEmpty_apply_optimalAbstractActions {well : AbstractWell} {c : Nat} (hc
     ((optimalAbstractActions well c).foldr (init := well) AbstractWellAction.apply).IsEmpty := by
   rw [AbstractWellAction.apply_list]
   simp [AbstractWell.IsEmpty, optimalAbstractActions, Nat.sub_eq_zero_iff_le]
-  apply Nat.le_add_sub_one_div
-  exact hc
+  rw [Nat.le_mul_iff_le_left hc]
+  apply Nat.le_refl
 
 theorem minimalAbstractWellActions {well : AbstractWell} {c : Nat} (hc : 0 < c) :
     MinimalAbstractWellActions well c ((well.totalWater + c - 1) / c) := by

HumanEvalLean/HumanEval116.lean

@@ -45,4 +45,4 @@ def check(candidate):
     assert True, "This prints if this assert fails 2 (also good for debugging!)"
 
 ```
--/
+-/