array getelem simp nf

Stream: lean4

[James Gallicchio]

is it possible for simp to normalize getElems to use either Fin arr.size or Nat in the index? Right now both are simp-normal, and rewriting between these forms is quickly becoming not worth the pain :weary:

I'm guessing the Nat-indexed access is quite reasonable to be simp-normal, and everything should be rewritten into that form.

[James Gallicchio]

(I still am suspicious whether the Fin form is even necessary, but I haven't tried removing it)

[James Gallicchio]

I'm also realizing the value of moving a SetElem class into std so we can do similar normalization for sets. I'm doing lots of manual proving that should just be solved by simp.

[Mario Carneiro]

James Gallicchio said:

is it possible for simp to normalize getElems to use either Fin arr.size or Nat in the index? Right now both are simp-normal, and rewriting between these forms is quickly becoming not worth the pain :weary:

are you sure? I see this:

@[simp] theorem getElem_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
    a[i] = a[i.1] := rfl

which suggests that the Nat form is simp-normal

[James Gallicchio]

:thinking: that does suggest that

[James Gallicchio]

why is that one not triggering? I will investigate

[James Gallicchio]

okay, I think this is just me not understanding simp :) I have a hypothesis roughly like \forall (i : Fin arr.size), arr[i] ..., and simp doesn't rewrite that getElem until the hypothesis is specialized.

[James Gallicchio]

er, no, it is rewriting it

[James Gallicchio]

hm. cannot reproduce anymore