search

coq-community / aac-tactics

Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]
https://coq-community.org/aac-tactics
Other
29 stars 21 forks source link

Replace calls to "vm_compute in hyps" by plain calls to vm_compute. #138

Open silene opened 5 months ago

silene commented 5 months ago

The terms are of type Internal.T env_sym, so invoking vm_compute in on them ends up strongly normalizing the function env_sym, which explodes. By using eval vm_compute instead, only the bodies get strongly normalized.

This is related to coq/coq#18917.

SkySkimmer commented 5 months ago

Is this different from vm_compute in (value of x)?

palmskog commented 5 months ago

@silene fine by me, do you advise this should be merged right away?

silene commented 5 months ago

@SkySkimmer No, it is the same. (That said, the location of the casts in the produced proof term might be slightly different. I never remember the precise rules for change, unfold, and vm_compute.)

@palmskog No hurry. It will only make things faster for users of aac_normalise, which I don't know if there are. So, it can wait until the next release.

SkySkimmer commented 5 months ago

Until https://github.com/coq/coq/pull/18796 there is no cast when using in hyp regardless of base tactic used.