Induction eliminator for `Array` and `Vector`

Stream: lean4

[Wrenna Robson]

I quite often find myself wanting to do inductive reasoning on Array and Vector without breaking into the way they are internally constructed.

Could we have something like the following?

--- We don't have this for some reason.
theorem eq_push_pop_back_of_size_ne_zero {xs : Array α} (h : xs.size ≠ 0) :
    xs = xs.pop.push (xs.back <| Nat.pos_of_ne_zero h) := by grind

@[elab_as_elim, induction_eliminator, grind =]
def Array.induction {C : Array α → Sort*} (empty : C #[])
    (push : ∀ (xs : Array α) (x : α), C xs → C (xs.push x))
    (xs : Array α) : C xs :=
  match hxs : xs.size with
  | 0 => eq_empty_of_size_eq_zero hxs ▸ empty
  | n + 1 => eq_push_pop_back_of_size_ne_zero
    (hxs ▸ Nat.succ_ne_zero _) ▸ push _ _ (induction empty push xs.pop)
  termination_by xs.size

@[elab_as_elim, induction_eliminator, grind =]
def Vector.induction {C : ∀ {n : ℕ}, Vector α n → Sort*} (empty : C #v[])
    (push : ∀ (n : ℕ) (xs : Vector α n) (x : α), C xs → C (xs.push x)) :
    {n : ℕ} → (xs : Vector α n) → C xs
  | 0, xs => xs.eq_empty ▸ empty
  | _ + 1, xs => xs.push_pop_back ▸ push _ _ _ (induction empty push _)

Note that it is hard to do reasoning like this in core by reducing an Array or Vector to a List because core lacks a suitable backwards inductive principle for List (and using pop/push is more natural for Array/Vector).

I don't know if these are efficient for programming purposes, but clearly they do eliminate to Sort*, so in principle I think you could use them to programmatically define things. If getElem syntax is preferred instead of back I think that would be also fine. I would be interested in people's thoughts: am I the only one who often finds herself wanting this kind of thing?

[Wrenna Robson]

Relatedly by the way: I think Array.pop_push and Vector.pop_push (and probably Vector.push_pop_back and some suitable version for Array) should have the grind attribute.

[Wrenna Robson]

Obviously these could also have a cases eliminator as well if you so wanted.

[Wrenna Robson]

@Kim Morrison I'm tagging you here because I know you have an interest in ongoing efforts to achieve feature parity between Array, Vector and List.

[Wrenna Robson]

(For List, I think this would probably want to look something like

@[elab_as_elim]
def reverseRec {motive : List α → Sort*} (nil : motive [])
    (append_singleton : ∀ (l : List α) (a : α), motive l → motive (l ++ [a])) : ∀ l, motive l
  | [] => nil
  | a :: l => (dropLast_concat_getLast (cons_ne_nil a l)) ▸
    append_singleton _ _ ((a :: l).dropLast.reverseRec nil append_singleton)
  termination_by l => l.length

Which is a different approach than that which Mathlib's List.reverseRecOn uses but IMO also a better one.)

[Wrenna Robson]

(For whatever reason, l ++ [a] is preferred over l.concat a I believe.)

[Kim Morrison]

This API is intentionally absent as my experience so far suggests that wanting it indicates an #xy problem. Happy to be convinced otherwise.

[Jakub Nowak]

Yeah, I agree with Kim. I think you can use Array for storing data when you wish to gain performance benefit, but any properties about the elements should be stated in terms of a.toList, not a itself. Because List is a logical model of Array. And if you need to do induction on array, it indicates you made an error of not using a.toList.

[Jakub Nowak]

It might be potentially useful to maybe use induction when the motive is not Prop? But I think all reasonable cases should be covered by other API, like iterators, fold etc.

[Eric Wieser]

This was also discussed in #general > Alternative induction principle for Arrays @ 💬

[Eric Wieser]

And #new members > MapM for List.Vector @ 💬

[Eric Wieser]

I'd lean towards saying that we should have the Array.induction API to prevent wasted time discussing this repeatedly, but the docstring should say something like

Note that using this to construct data is very inefficient, consider using ... instead.

My guess is also that this is still a handy thing to have as an induction principle to construct proofs.

[Wrenna Robson]

Kim Morrison said:

This API is intentionally absent as my experience so far suggests that wanting it indicates an #xy problem. Happy to be convinced otherwise.

What do you mean by an #xy problem?

I think what I would say is that I've found it to be needed very naturally when proving things about a program that uses Vector. Specifically reducing down to List would have just confused the situation: what I wanted was to prove properties about operators on Vectors that took a Vector and performed an operation on another Vector (of a different length). I suppose it's hard to convince you that this was natural: but please believe me when I say that I tried doing it the decomposition way and it was really annoying.

I am less sure about the need here for Array. The main reason you would want it is, as I say, because outside of Mathlib the tools for nicely doing proofs from the right on Lists do not exist. I don't actually think List and Array have the same logical model for this reason: the natural way to construct an Array is from the right (by pushing new elements), whereas the natural way to construct a list is from the left (by cons-ing new elements).

I will say that all of this is about proofs. I think Eric is right that using this to construct data would be an obvious trap and so it's possible we should only have this for Prop as deliberate design. I do think it's worth people understanding that it's also wrong to construct an Array using a List, or rather you can do so but it has an O(n) cost.

[Wrenna Robson]

(I will say, and this is a parenthetical remark deliberately, that the fact that Array appears to just be a wrapper around List, and this is true logically but NOT true computationally, I do regard as a much more perilous foot gun. It gives you the property that xs[k] = xs.toList[k], but as I say I think this is the trap: Array has the property that finding its size is O(1) (I think?), and adding and removing elements from the end is cheap and adding and removing elements further from the end is more expensive because you have to move memory. But that is the opposite of how List works, where cons-ing adds to the start, and appending elements to the end are expensive.

Personally I would love a world in which Array was much more tightly sealed, and it was clear that extracting it to a List, performing to toList operation, would give you a list that was the reverse of the list that the type is logically constructed from - because that is I think closer to the computational behaviour (it is O(n) to convert to/from a list to an array). But obviously this would constitute a major design change, and I did not wake up this morning and find myself transformed into Leo de Moura, so I don't expect that change to happen.)

[Wrenna Robson]

Oh: I will say that I have found using the above principle on Vector more well-behaved than inducting on the length (which you would think would behave much the same, but essentially lemmas that give the behaviour of operations on Vectors of the form xs.push x tend to be a bit nicer in practice than operations on Vectors of length n + 1).

[Wrenna Robson]

Having fairly long-term experience with working with Vectors down in the armpit if where maths meets computation, I think that's shaped my views here: I will say I was perfectly fine without these principles for some time, but recently adding them during a refactor to grind-ify a lot of my proofs saved me a frankly hilarious amount of proof lines when proving something about a somewhat tricky fold.

[Jakub Nowak]

Hm, I've just noticed that we have e.g. Array.foldl_toList as a simp lemma. If we want to go via the route of proving properties on array by reducing to list, than that simp lemma should be in the other direction.

[Jakub Nowak]

That might be one reason, why you find it easier to prove things directly on Array?

[Wrenna Robson]

I don't think that's a lemma I used but it does look pretty weird to me.

[Wrenna Robson]

Oh no it's just how it's appearing on my phone. No I didn't use that, but it is an example of the way the library points you away from breaking down to List. Which is consistent with the general principle that breaking something down into its construction is a code smell (and I believe this quite strongly): if you've defined a type made up of another, you probably did that for a good reason, so if that was a good reason don't break it up. If you have a program about Arrays, and you are reasoning on it using Arrays, why break it down? As I've already said, it'll be backwards anyway, and because Core lacks useful facility to reason backwards on a List you might just get yourself into a pickle. Why do it?

[Jakub Nowak]

Would you like to share one of the tricky theorems you had, for testing?

[Wrenna Robson]

Well currently I'm on the way to work - so I can't get easily. I would be happy to but I'm a bit concerned it might be quite difficult to extract it from the context!

[Wrenna Robson]

I will say that having looked up #xy problems, I don't think I believe in them - but I think that might be my bias against ESR in all forms showing.

[Jakub Nowak]

If it's not a problem you can share a link to repo or whole file.

[Wrenna Robson]

Oh, very happy to do that.

[Jakub Nowak]

Wrenna Robson said:

Oh no it's just how it's appearing on my phone. No I didn't use that, but it is an example of the way the library points you away from breaking down to List. Which is consistent with the general principle that breaking something down into its construction is a code smell (and I believe this quite strongly): if you've defined a type made up of another, you probably did that for a good reason, so if that was a good reason don't break it up. If you have a program about Arrays, and you are reasoning on it using Arrays, why break it down? As I've already said, it'll be backwards anyway, and because Core lacks useful facility to reason backwards on a List you might just get yourself into a pickle. Why do it?

If you're reasoning about Array you should break it down to List, because List is meant to be a semantical model of an Array.

[Wrenna Robson]

Right - but as I explained above because reasoning on List naturally happens on the left but you probably aren't wanting to reason about Array on the left, in practice I do not find that to be true.

[Wrenna Robson]

Also, I'm more likely to be working on Vector, and that's frankly two steps removed from an ordinary List.

[Wrenna Robson]

I don't feel it's overstating things to say that if the intent is that you never prove things about Array and only prove things about List, then I think there's many lemmas and hints and simplifications which feel constructed wrong as a joke.

[Wrenna Robson]

https://github.com/linesthatinterlace/controlbits/tree/master/CBConcrete

[Wrenna Robson]

This would be my repo

[Jakub Nowak]

Hm, maybe toList should return the reverse of an array, so thus push is translated directly to cons. Or we should improve List API so that it can work well backwards too. There's a lot of symmetry between List.cons and List.concat, but iirc there are lemmas about cons that are missing an equivalent statement about concat.

[Wrenna Robson]

Jakub Nowak said:

Hm, maybe toList should return the reverse of an array, so thus push is translated directly to cons. Or we should improve List API so that it can work well backwards too. There's a lot of symmetry between List.cons and List.concat, but iirc there are lemmas about cons that are missing an equivalent statement about concat.

The former is what I feel should be the case, yes - but as I say it seems such a major change that I don't expect it to ever happen.

There is a lot of symmetry between List.cons and List.concat, although note that the preferred spelling of xs.concat x is xs ++ [x] - as in, that is what it simplifies to. Now I disagree with that too but I've long accepted that's not an argument I can win.

[Wrenna Robson]

I think it would be nicer to use List.concat because passing to append can often lead to bringing in a bunch of append-logic that you may not actually want - like notably we do not automatically simplify as.push x to as ++ [x] for Arrays.

[Jakub Nowak]

Wrenna Robson said:

I don't feel it's overstating things to say that if the intent is that you never prove things about Array and only prove things about List, then I think there's many lemmas and hints and simplifications which feel constructed wrong as a joke.

I see that now too. Tbh, it looks like what I wrote here #lean4 > Induction eliminator for `Array` and `Vector` @ 💬 is completely wrong, and the intention of the API is to use Array for proofs as well. In which case, we should go full commitment in this direction, and we should have induction principle for Array. Maybe @Kim Morrison could shed more light on this, because now, I don't understand why he believes that API should be absent.

[Wrenna Robson]

I'm trying not to be too prescriptive in my opinions here - I don't pretend that my way is the best way or anything. But I am not new to this either and my control bits work has been a pretty extensive exercise in trying to produce a theory on a thing - and while I'm not sure there's a place for that work in the libraries, I have generated a bunch of opinions and lemmas which I am slowly trying to filter out and suggest for inclusion into the libraries where appropriate.

[Wrenna Robson]

Kim uses she/her, I thought?

[Wrenna Robson]

Apologies if I have that wrong.

[Wrenna Robson]

Jakub Nowak said:

Wrenna Robson said:

I don't feel it's overstating things to say that if the intent is that you never prove things about Array and only prove things about List, then I think there's many lemmas and hints and simplifications which feel constructed wrong as a joke.

I see that now too. Tbh, it looks like what I wrote here #lean4 > Induction eliminator for `Array` and `Vector` @ 💬 is completely wrong, and the intention of the API is to use Array for proofs as well. In which case, we should go full commitment in this direction, and we should have induction principle for Array. Maybe Kim Morrison could shed more light on this, because now, I don't understand why he believes that API should be absent.

I think to be fair to you what the API is is ambivalent. Which arguably is a perfectly fine approach - it's nice to give people different ways of doing things - but necessarily does create more surface area.

[Wrenna Robson]

Incidentally, while I am in general not a fan of Mathlib's List.Vector, it does fill a semantic niche: if you think of List as representing a fundamentally static value (whereas Vector and Array are dynamic), then actually the context I was using Vector (you want to look for condFlipBit in my repo) is more static than dynamic (I'm operating on a Vector - it's definitely dynamic - but using values in a Vector that is relatively more static - though because that vector could result from a dynamic process I have stored it that way). I might have used List.Vector there I suppose, because that's I think the only tool that semantically represents static arrays of a fixed size?

As it is, I did very much want to make sure things were as performant as I could manage (and I still have ways I could improve that) so I did use Vector to avoid any hidden List traps, anyway.

[Wrenna Robson]

The context, very shortly, is that you have some vector of values xs, and some vector of bits bs, which might be half the length but that isn't strictly necessary. You fold along bs, and for every bit in bs, you conditionally swap two values in xs, based on the index you are at. In this way the vector of bits acts to permute the members of the vector of values xs, but desirable for suitable types of value (specifically unsigned integers!) you can construct this swap operation in a way that doesn't branch on the value of the bits (not in Lean, I don't think we have a way to model that, but this motivates the construction). This means that you perform the permutation of the value vector in constant time.

[Wrenna Robson]

Essentially this work is about the algorithm/formula that lets you decompose an arbitrary permutation into a sequence of such twiddles

[Wrenna Robson]

And hence lets you permute arbitrary value vectors in constant time.

[Wrenna Robson]

Don't get distracted by this though, I just thought a little context might help. This is something I've been working on on and off for a good while, it was from my thesis, but I'm currently working with a PhD student to finally publish our work on some speed improvements to the algorithm that also happily make the verification elements easier to work with by removing a very much complex recursion in favour of a straightforward iterative loop.

[Jakub Nowak]

Wrenna Robson said:

I might have used List.Vector there I suppose, because that's I think the only tool that semantically represents static arrays of a fixed size?

Well, semantically List.Vector and Vector are the same. Just like List and Array are. The difference is mainly (and in ideal world should be the only) in compiled program. List.Vector doesn't have a constant time arbitrary access I think? So depending on how you use it, Vector can be significantly faster.

[Wrenna Robson]

I think essentially I regard the compiled behaviour as part of the semantics. I realise that might not be the technical definition.

[Wrenna Robson]

But like, if one thing represents "dynamic C-style arrays" and one thing represents "functional-programming style inductive lists", then these are to me different things that I should think about as different. The fact that they are naturally equivalent to each other notwithstanding.

[Jakub Nowak]

I should probably call it logical model, instead of semantics, to be more clear.

[Jakub Nowak]

And by which, I mean the kernel representation.

[Wrenna Robson]

Right, for sure.

[Wrenna Robson]

When you get down to the kernel representation I agree there's no distinction between Array and List, but we do care about the difference. That's why, for instance, Array.cons does not, I think, exist? It is a natural operation on the underlying list but not on the Array it represents.

[Jakub Nowak]

Array.cons isn't useful in programming, because it would have bad performance, and the fact that if someone uses Array they already care about performance. And because as you said, most reasoning on Array happens backward, there was no need for it in proofs either.

[Wrenna Robson]

Yeah 100% - I think it's good that it doesn't exist for that reason!

[Wrenna Robson]

And that's why I think I'm persuaded that the eliminators under discussion would not be good as general-purpose eliminators - because I don't think you'd want people to use them in programming.

[Jakub Nowak]

Oh, wait, there's Array.toList_push, which rewrites (xs.push x).toList = xs.toList ++ [x]. This is the direction I would want, it replaces array operation Array.push with list operation ++. On the other hand there's Array.foldr_toList which rewrites List.foldr f init xs.toList = foldr f init xs, and this is completely opposite. It replaces list operationList.foldr with array operation Array.foldr. I don't see what is the reasoning behind this.

[Wrenna Robson]

toList_push makes sense to me though: at the stage you have applied toList, that is the conversion you want to make (as xs ++ [a] is the simp-normal form of concat on Lists). But the latter one also makes sense to me - if you are folding over an array converted to a list, you could have just folded over the Array.

[Wrenna Robson]

I don't see that these are contradictory - if you convert to List, you should use the former, but if you have converted to List and are folding, really you should just have folded over the Array.

[Wrenna Robson]

I have a question for you: which do you consider the better extension lemma for Array, Array.ext or Array.ext'?

[Jakub Nowak]

Well, any direction can make sense in some context. But for simp we should simplify in the direction where there's more useful lemmas to be found. That's why I think we should always simplify to list operations.

[Wrenna Robson]

But there are a host of useful lemmas to be found for folding on Arrays!

[Wrenna Robson]

Consider Array.foldr_push

[Wrenna Robson]

Or indeed even something more exotic like Array.foldl_induction

[Wrenna Robson]

(Sorry if my replies are a little slow - I am finding the docs website very slow this morning.)

[Jakub Nowak]

But if you replace a.push with a.toList.concat than you can apply List.foldr_concat instead of Array.foldr_push.

If we have an API for Array as complete as for List, than we shouldn't simplify Array operations to List operations. But, we could also choose to not have any lemmas for Array at all, and prove everything via lists. This might make proving things about Arrays slightly harder in some cases, but I think in most cases this wouldn't make a difference, as long as you make sure to start your proofs with dsimp to rewrite all arrays to lists. Though I'm not too sure about how much of "slightly harder" this would be. And the important question is whether it's worth further working on and maintaining API for Array.

[Wrenna Robson]

Jakub Nowak said:

But if you replace a.push with a.toList.concat than you can apply List.foldr_concat instead of Array.foldr_push.

If we have an API for Array as complete as for List, than we shouldn't simplify Array operations to List operations. But, we could also choose to not have any lemmas for Array at all, and prove everything via lists. This might make proving things about Arrays slightly harder in some cases, but I think in most cases this wouldn't make a difference, as long as you make sure to start your proofs with dsimp to rewrite all arrays to lists. Though I'm not too sure about how much of "slightly harder" this would be. And the important question is whether it's worth further working on and maintaining API for Array.

Remember, we don't use List.concat, despite calling it that in theorem names :upside_down:

[Wrenna Robson]

You would have to replace a.push with (a.toList ++ [·]) as that is the normal form.

[Jakub Nowak]

Wrenna Robson said:

I have a question for you: which do you consider the better extension lemma for Array, Array.ext or Array.ext'?

I would say Array.ext'.

[Wrenna Robson]

That makes sense given your stated perspective! It is a little strange then that it is ext' and not ext. And it is Array.ext that is tagged as an ext lemma by... somewhere in the libraries, it might be a choice Mathlib makes.

[Wrenna Robson]

Moreover I would argue that most of the time it is the one that is more useful...

[Jakub Nowak]

Yeah, most of the API suggests, that it is what mathlib choses. In which case, I think we should have induction eliminator.

[Wrenna Robson]

You could reasonably argue it should only be in mathlib - I would make a case for Batteries at least (though I will admit I am not clear on the borderline).

[Wrenna Robson]

But I think it is a natural thing you would want to do in programming - at least sometimes.

[Jakub Nowak]

I should say, that my perspective might come from my software verification background. In software verification there's usually clear distinction between data, and the logical model of it.

[Wrenna Robson]

My background is... a whole mess of things. Which probably reflects my tendency to have a whole mess of approaches :)

[Jakub Nowak]

Jakub Nowak said:

Oh, wait, there's Array.toList_push, which rewrites (xs.push x).toList = xs.toList ++ [x]. This is the direction I would want, it replaces array operation Array.push with list operation ++. On the other hand there's Array.foldr_toList which rewrites List.foldr f init xs.toList = foldr f init xs, and this is completely opposite. It replaces list operationList.foldr with array operation Array.foldr. I don't see what is the reasoning behind this.

Yeah, I see the reasoning now. The point is, that if you explicitly use Array.toList, only than will simplifier simplify array operations to list operations.

[Wrenna Robson]

Yeah I totally agree - but only when you do that, you have to make that choice.

[Wrenna Robson]

For Vector, I would argue that Vector.ext is the only sensible extensionality lemma, myself - it just makes very little sense to me to drop that back to Lists.

[Wrenna Robson]

essentially, I prefer to argue that two vectors or arrays are equal by saying "well they have the same length" (don't need this for vectors) and "the element at each index is the same".

[Wrenna Robson]

Because if I argue instead "they are the same because the two lists are the same", how will I argue the two lists are the same? Almost certainly by... comparing the lengths and the value at indexes!

[Jakub Nowak]

I agree with you. I think my only point towards my approach is that almost all of Array API is duplicated code from List. Ideally, I would want for this duplication to not be necessary. But, unfortunately, it does make API easier for its consumers. I do hope that as the Lean languages gets better, notably automation tactics like grind, this duplication would end up not having any benefit. I'll still try to use your repo to check how much of an benefit it actually is.

[Wrenna Robson]

I can't say that all the code is there is definitely my best :) - I try to keep it up to date and improve it but it has grown over time.

[Wrenna Robson]

When I started this repo, Vector didn't exist - indeed at that stage I defined it for myself and had to remove it when it was officially added, but happily I had named all my lemmas the sensible thing so I could mostly strip out with no pain.

[Jakub Nowak]

Wrenna Robson said:

That makes sense given your stated perspective! It is a little strange then that it is ext' and not ext. And it is Array.ext that is tagged as an ext lemma by... somewhere in the libraries, it might be a choice Mathlib makes.

We made a mistake here, namely, Array it not in Mathlib. It's in Std.

[Wrenna Robson]

Yes, but I am not sure where the @[ext] attribute is :)

[Robin Arnez]

@[ext] is also core (docs#Lean.Parser.Attr.ext in Init.Ext)

[Wrenna Robson]

Yes, what I mean is I don't know where the @ext] attribute gets attached to Array.ext

[Wrenna Robson]

https://github.com/leanprover/lean4/blob/2fcce7258eeb6e324366bc25f9058293b04b7547/src/Init/Ext.lean#L85-L85

[Wrenna Robson]

However the answer is indeed Std!

[Wrenna Robson]

It is in Init.Ext

[Wrenna Robson]

Thanks for that, that is a sensible place to look.