Access non empty array

Stream: lean4

[Patrick Massot]

I know someone, probably Kyle, already answered this question recently but I can't find it. Where is

example {α: Type _} {a : Array α} (h : ¬ a.isEmpty) : 0 < a.size := sorry

hiding? Note that:

1. I can prove the lemma, this isn't the question
2. The context is I want to do

if h : myArray.isEmpty then
  ...
else
  let x := myArray[0]...

without getting an error.

[Henrik Böving]

Note that Array.isEmpty merely checks if 0 = a.sizenot only on a lean level but also in the optimized c version as array size is O(1) so you can rewrite to:

def test (xs : Array Nat) : Nat :=
  if h : 0 < xs.size then
    xs[0]
  else
    0

if you want. A quick loogle that checks for |- 0 < Array.size ?a sadly doesn't yield anything so I guess we dont have it (yet)?

[Patrick Massot]

Indeed I have a lot of code that look like your test function, but is really feels wrong from a readability point of view.

[Patrick Massot]

Especially when the first branch is very long and the second one very short.

[Sebastian Ullrich]

To be honest, if it's just for programming, don't shy away from myArray[0]! when it's convenient

[Sebastian Ullrich]

Especially since then you can do

if myArray.isEmpty then
  return ...
...

to avoid indenting the very long branch. We don't have a dependent version of that syntax yet.

[Patrick Massot]

This solution requires an Inhabited instance, right?

[Sebastian Ullrich]

Ah, but in programming we make everything inhabited!

[James Gallicchio]

if only.............. :sob:

[Patrick Massot]

failed to synthesize instance
  Inhabited Widget.InteractiveGoal

[Patrick Massot]

This Widget.InteractiveGoal is in core Lean and sits on top of many structures without Inhabited instances.

[Thomas Murrills]

I like this pattern for that specific context, but I realize it might be the opposite of what you want given the branch lengths:

if let some x := myArray[0]? then
  ...
else
  ...

(Alternatively, you could of course match on myArray[0]? and order the branches however you like, but I imagine that’s less readable.)

[Eric Wieser]

That could also be resolved with an unless syntax that is if with the actions swapped

[Sebastian Ullrich]

let some x := myArray[0]? | ...
...