Simpl by cbv

[MSoegtropIMC]

This PR adds the following functionality:

• an Elpi based set of functions to create lists of symbols used for delta reductions with cbv

  • the lists are constructed e.g. from all transparent definitions in a set of modules
  • detailed editing like removing or adding individual symbols is supported
  • the lists are named and one can create as many individual lists as required and use them by name in reduction tactics
  • the lists are written to Coq files in Elpi and Ltac2 format and checked into Git, so that Elpi is not required to run VST
  • the Elpi version required to create the lists is 1.16.0 (one newer as in current Coq Platform)
  • the symbol lists are expected to change rarely, so checking in the files is likely not an issue

• a set of Ltac2 functions and tactics which perform restricted cbv reductions

  • one can supply named delta symbol lists created with the tools above
  • one can restrict the reductions to the arguments of the application of a specific head symbol
  • VST specific variants exist which add Clightgen generated names for symbol table indices to the delta symbol list

• a similar set of reduction functions written in Elpi is also supplied, but this is experimental

  • the main limitation is that Elpi cannot yet handle mutual fixpoints

• the simplification by cbv is prepared for use in one place in file floyd/go_lower.v by replacing a call to simpl with a call to a dedicated tactic. But currently this tactic is still defined to use simpl because switching to cbv leads to some differences in goals left by the entailer.

The point of this PR is two fold:

• make VST floyd faster - I have seen cases were cbv reduction takes 30ms where simpl takes 70s.
• make VST floyd more reliable - using simple on terms which contain user terms like variable values from the C program can lead to arbitrary blow up. By contrast cbv with a well defined delta symbol list does only very specific reductions

I expect to do another PR soon which contains a reflexive tactic for Z/Int range proofs - a common goal in entailment. Larger rework in the entailer caused by the move to cbv should wait until this PR.

Creating two new top level folders "elpi" and "ltac2" might be excessive - maybe these should go under floyd. I expect that long term VST will use more ltac2 and elpi tactics, so that having such folders makes sense. The Ltac2 standard library is a bit terse, so that it is common to have a bit of Ltac2 utility code, which needs to be organised.

[MSoegtropIMC]

@andrew-appel : sorry there is one issue with this PR - I did it on Apple silicon (ARM) - the symbol tables will be different for Intel and ARM. I can check this tomorrow - today I don't have access to an Intel machine.

I also need to think about a way to abstract this ...

[MSoegtropIMC]

FYI: I have to delay this a bit - I am working on the Coq Platform release (after the 8.16.1 release).