Merge branch 'lean-pr-testing-2688' into lean4-2679

Std/Data/Fin/Lemmas.lean

@@ -14,7 +14,8 @@ namespace Fin
 /-- If you actually have an element of `Fin n`, then the `n` is always positive -/
 theorem size_pos (i : Fin n) : 0 < n := Nat.lt_of_le_of_lt (Nat.zero_le _) i.2
 
-theorem mod_def (a m : Fin n) : a % m = Fin.mk ((a % m) % n) (Nat.mod_lt _ a.size_pos) := rfl
+theorem mod_def (a m : Fin n) : a % m = Fin.mk (a % m) (Nat.lt_of_le_of_lt (Nat.mod_le _ _) a.2) :=
+  rfl
 
 theorem mul_def (a b : Fin n) : a * b = Fin.mk ((a * b) % n) (Nat.mod_lt _ a.size_pos) := rfl
 
@@ -58,13 +59,13 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
 @[simp] theorem ofNat'_zero_val : (Fin.ofNat' 0 h).val = 0 := Nat.zero_mod _
 
 @[simp] theorem mod_val (a b : Fin n) : (a % b).val = a.val % b.val :=
-  Nat.mod_eq_of_lt (Nat.lt_of_le_of_lt (Nat.mod_le ..) a.2)
+  rfl
 
 @[simp] theorem div_val (a b : Fin n) : (a / b).val = a.val / b.val :=
-  Nat.mod_eq_of_lt (Nat.lt_of_le_of_lt (Nat.div_le_self ..) a.2)
+  rfl
 
 @[simp] theorem modn_val (a : Fin n) (b : Nat) : (a.modn b).val = a.val % b :=
-  Nat.mod_eq_of_lt (Nat.lt_of_le_of_lt (Nat.mod_le ..) a.2)
+  rfl
 
 theorem ite_val {n : Nat} {c : Prop} [Decidable c] {x : c → Fin n} (y : ¬c → Fin n) :
     (if h : c then x h else y h).val = if h : c then (x h).val else (y h).val := by

Std/Data/List/Basic.lean

@@ -1459,6 +1459,27 @@ zipRight = zipWithRight prod.mk
 -/
 @[inline] def zipRight : List α → List β → List (Option α × β) := zipWithRight Prod.mk
 
+/--
+Version of `List.zipWith` that continues to the end of both lists, passing `none` to one argument
+once the shorter list has run out.
+-/
+-- TODO We should add a tail-recursive version as we do for other `zip` functions above.
+def zipWithAll (f : Option α → Option β → γ) : List α → List β → List γ
+  | [], bs => bs.map fun b => f none (some b)
+  | a :: as, [] => (a :: as).map fun a => f (some a) none
+  | a :: as, b :: bs => f a b :: zipWithAll f as bs
+
+@[simp] theorem zipWithAll_nil_right :
+    zipWithAll f as [] = as.map fun a => f (some a) none := by
+  cases as <;> rfl
+
+@[simp] theorem zipWithAll_nil_left :
+    zipWithAll f [] bs = bs.map fun b => f none (some b) := by
+  rw [zipWithAll]
+
+@[simp] theorem zipWithAll_cons_cons :
+    zipWithAll f (a :: as) (b :: bs) = f (some a) (some b) :: zipWithAll f as bs := rfl
+
 /--
 If all elements of `xs` are `some xᵢ`, `allSome xs` returns the `xᵢ`. Otherwise
 it returns `none`.

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.2.0-rc1
+leanprover/lean4-pr-releases:pr-release-2688