Rewrite all instances of a type

Stream: Is there code for X?

[Jeremy Salwen]

Hello, I want to rewrite all expressions of type Array in my expression using an equality List.toArray (Array.toList a) = a. I tried using simp with singlePass option:

import Mathlib.Tactic.NormCast
import Std.Data.Array.Lemmas
import Std.Data.Array.Basic
import Std.Tactic.NormCast.Ext
import Mathlib.Tactic.SimpRw

open Lean Meta

lemma toArrayRoundtrip (a:Array α): List.toArray (Array.toList a) = a := sorry


lemma all_array (a:Array α) (b: Array α) (p: α -> Bool): (Array.all a p) ∧ (Array.all b p) = Array.all (a++b) p := by
    simp (config := {singlePass := true}) only [← toArrayRoundtrip]

But it does not rewrite all instances, (although it does most of them):

⊢ Array.all a p 0 (Array.size (List.toArray (Array.toList a))) = true ∧
  Array.all b p 0 (Array.size (List.toArray (Array.toList b))) =
    Array.all (a ++ b) p 0
      (Array.size (List.toArray (Array.toList (List.toArray (Array.toList a) ++ List.toArray (Array.toList b)))))

What is the reason it is skipping some instances of a? Is there some way I can configure it to do all of them?

[Yaël Dillies]

Un #xy-ing, I assume you want to do this to derive an Array result from the corresponding List one? The better solution in that case is refine Array.toList_injective ?_ and then push the toList inwards (which hopefully simp lemmas are already configured to do).

[Jeremy Salwen]

I think you have gone a bit to far in deciphering my problem. I am experimenting with writing tactics, and I really do want to understand what is happening here.

[Yaël Dillies]

At any rate, you have to explain exactly what you mean by "all instances", because when you rewrite a = List.toArray (Array.toList a), you get a new occurrence of a.

[Mario Carneiro]

with singlePass mode I think that is not a problem because once a subterm is rewritten it is not revisited

[Mario Carneiro]

I think the main issue here is that Array.all is a dependent function and so simp is bad at rewriting occurrences of a

[Mario Carneiro]

this is probably poor API design, the dependent args are defaulted so you don't notice them until you try to rewrite

[Eric Wieser]

Why is docs4#Array.all dependent?

[Mario Carneiro]

I guess so that you can specify the start and stop points?

[Eric Wieser]

Wait what, why does it have start and stop arguments?

[Mario Carneiro]

seems like a better use for Subarray.all

[Eric Wieser]

I didn't know docs4#Subarray existed, and was about to advocate for it

[Mario Carneiro]

in fact I would bet that those arguments exist exactly because they are needed by Subarray.all

[Mario Carneiro]

but having them secretly there in the main function causes a lot of issues

[Eric Wieser]

Yaël Dillies said:

The better solution in that case is refine Array.toList_injective ?_ and then push the toList inwards (which hopefully simp lemmas are already configured to do).

I'm not convinced by this; I think the "better" solution is to induct on a and b

[Eric Wieser]

I don't know what the default induction principle on Array is (it would be great if the docs would show this), but if it's not the one that introduces List.toArray then there should be a manual one that does.

[Mario Carneiro]

If you just destruct it you get Array.mk, not List.toArray

[Yaël Dillies]

Are you sure? Your solution requires rewriting distributivity lemmas backwards. Mine only requires them forward.

[Yaël Dillies]

In particular, in your solution it will be hard to handle [] ++ List.toArray l.

[Mario Carneiro]

you want to prefer Array.mk and Array.data over List.toArray and Array.toList

[Mario Carneiro]

yes, both pairs of functions exist and they are not defeq

[Eric Wieser]

Why?

[Mario Carneiro]

because List.toArray is the definition of Array.mk

[Mario Carneiro]

which is brain warping since Array.mk is the constructor

[Eric Wieser]

docs4#List.toArray

[Mario Carneiro]

from a proving standpoint, List.toArray is just a rube goldberg way to write the constructor

[Eric Wieser]

Should it be private?

[Mario Carneiro]

I think that would help (and renaming it to e.g. Array.mkImpl)

[Yaël Dillies]

/heavily marked as not for use?

[Eric Wieser]

The only reason it exists is the attribute that connects it to the compiler, right?

[Mario Carneiro]

right, it could be private

[Mario Carneiro]

it is nice to know we can prove the two functions equal, not sure where that would go otherwise

[Eric Wieser]

Can we use that fact with @[csimp]?

[Mario Carneiro]

I thought about that but it would probably throw the compiler for a loop (literally) since it's trying to make Array.mk call List.toArray

[Jeremy Salwen]

Mario Carneiro said:

I think the main issue here is that Array.all is a dependent function and so simp is bad at rewriting occurrences of a

I see that makes sense. simp is the best way we have to rewrite dependent types though, right? There is not some other tool that would be better at rewriting here?