array induction

Stream: general

[Sean Leather]

Given a theorem statement involving an array, what might I use in the proof where I would normally use induction if the array were instead a list?

[Sean Leather]

In particular, I have array.to_list in the statement. It seems like I might use induction on the nat size of the array, since the core of array.to_list is d_array.rev_iterate_aux.

[Sean Leather]

Or: not the size but the index into the d_array.

[Mario Carneiro]

It depends on the statement

[Mario Carneiro]

If you can have the array length vary, it might be easier to prove by induction over all vectors of any length

[Mario Carneiro]

If the array is fixed, then you may need to do induction on the index, which is messier

[Sean Leather]

So, I've got this:

@[simp] theorem to_list_zero (a : array 0 α) : a.to_list = [] := rfl

And I'm looking at this:

@[simp] theorem to_list_succ {n : ℕ} (a : array (n+1) α) :
  a.to_list = a.read ⟨n, nat.lt_succ_self n⟩ :: a.pop_back.to_list := _

But I think to_list does a reverse fold, which means the above is not true.

[Mario Carneiro]

to_list produces a list in the same order as the index

[Mario Carneiro]

rev_list produces a list in reverse order (which turns out to be a bit easier to define)

[Mario Carneiro]

so I think you want that statement to be on rev_list

[Minchao Wu]

This reminds me something: do we have an eliminator for finset that eliminates a s : finset to any Sort?

[Minchao Wu]

Somewhere in mathlib?

[Mario Carneiro]

If it is going all the way back to lists under permutation, it's easier to just do cases on the finset and the quot.lift, i.e. define it via multiset

[Mario Carneiro]

what would the type of such an eliminator be?

[Mario Carneiro]

Plus, if you are doing dependent elimination over a quotient the compatibility hypothesis is a mess to work with

[Minchao Wu]

Right, I just looked into the multiset.lean and saw your comments on the dependent recursor