better way to write `rangeStepAux`

Stream: lean4

[Joseph O]

I have this function, but it is not structural recursion.

protected def List.rangeStepAux (m n : Nat) (l : List Nat): List Nat :=
  if n = m then
    l
  else
    List.rangeStepAux m (n+2) (l.take n |>.append $ l.drop (n+1) |>.take (l.length - (n+1)))

What different/better ways are there to do this where I won't have to prove termination, and, I would prefer no code, and rather verbal suggestions so I can try to work this out myself. Thanks in advance!

[Mario Carneiro]

use partial

[Mario Carneiro]

I don't really know what your function is supposed to do, but it infinite loops when I test it

[Mario Carneiro]

so proving termination is probably going to be difficult

[Joseph O]

Mario Carneiro said:

I don't really know what your function is supposed to do, but it infinite loops when I test it

Make a range from 0-n, and skip every mth term

[Mario Carneiro]

so like 1,2,4,5,7,8?

[Mario Carneiro]

Your algorithm also looks cubic

[Joseph O]

Mario Carneiro said:

so like 1,2,4,5,7,8?

yes. that would be skipping every third term

[Mario Carneiro]

What do you do if m is negative, if the start point is greater than the end point, or if the end point is not a multiple of the step? Lots of things cause that code to miss its exit point

[Joseph O]

Mario Carneiro said:

Your algorithm also looks cubic

im thinking of scratching my algorithm

[Joseph O]

Mario Carneiro said:

What do you do if m is negative, if the start point is greater than the end point, or if the end point is not a multiple of the step? Lots of things cause that code to miss its exit point

m will never be negative

[Mario Carneiro]

your function signature doesn't say so

[Joseph O]

(m n : Nat)

[Mario Carneiro]

er I meant the other thing

[Mario Carneiro]

the start point can be greater than the end point in the aux function

[Mario Carneiro]

also a step size of 0 is bad

[Joseph O]

Yes, but I use this in a function rangeStep where I use it correctly

[Mario Carneiro]

okay, then rangeStepAux needs hypotheses asserting that it's being called correctly

[Joseph O]

But I would like to use a different algorithm? Do you have ideas for a different one?

[Mario Carneiro]

sure, this sounds like (range n).filter (\lam i, i % m != 0)

[Joseph O]

Mario Carneiro said:

okay, then rangeStepAux needs hypotheses asserting that it's being called correctly

ok. I cant do that, but I dont really have to worry about what you said, because i'm pretty sure that cant appen

[Mario Carneiro]

You misunderstand. You say that rangeStep checks that certain boundary cases don't happen, while rangeStepAux relies on those boundary cases not being inputs. That means that rangeStepAux needs to assert that the bad cases are not legal in its type signature or else you won't be able to prove termination

[Mario Carneiro]

because rangeStepAux is just a regular function, people can call it themselves if they want

[Mario Carneiro]

For example

protected def List.rangeStepAux (start stop step : Nat) (h : start ≤ stop) (s0 : step ≠ 0) : List Nat := sorry

[Joseph O]

but I made it protected so people cant use it

[Mario Carneiro]

nope, that's not what protected means

[Joseph O]

or do I have to use private, if that is a keyword

[Mario Carneiro]

protected means you have to write List.rangeStepAux even if you open List

[Joseph O]

Ah. If I use private, will that allow people not to use it?

[Mario Carneiro]

private makes the function not easily accessible outside the current section

[Joseph O]

oh

[Mario Carneiro]

but it's not air tight and more to the point it is not something you can use to do proofs

[Mario Carneiro]

if you want to know that a fact is true, you take it as an argument

[Joseph O]

right

[Mario Carneiro]

this makes the function inconvenient to call, but that's fine since this is an aux function

[Joseph O]

Mario Carneiro said:

For example

protected def List.rangeStepAux (start stop step : Nat) (h : start ≤ stop) (s0 : step ≠ 0) : List Nat := sorry

I dont take start as an argument

[Joseph O]

At least with my current algorithm

[Mario Carneiro]

in your code start was n and stop was m and step was... 2?

[Mario Carneiro]

So start is the current value, it increases until it exceeds stop

[Joseph O]

Mario Carneiro said:

in your code start was n and stop was m and step was... 2?

sorry if it was very unclear. m was stop, and n was step

[Joseph O]

I should have made that more clear

[Mario Carneiro]

If that's the case, then your step increased by 2 on every iteration

[Mario Carneiro]

maybe you and I mean different things by "step"

[Joseph O]

ah, that is not what i meant. I meant to increase by step

[Joseph O]

Let me see what fixing my mistake does.

[Joseph O]

I still seem to need to prove termination

[Mario Carneiro]

well yes, but now it's actually provable (hopefully)

[Mario Carneiro]

if you don't want to prove termination you can use partial, but if it is actually nonterminating for some inputs then users will not like it

[Mario Carneiro]

but if your definition is not structurally recursive then in all likelihood you will need to prove termination manually assuming no partial

[Mario Carneiro]

note that mathlib will almost certainly want such a function to not be partial because you can't prove facts about partial functions

[Joseph O]

Yes. The only problem now is, how can we prove termination? On what case. I think I have an idea.

[Joseph O]

protected def List.rangeStepAux (stop step : Nat) (l : List Nat): List Nat :=
  if step = stop then
    l
  else
    List.rangeStepAux stop (step*2) (l.take step |>.append $ l.drop (step+1) |>.take (l.length - (step+1)))
termination_by List.rangeStepAux m n _ => n = m

i think I am close?

[Mario Carneiro]

This code has exactly the same nontermination issues as the original

[Mario Carneiro]

I would rename step to start btw

[Mario Carneiro]

the step is 2 there

[Mario Carneiro]

your termination measure should be stop - start most likely

[Joseph O]

Wait, I still didn't fix the previous bug

[Joseph O]

Actually nevermind

[Joseph O]

Mario Carneiro said:

I would rename step to start btw

Why?

[Mario Carneiro]

because it's not a step

[Mario Carneiro]

it's the first value produced by the code

[Joseph O]

Ok

[Joseph O]

Right

[Joseph O]

Mario Carneiro said:

your termination measure should be stop - start most likely

hmm

[Joseph O]

And what could I compare that with? stop - start = 0?

[Mario Carneiro]

nothing, termination_by is expecting an expression of type Nat (or other well ordered type)

[Joseph O]

Ah. So just that. I will try it

[Joseph O]

I get this image.png

[Mauricio Collares]

The argument order in your recursive call seems wrong

[Joseph O]

You may be right

[Joseph O]

So now it results into something that will be false most of the time image.png

[Mauricio Collares]

Why? This is now true unless start == 0. By the way, originally you had +2 and now you have *2, is that intentional?

[Mauricio Collares]

I guess I am having trouble understanding what the function is supposed to do, so it's entirely possible that my suggestion makes no sense

[Mauricio Collares]

I would recommend making the function partial and running it to check if the outputs match what you expect, before proving termination

[Joseph O]

Mauricio Collares said:

Why? This is now true unless start = 0. By the way, originally (before renaming from m n to start stop) you had +2 and now you have *2, is that intentional?

The +2 was a mistake

[Joseph O]

Mauricio Collares said:

I guess I am having trouble understanding what the function is supposed to do, so it's entirely possible that my suggestion makes no sense

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/better.20way.20to.20write.20.60rangeStepAux.60/near/272821546

[Joseph O]

Mario Carneiro said:

sure, this sounds like (range n).filter (\lam i, i % m != 0)

I missed this entirely

[Joseph O]

This is a filter, I just didn’t know how to keep track of something. thanks again,

[Mario Carneiro]

Joseph O said:

Mauricio Collares said:

Why? This is now true unless start = 0. By the way, originally (before renaming from m n to start stop) you had +2 and now you have *2, is that intentional?

The +2 was a mistake

The *2 looks like even more of a mistake. start will go over powers of 2, which doesn't seem to have anything to do with your goal

[Joseph O]

Now I solved this without recursion or an auxiliary function

def List.rangeStep (start stop step : Nat) :=
  (List.drop start $ List.range stop).filter (fun i => i % step ≠ 0)

[Joseph O]

Thanks so much for your algorithm idea

[Mario Carneiro]

I think there is a variant on range that lets you control the starting point

[Joseph O]

Is there?

[Mario Carneiro]

/-- `range' s n` is the list of numbers `[s, s+1, ..., s+n-1]`.
  It is intended mainly for proving properties of `range` and `iota`. -/
@[simp]
def range' : ℕ → ℕ → List ℕ
| s, 0 => []
| s, n+1 => s :: range' (s+1) n

[Mario Carneiro]

so it is start and len

[Mario Carneiro]

where len is stop - start

[Joseph O]

Ah thank you

[Joseph O]

I didn't know

[Mario Carneiro]

that's in mathlib(4)

[Joseph O]

Ah, im afraid I cant use it then

[Reid Barton]

Well, in another sense, it's on Zulip, in Mario's message.

[Joseph O]

Well yes, but I would have to either inline it into my functions or make it private which in lean 4 i dont think is possible

[Mario Carneiro]

or just copy it into your project

[Mario Carneiro]

you can't inline it anyway, it's a recursive function

[Joseph O]

Mario Carneiro said:

you can't inline it anyway, it's a recursive function

I meant localize it with let rec

[Joseph O]

Mario Carneiro said:

or just copy it into your project

under the given circumstances, I cant do that either

[Mario Carneiro]

I don't really understand your decision procedures

[Mario Carneiro]

what are the circumstances?

[Joseph O]

I’m contributing somewhere

[Henrik Böving]

Besides you can make it private Lean 4 does have a private keyword.

[Joseph O]

Mario told me it is not exactly private

[Joseph O]

and can be accessed

[Henrik Böving]

And why is it an issue if some helper range function can be accessed?

[Joseph O]

I don’t know if the maintainers would like that, since they should be declared under the List namespace

[Joseph O]

I could add them there, but as said, I don’t think the Lean4 maintainers want new list methods in their std

[Kevin Buzzard]

My understanding from the Lean 4 FAQ is that right now unrequested pull requests are not welcome.

[Kevin Buzzard]

OTOH the more experimental #mathlib4 repo is much more open to PRs.

[Joseph O]

Kevin Buzzard said:

My understanding from the Lean 4 FAQ is that right now unrequested pull requests are not welcome.

Oh.

[Joseph O]

I guess I will make an issue to see if they would want it.

[Kevin Buzzard]

My advice would be to leave them alone for now.

[Kevin Buzzard]

They haven't even made an official release yet and have other things to worry about.

[Joseph O]

Ok. Yet I wasn't bothering them in the first place. Either way, I will keep this change until they accept pull requests

[Notification Bot]

Joseph O has marked this topic as resolved.

[Notification Bot]

Joseph O has marked this topic as unresolved.

[Joseph O]

They did say I could share my idea on Zulip

here it is:
add a toList method for the Range structure found in Init.Data.Range so that you can use the list methods to apply transformations on it.

As well as a toString and Repr instance, but that isnt important