rcases speed

Stream: lean4

[Jakob von Raumer]

I have a big proof goal with lots of existentially bound variables and I destruct it like this:

  rintro ⟨_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,h⟩
  rcases h with ⟨_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,h⟩
  rcases h with ⟨_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,h⟩

Is there any faster way to do this?

[Johan Commelin]

Do you mean faster or shorter? Maybe something with repeat?

[Jakob von Raumer]

Faster :sweat_smile:

[Mario Carneiro]

how fast is it? MWE?

[Mario Carneiro]

I think this will be slow because there will be many instantiate calls to create the fvars, which results in quadratic behavior. This is a really hard problem somewhat fundamental to locally nameless processing of DTT

[Mario Carneiro]

@Jakob von Raumer But I would be remiss to not ask for an #xy of your problem here. Why do you have so many existentials?

[Geoffrey Irving]

The pun is really loud here.

[Jakob von Raumer]

@Mario Carneiro In short, the proof terms are automatically generated and correspond to the semantics of functions, with intermediate results of operations often bound existentially

[Jakob von Raumer]

Thanks for the explanation anyways, seems like there's probably not really an easy way around it then

[Jakob von Raumer]

Will try to create an MWE

[Jakob von Raumer]

iterate 116 (rcases h with ⟨_,h⟩) is definitely quicker, at least