Accessors

Stream: lean4

[James Gallicchio]

This may not be a Lean 4 issue, but what should I try debugging if I have a term { val := i, isLt := (_ : i < cap + cap) }.val that isn't reducing?

Setting pp.all true doesn't show anything weird...

[Leonardo de Moura]

It is hard to tell what is going on without seeing the whole example.

[James Gallicchio]

theorem Nat.lt_of_lt_le {x y z : Nat} : x < y → y ≤ z → x < z := by
  intro h h'
  induction h'
  assumption
  apply Nat.le_step
  assumption

structure ArrayBuffer (α) where
  cap : Nat
  backing : Fin cap → Option α
  size : Nat
  h_size : size ≤ cap
  h_full : ∀ i, (h:i < size) → (backing ⟨i, Nat.lt_of_lt_le h h_size⟩).isSome

namespace ArrayBuffer

def grow : ArrayBuffer α → ArrayBuffer α :=
λ ⟨cap, backing, size, h_size, h_full⟩ =>
  ⟨cap + cap,
    λ i => if h:i < cap then backing ⟨i,h⟩ else none,
    size,
    Nat.le_trans h_size (Nat.le_add_left _ _),
    by intro i h
       simp
       sorry⟩

Definitely doing some funky stuff here. I can work around it by changing the h_full to ∀ i, (h:i.val < size) → (backing i).isSome, but I'm nonetheless curious why this doesn't work/how to avoid it in general

[James Gallicchio]

At the sorry, to progress we need to reduce { val := i, isLt := _ }.val to i, which I think should just work. Not sure why it doesn't.

[Leonardo de Moura]

Pushed a fix for this issue https://github.com/leanprover/lean4/commit/86fc089e07c58d14c5178cd8e40725518b2ae98e

[James Gallicchio]

Oh hah that makes much more sense! I thought I was going crazy

[James Gallicchio]

Thank you!

[Leonardo de Moura]

Added your example to the test suite too https://github.com/leanprover/lean4/commit/7fda1f47f82e88275576dbcd3f13c5d3bef21384

[James Gallicchio]

While you're here, this is working towards reimplementing Array in terms of fixed size arrays (and then implementing unbounded arrays within Lean). Was there a reason for going with UBAs as the built-in?

[James Gallicchio]

Just for simplicity of the bootstrapping?

[Leonardo de Moura]

Yes, it is simple, and we could easily provide an efficient implementation for functions such as Array.push. Array.push is very fast if the array is not shared and there is space left.