~vigoux/busybeaver-devel

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

Marcelo Fornet <mfornet94@gmail.com>
Details
Message ID
<20240918201213.86458-1-marcelo.fornet@proton.me>
DKIM signature
pass
Download raw message
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

Marcelo Fornet <mfornet94@gmail.com>
Details
Message ID
<20240918201213.86458-2-marcelo.fornet@proton.me>
In-Reply-To
<20240918201213.86458-1-marcelo.fornet@proton.me> (view parent)
DKIM signature
pass
Download raw message
Patch: +431 -0
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

Marcelo Fornet <mfornet94@gmail.com>
Details
Message ID
<20240918201213.86458-3-marcelo.fornet@proton.me>
In-Reply-To
<20240918201213.86458-1-marcelo.fornet@proton.me> (view parent)
DKIM signature
pass
Download raw message
Patch: +7 -7
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

Marcelo Fornet <mfornet94@gmail.com>
Details
Message ID
<20240918201213.86458-4-marcelo.fornet@proton.me>
In-Reply-To
<20240918201213.86458-1-marcelo.fornet@proton.me> (view parent)
DKIM signature
pass
Download raw message
Patch: +12 -12
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

Marcelo Fornet <mfornet94@gmail.com>
Details
Message ID
<20240918201213.86458-5-marcelo.fornet@proton.me>
In-Reply-To
<20240918201213.86458-1-marcelo.fornet@proton.me> (view parent)
DKIM signature
pass
Download raw message
Patch: +68 -60
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

Marcelo Fornet <mfornet94@gmail.com>
Details
Message ID
<20240918201213.86458-6-marcelo.fornet@proton.me>
In-Reply-To
<20240918201213.86458-1-marcelo.fornet@proton.me> (view parent)
DKIM signature
pass
Download raw message
Patch: +104 -126
- 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

Marcelo Fornet <mfornet94@gmail.com>
Details
Message ID
<20240918201213.86458-7-marcelo.fornet@proton.me>
In-Reply-To
<20240918201213.86458-1-marcelo.fornet@proton.me> (view parent)
DKIM signature
pass
Download raw message
Patch: +35 -71
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

Marcelo Fornet <mfornet94@gmail.com>
Details
Message ID
<20240918201213.86458-8-marcelo.fornet@proton.me>
In-Reply-To
<20240918201213.86458-1-marcelo.fornet@proton.me> (view parent)
DKIM signature
pass
Download raw message
Patch: +5 -10
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

builds.sr.ht <builds@sr.ht>
Details
Message ID
<D49OTF8TIKGI.F47KH37UJ0RT@fra02>
In-Reply-To
<20240918201213.86458-8-marcelo.fornet@proton.me> (view parent)
DKIM signature
missing
Download raw message
busybeaver/patches/.build.yml: SUCCESS in 7m57s

[Efficient z-function implementation][0] v2 from [Marcelo Fornet][1]

[0]: https://lists.sr.ht/~vigoux/busybeaver-devel/patches/55100
[1]: mfornet94@gmail.com

✓ #1331649 SUCCESS busybeaver/patches/.build.yml https://builds.sr.ht/~vigoux/job/1331649
Details
Message ID
<D4AHZBMO5ML9.35IYYLT3QZ52L@vigoux.eu>
In-Reply-To
<20240918201213.86458-1-marcelo.fornet@proton.me> (view parent)
DKIM signature
pass
Download raw message
Thanks!

I added some small style changes, but it is otherwise great !

To git@git.sr.ht:~vigoux/busybeaver
   e366421f84a0..5cfe4e7ee946  master -> master
Reply to thread Export thread (mbox)