feat: add grind annotations for list and array slices (#11993)
This PR adds `grind` annotations to the lemmas about `Subarray` and `ListSlice`.
This commit is contained in:
Paul Reichert
GitHub
parent
196cdb6039
commit
4af9cc0592
4 changed files with 221 additions and 53 deletions
|
|
@ -148,6 +148,7 @@ theorem Subarray.copy_eq_toArray {s : Subarray α} :
|
|||
s.copy = s.toArray :=
|
||||
(rfl)
|
||||
|
||||
@[grind =]
|
||||
theorem Subarray.sliceToArray_eq_toArray {s : Subarray α} :
|
||||
Slice.toArray s = s.toArray :=
|
||||
(rfl)
|
||||
|
|
|
|||
|
|
@ -119,6 +119,13 @@ public theorem forIn_toList {α : Type u} {s : Subarray α}
|
|||
ForIn.forIn s.toList init f = ForIn.forIn s init f :=
|
||||
Slice.forIn_toList
|
||||
|
||||
@[grind =]
|
||||
public theorem forIn_eq_forIn_toList {α : Type u} {s : Subarray α}
|
||||
{m : Type v → Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ}
|
||||
{f : α → γ → m (ForInStep γ)} :
|
||||
ForIn.forIn s init f = ForIn.forIn s.toList init f :=
|
||||
forIn_toList.symm
|
||||
|
||||
@[simp]
|
||||
public theorem forIn_toArray {α : Type u} {s : Subarray α}
|
||||
{m : Type v → Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ}
|
||||
|
|
@ -167,22 +174,22 @@ public theorem Array.toSubarray_eq_min {xs : Array α} {lo hi : Nat} :
|
|||
simp only [Array.toSubarray]
|
||||
split <;> split <;> simp [Nat.min_eq_right (Nat.le_of_not_ge _), *]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem Array.array_toSubarray {xs : Array α} {lo hi : Nat} :
|
||||
(xs.toSubarray lo hi).array = xs := by
|
||||
simp [toSubarray_eq_min, Subarray.array]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem Array.start_toSubarray {xs : Array α} {lo hi : Nat} :
|
||||
(xs.toSubarray lo hi).start = min lo (min hi xs.size) := by
|
||||
simp [toSubarray_eq_min, Subarray.start]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem Array.stop_toSubarray {xs : Array α} {lo hi : Nat} :
|
||||
(xs.toSubarray lo hi).stop = min hi xs.size := by
|
||||
simp [toSubarray_eq_min, Subarray.stop]
|
||||
|
||||
theorem Subarray.toList_eq {xs : Subarray α} :
|
||||
public theorem Subarray.toList_eq {xs : Subarray α} :
|
||||
xs.toList = (xs.array.extract xs.start xs.stop).toList := by
|
||||
let aslice := xs
|
||||
obtain ⟨⟨array, start, stop, h₁, h₂⟩⟩ := xs
|
||||
|
|
@ -199,45 +206,46 @@ theorem Subarray.toList_eq {xs : Subarray α} :
|
|||
simp [Subarray.array, Subarray.start, Subarray.stop]
|
||||
simp [this, ListSlice.toList_eq, lslice]
|
||||
|
||||
@[grind =]
|
||||
public theorem Subarray.size_eq {xs : Subarray α} :
|
||||
xs.size = xs.stop - xs.start := by
|
||||
simp [Subarray.size]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem Subarray.toArray_toList {xs : Subarray α} :
|
||||
xs.toList.toArray = xs.toArray := by
|
||||
simp [Std.Slice.toList, Subarray.toArray, Std.Slice.toArray]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem Subarray.toList_toArray {xs : Subarray α} :
|
||||
xs.toArray.toList = xs.toList := by
|
||||
simp [Std.Slice.toList, Subarray.toArray, Std.Slice.toArray]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem Subarray.length_toList {xs : Subarray α} :
|
||||
xs.toList.length = xs.size := by
|
||||
have : xs.start ≤ xs.stop := xs.internalRepresentation.start_le_stop
|
||||
have : xs.stop ≤ xs.array.size := xs.internalRepresentation.stop_le_array_size
|
||||
simp [Subarray.toList_eq, Subarray.size]; omega
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem Subarray.size_toArray {xs : Subarray α} :
|
||||
xs.toArray.size = xs.size := by
|
||||
simp [← Subarray.toArray_toList, Subarray.size, Slice.size, SliceSize.size, start, stop]
|
||||
|
||||
namespace Array
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem array_mkSlice_rco {xs : Array α} {lo hi : Nat} :
|
||||
xs[lo...hi].array = xs := by
|
||||
simp [Std.Rco.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem start_mkSlice_rco {xs : Array α} {lo hi : Nat} :
|
||||
xs[lo...hi].start = min lo (min hi xs.size) := by
|
||||
simp [Std.Rco.Sliceable.mkSlice]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem stop_mkSlice_rco {xs : Array α} {lo hi : Nat} :
|
||||
xs[lo...hi].stop = min hi xs.size := by
|
||||
simp [Std.Rco.Sliceable.mkSlice]
|
||||
|
|
@ -246,14 +254,14 @@ public theorem mkSlice_rco_eq_mkSlice_rco_min {xs : Array α} {lo hi : Nat} :
|
|||
xs[lo...hi] = xs[(min lo (min hi xs.size))...(min hi xs.size)] := by
|
||||
simp [Std.Rco.Sliceable.mkSlice, Array.toSubarray_eq_min]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem toList_mkSlice_rco {xs : Array α} {lo hi : Nat} :
|
||||
xs[lo...hi].toList = (xs.toList.take hi).drop lo := by
|
||||
rw [List.take_eq_take_min, List.drop_eq_drop_min]
|
||||
simp [Std.Rco.Sliceable.mkSlice, Subarray.toList_eq, List.take_drop,
|
||||
Nat.add_sub_of_le (Nat.min_le_right _ _)]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem toArray_mkSlice_rco {xs : Array α} {lo hi : Nat} :
|
||||
xs[lo...hi].toArray = xs.extract lo hi := by
|
||||
simp only [← Subarray.toArray_toList, toList_mkSlice_rco]
|
||||
|
|
@ -266,12 +274,12 @@ public theorem toArray_mkSlice_rco {xs : Array α} {lo hi : Nat} :
|
|||
· simp; omega
|
||||
· simp; omega
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem size_mkSlice_rco {xs : Array α} {lo hi : Nat} :
|
||||
xs[lo...hi].size = min hi xs.size - lo := by
|
||||
simp [← Subarray.length_toList]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_rcc_eq_mkSlice_rco {xs : Array α} {lo hi : Nat} :
|
||||
xs[lo...=hi] = xs[lo...(hi + 1)] := by
|
||||
simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
|
||||
|
|
@ -280,7 +288,7 @@ public theorem mkSlice_rcc_eq_mkSlice_rco_min {xs : Array α} {lo hi : Nat} :
|
|||
xs[lo...=hi] = xs[(min lo (min (hi + 1) xs.size))...(min (hi + 1) xs.size)] := by
|
||||
simp [mkSlice_rco_eq_mkSlice_rco_min]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem array_mkSlice_rcc {xs : Array α} {lo hi : Nat} :
|
||||
xs[lo...=hi].array = xs := by
|
||||
simp [Std.Rcc.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
|
||||
|
|
@ -325,7 +333,7 @@ public theorem stop_mkSlice_rci {xs : Array α} {lo : Nat} :
|
|||
xs[lo...*].stop = xs.size := by
|
||||
simp [Std.Rci.Sliceable.mkSlice, Std.Rci.HasRcoIntersection.intersection]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_rci_eq_mkSlice_rco {xs : Array α} {lo : Nat} :
|
||||
xs[lo...*] = xs[lo...xs.size] := by
|
||||
simp [Std.Rci.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice, Std.Rci.HasRcoIntersection.intersection]
|
||||
|
|
@ -344,7 +352,7 @@ public theorem toArray_mkSlice_rci {xs : Array α} {lo : Nat} :
|
|||
xs[lo...*].toArray = xs.extract lo := by
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem size_mkSlice_rci {xs : Array α} {lo : Nat} :
|
||||
xs[lo...*].size = xs.size - lo := by
|
||||
simp [← Subarray.length_toList]
|
||||
|
|
@ -364,7 +372,7 @@ public theorem stop_mkSlice_roo {xs : Array α} {lo hi : Nat} :
|
|||
xs[lo<...hi].stop = min hi xs.size := by
|
||||
simp [Std.Roo.Sliceable.mkSlice]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_roo_eq_mkSlice_rco {xs : Array α} {lo hi : Nat} :
|
||||
xs[lo<...hi] = xs[(lo + 1)...hi] := by
|
||||
simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
|
||||
|
|
@ -408,6 +416,11 @@ public theorem mkSlice_roc_eq_mkSlice_roo {xs : Array α} {lo hi : Nat} :
|
|||
xs[lo<...=hi] = xs[lo<...(hi + 1)] := by
|
||||
simp [Std.Roc.Sliceable.mkSlice, Std.Roo.Sliceable.mkSlice]
|
||||
|
||||
@[grind =]
|
||||
public theorem mkSlice_roc_eq_mkSlice_rco {xs : Array α} {lo hi : Nat} :
|
||||
xs[lo<...=hi] = xs[(lo + 1)...(hi + 1)] := by
|
||||
simp
|
||||
|
||||
public theorem mkSlice_roc_eq_mkSlice_roo_min {xs : Array α} {lo hi : Nat} :
|
||||
xs[lo<...=hi] = xs[(min (lo + 1) (min (hi + 1) xs.size))...(min (hi + 1) xs.size)] := by
|
||||
simp [mkSlice_rco_eq_mkSlice_rco_min]
|
||||
|
|
@ -452,6 +465,11 @@ public theorem mkSlice_roi_eq_mkSlice_roo {xs : Array α} {lo : Nat} :
|
|||
xs[lo<...*] = xs[lo<...xs.size] := by
|
||||
simp [mkSlice_rci_eq_mkSlice_rco]
|
||||
|
||||
@[grind =]
|
||||
public theorem mkSlice_roi_eq_mkSlice_rco {xs : Array α} {lo : Nat} :
|
||||
xs[lo<...*] = xs[(lo + 1)...xs.size] := by
|
||||
simp [mkSlice_rci_eq_mkSlice_rco]
|
||||
|
||||
public theorem mkSlice_roi_eq_mkSlice_roo_min {xs : Array α} {lo : Nat} :
|
||||
xs[lo<...*] = xs[(min (lo + 1) xs.size)...xs.size] := by
|
||||
simp [mkSlice_rco_eq_mkSlice_rco_min]
|
||||
|
|
@ -476,7 +494,7 @@ public theorem array_mkSlice_rio {xs : Array α} {hi : Nat} :
|
|||
xs[*...hi].array = xs := by
|
||||
simp [Std.Rio.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem start_mkSlice_rio {xs : Array α} {hi : Nat} :
|
||||
xs[*...hi].start = 0 := by
|
||||
simp [Std.Rio.Sliceable.mkSlice]
|
||||
|
|
@ -486,7 +504,7 @@ public theorem stop_mkSlice_rio {xs : Array α} {hi : Nat} :
|
|||
xs[*...hi].stop = min hi xs.size := by
|
||||
simp [Std.Rio.Sliceable.mkSlice]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_rio_eq_mkSlice_rco {xs : Array α} {hi : Nat} :
|
||||
xs[*...hi] = xs[0...hi] := by
|
||||
simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
|
||||
|
|
@ -515,7 +533,7 @@ public theorem array_mkSlice_ric {xs : Array α} {hi : Nat} :
|
|||
xs[*...=hi].array = xs := by
|
||||
simp [Std.Ric.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem start_mkSlice_ric {xs : Array α} {hi : Nat} :
|
||||
xs[*...=hi].start = 0 := by
|
||||
simp [Std.Ric.Sliceable.mkSlice]
|
||||
|
|
@ -530,6 +548,11 @@ public theorem mkSlice_ric_eq_mkSlice_rio {xs : Array α} {hi : Nat} :
|
|||
xs[*...=hi] = xs[*...(hi + 1)] := by
|
||||
simp [Std.Ric.Sliceable.mkSlice, Std.Rio.Sliceable.mkSlice]
|
||||
|
||||
@[grind =]
|
||||
public theorem mkSlice_ric_eq_mkSlice_rco {xs : Array α} {hi : Nat} :
|
||||
xs[*...=hi] = xs[0...(hi + 1)] := by
|
||||
simp
|
||||
|
||||
public theorem mkSlice_ric_eq_mkSlice_rio_min {xs : Array α} {hi : Nat} :
|
||||
xs[*...=hi] = xs[*...(min (hi + 1) xs.size)] := by
|
||||
simp [mkSlice_rco_eq_mkSlice_rco_min]
|
||||
|
|
@ -559,11 +582,16 @@ public theorem mkSlice_rii_eq_mkSlice_rio {xs : Array α} :
|
|||
xs[*...*] = xs[*...xs.size] := by
|
||||
simp [mkSlice_rci_eq_mkSlice_rco]
|
||||
|
||||
@[grind =]
|
||||
public theorem mkSlice_rii_eq_mkSlice_rco {xs : Array α} :
|
||||
xs[*...*] = xs[0...xs.size] := by
|
||||
simp
|
||||
|
||||
public theorem mkSlice_rii_eq_mkSlice_rio_min {xs : Array α} :
|
||||
xs[*...*] = xs[*...xs.size] := by
|
||||
simp [mkSlice_rco_eq_mkSlice_rco_min]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem toList_mkSlice_rii {xs : Array α} :
|
||||
xs[*...*].toList = xs.toList := by
|
||||
rw [mkSlice_rii_eq_mkSlice_rci, toList_mkSlice_rci, List.drop_zero]
|
||||
|
|
@ -573,7 +601,7 @@ public theorem toArray_mkSlice_rii {xs : Array α} :
|
|||
xs[*...*].toArray = xs := by
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem size_mkSlice_rii {xs : Array α} :
|
||||
xs[*...*].size = xs.size := by
|
||||
simp [← Subarray.length_toList]
|
||||
|
|
@ -583,12 +611,12 @@ public theorem array_mkSlice_rii {xs : Array α} :
|
|||
xs[*...*].array = xs := by
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem start_mkSlice_rii {xs : Array α} :
|
||||
xs[*...*].start = 0 := by
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem stop_mkSlice_rii {xs : Array α} :
|
||||
xs[*...*].stop = xs.size := by
|
||||
simp [Std.Rii.Sliceable.mkSlice]
|
||||
|
|
@ -599,7 +627,7 @@ section SubarraySlices
|
|||
|
||||
namespace Subarray
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem toList_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
|
||||
xs[lo...hi].toList = (xs.toList.take hi).drop lo := by
|
||||
simp only [Std.Rco.Sliceable.mkSlice, Std.Rco.HasRcoIntersection.intersection, toList_eq,
|
||||
|
|
@ -608,12 +636,12 @@ public theorem toList_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
|
|||
rw [Nat.add_sub_cancel' (by omega)]
|
||||
simp [Subarray.size, ← Array.length_toList, ← List.take_eq_take_min, Nat.add_comm xs.start]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem toArray_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
|
||||
xs[lo...hi].toArray = xs.toArray.extract lo hi := by
|
||||
simp [← Subarray.toArray_toList, List.drop_take]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_rcc_eq_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
|
||||
xs[lo...=hi] = xs[lo...(hi + 1)] := by
|
||||
simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
|
||||
|
|
@ -629,7 +657,7 @@ public theorem toArray_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} :
|
|||
xs[lo...=hi].toArray = xs.toArray.extract lo (hi + 1) := by
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_rci_eq_mkSlice_rco {xs : Subarray α} {lo : Nat} :
|
||||
xs[lo...*] = xs[lo...xs.size] := by
|
||||
simp [Std.Rci.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
|
||||
|
|
@ -651,12 +679,17 @@ public theorem mkSlice_roc_eq_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
|
|||
simp [Std.Roc.Sliceable.mkSlice, Std.Roo.Sliceable.mkSlice,
|
||||
Std.Roc.HasRcoIntersection.intersection, Std.Roo.HasRcoIntersection.intersection]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_roo_eq_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
|
||||
xs[lo<...hi] = xs[(lo + 1)...hi] := by
|
||||
simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
|
||||
Std.Roo.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection]
|
||||
|
||||
@[grind =]
|
||||
public theorem mkSlice_roc_eq_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
|
||||
xs[lo<...=hi] = xs[(lo + 1)...(hi + 1)] := by
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
public theorem toList_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
|
||||
xs[lo<...hi].toList = (xs.toList.take hi).drop (lo + 1) := by
|
||||
|
|
@ -670,8 +703,7 @@ public theorem toArray_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
|
|||
@[simp]
|
||||
public theorem mkSlice_roc_eq_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} :
|
||||
xs[lo<...=hi] = xs[(lo + 1)...=hi] := by
|
||||
simp [Std.Roc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
|
||||
Std.Roc.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
public theorem toList_mkSlice_roc {xs : Subarray α} {lo hi : Nat} :
|
||||
|
|
@ -689,6 +721,11 @@ public theorem mkSlice_roi_eq_mkSlice_rci {xs : Subarray α} {lo : Nat} :
|
|||
simp [Std.Roi.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice,
|
||||
Std.Roi.HasRcoIntersection.intersection, Std.Rci.HasRcoIntersection.intersection]
|
||||
|
||||
@[grind =]
|
||||
public theorem mkSlice_roi_eq_mkSlice_rco {xs : Subarray α} {lo : Nat} :
|
||||
xs[lo<...*] = xs[(lo + 1)...xs.size] := by
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
public theorem toList_mkSlice_roi {xs : Subarray α} {lo : Nat} :
|
||||
xs[lo<...*].toList = xs.toList.drop (lo + 1) := by
|
||||
|
|
@ -705,12 +742,17 @@ public theorem mkSlice_ric_eq_mkSlice_rio {xs : Subarray α} {hi : Nat} :
|
|||
simp [Std.Ric.Sliceable.mkSlice, Std.Rio.Sliceable.mkSlice,
|
||||
Std.Ric.HasRcoIntersection.intersection, Std.Rio.HasRcoIntersection.intersection]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_rio_eq_mkSlice_rco {xs : Subarray α} {hi : Nat} :
|
||||
xs[*...hi] = xs[0...hi] := by
|
||||
simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
|
||||
Std.Rio.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection]
|
||||
|
||||
@[grind =]
|
||||
public theorem mkSlice_ric_eq_mkSlice_rco {xs : Subarray α} {hi : Nat} :
|
||||
xs[*...=hi] = xs[0...(hi + 1)] := by
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
public theorem toList_mkSlice_rio {xs : Subarray α} {hi : Nat} :
|
||||
xs[*...hi].toList = xs.toList.take hi := by
|
||||
|
|
@ -737,7 +779,7 @@ public theorem toArray_mkSlice_ric {xs : Subarray α} {hi : Nat} :
|
|||
xs[*...=hi].toArray = xs.toArray.extract 0 (hi + 1) := by
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_rii {xs : Subarray α} :
|
||||
xs[*...*] = xs := by
|
||||
simp [Std.Rii.Sliceable.mkSlice]
|
||||
|
|
|
|||
|
|
@ -47,21 +47,28 @@ public theorem toList_eq {xs : ListSlice α} :
|
|||
simp only [Std.Slice.toList, toList_internalIter]
|
||||
rfl
|
||||
|
||||
@[simp, grind =]
|
||||
public theorem toArray_toList {xs : ListSlice α} :
|
||||
xs.toList.toArray = xs.toArray := by
|
||||
simp [Std.Slice.toArray, Std.Slice.toList]
|
||||
|
||||
@[simp, grind =]
|
||||
public theorem toList_toArray {xs : ListSlice α} :
|
||||
xs.toArray.toList = xs.toList := by
|
||||
simp [Std.Slice.toArray, Std.Slice.toList]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem length_toList {xs : ListSlice α} :
|
||||
xs.toList.length = xs.size := by
|
||||
simp [ListSlice.toList_eq, Std.Slice.size, Std.Slice.SliceSize.size, ← Iter.length_toList_eq_count,
|
||||
toList_internalIter]; rfl
|
||||
|
||||
@[simp]
|
||||
@[grind =]
|
||||
public theorem size_eq_length_toList {xs : ListSlice α} :
|
||||
xs.size = xs.toList.length :=
|
||||
length_toList.symm
|
||||
|
||||
@[simp, grind =]
|
||||
public theorem size_toArray {xs : ListSlice α} :
|
||||
xs.toArray.size = xs.size := by
|
||||
simp [← ListSlice.toArray_toList]
|
||||
|
|
@ -70,7 +77,7 @@ end ListSlice
|
|||
|
||||
namespace List
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem toList_mkSlice_rco {xs : List α} {lo hi : Nat} :
|
||||
xs[lo...hi].toList = (xs.take hi).drop lo := by
|
||||
rw [List.take_eq_take_min, List.drop_eq_drop_min]
|
||||
|
|
@ -81,17 +88,17 @@ public theorem toList_mkSlice_rco {xs : List α} {lo hi : Nat} :
|
|||
· have : min hi xs.length ≤ lo := by omega
|
||||
simp [h, Nat.min_eq_right this]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem toArray_mkSlice_rco {xs : List α} {lo hi : Nat} :
|
||||
xs[lo...hi].toArray = ((xs.take hi).drop lo).toArray := by
|
||||
simp [← ListSlice.toArray_toList]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem size_mkSlice_rco {xs : List α} {lo hi : Nat} :
|
||||
xs[lo...hi].size = min hi xs.length - lo := by
|
||||
simp [← ListSlice.length_toList]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_rcc_eq_mkSlice_rco {xs : List α} {lo hi : Nat} :
|
||||
xs[lo...=hi] = xs[lo...(hi + 1)] := by
|
||||
simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
|
||||
|
|
@ -122,12 +129,22 @@ public theorem toArray_mkSlice_rci {xs : List α} {lo : Nat} :
|
|||
xs[lo...*].toArray = (xs.drop lo).toArray := by
|
||||
simp [← ListSlice.toArray_toList]
|
||||
|
||||
@[grind =]
|
||||
public theorem toList_mkSlice_rci_eq_toList_mkSlice_rco {xs : List α} {lo : Nat} :
|
||||
xs[lo...*].toList = xs[lo...xs.length].toList := by
|
||||
simp
|
||||
|
||||
@[grind =]
|
||||
public theorem toArray_mkSlice_rci_eq_toArray_mkSlice_rco {xs : List α} {lo : Nat} :
|
||||
xs[lo...*].toArray = xs[lo...xs.length].toArray := by
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
public theorem size_mkSlice_rci {xs : List α} {lo : Nat} :
|
||||
xs[lo...*].size = xs.length - lo := by
|
||||
simp [← ListSlice.length_toList]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_roo_eq_mkSlice_rco {xs : List α} {lo hi : Nat} :
|
||||
xs[lo<...hi] = xs[(lo + 1)...hi] := by
|
||||
simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
|
||||
|
|
@ -152,6 +169,11 @@ public theorem mkSlice_roc_eq_mkSlice_roo {xs : List α} {lo hi : Nat} :
|
|||
xs[lo<...=hi] = xs[lo<...(hi + 1)] := by
|
||||
simp [Std.Roc.Sliceable.mkSlice, Std.Roo.Sliceable.mkSlice]
|
||||
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_roc_eq_mkSlice_rco {xs : List α} {lo hi : Nat} :
|
||||
xs[lo<...=hi] = xs[(lo + 1)...(hi + 1)] := by
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
public theorem toList_mkSlice_roc {xs : List α} {lo hi : Nat} :
|
||||
xs[lo<...=hi].toList = (xs.take (hi + 1)).drop (lo + 1) := by
|
||||
|
|
@ -167,11 +189,27 @@ public theorem size_mkSlice_roc {xs : List α} {lo hi : Nat} :
|
|||
xs[lo<...=hi].size = min (hi + 1) xs.length - (lo + 1) := by
|
||||
simp [← ListSlice.length_toList]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_roi_eq_mkSlice_rci {xs : List α} {lo : Nat} :
|
||||
xs[lo<...*] = xs[(lo + 1)...*] := by
|
||||
simp [Std.Roi.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice]
|
||||
|
||||
public theorem toList_mkSlice_roi_eq_toList_mkSlice_roo {xs : List α} {lo : Nat} :
|
||||
xs[lo<...*].toList = xs[lo<...xs.length].toList := by
|
||||
simp
|
||||
|
||||
public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_roo {xs : List α} {lo : Nat} :
|
||||
xs[lo<...*].toArray = xs[lo<...xs.length].toArray := by
|
||||
simp
|
||||
|
||||
public theorem toList_mkSlice_roi_eq_toList_mkSlice_rco {xs : List α} {lo : Nat} :
|
||||
xs[lo<...*].toList = xs[(lo + 1)...xs.length].toList := by
|
||||
simp
|
||||
|
||||
public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_rco {xs : List α} {lo : Nat} :
|
||||
xs[lo<...*].toArray = xs[(lo + 1)...xs.length].toArray := by
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
public theorem toList_mkSlice_roi {xs : List α} {lo : Nat} :
|
||||
xs[lo<...*].toList = xs.drop (lo + 1) := by
|
||||
|
|
@ -187,7 +225,7 @@ public theorem size_mkSlice_roi {xs : List α} {lo : Nat} :
|
|||
xs[lo<...*].size = xs.length - (lo + 1) := by
|
||||
simp [← ListSlice.length_toList]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_rio_eq_mkSlice_rco {xs : List α} {hi : Nat} :
|
||||
xs[*...hi] = xs[0...hi] := by
|
||||
simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
|
||||
|
|
@ -212,6 +250,11 @@ public theorem mkSlice_ric_eq_mkSlice_rio {xs : List α} {hi : Nat} :
|
|||
xs[*...=hi] = xs[*...(hi + 1)] := by
|
||||
simp [Std.Ric.Sliceable.mkSlice, Std.Rio.Sliceable.mkSlice]
|
||||
|
||||
@[grind =]
|
||||
public theorem mkSlice_ric_eq_mkSlice_rco {xs : List α} {hi : Nat} :
|
||||
xs[*...=hi] = xs[0...(hi + 1)] := by
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
public theorem toList_mkSlice_ric {xs : List α} {hi : Nat} :
|
||||
xs[*...=hi].toList = xs.take (hi + 1) := by
|
||||
|
|
@ -227,11 +270,19 @@ public theorem size_mkSlice_ric {xs : List α} {hi : Nat} :
|
|||
xs[*...=hi].size = min (hi + 1) xs.length := by
|
||||
simp [← ListSlice.length_toList]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_rii_eq_mkSlice_rci {xs : List α} :
|
||||
xs[*...*] = xs[0...*] := by
|
||||
simp [Std.Rii.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice]
|
||||
|
||||
public theorem toList_mkSlice_rii_eq_toList_mkSlice_rco {xs : List α} :
|
||||
xs[*...*].toList = xs[0...xs.length].toList := by
|
||||
simp
|
||||
|
||||
public theorem toArray_mkSlice_rii_eq_toArray_mkSlice_rco {xs : List α} :
|
||||
xs[*...*].toArray = xs[0...xs.length].toArray := by
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
public theorem toList_mkSlice_rii {xs : List α} :
|
||||
xs[*...*].toList = xs := by
|
||||
|
|
@ -253,7 +304,7 @@ section ListSubslices
|
|||
|
||||
namespace ListSlice
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem toList_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
|
||||
xs[lo...hi].toList = (xs.toList.take hi).drop lo := by
|
||||
simp only [instSliceableListSliceNat_1, List.toList_mkSlice_rco, ListSlice.toList_eq (xs := xs)]
|
||||
|
|
@ -262,12 +313,12 @@ public theorem toList_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
|
|||
· simp
|
||||
· simp [List.take_take, Nat.min_comm]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem toArray_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
|
||||
xs[lo...hi].toArray = xs.toArray.extract lo hi := by
|
||||
simp [← toArray_toList, List.drop_take]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_rcc_eq_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
|
||||
xs[lo...=hi] = xs[lo...(hi + 1)] := by
|
||||
simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
|
||||
|
|
@ -295,9 +346,19 @@ public theorem toArray_mkSlice_rci {xs : ListSlice α} {lo : Nat} :
|
|||
xs[lo...*].toArray = xs.toArray.extract lo := by
|
||||
simp only [← toArray_toList, toList_mkSlice_rci]
|
||||
rw (occs := [1]) [← List.take_length (l := List.drop lo xs.toList)]
|
||||
simp [- toArray_toList]
|
||||
|
||||
@[grind =]
|
||||
public theorem toList_mkSlice_rci_eq_toList_mkSlice_rco {xs : ListSlice α} {lo : Nat} :
|
||||
xs[lo...*].toList = xs[lo...xs.size].toList := by
|
||||
simp [← length_toList, - Slice.length_toList_eq_size]
|
||||
|
||||
@[grind =]
|
||||
public theorem toArray_mkSlice_rci_eq_toArray_mkSlice_rco {xs : ListSlice α} {lo : Nat} :
|
||||
xs[lo...*].toArray = xs[lo...xs.size].toArray := by
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_roo_eq_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
|
||||
xs[lo<...hi] = xs[(lo + 1)...hi] := by
|
||||
simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
|
||||
|
|
@ -322,6 +383,11 @@ public theorem mkSlice_roc_eq_mkSlice_rcc {xs : ListSlice α} {lo hi : Nat} :
|
|||
xs[lo<...=hi] = xs[(lo + 1)...=hi] := by
|
||||
simp [Std.Roc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
|
||||
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_roc_eq_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
|
||||
xs[lo<...=hi] = xs[(lo + 1)...(hi + 1)] := by
|
||||
simp [Std.Roc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
|
||||
|
||||
@[simp]
|
||||
public theorem toList_mkSlice_roc {xs : ListSlice α} {lo hi : Nat} :
|
||||
xs[lo<...=hi].toList = (xs.toList.take (hi + 1)).drop (lo + 1) := by
|
||||
|
|
@ -332,11 +398,28 @@ public theorem toArray_mkSlice_roc {xs : ListSlice α} {lo hi : Nat} :
|
|||
xs[lo<...=hi].toArray = xs.toArray.extract (lo + 1) (hi + 1) := by
|
||||
simp [← toArray_toList, List.drop_take]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_roi_eq_mkSlice_rci {xs : ListSlice α} {lo : Nat} :
|
||||
xs[lo<...*] = xs[(lo + 1)...*] := by
|
||||
simp [Std.Roi.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice]
|
||||
|
||||
public theorem toList_mkSlice_roi_eq_toList_mkSlice_roo {xs : ListSlice α} {lo : Nat} :
|
||||
xs[lo<...*].toList = xs[lo<...xs.size].toList := by
|
||||
simp [← length_toList, - Slice.length_toList_eq_size]
|
||||
|
||||
public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_roo {xs : ListSlice α} {lo : Nat} :
|
||||
xs[lo<...*].toArray = xs[lo<...xs.size].toArray := by
|
||||
simp only [mkSlice_roi_eq_mkSlice_rci, toArray_mkSlice_rci, size_toArray_eq_size,
|
||||
mkSlice_roo_eq_mkSlice_rco, toArray_mkSlice_rco]
|
||||
|
||||
public theorem toList_mkSlice_roi_eq_toList_mkSlice_rco {xs : ListSlice α} {lo : Nat} :
|
||||
xs[lo<...*].toList = xs[(lo + 1)...xs.size].toList := by
|
||||
simp [← length_toList, - Slice.length_toList_eq_size]
|
||||
|
||||
public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_rco {xs : ListSlice α} {lo : Nat} :
|
||||
xs[lo<...*].toArray = xs[(lo + 1)...xs.size].toArray := by
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
public theorem toList_mkSlice_roi {xs : ListSlice α} {lo : Nat} :
|
||||
xs[lo<...*].toList = xs.toList.drop (lo + 1) := by
|
||||
|
|
@ -347,9 +430,9 @@ public theorem toArray_mkSlice_roi {xs : ListSlice α} {lo : Nat} :
|
|||
xs[lo<...*].toArray = xs.toArray.extract (lo + 1) := by
|
||||
simp only [← toArray_toList, toList_mkSlice_roi]
|
||||
rw (occs := [1]) [← List.take_length (l := List.drop (lo + 1) xs.toList)]
|
||||
simp
|
||||
simp [- toArray_toList]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_rio_eq_mkSlice_rco {xs : ListSlice α} {hi : Nat} :
|
||||
xs[*...hi] = xs[0...hi] := by
|
||||
simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
|
||||
|
|
@ -374,6 +457,11 @@ public theorem mkSlice_ric_eq_mkSlice_rcc {xs : ListSlice α} {hi : Nat} :
|
|||
xs[*...=hi] = xs[0...=hi] := by
|
||||
simp [Std.Ric.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
|
||||
|
||||
@[grind =]
|
||||
public theorem mkSlice_ric_eq_mkSlice_rco {xs : ListSlice α} {hi : Nat} :
|
||||
xs[*...=hi] = xs[0...(hi + 1)] := by
|
||||
simp [Std.Ric.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
|
||||
|
||||
@[simp]
|
||||
public theorem toList_mkSlice_ric {xs : ListSlice α} {hi : Nat} :
|
||||
xs[*...=hi].toList = xs.toList.take (hi + 1) := by
|
||||
|
|
@ -384,7 +472,7 @@ public theorem toArray_mkSlice_ric {xs : ListSlice α} {hi : Nat} :
|
|||
xs[*...=hi].toArray = xs.toArray.extract 0 (hi + 1) := by
|
||||
simp [← toArray_toList]
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
public theorem mkSlice_rii {xs : ListSlice α} :
|
||||
xs[*...*] = xs := by
|
||||
simp [Std.Rii.Sliceable.mkSlice]
|
||||
|
|
|
|||
|
|
@ -121,3 +121,40 @@ example : [1, 2, 3, 4, 5][1...*][*...2].toArray = #[2, 3] := by simp
|
|||
example : [1, 2, 3, 4, 5][1...*][*...=2].toArray = #[2, 3, 4] := by simp
|
||||
example : [1, 2, 3, 4, 5][1...*][*...*].toArray = #[2, 3, 4, 5] := by simp
|
||||
example : [1, 2, 3][0...2][*...*].toArray = #[1, 2] := by simp
|
||||
|
||||
example (xs : List α) : xs[*...5].size = xs[0...5].size := by
|
||||
grind
|
||||
|
||||
example {xs : List α} {lo hi : Nat} :
|
||||
xs[lo...=hi].toList = (xs.take (hi + 1)).drop lo := by
|
||||
grind
|
||||
|
||||
-- verify that grind is powerful enough to prove some lemmas that are not grind-annotated
|
||||
example : type_of% @List.toList_mkSlice_rcc := by grind
|
||||
example : type_of% @List.toArray_mkSlice_rcc := by grind
|
||||
example : type_of% @List.size_mkSlice_rcc := by grind
|
||||
example : type_of% @List.toList_mkSlice_rci := by grind
|
||||
example : type_of% @List.toArray_mkSlice_rci := by grind
|
||||
example : type_of% @List.toArray_mkSlice_roi := by grind
|
||||
example : type_of% @List.toArray_mkSlice_ric := by grind
|
||||
example : type_of% @List.toArray_mkSlice_rii_eq_toArray_mkSlice_rco := by grind
|
||||
example : type_of% @List.toArray_mkSlice_roc := by grind
|
||||
example : type_of% @List.toList_mkSlice_ric := by grind
|
||||
|
||||
example (xs : List Nat) : xs[1...=4][2...3].toList = xs[3...4].toList := by
|
||||
grind [List.take_drop, List.drop_drop]
|
||||
|
||||
example : type_of% @Array.toArray_mkSlice_rcc := by grind
|
||||
example : type_of% @Array.toArray_mkSlice_rcc := by grind
|
||||
example : type_of% @Array.size_mkSlice_rcc := by grind
|
||||
example : type_of% @Array.toArray_mkSlice_rci := by grind
|
||||
example : type_of% @Array.toArray_mkSlice_rci := by grind
|
||||
example : type_of% @Array.toArray_mkSlice_roi := by grind
|
||||
example : type_of% @Array.toArray_mkSlice_ric := by grind
|
||||
example : type_of% @Array.toArray_mkSlice_roc := by grind
|
||||
example : type_of% @Array.toArray_mkSlice_ric := by grind
|
||||
|
||||
example (xs : Array Nat) : xs[1...=4][2...3].toList = xs[3...4].toList := by
|
||||
grind [List.take_drop, List.drop_drop]
|
||||
|
||||
example (xs : Array Nat) : xs[1...=4][2...3].toArray = xs[3...4].toArray := by grind
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue