This thread contains a patchset. You're looking at the original emails,
but you may wish to use the patch review UI.
Review patch
9
3
[PATCH busybeaver v2 0/7] Efficient z-function implementation
Z-Function: Given a string s, computes the z-table such that z[i] is
the size of the longest string starting at i that is a prefix of the
original string. For more details see:
https://cp-algorithms.com/string/z-function.html
This algorithm will be used to implement some deciders efficiently,
in particular see:
https://todo.sr.ht/~vigoux/busybeaver/5
The current patch provides the construction of the table, and the
proofs that the implementation is correct.
Marcelo Fornet (7):
feat: Start implementation of z-function
remove by exact when they were not necessary
fix: id symm
readable calc
more style changes
remove instances of refine
address other comments
Busybeaver/ZFunction.lean | 376 ++++++++++++++++++++++++++++++++++++++
1 file changed, 376 insertions(+)
create mode 100644 Busybeaver/ZFunction.lean
--
2.39.3 (Apple Git-146)
[PATCH busybeaver v2 1/7] feat: Start implementation of z-function
From: Marcelo Fornet <mfornet94@gmail.com>
- Define ZFunction structure object
- Build z-function table
fix: rename structure so lean doesn't complain
feat(zf): [WIP] Write proofs for z-function
fix: More proves on z-function
feat: continue the proof
loop extend is proved
start working on the important part of the proof
finish proof for z-function. It is correct.
Signed-off-by: Marcelo Fornet <marcelo.fornet@proton.me>
---
Busybeaver/ZFunction.lean | 431 ++++++++++++++++++++++++++++++++++++++
1 file changed, 431 insertions(+)
create mode 100644 Busybeaver/ZFunction.lean
diff --git a/Busybeaver/ZFunction.lean b/Busybeaver/ZFunction.lean
new file mode 100644
index 0000000..41321c5
--- /dev/null
+++ b/Busybeaver/ZFunction.lean
@@ -0,0 +1,431 @@
+ --- Implement Z-Function
+ --- https://cp-algorithms.com/string/z-function.html
+ import Init.Data.Range
+ import Init.Data.Nat.Basic
+ import Init.Data.List.Lemmas
+ import Mathlib.Data.Finset.Basic
+ import Mathlib.Tactic.Linarith
+
+ namespace ZFunction
+
+ def longest (as : List α) (p : List α → Prop) : Prop :=
+ p as ∧ ∀ x, p x → x.length ≤ as.length
+
+ lemma is_prefix_eq [BEq α] (as bs: List α) (hp : bs <+: as) (hb : i < bs.length) :
+ as[i]'(hb.trans_le hp.length_le) = bs[i] := by
+ exact Eq.symm (List.IsPrefix.getElem hp hb)
+
+ def slice (as : List α) (start size : ℕ) : List α :=
+ (as.drop start).take size
+
+ def correct_z_function_value [BEq α] (as : List α) (i z : ℕ) : Prop :=
+ i + z ≤ as.length ∧ longest (slice as i z) (fun x => x <+: as ∧ x <+: as.drop i)
+
+ structure PartialZArray [BEq α] (as : Array α) where
+ table : Array ℕ
+ is_z_function : (hb : i < table.data.length) →
+ correct_z_function_value as.data i (table.get ⟨i, hb⟩)
+
+ def PartialZArray.init [BEq α] (as : Array α) : PartialZArray as :=
+ let table := (Array.mkEmpty as.size).push as.size
+ let he : table = #[as.size] := rfl
+ ⟨table, (by
+ rw [he]
+ intro i b
+ simp at b
+ unfold correct_z_function_value
+ simp [b]
+ unfold slice
+ constructor
+ · simp
+ · intro x hp
+ simp
+ exact List.IsPrefix.length_le hp
+ )⟩
+
+ structure ZArray [BEq α] (as : Array α) where
+ z_array : PartialZArray as
+ complete : z_array.table.data.length = as.data.length
+
+ def ZArray.empty [BEq α] (as : Array α) (he : 0 = as.size): ZArray as :=
+ ⟨⟨Array.mkEmpty as.size, by simp⟩, by simp; assumption⟩
+
+ structure LoopExtend [BEq α] (as : List α) (i : ℕ) where
+ z : ℕ
+ h : correct_z_function_value as i z
+
+ lemma get_add_sub (l : List α) (h1 : 0 < a) (h2 : a < l.length) : l[a] = l[a - 1 + 1] := by
+ refine getElem_congr ?h'
+ exact (Nat.sub_eq_iff_eq_add h1).mp rfl
+
+ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slice as.data i z) <+: as.data) (hb : i + z ≤ as.data.length): LoopExtend as.data i :=
+ have hz : (slice as.data i z).length = z := by
+ unfold slice
+ simp
+ exact Nat.le_sub_of_add_le' hb
+
+ if b : i + z < as.size then
+ have hm : min (z + 1) (as.data.length - i) = z + 1 := by
+ simp
+ exact Nat.le_sub_of_add_le' b
+
+ have hbz : as.size = as.data.length := by simp
+
+ if he : as[z]'(by linarith) = as[i + z] then
+ loop_extend as i (z + 1) (by
+ let ⟨tail, hp'⟩ := hp
+ use tail.drop 1
+ apply List.ext_get
+ · unfold slice
+ simp
+ refine Eq.symm ((fun {b a c} h ↦ (Nat.sub_eq_iff_eq_add h).mp) ?_ ?_)
+ · have h0 : (slice as.data i z ++ tail).length = as.data.length := congrArg List.length hp'
+ have h1 : (slice as.data i z ++ tail).length = (slice as.data i z).length + tail.length := List.length_append (slice as.data i z) tail
+ rw [h1] at h0
+ refine Nat.sub_le_of_le_add ?_
+ refine Nat.le_add_right_of_le ?_
+ linarith
+ · rw [hm]
+ have h1 : (slice as.data i z ++ tail).length = as.data.length := congrArg List.length hp'
+ have h2 : (slice as.data i z ++ tail).length = (slice as.data i z).length + tail.length := List.length_append (slice as.data i z) tail
+ rw [h2] at h1
+ rw [hz] at h1
+ rw [hbz, ← h1]
+ calc z + tail.length - (tail.length - 1) = z + (tail.length - (tail.length - 1)) := by (refine Nat.add_sub_assoc ?h z; exact Nat.sub_le tail.length 1)
+ _ = z + (tail.length - tail.length + 1) := by (
+ refine Eq.symm ((fun {m k n} ↦ Nat.add_left_cancel_iff.mpr) ?_)
+ simp
+ exact Eq.symm (Nat.sub_sub_self (by linarith)))
+ _ = z + 1 := by simp
+ · unfold slice
+ simp
+ intro n h₁ h₂
+ by_cases hs : n ≤ z
+ · have h0 : (List.take (z + 1) (List.drop i as.data)).length = z + 1 := by
+ simp
+ exact Nat.le_sub_of_add_le' b
+ have h1 : (List.take (z + 1) (List.drop i as.data) ++ tail.tail)[n]'(by
+ simp
+ rw [hm]
+ exact Nat.lt_of_lt_of_eq h₁ (congrFun (congrArg HAdd.hAdd hm) (tail.length - 1))) = (List.take (z + 1) (List.drop i as.data))[n] := by
+ apply List.getElem_append_left
+
+ rw [h1]
+ have h2 : (List.take (z + 1) (List.drop i as.data))[n] = as.data[i + n] := by
+ -- apply List.getElem_take
+ have h2a : (List.drop i as.data)[n]'(by
+ simp
+ calc n ≤ z := hs
+ _ < as.data.length - i := by exact Nat.lt_sub_iff_add_lt'.mpr b) = (List.take (z + 1) (List.drop i as.data))[n] := by
+ have hib : n < (List.drop i as.data).length := by
+ simp
+ calc n ≤ z := hs
+ _ ≤ (i + z) - i := le_add_tsub_swap
+ _ < as.data.length - i := by (
+ refine Nat.sub_lt_sub_right ?_ b
+ exact Nat.le_add_right i z)
+
+ apply List.getElem_take (List.drop i as.data) hib (by linarith)
+
+ rw [← h2a]
+ exact List.getElem_drop' as.data
+ rw [h2]
+
+ by_cases h3 : n = z
+ · have h4 : as.data[z] = as.data[n] := getElem_congr (id (Eq.symm h3))
+ have h5 : as.data[i + z] = as.data[i + n] := getElem_congr (congrArg (HAdd.hAdd i) (id (Eq.symm h3)))
+ rw [← h4, ← h5]
+ exact id (Eq.symm he)
+ · push_neg at h3
+ have h4 : n < z := Nat.lt_of_le_of_ne hs h3
+ have h5 : n < (slice as.data i z).length := by
+ rw [hz]
+ exact h4
+ have h6 : (slice as.data i z)[n]'h5 = as.data[i + n] := by
+ unfold slice
+ have hnt : (List.drop i as.data)[n]'(by
+ simp
+ calc n < z := h4
+ _ ≤ (i + z) - i := by exact le_add_tsub_swap
+ _ < as.data.length - i := by (
+ refine Nat.sub_lt_sub_right ?_ b
+ exact Nat.le_add_right i z
+ )
+ ) = (List.take z (List.drop i as.data))[n] := by
+ apply List.getElem_take (as.data.drop i) (by
+ simp
+ calc n < z := h4
+ _ ≤ (i + z) - i := by exact le_add_tsub_swap
+ _ < as.data.length - i := by (
+ refine Nat.sub_lt_sub_right ?_ b
+ exact Nat.le_add_right i z
+ )
+ ) (by linarith)
+ rw [← hnt]
+ exact List.getElem_drop' as.data
+ have h7 : (slice as.data i z)[n]'h5 = as.data[n] := Eq.symm (is_prefix_eq as.data (slice as.data i z) hp h5)
+ rw [← h6, ← h7]
+ · have h₆ : (slice as.data i z).length + tail.length = as.data.length := by
+ nth_rewrite 2 [← hp']
+ exact Eq.symm (List.length_append (slice as.data i z) tail)
+ rw [hz] at h₆
+ have h₅ : n - (z + 1) < tail.length - 1 := by
+ calc n - (z + 1) < as.size - (z + 1) := by (exact Nat.sub_lt_sub_right (by linarith[hs]) h₂)
+ _ = as.data.length - (z + 1) := by simp
+ _ = z + tail.length - (z + 1) := by rw[← h₆]
+ _ = tail.length - 1 := Nat.add_sub_add_left z tail.length 1
+ have h1 : (List.take (z + 1) (List.drop i as.data) ++ tail.tail)[n]'(by simp; exact h₁) =
+ tail.tail[n - (List.take (z + 1) (List.drop i as.data)).length]'(by simp; rw[hm]; exact h₅) := by
+ apply List.getElem_append_right
+ simp
+ intro h
+ push_neg at hs
+ linarith
+ rw [h1]
+ simp
+
+ have ht : tail.tail[n - min (z + 1) (as.data.length - i)]'(by rw [hm, List.length_tail tail]; exact h₅) =
+ tail.tail[n - (z + 1)]'(by rw [List.length_tail tail]; exact h₅) := getElem_congr (congrArg (HSub.hSub n) hm)
+ rw [ht]
+ clear ht
+
+ have ht : as.data[n] = (slice as.data i z ++ tail)[n]'(by
+ simp
+ rw [hz, h₆]
+ exact h₂) := by
+ exact List.getElem_of_eq (id (Eq.symm hp')) h₂
+ rw [ht]
+ clear ht
+
+ have hmw : n - (z + 1) < tail.tail.length := by
+ rw [List.length_tail tail]
+ exact h₅
+
+ have ht : tail.tail[n - (z + 1)] = tail[n - z] := by
+ have hi : tail.tail[n - (z + 1)] = tail.tail[n - z - 1] := by rfl
+ rw [hi]
+ have hj : tail[n - z] = tail[n - z - 1 + 1] := by
+ apply get_add_sub
+ exact tsub_pos_iff_not_le.mpr hs
+ rw [hj]
+ clear hj
+ have h₂ : 0 < tail.length := by linarith
+ have hin : n - (z + 1) = n - z - 1 := by rfl
+ apply List.get_tail _ (n - z - 1) (by rw[List.length_tail tail, ←hin]; exact h₅) (by
+ rw [← hin]
+ calc n - (z + 1) + 1 < tail.length - 1 + 1 := by linarith
+ _ = tail.length := by exact Nat.sub_add_cancel h₂
+ )
+ rw [ht]
+ clear ht
+
+ rw [List.getElem_append_right (slice as.data i z) tail (by push_neg; rw [hz]; linarith)]
+ exact getElem_congr (congrArg (HSub.hSub n) (id (Eq.symm hz)))
+ ) b
+ else
+ {z := z, h := by
+ constructor
+ · exact hb
+ · constructor
+ ·
+ unfold slice
+ simp
+ constructor
+ · exact hp
+ · exact List.take_prefix z (List.drop i as.data)
+ · intro x hp'
+ have ht : (slice as.data i z).length = z := by
+ unfold slice
+ simp
+ exact Nat.le_sub_of_add_le' hb
+ rw [ht]
+ contrapose! he
+ have hle : as[z] = x[z] := is_prefix_eq _ _ hp'.1 he
+ rw [hle]
+ let hp'2 := hp'.2
+ let ls := List.drop i as.data
+ have h3 : ls[z]'(List.lt_length_drop as.data b) = x[z] := is_prefix_eq ls x hp'2 he
+ have h4 : ls[z]'(List.lt_length_drop as.data b) = as[i + z] := List.getElem_drop' as.data
+ rw [← h4, h3]
+ }
+ else
+ {z := z, h := by
+ constructor
+ · exact hb
+ · constructor
+ · simp
+ constructor
+ · exact hp
+ · unfold slice
+ exact List.take_prefix z (List.drop i as.data)
+ · intro x hp'
+ refine List.IsPrefix.length_le ?right.h
+ unfold slice
+ let hs := hp'.2
+ push_neg at b
+ refine List.prefix_take_iff.mpr ?right.h.a
+ constructor
+ · exact hp'.2
+ · have h1 : x.length ≤ (as.data.drop i).length := List.IsPrefix.length_le hs
+ have h2 : (as.data.drop i).length ≤ z := by
+ simp
+ linarith
+ linarith
+ }
+
+ def loop_build_table [BEq α] [DecidableEq α] (size i l r: ℕ) (zarray : PartialZArray as) (he : i = zarray.table.data.length) (hi : 0 < i) (hl : 0 < l) (hs : size + i = as.data.length) (hr : r ≤ as.data.length) (hg : l ≤ r) (hpre : slice as.data l (r - l) <+: as.data) (hlil : l ≤ i): ZArray (α := α) as :=
+ match size with
+ | 0 => ⟨zarray, by linarith[hs]⟩
+ | n + 1 => (
+
+ have hib : i - l < zarray.table.size := by
+ calc i - l < i := by exact Nat.sub_lt hi hl
+ _ = zarray.table.size := he
+ let t := min (r - i) (zarray.table[i - l]'(hib))
+
+ let z := if i < r then t else 0
+
+ let ⟨z, hz⟩ := loop_extend as i z (by
+ by_cases hiz : i < r
+ · have hzt : z = t := if_pos hiz
+ rw [hzt]
+
+ have ht : t ≤ r - i := by exact Nat.min_le_left (r - i) zarray.table[i - l]
+ have hlir : i ≤ r := by exact Nat.le_of_succ_le hiz
+
+ suffices slice as.data i t = as.data.take t by (
+ rw [this]
+ apply List.prefix_iff_eq_take.mpr
+ simp
+ )
+
+ have h₃ : slice as.data l (r - l) = as.data.take (r - l) := by
+ let hpre₁ := List.prefix_iff_eq_take.mp hpre
+ rw [hpre₁]
+ unfold slice
+ simp
+ have hl : r - l ≤ as.size - l := Nat.sub_le_sub_right hr l
+ have hr : r - l ≤ as.size := by calc
+ r - l ≤ as.size - l := by exact hl
+ _ ≤ as.size := by exact Nat.sub_le as.size l
+ simp [hl, hr]
+
+ have h₄ : slice as.data (i - l) t = as.data.take t := by
+ have hb : i - l < zarray.table.data.length := by
+ linarith
+ have hl0 : t < as.size - (i - l) := by calc
+ t ≤ r - i := ht
+ _ ≤ as.size - i := Nat.sub_le_sub_right hr i
+ _ < as.size - i + l := Nat.lt_add_of_pos_right hl
+ _ = as.size + l - i := by (
+ refine Eq.symm (Nat.sub_add_comm ?htt)
+ exact Nat.le_trans hlir hr
+ )
+ _ = as.size - (i - l) := by exact Nat.Simproc.add_sub_le as.size hlil
+
+ let hpre := (zarray.is_z_function hb).right.left.left
+ simp at hpre
+ have hpres : slice as.data (i - l) t <+: as.data := by
+ suffices slice as.data (i - l) t <+: slice as.data (i - l) zarray.table[i - l] from List.IsPrefix.trans this hpre
+ unfold slice
+ refine (List.prefix_take_le_iff ?hm).mpr ?_
+ · simp
+ exact hl0
+ · exact Nat.min_le_right (r - i) zarray.table[i - l]
+ let hpre₁ := List.prefix_iff_eq_take.mp hpres
+ rw [hpre₁]
+ unfold slice
+ simp
+
+ have hl : t ≤ as.size - (i - l) := Nat.le_of_succ_le hl0
+ have hr : t ≤ as.size := by calc
+ t ≤ as.size - (i - l) := hl
+ _ ≤ as.size := Nat.sub_le as.size (i - l)
+ simp [hl, hr]
+
+ have hl : i - l + t ≤ r - l := by
+ calc i - l + t ≤ i - l + (r - i) := by exact Nat.add_le_add_left ht (i - l)
+ _ = i + (r - i) - l := by exact Eq.symm (Nat.sub_add_comm hlil)
+ _ = r - l := by aesop
+
+ have h₅ : slice as.data i t = slice (slice as.data l (r - l)) (i - l) t := by
+ unfold slice
+ nth_rewrite 2 [List.take_drop]
+ rw [List.take_take, min_eq_left hl, List.drop_take]
+ simp
+ suffices i - l + l = i by (rw [this])
+ exact Nat.sub_add_cancel hlil
+
+ have h₆ : slice (List.take (r - l) as.data) (i - l) t = slice as.data (i - l) t := by
+ unfold slice
+ rw [List.take_drop, List.take_take, min_eq_left hl, List.drop_take]
+ suffices i - l + t - (i - l) = t by (rw [this])
+ simp
+ rw [h₅, h₃, h₆, h₄]
+ · have hz0 : z = 0 := if_neg hiz
+ rw [hz0]
+ unfold slice
+ simp) (by
+ by_cases hiz : i < r
+ · have hzt : z = t := if_pos hiz
+ have hlt : t ≤ r - i := Nat.min_le_left (r - i) zarray.table[i - l]
+ have htr : i ≤ r := Nat.le_of_succ_le hiz
+ calc i + z = i + t := by exact congrArg (HAdd.hAdd i) hzt
+ _ ≤ i + (r - i) := by linarith[hlt]
+ _ = r := Nat.add_sub_of_le htr
+ _ ≤ as.data.length := hr
+ · have hz0 : z = 0 := if_neg hiz
+ simp [hz0]
+ simp at hs
+ linarith
+ )
+ let new_table := zarray.table.push z
+ have hnew_table_size : new_table.data.length = zarray.table.data.length + 1 := Array.size_push zarray.table z
+
+ let new_zarray := ⟨new_table, by
+ intro j hb'
+ by_cases h : j < zarray.table.data.length
+ · have hje : new_table.get ⟨j, hb'⟩ = zarray.table.get ⟨j, h⟩ := by
+ apply Array.get_push_lt
+ rw [hje]
+ exact zarray.is_z_function h
+ · simp
+ have hiv : j = i := by
+ push_neg at h
+ rw [he]
+ rw [hnew_table_size] at hb'
+ linarith
+ have hlast : new_table[j] = z := by
+ rw [Array.get_push]
+ simp
+ intro h'
+ contradiction
+ rw [hlast]
+ rw [hiv]
+ exact hz
+ ⟩
+
+ if hnb : i + z > r then
+ loop_build_table n (i + 1) i (i + z) (new_zarray) (by
+ rw [he]; simp;
+ exact Eq.symm (Array.size_push zarray.table z)
+ ) (by linarith) hi (by linarith) hz.left (by linarith) (by
+ suffices i + z - i = z by (rw[this]; exact hz.right.left.left)
+ simp
+ ) (by linarith)
+ else
+ loop_build_table n (i + 1) l r (new_zarray) (by
+ rw [he]; simp;
+ exact Eq.symm (Array.size_push zarray.table z)
+ ) (by linarith) hl (by linarith) hr hg hpre (by linarith)
+ )
+
+ def z_function [BEq α] [DecidableEq α] (as : Array α) : ZArray as :=
+ if he : 0 = as.size
+ then ZArray.empty as he
+ else
+ loop_build_table (as.size - 1) 1 1 1 (PartialZArray.init as) (rfl) (by trivial) (by trivial) (Nat.succ_pred_eq_of_ne_zero fun a ↦ he (id (Eq.symm a))) (Nat.one_le_iff_ne_zero.mpr fun a ↦ he (id (Eq.symm a))) (by trivial) (by unfold slice; simp) (by trivial)
+
+ #eval! (z_function #[1, 2, 1, 2, 1, 2, 3, 1, 2, 1, 3]).z_array.table
+
+ end ZFunction
--
2.39.3 (Apple Git-146)
[PATCH busybeaver v2 2/7] remove by exact when they were not necessary
Signed-off-by: Marcelo Fornet <marcelo.fornet@proton.me>
---
Busybeaver/ZFunction.lean | 14 +++++++ -------
1 file changed, 7 insertions(+), 7 deletions(-)
diff --git a/Busybeaver/ZFunction.lean b/Busybeaver/ZFunction.lean
index 41321c5..e657ef1 100644
--- a/Busybeaver/ZFunction.lean
+++ b/Busybeaver/ZFunction.lean
@@ -116,7 +116,7 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
have h2a : (List.drop i as.data)[n]'(by
simp
calc n ≤ z := hs
- _ < as.data.length - i := by exact Nat.lt_sub_iff_add_lt'.mpr b) = (List.take (z + 1) (List.drop i as.data))[n] := by
+ _ < as.data.length - i := Nat.lt_sub_iff_add_lt'.mpr b) = (List.take (z + 1) (List.drop i as.data))[n] := by
have hib : n < (List.drop i as.data).length := by
simp
calc n ≤ z := hs
@@ -146,7 +146,7 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
have hnt : (List.drop i as.data)[n]'(by
simp
calc n < z := h4
- _ ≤ (i + z) - i := by exact le_add_tsub_swap
+ _ ≤ (i + z) - i := le_add_tsub_swap
_ < as.data.length - i := by (
refine Nat.sub_lt_sub_right ?_ b
exact Nat.le_add_right i z
@@ -214,7 +214,7 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
apply List.get_tail _ (n - z - 1) (by rw[List.length_tail tail, ←hin]; exact h₅) (by
rw [← hin]
calc n - (z + 1) + 1 < tail.length - 1 + 1 := by linarith
- _ = tail.length := by exact Nat.sub_add_cancel h₂
+ _ = tail.length := Nat.sub_add_cancel h₂
)
rw [ht]
clear ht
@@ -290,8 +290,8 @@ def loop_build_table [BEq α] [DecidableEq α] (size i l r: ℕ) (zarray : Parti
· have hzt : z = t := if_pos hiz
rw [hzt]
- have ht : t ≤ r - i := by exact Nat.min_le_left (r - i) zarray.table[i - l]
- have hlir : i ≤ r := by exact Nat.le_of_succ_le hiz
+ have ht : t ≤ r - i := Nat.min_le_left (r - i) zarray.table[i - l]
+ have hlir : i ≤ r := Nat.le_of_succ_le hiz
suffices slice as.data i t = as.data.take t by (
rw [this]
@@ -321,7 +321,7 @@ def loop_build_table [BEq α] [DecidableEq α] (size i l r: ℕ) (zarray : Parti
refine Eq.symm (Nat.sub_add_comm ?htt)
exact Nat.le_trans hlir hr
)
- _ = as.size - (i - l) := by exact Nat.Simproc.add_sub_le as.size hlil
+ _ = as.size - (i - l) := Nat.Simproc.add_sub_le as.size hlil
let hpre := (zarray.is_z_function hb).right.left.left
simp at hpre
@@ -345,7 +345,7 @@ def loop_build_table [BEq α] [DecidableEq α] (size i l r: ℕ) (zarray : Parti
have hl : i - l + t ≤ r - l := by
calc i - l + t ≤ i - l + (r - i) := by exact Nat.add_le_add_left ht (i - l)
- _ = i + (r - i) - l := by exact Eq.symm (Nat.sub_add_comm hlil)
+ _ = i + (r - i) - l := Eq.symm (Nat.sub_add_comm hlil)
_ = r - l := by aesop
have h₅ : slice as.data i t = slice (slice as.data l (r - l)) (i - l) t := by
--
2.39.3 (Apple Git-146)
[PATCH busybeaver v2 3/7] fix: id symm
Signed-off-by: Marcelo Fornet <marcelo.fornet@proton.me>
---
Busybeaver/ZFunction.lean | 24 ++++++++++++ ------------
1 file changed, 12 insertions(+), 12 deletions(-)
diff --git a/Busybeaver/ZFunction.lean b/Busybeaver/ZFunction.lean
index e657ef1..8026847 100644
--- a/Busybeaver/ZFunction.lean
+++ b/Busybeaver/ZFunction.lean
@@ -12,7 +12,7 @@ def longest (as : List α) (p : List α → Prop) : Prop :=
p as ∧ ∀ x, p x → x.length ≤ as.length
lemma is_prefix_eq [BEq α] (as bs: List α) (hp : bs <+: as) (hb : i < bs.length) :
- as[i]'(hb.trans_le hp.length_le) = bs[i] := by
+ as[i]'(hb.trans_le hp.length_le) = bs[i] := by
exact Eq.symm (List.IsPrefix.getElem hp hb)
def slice (as : List α) (start size : ℕ) : List α :=
@@ -29,7 +29,7 @@ structure PartialZArray [BEq α] (as : Array α) where
def PartialZArray.init [BEq α] (as : Array α) : PartialZArray as :=
let table := (Array.mkEmpty as.size).push as.size
let he : table = #[as.size] := rfl
- ⟨table, (by
+ ⟨table, by
rw [he]
intro i b
simp at b
@@ -41,7 +41,7 @@ def PartialZArray.init [BEq α] (as : Array α) : PartialZArray as :=
· intro x hp
simp
exact List.IsPrefix.length_le hp
- )⟩
+ ⟩
structure ZArray [BEq α] (as : Array α) where
z_array : PartialZArray as
@@ -132,10 +132,10 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
rw [h2]
by_cases h3 : n = z
- · have h4 : as.data[z] = as.data[n] := getElem_congr (id (Eq.symm h3))
- have h5 : as.data[i + z] = as.data[i + n] := getElem_congr (congrArg (HAdd.hAdd i) (id (Eq.symm h3)))
+ · have h4 : as.data[z] = as.data[n] := getElem_congr h3.symm
+ have h5 : as.data[i + z] = as.data[i + n] := getElem_congr (congrArg (HAdd.hAdd i) h3.symm)
rw [← h4, ← h5]
- exact id (Eq.symm he)
+ exact he.symm
· push_neg at h3
have h4 : n < z := Nat.lt_of_le_of_ne hs h3
have h5 : n < (slice as.data i z).length := by
@@ -190,10 +190,10 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
clear ht
have ht : as.data[n] = (slice as.data i z ++ tail)[n]'(by
- simp
- rw [hz, h₆]
- exact h₂) := by
- exact List.getElem_of_eq (id (Eq.symm hp')) h₂
+ simp
+ rw [hz, h₆]
+ exact h₂) :=
+ List.getElem_of_eq hp'.symm h₂
rw [ht]
clear ht
@@ -220,7 +220,7 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
clear ht
rw [List.getElem_append_right (slice as.data i z) tail (by push_neg; rw [hz]; linarith)]
- exact getElem_congr (congrArg (HSub.hSub n) (id (Eq.symm hz)))
+ exact getElem_congr (congrArg (HSub.hSub n) (hz.symm))
) b
else
{z := z, h := by
@@ -424,7 +424,7 @@ def z_function [BEq α] [DecidableEq α] (as : Array α) : ZArray as :=
if he : 0 = as.size
then ZArray.empty as he
else
- loop_build_table (as.size - 1) 1 1 1 (PartialZArray.init as) (rfl) (by trivial) (by trivial) (Nat.succ_pred_eq_of_ne_zero fun a ↦ he (id (Eq.symm a))) (Nat.one_le_iff_ne_zero.mpr fun a ↦ he (id (Eq.symm a))) (by trivial) (by unfold slice; simp) (by trivial)
+ loop_build_table (as.size - 1) 1 1 1 (PartialZArray.init as) rfl (by trivial) (by trivial) (Nat.succ_pred_eq_of_ne_zero fun a ↦ he a.symm) (Nat.one_le_iff_ne_zero.mpr fun a ↦ he a.symm) (by trivial) (by unfold slice; simp) (by trivial)
#eval! (z_function #[1, 2, 1, 2, 1, 2, 3, 1, 2, 1, 3]).z_array.table
--
2.39.3 (Apple Git-146)
[PATCH busybeaver v2 4/7] readable calc
Signed-off-by: Marcelo Fornet <marcelo.fornet@proton.me>
---
Busybeaver/ZFunction.lean | 128 ++++++++++++++++++++ ------------------
1 file changed, 68 insertions(+), 60 deletions(-)
diff --git a/Busybeaver/ZFunction.lean b/Busybeaver/ZFunction.lean
index 8026847..bf5718b 100644
--- a/Busybeaver/ZFunction.lean
+++ b/Busybeaver/ZFunction.lean
@@ -91,12 +91,13 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
rw [h2] at h1
rw [hz] at h1
rw [hbz, ← h1]
- calc z + tail.length - (tail.length - 1) = z + (tail.length - (tail.length - 1)) := by (refine Nat.add_sub_assoc ?h z; exact Nat.sub_le tail.length 1)
- _ = z + (tail.length - tail.length + 1) := by (
+ calc z + tail.length - (tail.length - 1)
+ _ = z + (tail.length - (tail.length - 1)) := by refine Nat.add_sub_assoc ?h z; exact Nat.sub_le tail.length 1
+ _ = z + (tail.length - tail.length + 1) := by
refine Eq.symm ((fun {m k n} ↦ Nat.add_left_cancel_iff.mpr) ?_)
simp
- exact Eq.symm (Nat.sub_sub_self (by linarith)))
- _ = z + 1 := by simp
+ exact Eq.symm (Nat.sub_sub_self (by linarith))
+ _ = z + 1 := by simp
· unfold slice
simp
intro n h₁ h₂
@@ -115,16 +116,17 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
-- apply List.getElem_take
have h2a : (List.drop i as.data)[n]'(by
simp
- calc n ≤ z := hs
- _ < as.data.length - i := Nat.lt_sub_iff_add_lt'.mpr b) = (List.take (z + 1) (List.drop i as.data))[n] := by
+ calc n
+ _ ≤ z := hs
+ _ < as.data.length - i := Nat.lt_sub_iff_add_lt'.mpr b) = (List.take (z + 1) (List.drop i as.data))[n] := by
have hib : n < (List.drop i as.data).length := by
simp
- calc n ≤ z := hs
- _ ≤ (i + z) - i := le_add_tsub_swap
- _ < as.data.length - i := by (
- refine Nat.sub_lt_sub_right ?_ b
- exact Nat.le_add_right i z)
-
+ calc n
+ _ ≤ z := hs
+ _ ≤ (i + z) - i := le_add_tsub_swap
+ _ < as.data.length - i := by
+ refine Nat.sub_lt_sub_right ?_ b
+ exact Nat.le_add_right i z
apply List.getElem_take (List.drop i as.data) hib (by linarith)
rw [← h2a]
@@ -138,54 +140,57 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
exact he.symm
· push_neg at h3
have h4 : n < z := Nat.lt_of_le_of_ne hs h3
- have h5 : n < (slice as.data i z).length := by
- rw [hz]
- exact h4
+ have h5 : n < (slice as.data i z).length := by rw [hz]; exact h4
have h6 : (slice as.data i z)[n]'h5 = as.data[i + n] := by
unfold slice
have hnt : (List.drop i as.data)[n]'(by
- simp
- calc n < z := h4
- _ ≤ (i + z) - i := le_add_tsub_swap
- _ < as.data.length - i := by (
+ simp
+ calc n
+ _ < z := h4
+ _ ≤ (i + z) - i := le_add_tsub_swap
+ _ < as.data.length - i := by
refine Nat.sub_lt_sub_right ?_ b
exact Nat.le_add_right i z
- )
- ) = (List.take z (List.drop i as.data))[n] := by
+ ) = (List.take z (List.drop i as.data))[n] := by
apply List.getElem_take (as.data.drop i) (by
simp
- calc n < z := h4
- _ ≤ (i + z) - i := by exact le_add_tsub_swap
- _ < as.data.length - i := by (
- refine Nat.sub_lt_sub_right ?_ b
- exact Nat.le_add_right i z
- )
+ calc n
+ _ < z := h4
+ _ ≤ (i + z) - i := le_add_tsub_swap
+ _ < as.data.length - i := by
+ refine Nat.sub_lt_sub_right ?_ b
+ exact Nat.le_add_right i z
) (by linarith)
rw [← hnt]
exact List.getElem_drop' as.data
have h7 : (slice as.data i z)[n]'h5 = as.data[n] := Eq.symm (is_prefix_eq as.data (slice as.data i z) hp h5)
rw [← h6, ← h7]
- · have h₆ : (slice as.data i z).length + tail.length = as.data.length := by
- nth_rewrite 2 [← hp']
- exact Eq.symm (List.length_append (slice as.data i z) tail)
+ · have h₆ : (slice as.data i z).length + tail.length = as.data.length := by {
+ nth_rewrite 2 [← hp']
+ exact Eq.symm (List.length_append (slice as.data i z) tail)
+ }
rw [hz] at h₆
+
have h₅ : n - (z + 1) < tail.length - 1 := by
- calc n - (z + 1) < as.size - (z + 1) := by (exact Nat.sub_lt_sub_right (by linarith[hs]) h₂)
+ calc n - (z + 1)
+ _ < as.size - (z + 1) := Nat.sub_lt_sub_right (by linarith[hs]) h₂
_ = as.data.length - (z + 1) := by simp
_ = z + tail.length - (z + 1) := by rw[← h₆]
_ = tail.length - 1 := Nat.add_sub_add_left z tail.length 1
+
have h1 : (List.take (z + 1) (List.drop i as.data) ++ tail.tail)[n]'(by simp; exact h₁) =
- tail.tail[n - (List.take (z + 1) (List.drop i as.data)).length]'(by simp; rw[hm]; exact h₅) := by
+ tail.tail[n - (List.take (z + 1) (List.drop i as.data)).length]'(by simp; rw[hm]; exact h₅) := by {
apply List.getElem_append_right
simp
intro h
push_neg at hs
linarith
+ }
rw [h1]
simp
have ht : tail.tail[n - min (z + 1) (as.data.length - i)]'(by rw [hm, List.length_tail tail]; exact h₅) =
- tail.tail[n - (z + 1)]'(by rw [List.length_tail tail]; exact h₅) := getElem_congr (congrArg (HSub.hSub n) hm)
+ tail.tail[n - (z + 1)]'(by rw [List.length_tail tail]; exact h₅) := getElem_congr (congrArg (HSub.hSub n) hm)
rw [ht]
clear ht
@@ -201,21 +206,23 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
rw [List.length_tail tail]
exact h₅
- have ht : tail.tail[n - (z + 1)] = tail[n - z] := by
+ have ht : tail.tail[n - (z + 1)] = tail[n - z] := by {
have hi : tail.tail[n - (z + 1)] = tail.tail[n - z - 1] := by rfl
rw [hi]
- have hj : tail[n - z] = tail[n - z - 1 + 1] := by
+ have hj : tail[n - z] = tail[n - z - 1 + 1] := by {
apply get_add_sub
exact tsub_pos_iff_not_le.mpr hs
+ }
rw [hj]
clear hj
have h₂ : 0 < tail.length := by linarith
have hin : n - (z + 1) = n - z - 1 := by rfl
apply List.get_tail _ (n - z - 1) (by rw[List.length_tail tail, ←hin]; exact h₅) (by
rw [← hin]
- calc n - (z + 1) + 1 < tail.length - 1 + 1 := by linarith
- _ = tail.length := Nat.sub_add_cancel h₂
- )
+ calc n - (z + 1) + 1
+ _ < tail.length - 1 + 1 := by linarith
+ _ = tail.length := Nat.sub_add_cancel h₂)
+ }
rw [ht]
clear ht
@@ -279,8 +286,9 @@ def loop_build_table [BEq α] [DecidableEq α] (size i l r: ℕ) (zarray : Parti
| n + 1 => (
have hib : i - l < zarray.table.size := by
- calc i - l < i := by exact Nat.sub_lt hi hl
- _ = zarray.table.size := he
+ calc i - l
+ _ < i := Nat.sub_lt hi hl
+ _ = zarray.table.size := he
let t := min (r - i) (zarray.table[i - l]'(hib))
let z := if i < r then t else 0
@@ -305,27 +313,26 @@ def loop_build_table [BEq α] [DecidableEq α] (size i l r: ℕ) (zarray : Parti
unfold slice
simp
have hl : r - l ≤ as.size - l := Nat.sub_le_sub_right hr l
- have hr : r - l ≤ as.size := by calc
- r - l ≤ as.size - l := by exact hl
- _ ≤ as.size := by exact Nat.sub_le as.size l
+ have hr : r - l ≤ as.size := calc r - l
+ _ ≤ as.size - l := hl
+ _ ≤ as.size := Nat.sub_le as.size l
simp [hl, hr]
have h₄ : slice as.data (i - l) t = as.data.take t := by
- have hb : i - l < zarray.table.data.length := by
- linarith
- have hl0 : t < as.size - (i - l) := by calc
- t ≤ r - i := ht
+ have hb : i - l < zarray.table.data.length := by linarith
+ have hl0 : t < as.size - (i - l) := calc t
+ _ ≤ r - i := ht
_ ≤ as.size - i := Nat.sub_le_sub_right hr i
_ < as.size - i + l := Nat.lt_add_of_pos_right hl
- _ = as.size + l - i := by (
+ _ = as.size + l - i := by {
refine Eq.symm (Nat.sub_add_comm ?htt)
exact Nat.le_trans hlir hr
- )
+ }
_ = as.size - (i - l) := Nat.Simproc.add_sub_le as.size hlil
let hpre := (zarray.is_z_function hb).right.left.left
simp at hpre
- have hpres : slice as.data (i - l) t <+: as.data := by
+ have hpres : slice as.data (i - l) t <+: as.data := by
suffices slice as.data (i - l) t <+: slice as.data (i - l) zarray.table[i - l] from List.IsPrefix.trans this hpre
unfold slice
refine (List.prefix_take_le_iff ?hm).mpr ?_
@@ -338,15 +345,15 @@ def loop_build_table [BEq α] [DecidableEq α] (size i l r: ℕ) (zarray : Parti
simp
have hl : t ≤ as.size - (i - l) := Nat.le_of_succ_le hl0
- have hr : t ≤ as.size := by calc
- t ≤ as.size - (i - l) := hl
+ have hr : t ≤ as.size := calc t
+ _ ≤ as.size - (i - l) := hl
_ ≤ as.size := Nat.sub_le as.size (i - l)
simp [hl, hr]
- have hl : i - l + t ≤ r - l := by
- calc i - l + t ≤ i - l + (r - i) := by exact Nat.add_le_add_left ht (i - l)
- _ = i + (r - i) - l := Eq.symm (Nat.sub_add_comm hlil)
- _ = r - l := by aesop
+ have hl : i - l + t ≤ r - l := calc i - l + t
+ _ ≤ i - l + (r - i) := Nat.add_le_add_left ht (i - l)
+ _ = i + (r - i) - l := Eq.symm (Nat.sub_add_comm hlil)
+ _ = r - l := by aesop
have h₅ : slice as.data i t = slice (slice as.data l (r - l)) (i - l) t := by
unfold slice
@@ -370,10 +377,11 @@ def loop_build_table [BEq α] [DecidableEq α] (size i l r: ℕ) (zarray : Parti
· have hzt : z = t := if_pos hiz
have hlt : t ≤ r - i := Nat.min_le_left (r - i) zarray.table[i - l]
have htr : i ≤ r := Nat.le_of_succ_le hiz
- calc i + z = i + t := by exact congrArg (HAdd.hAdd i) hzt
- _ ≤ i + (r - i) := by linarith[hlt]
- _ = r := Nat.add_sub_of_le htr
- _ ≤ as.data.length := hr
+ calc i + z
+ _ = i + t := congrArg (HAdd.hAdd i) hzt
+ _ ≤ i + (r - i) := by linarith[hlt]
+ _ = r := Nat.add_sub_of_le htr
+ _ ≤ as.data.length := hr
· have hz0 : z = 0 := if_neg hiz
simp [hz0]
simp at hs
--
2.39.3 (Apple Git-146)
[PATCH busybeaver v2 5/7] more style changes
- replace have with show ... from ...
- use more calc
Signed-off-by: Marcelo Fornet <marcelo.fornet@proton.me>
---
Busybeaver/ZFunction.lean | 230 +++++++++++++++++ ---------------------
1 file changed, 104 insertions(+), 126 deletions(-)
diff --git a/Busybeaver/ZFunction.lean b/Busybeaver/ZFunction.lean
index bf5718b..9ddff63 100644
--- a/Busybeaver/ZFunction.lean
+++ b/Busybeaver/ZFunction.lean
@@ -28,9 +28,8 @@ structure PartialZArray [BEq α] (as : Array α) where
def PartialZArray.init [BEq α] (as : Array α) : PartialZArray as :=
let table := (Array.mkEmpty as.size).push as.size
- let he : table = #[as.size] := rfl
⟨table, by
- rw [he]
+ rw [show table = #[as.size] from rfl]
intro i b
simp at b
unfold correct_z_function_value
@@ -69,7 +68,7 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
simp
exact Nat.le_sub_of_add_le' b
- have hbz : as.size = as.data.length := by simp
+ have h_sz_len : as.size = as.data.length := by simp
if he : as[z]'(by linarith) = as[i + z] then
loop_extend as i (z + 1) (by
@@ -85,65 +84,70 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
refine Nat.sub_le_of_le_add ?_
refine Nat.le_add_right_of_le ?_
linarith
- · rw [hm]
- have h1 : (slice as.data i z ++ tail).length = as.data.length := congrArg List.length hp'
- have h2 : (slice as.data i z ++ tail).length = (slice as.data i z).length + tail.length := List.length_append (slice as.data i z) tail
- rw [h2] at h1
- rw [hz] at h1
- rw [hbz, ← h1]
- calc z + tail.length - (tail.length - 1)
+ · have h₁ := calc z + tail.length
+ _ = (slice as.data i z).length + tail.length := by rw [hz]
+ _ = (slice as.data i z ++ tail).length := List.length_append (slice as.data i z) tail |>.symm
+ _ = as.data.length := congrArg List.length hp'
+
+ calc as.size - (tail.length - 1)
+ _ = z + tail.length - (tail.length - 1) := by rw [h_sz_len, ← h₁]
_ = z + (tail.length - (tail.length - 1)) := by refine Nat.add_sub_assoc ?h z; exact Nat.sub_le tail.length 1
_ = z + (tail.length - tail.length + 1) := by
refine Eq.symm ((fun {m k n} ↦ Nat.add_left_cancel_iff.mpr) ?_)
simp
exact Eq.symm (Nat.sub_sub_self (by linarith))
_ = z + 1 := by simp
+ _ = min (z + 1) (as.size - i) := hm.symm
· unfold slice
simp
intro n h₁ h₂
by_cases hs : n ≤ z
- · have h0 : (List.take (z + 1) (List.drop i as.data)).length = z + 1 := by
+ · have hi₁ : (List.take (z + 1) (List.drop i as.data)).length = z + 1 := by
simp
exact Nat.le_sub_of_add_le' b
- have h1 : (List.take (z + 1) (List.drop i as.data) ++ tail.tail)[n]'(by
- simp
- rw [hm]
- exact Nat.lt_of_lt_of_eq h₁ (congrFun (congrArg HAdd.hAdd hm) (tail.length - 1))) = (List.take (z + 1) (List.drop i as.data))[n] := by
- apply List.getElem_append_left
-
- rw [h1]
- have h2 : (List.take (z + 1) (List.drop i as.data))[n] = as.data[i + n] := by
- -- apply List.getElem_take
- have h2a : (List.drop i as.data)[n]'(by
- simp
- calc n
- _ ≤ z := hs
- _ < as.data.length - i := Nat.lt_sub_iff_add_lt'.mpr b) = (List.take (z + 1) (List.drop i as.data))[n] := by
- have hib : n < (List.drop i as.data).length := by
+
+ rw [
+ show (List.take (z + 1) (List.drop i as.data) ++ tail.tail)[n]'(by
simp
- calc n
- _ ≤ z := hs
- _ ≤ (i + z) - i := le_add_tsub_swap
- _ < as.data.length - i := by
- refine Nat.sub_lt_sub_right ?_ b
- exact Nat.le_add_right i z
- apply List.getElem_take (List.drop i as.data) hib (by linarith)
-
- rw [← h2a]
- exact List.getElem_drop' as.data
- rw [h2]
+ rw [hm]
+ exact Nat.lt_of_lt_of_eq h₁ (congrFun (congrArg HAdd.hAdd hm) (tail.length - 1)))
+ = (List.take (z + 1) (List.drop i as.data))[n] by apply List.getElem_append_left,
+
+ show (List.take (z + 1) (List.drop i as.data))[n] = as.data[i + n] by {
+ rw [
+ show (List.take (z + 1) (List.drop i as.data))[n] = (List.drop i as.data)[n]'(by
+ simp
+ calc n
+ _ ≤ z := hs
+ _ < as.data.length - i := Nat.lt_sub_iff_add_lt'.mpr b) by {
+ symm
+ apply List.getElem_take (List.drop i as.data) (by
+ simp
+ calc n
+ _ ≤ z := hs
+ _ ≤ (i + z) - i := le_add_tsub_swap
+ _ < as.data.length - i := by
+ refine Nat.sub_lt_sub_right ?_ b
+ exact Nat.le_add_right i z) (by linarith)
+ }
+ ]
+ exact List.getElem_drop' as.data
+ }
+ ]
by_cases h3 : n = z
- · have h4 : as.data[z] = as.data[n] := getElem_congr h3.symm
- have h5 : as.data[i + z] = as.data[i + n] := getElem_congr (congrArg (HAdd.hAdd i) h3.symm)
- rw [← h4, ← h5]
- exact he.symm
+ · calc as.data[i + n]
+ _ = as.data[i + z] := getElem_congr (congrArg (HAdd.hAdd i) h3)
+ _ = as[z] := he.symm
+ _ = as.data[n] := getElem_congr h3.symm
· push_neg at h3
have h4 : n < z := Nat.lt_of_le_of_ne hs h3
have h5 : n < (slice as.data i z).length := by rw [hz]; exact h4
- have h6 : (slice as.data i z)[n]'h5 = as.data[i + n] := by
+ rw [
+ show as.data[i + n] = (slice as.data i z)[n]'h5 by
+ symm
unfold slice
- have hnt : (List.drop i as.data)[n]'(by
+ rw [show (List.take z (List.drop i as.data))[n] = (List.drop i as.data)[n]'(by
simp
calc n
_ < z := h4
@@ -151,7 +155,8 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
_ < as.data.length - i := by
refine Nat.sub_lt_sub_right ?_ b
exact Nat.le_add_right i z
- ) = (List.take z (List.drop i as.data))[n] := by
+ ) by
+ symm
apply List.getElem_take (as.data.drop i) (by
simp
calc n
@@ -161,72 +166,58 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
refine Nat.sub_lt_sub_right ?_ b
exact Nat.le_add_right i z
) (by linarith)
- rw [← hnt]
- exact List.getElem_drop' as.data
- have h7 : (slice as.data i z)[n]'h5 = as.data[n] := Eq.symm (is_prefix_eq as.data (slice as.data i z) hp h5)
- rw [← h6, ← h7]
- · have h₆ : (slice as.data i z).length + tail.length = as.data.length := by {
+ ]
+ exact List.getElem_drop' as.data,
+
+ is_prefix_eq as.data (slice as.data i z) hp h5
+ ]
+ · have h₆ : z + tail.length = as.data.length := by {
+ rw [← hz]
nth_rewrite 2 [← hp']
exact Eq.symm (List.length_append (slice as.data i z) tail)
}
- rw [hz] at h₆
- have h₅ : n - (z + 1) < tail.length - 1 := by
- calc n - (z + 1)
+ have h₅ := calc n - (z + 1)
_ < as.size - (z + 1) := Nat.sub_lt_sub_right (by linarith[hs]) h₂
_ = as.data.length - (z + 1) := by simp
_ = z + tail.length - (z + 1) := by rw[← h₆]
_ = tail.length - 1 := Nat.add_sub_add_left z tail.length 1
- have h1 : (List.take (z + 1) (List.drop i as.data) ++ tail.tail)[n]'(by simp; exact h₁) =
- tail.tail[n - (List.take (z + 1) (List.drop i as.data)).length]'(by simp; rw[hm]; exact h₅) := by {
+ rw [show (List.take (z + 1) (List.drop i as.data) ++ tail.tail)[n]'(by simp; exact h₁) =
+ tail.tail[n - (List.take (z + 1) (List.drop i as.data)).length]'(by simp; rw[hm]; exact h₅) by {
apply List.getElem_append_right
simp
intro h
push_neg at hs
linarith
- }
- rw [h1]
+ }]
+
simp
+ rw [
+ show tail.tail[n - min (z + 1) (as.data.length - i)]'(by rw [hm, List.length_tail tail]; exact h₅) =
+ tail.tail[n - (z + 1)]'(by rw [List.length_tail tail]; exact h₅)
+ from getElem_congr (congrArg (HSub.hSub n) hm),
- have ht : tail.tail[n - min (z + 1) (as.data.length - i)]'(by rw [hm, List.length_tail tail]; exact h₅) =
- tail.tail[n - (z + 1)]'(by rw [List.length_tail tail]; exact h₅) := getElem_congr (congrArg (HSub.hSub n) hm)
- rw [ht]
- clear ht
-
- have ht : as.data[n] = (slice as.data i z ++ tail)[n]'(by
- simp
- rw [hz, h₆]
- exact h₂) :=
- List.getElem_of_eq hp'.symm h₂
- rw [ht]
- clear ht
-
- have hmw : n - (z + 1) < tail.tail.length := by
- rw [List.length_tail tail]
- exact h₅
-
- have ht : tail.tail[n - (z + 1)] = tail[n - z] := by {
- have hi : tail.tail[n - (z + 1)] = tail.tail[n - z - 1] := by rfl
- rw [hi]
- have hj : tail[n - z] = tail[n - z - 1 + 1] := by {
+ show as.data[n] = (slice as.data i z ++ tail)[n]'(by simp; rw [hz, h₆]; exact h₂)
+ from List.getElem_of_eq hp'.symm h₂
+ ]
+
+ have hmw : n - (z + 1) < tail.tail.length := by rw [List.length_tail tail]; exact h₅
+
+ rw [show tail.tail[n - (z + 1)]'hmw = tail[n - z] by {
+ rw [show tail[n - z] = tail[n - z - 1 + 1] by {
apply get_add_sub
exact tsub_pos_iff_not_le.mpr hs
- }
- rw [hj]
- clear hj
- have h₂ : 0 < tail.length := by linarith
+ }]
have hin : n - (z + 1) = n - z - 1 := by rfl
apply List.get_tail _ (n - z - 1) (by rw[List.length_tail tail, ←hin]; exact h₅) (by
rw [← hin]
calc n - (z + 1) + 1
_ < tail.length - 1 + 1 := by linarith
- _ = tail.length := Nat.sub_add_cancel h₂)
- }
- rw [ht]
- clear ht
-
- rw [List.getElem_append_right (slice as.data i z) tail (by push_neg; rw [hz]; linarith)]
+ _ = tail.length := Nat.sub_add_cancel (by linarith))
+ },
+ List.getElem_append_right (slice as.data i z) tail (by push_neg; rw [hz]; linarith)
+ ]
exact getElem_congr (congrArg (HSub.hSub n) (hz.symm))
) b
else
@@ -234,26 +225,19 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
constructor
· exact hb
· constructor
- ·
- unfold slice
+ · unfold slice
simp
constructor
· exact hp
· exact List.take_prefix z (List.drop i as.data)
· intro x hp'
- have ht : (slice as.data i z).length = z := by
- unfold slice
- simp
- exact Nat.le_sub_of_add_le' hb
- rw [ht]
+ rw [hz]
contrapose! he
- have hle : as[z] = x[z] := is_prefix_eq _ _ hp'.1 he
- rw [hle]
- let hp'2 := hp'.2
let ls := List.drop i as.data
- have h3 : ls[z]'(List.lt_length_drop as.data b) = x[z] := is_prefix_eq ls x hp'2 he
- have h4 : ls[z]'(List.lt_length_drop as.data b) = as[i + z] := List.getElem_drop' as.data
- rw [← h4, h3]
+ calc as[z]
+ _ = x[z] := is_prefix_eq _ _ hp'.1 he
+ _ = ls[z]'(List.lt_length_drop as.data b) := is_prefix_eq ls x hp'.2 he |>.symm
+ _ = as[i + z] := List.getElem_drop' as.data
}
else
{z := z, h := by
@@ -273,11 +257,9 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
refine List.prefix_take_iff.mpr ?right.h.a
constructor
· exact hp'.2
- · have h1 : x.length ≤ (as.data.drop i).length := List.IsPrefix.length_le hs
- have h2 : (as.data.drop i).length ≤ z := by
- simp
- linarith
- linarith
+ · calc x.length
+ _ ≤ (as.data.drop i).length := List.IsPrefix.length_le hs
+ _ ≤ z := by simp; linarith
}
def loop_build_table [BEq α] [DecidableEq α] (size i l r: ℕ) (zarray : PartialZArray as) (he : i = zarray.table.data.length) (hi : 0 < i) (hl : 0 < l) (hs : size + i = as.data.length) (hr : r ≤ as.data.length) (hg : l ≤ r) (hpre : slice as.data l (r - l) <+: as.data) (hlil : l ≤ i): ZArray (α := α) as :=
@@ -285,12 +267,11 @@ def loop_build_table [BEq α] [DecidableEq α] (size i l r: ℕ) (zarray : Parti
| 0 => ⟨zarray, by linarith[hs]⟩
| n + 1 => (
- have hib : i - l < zarray.table.size := by
- calc i - l
- _ < i := Nat.sub_lt hi hl
- _ = zarray.table.size := he
- let t := min (r - i) (zarray.table[i - l]'(hib))
+ have hib := calc i - l
+ _ < i := Nat.sub_lt hi hl
+ _ = zarray.table.size := he
+ let t := min (r - i) (zarray.table[i - l]'(hib))
let z := if i < r then t else 0
let ⟨z, hz⟩ := loop_extend as i z (by
@@ -388,28 +369,25 @@ def loop_build_table [BEq α] [DecidableEq α] (size i l r: ℕ) (zarray : Parti
linarith
)
let new_table := zarray.table.push z
- have hnew_table_size : new_table.data.length = zarray.table.data.length + 1 := Array.size_push zarray.table z
let new_zarray := ⟨new_table, by
intro j hb'
by_cases h : j < zarray.table.data.length
- · have hje : new_table.get ⟨j, hb'⟩ = zarray.table.get ⟨j, h⟩ := by
- apply Array.get_push_lt
- rw [hje]
+ · rw [show new_table.get ⟨j, hb'⟩ = zarray.table.get ⟨j, h⟩ by apply Array.get_push_lt]
exact zarray.is_z_function h
· simp
- have hiv : j = i := by
- push_neg at h
- rw [he]
- rw [hnew_table_size] at hb'
- linarith
- have hlast : new_table[j] = z := by
- rw [Array.get_push]
- simp
- intro h'
- contradiction
- rw [hlast]
- rw [hiv]
+ rw [
+ show new_table[j] = z by {
+ rw [Array.get_push]
+ simp
+ intro h'
+ contradiction },
+ show j = i by {
+ push_neg at h
+ rw [he]
+ rw [show new_table.data.length = zarray.table.data.length + 1 from Array.size_push zarray.table z] at hb'
+ linarith }
+ ]
exact hz
⟩
--
2.39.3 (Apple Git-146)
[PATCH busybeaver v2 6/7] remove instances of refine
Signed-off-by: Marcelo Fornet <marcelo.fornet@proton.me>
---
Busybeaver/ZFunction.lean | 106 +++++++++++++ -------------------------
1 file changed, 35 insertions(+), 71 deletions(-)
diff --git a/Busybeaver/ZFunction.lean b/Busybeaver/ZFunction.lean
index 9ddff63..1bbe4d3 100644
--- a/Busybeaver/ZFunction.lean
+++ b/Busybeaver/ZFunction.lean
@@ -53,10 +53,6 @@ structure LoopExtend [BEq α] (as : List α) (i : ℕ) where
z : ℕ
h : correct_z_function_value as i z
- lemma get_add_sub (l : List α) (h1 : 0 < a) (h2 : a < l.length) : l[a] = l[a - 1 + 1] := by
- refine getElem_congr ?h'
- exact (Nat.sub_eq_iff_eq_add h1).mp rfl
-
def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slice as.data i z) <+: as.data) (hb : i + z ≤ as.data.length): LoopExtend as.data i :=
have hz : (slice as.data i z).length = z := by
unfold slice
@@ -77,13 +73,8 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
apply List.ext_get
· unfold slice
simp
- refine Eq.symm ((fun {b a c} h ↦ (Nat.sub_eq_iff_eq_add h).mp) ?_ ?_)
- · have h0 : (slice as.data i z ++ tail).length = as.data.length := congrArg List.length hp'
- have h1 : (slice as.data i z ++ tail).length = (slice as.data i z).length + tail.length := List.length_append (slice as.data i z) tail
- rw [h1] at h0
- refine Nat.sub_le_of_le_add ?_
- refine Nat.le_add_right_of_le ?_
- linarith
+ symm
+ apply (Nat.sub_eq_iff_eq_add _).mp
· have h₁ := calc z + tail.length
_ = (slice as.data i z).length + tail.length := by rw [hz]
_ = (slice as.data i z ++ tail).length := List.length_append (slice as.data i z) tail |>.symm
@@ -91,13 +82,19 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
calc as.size - (tail.length - 1)
_ = z + tail.length - (tail.length - 1) := by rw [h_sz_len, ← h₁]
- _ = z + (tail.length - (tail.length - 1)) := by refine Nat.add_sub_assoc ?h z; exact Nat.sub_le tail.length 1
+ _ = z + (tail.length - (tail.length - 1)) := Nat.add_sub_assoc (Nat.sub_le tail.length 1) z
_ = z + (tail.length - tail.length + 1) := by
- refine Eq.symm ((fun {m k n} ↦ Nat.add_left_cancel_iff.mpr) ?_)
- simp
- exact Eq.symm (Nat.sub_sub_self (by linarith))
+ apply Nat.add_left_cancel_iff.mpr
+ rw [Nat.add_eq_right.mpr (Nat.sub_self tail.length)]
+ exact (Nat.sub_sub_self (by linarith))
_ = z + 1 := by simp
_ = min (z + 1) (as.size - i) := hm.symm
+ · have h0 : (slice as.data i z ++ tail).length = as.data.length := congrArg List.length hp'
+ have h1 : (slice as.data i z ++ tail).length = (slice as.data i z).length + tail.length := List.length_append (slice as.data i z) tail
+ rw [h1] at h0
+ apply Nat.sub_le_of_le_add
+ apply Nat.le_add_right_of_le
+ linarith
· unfold slice
simp
intro n h₁ h₂
@@ -126,9 +123,7 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
calc n
_ ≤ z := hs
_ ≤ (i + z) - i := le_add_tsub_swap
- _ < as.data.length - i := by
- refine Nat.sub_lt_sub_right ?_ b
- exact Nat.le_add_right i z) (by linarith)
+ _ < as.data.length - i := Nat.sub_lt_sub_right (Nat.le_add_right i z) b) (by linarith)
}
]
exact List.getElem_drop' as.data
@@ -147,26 +142,14 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
show as.data[i + n] = (slice as.data i z)[n]'h5 by
symm
unfold slice
- rw [show (List.take z (List.drop i as.data))[n] = (List.drop i as.data)[n]'(by
- simp
- calc n
- _ < z := h4
- _ ≤ (i + z) - i := le_add_tsub_swap
- _ < as.data.length - i := by
- refine Nat.sub_lt_sub_right ?_ b
- exact Nat.le_add_right i z
- ) by
- symm
- apply List.getElem_take (as.data.drop i) (by
- simp
- calc n
- _ < z := h4
- _ ≤ (i + z) - i := le_add_tsub_swap
- _ < as.data.length - i := by
- refine Nat.sub_lt_sub_right ?_ b
- exact Nat.le_add_right i z
- ) (by linarith)
- ]
+ have hi₂ := calc n
+ _ < z := h4
+ _ ≤ (i + z) - i := le_add_tsub_swap
+ _ < as.data.length - i := Nat.sub_lt_sub_right (Nat.le_add_right i z) b
+ _ = (as.data.drop i).length := by simp
+
+ rw [show (List.take z (List.drop i as.data))[n] = (List.drop i as.data)[n]
+ from List.getElem_take (as.data.drop i) hi₂ (by linarith) |>.symm]
exact List.getElem_drop' as.data,
is_prefix_eq as.data (slice as.data i z) hp h5
@@ -205,10 +188,8 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
have hmw : n - (z + 1) < tail.tail.length := by rw [List.length_tail tail]; exact h₅
rw [show tail.tail[n - (z + 1)]'hmw = tail[n - z] by {
- rw [show tail[n - z] = tail[n - z - 1 + 1] by {
- apply get_add_sub
- exact tsub_pos_iff_not_le.mpr hs
- }]
+ rw [show tail[n - z] = tail[n - z - 1 + 1] from
+ getElem_congr ((Nat.sub_eq_iff_eq_add (tsub_pos_iff_not_le.mpr hs)).mp rfl)]
have hin : n - (z + 1) = n - z - 1 := by rfl
apply List.get_tail _ (n - z - 1) (by rw[List.length_tail tail, ←hin]; exact h₅) (by
rw [← hin]
@@ -225,11 +206,8 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
constructor
· exact hb
· constructor
- · unfold slice
- simp
- constructor
- · exact hp
- · exact List.take_prefix z (List.drop i as.data)
+ · simp
+ exact ⟨hp, List.take_prefix z (List.drop i as.data)⟩
· intro x hp'
rw [hz]
contrapose! he
@@ -245,21 +223,14 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
· exact hb
· constructor
· simp
- constructor
- · exact hp
- · unfold slice
- exact List.take_prefix z (List.drop i as.data)
+ exact ⟨hp, List.take_prefix z (List.drop i as.data)⟩
· intro x hp'
- refine List.IsPrefix.length_le ?right.h
- unfold slice
- let hs := hp'.2
+ apply List.IsPrefix.length_le
push_neg at b
- refine List.prefix_take_iff.mpr ?right.h.a
- constructor
- · exact hp'.2
- · calc x.length
- _ ≤ (as.data.drop i).length := List.IsPrefix.length_le hs
- _ ≤ z := by simp; linarith
+ apply List.prefix_take_iff.mpr
+ exact ⟨hp'.2, calc x.length
+ _ ≤ (as.data.drop i).length := List.IsPrefix.length_le hp'.2
+ _ ≤ z := by simp; linarith⟩
}
def loop_build_table [BEq α] [DecidableEq α] (size i l r: ℕ) (zarray : PartialZArray as) (he : i = zarray.table.data.length) (hi : 0 < i) (hl : 0 < l) (hs : size + i = as.data.length) (hr : r ≤ as.data.length) (hg : l ≤ r) (hpre : slice as.data l (r - l) <+: as.data) (hlil : l ≤ i): ZArray (α := α) as :=
@@ -305,21 +276,16 @@ def loop_build_table [BEq α] [DecidableEq α] (size i l r: ℕ) (zarray : Parti
_ ≤ r - i := ht
_ ≤ as.size - i := Nat.sub_le_sub_right hr i
_ < as.size - i + l := Nat.lt_add_of_pos_right hl
- _ = as.size + l - i := by {
- refine Eq.symm (Nat.sub_add_comm ?htt)
- exact Nat.le_trans hlir hr
- }
+ _ = as.size + l - i := Nat.sub_add_comm (Nat.le_trans hlir hr) |>.symm
_ = as.size - (i - l) := Nat.Simproc.add_sub_le as.size hlil
let hpre := (zarray.is_z_function hb).right.left.left
simp at hpre
have hpres : slice as.data (i - l) t <+: as.data := by
- suffices slice as.data (i - l) t <+: slice as.data (i - l) zarray.table[i - l] from List.IsPrefix.trans this hpre
+ suffices slice as.data (i - l) t <+: slice as.data (i - l) zarray.table[i - l] from
+ List.IsPrefix.trans this hpre
unfold slice
- refine (List.prefix_take_le_iff ?hm).mpr ?_
- · simp
- exact hl0
- · exact Nat.min_le_right (r - i) zarray.table[i - l]
+ exact (List.prefix_take_le_iff (by simp; exact hl0)).mpr (Nat.min_le_right (r - i) zarray.table[i - l])
let hpre₁ := List.prefix_iff_eq_take.mp hpres
rw [hpre₁]
unfold slice
@@ -412,6 +378,4 @@ def z_function [BEq α] [DecidableEq α] (as : Array α) : ZArray as :=
else
loop_build_table (as.size - 1) 1 1 1 (PartialZArray.init as) rfl (by trivial) (by trivial) (Nat.succ_pred_eq_of_ne_zero fun a ↦ he a.symm) (Nat.one_le_iff_ne_zero.mpr fun a ↦ he a.symm) (by trivial) (by unfold slice; simp) (by trivial)
- #eval! (z_function #[1, 2, 1, 2, 1, 2, 3, 1, 2, 1, 3]).z_array.table
-
end ZFunction
--
2.39.3 (Apple Git-146)
[PATCH busybeaver v2 7/7] address other comments
Signed-off-by: Marcelo Fornet <marcelo.fornet@proton.me>
---
Busybeaver/ZFunction.lean | 15 +++++ ----------
1 file changed, 5 insertions(+), 10 deletions(-)
diff --git a/Busybeaver/ZFunction.lean b/Busybeaver/ZFunction.lean
index 1bbe4d3..c4332cf 100644
--- a/Busybeaver/ZFunction.lean
+++ b/Busybeaver/ZFunction.lean
@@ -64,7 +64,7 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
simp
exact Nat.le_sub_of_add_le' b
- have h_sz_len : as.size = as.data.length := by simp
+ have h_sz_len : as.size = as.data.length := by rfl
if he : as[z]'(by linarith) = as[i + z] then
loop_extend as i (z + 1) (by
@@ -131,10 +131,8 @@ def loop_extend [BEq α] [DecidableEq α] (as: Array α) (i z : ℕ) (hp : (slic
]
by_cases h3 : n = z
- · calc as.data[i + n]
- _ = as.data[i + z] := getElem_congr (congrArg (HAdd.hAdd i) h3)
- _ = as[z] := he.symm
- _ = as.data[n] := getElem_congr h3.symm
+ · cases h3
+ exact he.symm
· push_neg at h3
have h4 : n < z := Nat.lt_of_le_of_ne hs h3
have h5 : n < (slice as.data i z).length := by rw [hz]; exact h4
@@ -260,8 +258,7 @@ def loop_build_table [BEq α] [DecidableEq α] (size i l r: ℕ) (zarray : Parti
)
have h₃ : slice as.data l (r - l) = as.data.take (r - l) := by
- let hpre₁ := List.prefix_iff_eq_take.mp hpre
- rw [hpre₁]
+ rw [List.prefix_iff_eq_take.mp hpre]
unfold slice
simp
have hl : r - l ≤ as.size - l := Nat.sub_le_sub_right hr l
@@ -286,11 +283,9 @@ def loop_build_table [BEq α] [DecidableEq α] (size i l r: ℕ) (zarray : Parti
List.IsPrefix.trans this hpre
unfold slice
exact (List.prefix_take_le_iff (by simp; exact hl0)).mpr (Nat.min_le_right (r - i) zarray.table[i - l])
- let hpre₁ := List.prefix_iff_eq_take.mp hpres
- rw [hpre₁]
+ rw [List.prefix_iff_eq_take.mp hpres]
unfold slice
simp
-
have hl : t ≤ as.size - (i - l) := Nat.le_of_succ_le hl0
have hr : t ≤ as.size := calc t
_ ≤ as.size - (i - l) := hl
--
2.39.3 (Apple Git-146)
[busybeaver/patches/.build.yml] build success
Thanks!
I added some small style changes, but it is otherwise great !
To git@git.sr.ht:~vigoux/busybeaver
e366421f84a0..5cfe4e7ee946 master -> master