feat: add more lemmas about Array and List slices, support subslices (#11178)

This PR provides more lemmas about `Subarray` and `ListSlice` and it
also adds support for subslices of these two types of slices.

Author: datokrat

src/Init/Data/List/Lemmas.lean

@@ -298,6 +298,12 @@ theorem ext_getElem {l₁ l₂ : List α} (hl : length l₁ = length l₂)
       have h₁ := Nat.le_of_not_lt h₁
       rw [getElem?_eq_none h₁, getElem?_eq_none]; rwa [← hl]
 
+theorem ext_getElem_iff {l₁ l₂ : List α} :
+    l₁ = l₂ ↔ l₁.length = l₂.length ∧ ∀ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length), l₁[i]'h₁ = l₂[i]'h₂ := by
+  constructor
+  · simp +contextual
+  · exact fun h => ext_getElem h.1 h.2
+
 @[simp] theorem getElem_concat_length {l : List α} {a : α} {i : Nat} (h : i = l.length) (w) :
     (l ++ [a])[i]'w = a := by
   subst h; simp

src/Init/Data/List/Nat/TakeDrop.lean

@@ -374,6 +374,22 @@ theorem drop_take : ∀ {i j : Nat} {l : List α}, drop i (take j l) = take (j -
   rw [drop_take]
   simp
 
+@[simp]
+theorem drop_eq_drop_iff :
+    ∀ {l : List α} {i j : Nat}, l.drop i = l.drop j ↔ min i l.length = min j l.length
+  | [], i, j => by simp
+  | _ :: xs, 0, 0 => by simp
+  | x :: xs, i + 1, 0 => by
+    rw [List.ext_getElem_iff]
+    simp [succ_min_succ, show ¬ xs.length - i = xs.length + 1 by omega]
+  | x :: xs, 0, j + 1 => by
+    rw [List.ext_getElem_iff]
+    simp [succ_min_succ, show ¬ xs.length + 1 = xs.length - j by omega]
+  | x :: xs, i + 1, j + 1 => by simp [succ_min_succ, drop_eq_drop_iff]
+
+theorem drop_eq_drop_min {l : List α} {i : Nat} : l.drop i = l.drop (min i l.length) := by
+  simp
+
 theorem take_reverse {α} {xs : List α} {i : Nat} :
     xs.reverse.take i = (xs.drop (xs.length - i)).reverse := by
   by_cases h : i ≤ xs.length

src/Init/Data/Range/Polymorphic/Lemmas.lean

@@ -2846,6 +2846,7 @@ public theorem size_eq_if_rcc [LE α] [DecidableLE α] [UpwardEnumerable α]
   · split <;> simp [*]
   · rfl
 
+@[simp]
 public theorem length_toList [LE α] [DecidableLE α] [UpwardEnumerable α]
     [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
     [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] :
@@ -2864,6 +2865,7 @@ public theorem length_toList [LE α] [DecidableLE α] [UpwardEnumerable α]
         simp [h, ← ih _ h]
     · simp
 
+@[simp]
 public theorem size_toArray [LE α] [DecidableLE α] [UpwardEnumerable α]
     [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
     [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] :
@@ -2988,13 +2990,15 @@ public theorem size_eq_match_roc [LE α] [DecidableLE α] [UpwardEnumerable α]
   rw [size_eq_match_rcc]
   simp [Rcc.size_eq_if_roc]
 
+@[simp]
 public theorem length_toList [LE α] [DecidableLE α] [UpwardEnumerable α]
     [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
     [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] :
     r.toList.length = r.size := by
   simp only [toList_eq_match_rcc, size_eq_match_rcc]
   split <;> simp [Rcc.length_toList]
 
+@[simp]
 public theorem size_toArray [LE α] [DecidableLE α] [UpwardEnumerable α]
     [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
     [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] :
@@ -3094,13 +3098,15 @@ public theorem size_eq_match_roc [Least? α] [LE α] [DecidableLE α] [UpwardEnu
   rw [size_eq_match_rcc]
   simp [Rcc.size_eq_if_roc]
 
+@[simp]
 public theorem length_toList [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α]
     [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
     [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] :
     r.toList.length = r.size := by
   rw [toList_eq_match_rcc, size_eq_match_rcc]
   split <;> simp [Rcc.length_toList]
 
+@[simp]
 public theorem size_toArray [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α]
     [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
     [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] :
@@ -3223,6 +3229,7 @@ public theorem size_eq_if_rcc [LT α] [DecidableLT α] [UpwardEnumerable α]
   · split <;> simp [*]
   · rfl
 
+@[simp]
 public theorem length_toList [LT α] [DecidableLT α] [UpwardEnumerable α]
     [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] :
@@ -3241,6 +3248,7 @@ public theorem length_toList [LT α] [DecidableLT α] [UpwardEnumerable α]
         simp [h, ← ih _ h]
     · simp
 
+@[simp]
 public theorem size_toArray [LT α] [DecidableLT α] [UpwardEnumerable α]
     [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] :
@@ -3366,13 +3374,15 @@ public theorem size_eq_match_roc [LT α] [DecidableLT α] [UpwardEnumerable α]
   rw [size_eq_match_rcc]
   simp [Rco.size_eq_if_roo]
 
+@[simp]
 public theorem length_toList [LT α] [DecidableLT α] [UpwardEnumerable α]
     [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] :
     r.toList.length = r.size := by
   simp only [toList_eq_match_rco, size_eq_match_rcc]
   split <;> simp [Rco.length_toList]
 
+@[simp]
 public theorem size_toArray [LT α] [DecidableLT α] [UpwardEnumerable α]
     [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] :
@@ -3472,13 +3482,15 @@ public theorem size_eq_match_roc [Least? α] [LT α] [DecidableLT α] [UpwardEnu
   rw [size_eq_match_rcc]
   simp [Rco.size_eq_if_roo]
 
+@[simp]
 public theorem length_toList [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α]
     [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] :
     r.toList.length = r.size := by
   rw [toList_eq_match_rco, size_eq_match_rcc]
   split <;> simp [Rco.length_toList]
 
+@[simp]
 public theorem size_toArray [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α]
     [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] :
@@ -3590,6 +3602,7 @@ public theorem size_eq_match_rci [UpwardEnumerable α] [Rxi.HasSize α] [LawfulU
   simp only [Rci.size]
   split <;> simp [*]
 
+@[simp]
 public theorem length_toList [UpwardEnumerable α] [Rxi.HasSize α] [LawfulUpwardEnumerable α]
     [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] :
     r.toList.length = r.size := by
@@ -3605,6 +3618,7 @@ public theorem length_toList [UpwardEnumerable α] [Rxi.HasSize α] [LawfulUpwar
     · simp only [Nat.add_right_cancel_iff, *] at h
       simp [ih _ h, h]
 
+@[simp]
 public theorem size_toArray [UpwardEnumerable α] [Rxi.HasSize α] [LawfulUpwardEnumerable α]
     [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] :
     r.toArray.size = r.size := by
@@ -3711,12 +3725,14 @@ public theorem size_eq_match_roi [UpwardEnumerable α] [Rxi.HasSize α] [LawfulU
   rw [size_eq_match_rci]
   simp [Rci.size_eq_size_roi]
 
+@[simp]
 public theorem length_toList [UpwardEnumerable α] [Rxi.HasSize α] [LawfulUpwardEnumerable α]
     [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] :
     r.toList.length = r.size := by
   simp only [toList_eq_match_rci, size_eq_match_rci]
   split <;> simp [Rci.length_toList]
 
+@[simp]
 public theorem size_toArray [UpwardEnumerable α] [Rxi.HasSize α] [LawfulUpwardEnumerable α]
     [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] :
     r.toArray.size = r.size := by
@@ -3809,13 +3825,15 @@ public theorem size_eq_match_roi [Least? α] [UpwardEnumerable α] [Rxi.HasSize
   rw [size_eq_match_rci]
   simp [Rci.size_eq_size_roi]
 
+@[simp]
 public theorem length_toList [Least? α] [UpwardEnumerable α]
     [Rxi.HasSize α] [LawfulUpwardEnumerable α]
     [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] :
     r.toList.length = r.size := by
   rw [toList_eq_match_rci, size_eq_match_rci]
   split <;> simp [Rci.length_toList]
 
+@[simp]
 public theorem size_toArray [Least? α] [UpwardEnumerable α]
     [Rxi.HasSize α] [LawfulUpwardEnumerable α]
     [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] :

src/Init/Data/Slice/Array/Basic.lean

@@ -23,45 +23,82 @@ variable {α : Type u}
 
 instance : Rcc.Sliceable (Array α) Nat (Subarray α) where
   mkSlice xs range :=
-    let halfOpenRange := Rcc.HasRcoIntersection.intersection range 0...<xs.size
-    (xs.toSubarray halfOpenRange.lower halfOpenRange.upper)
+    xs.toSubarray range.lower (range.upper + 1)
 
 instance : Rco.Sliceable (Array α) Nat (Subarray α) where
   mkSlice xs range :=
-    let halfOpenRange := Rco.HasRcoIntersection.intersection range 0...<xs.size
-    (xs.toSubarray halfOpenRange.lower halfOpenRange.upper)
+    xs.toSubarray range.lower range.upper
 
 instance : Rci.Sliceable (Array α) Nat (Subarray α) where
   mkSlice xs range :=
     let halfOpenRange := Rci.HasRcoIntersection.intersection range 0...<xs.size
-    (xs.toSubarray halfOpenRange.lower halfOpenRange.upper)
+    xs.toSubarray halfOpenRange.lower halfOpenRange.upper
 
 instance : Roc.Sliceable (Array α) Nat (Subarray α) where
   mkSlice xs range :=
-    let halfOpenRange := Roc.HasRcoIntersection.intersection range 0...<xs.size
-    (xs.toSubarray halfOpenRange.lower halfOpenRange.upper)
+    xs.toSubarray (range.lower + 1) (range.upper + 1)
 
 instance : Roo.Sliceable (Array α) Nat (Subarray α) where
   mkSlice xs range :=
-    let halfOpenRange := Roo.HasRcoIntersection.intersection range 0...<xs.size
-    (xs.toSubarray halfOpenRange.lower halfOpenRange.upper)
+    xs.toSubarray (range.lower + 1) range.upper
 
 instance : Roi.Sliceable (Array α) Nat (Subarray α) where
   mkSlice xs range :=
     let halfOpenRange := Roi.HasRcoIntersection.intersection range 0...<xs.size
-    (xs.toSubarray halfOpenRange.lower halfOpenRange.upper)
+    xs.toSubarray halfOpenRange.lower halfOpenRange.upper
 
 instance : Ric.Sliceable (Array α) Nat (Subarray α) where
   mkSlice xs range :=
-    let halfOpenRange := Ric.HasRcoIntersection.intersection range 0...<xs.size
-    (xs.toSubarray halfOpenRange.lower halfOpenRange.upper)
+    xs.toSubarray 0 (range.upper + 1)
 
 instance : Rio.Sliceable (Array α) Nat (Subarray α) where
   mkSlice xs range :=
-    let halfOpenRange := Rio.HasRcoIntersection.intersection range 0...<xs.size
-    (xs.toSubarray halfOpenRange.lower halfOpenRange.upper)
+    xs.toSubarray 0 range.upper
 
 instance : Rii.Sliceable (Array α) Nat (Subarray α) where
   mkSlice xs _ :=
-    let halfOpenRange := 0...<xs.size
-    (xs.toSubarray halfOpenRange.lower halfOpenRange.upper)
+    xs.toSubarray 0 xs.size
+
+instance : Rcc.Sliceable (Subarray α) Nat (Subarray α) where
+  mkSlice xs range :=
+    let halfOpenRange := Rcc.HasRcoIntersection.intersection range 0...<xs.size
+    xs.array[(halfOpenRange.lower + xs.start)...(halfOpenRange.upper + xs.start)]
+
+instance : Rco.Sliceable (Subarray α) Nat (Subarray α) where
+  mkSlice xs range :=
+    let halfOpenRange := Rco.HasRcoIntersection.intersection range 0...<xs.size
+    xs.array[(halfOpenRange.lower + xs.start)...(halfOpenRange.upper + xs.start)]
+
+instance : Rci.Sliceable (Subarray α) Nat (Subarray α) where
+  mkSlice xs range :=
+    let halfOpenRange := Rci.HasRcoIntersection.intersection range 0...<xs.size
+    xs.array[(halfOpenRange.lower + xs.start)...(halfOpenRange.upper + xs.start)]
+
+instance : Roc.Sliceable (Subarray α) Nat (Subarray α) where
+  mkSlice xs range :=
+    let halfOpenRange := Roc.HasRcoIntersection.intersection range 0...<xs.size
+    xs.array[(halfOpenRange.lower + xs.start)...(halfOpenRange.upper + xs.start)]
+
+instance : Roo.Sliceable (Subarray α) Nat (Subarray α) where
+  mkSlice xs range :=
+    let halfOpenRange := Roo.HasRcoIntersection.intersection range 0...<xs.size
+    xs.array[(halfOpenRange.lower + xs.start)...(halfOpenRange.upper + xs.start)]
+
+instance : Roi.Sliceable (Subarray α) Nat (Subarray α) where
+  mkSlice xs range :=
+    let halfOpenRange := Roi.HasRcoIntersection.intersection range 0...<xs.size
+    xs.array[(halfOpenRange.lower + xs.start)...(halfOpenRange.upper + xs.start)]
+
+instance : Ric.Sliceable (Subarray α) Nat (Subarray α) where
+  mkSlice xs range :=
+    let halfOpenRange := Ric.HasRcoIntersection.intersection range 0...<xs.size
+    xs.array[(halfOpenRange.lower + xs.start)...(halfOpenRange.upper + xs.start)]
+
+instance : Rio.Sliceable (Subarray α) Nat (Subarray α) where
+  mkSlice xs range :=
+    let halfOpenRange := Rio.HasRcoIntersection.intersection range 0...<xs.size
+    xs.array[(halfOpenRange.lower + xs.start)...(halfOpenRange.upper + xs.start)]
+
+instance : Rii.Sliceable (Subarray α) Nat (Subarray α) where
+  mkSlice xs _ :=
+    xs