Add PCUIC versions of tmQuote and related template monad definitions

[JasonGross]

On top of #774

This will allow easier creation of developments that reason about doubly-quoted terms and judgments. (In particular, I'm trying to prove Löb's theorem.)

This PR should compile, and I think it's basically ready, but I'm not terribly happy with the names, and it currently uses a hack to get a fixpoint combinator in the template monad. Please suggest better names, better organization, better implementations, etc.

Note that I needed Local Unset Universe Minimization ToSet. in a couple places to avoid universe inconsistencies.

[TheoWinterhalter]

I'm not sure I understand the goal of having the template monad in PCUIC. PCUIC does not have a runtime so what is it supposed to be?

To my mind, PCUIC should be plainly about the theory / specification, and Template should be about the implementation. In that respect, having the type checker in PCUIC is wrong but well…

[JasonGross]

I guess calling it "a PCUIC version of the template monad" is perhaps a bit misleading or over-general; the thing I actually need here is "a PCUIC version of tmQuote".

I have written a Gallina function quote : Template.Ast.term -> Template.Ast.term whose behavior on ground terms is the same as the tactic quote_term. Judicious use of automation means that it only took 100 loc. I now want to prove that this function generates only well-typed terms, and in particular that it takes quoted sorts to doubly-quoted sorts, takes types to doubly-quoted types, and takes terms to well-typed doubly-quoted terms of the doubly-quoted type (at least in the empty context). As I understand it, typing judgments exist only on PCUICAst.term (is this right?), so I need a Gallina function quote that adds a layer of quotation for these ASTs (and typing judgments). In writing these functions, it's convenient to be able to bypass the template AST entirely and have quotation tactics that deal only with PCUIC, because that makes writing automation to build the quoter simpler.

Said another way, I'm trying to prove Löb's theorem about the theory. This is a lot nicer if I can leverage notations and tactics to to quotation for me rather than having to do it all by hand.

[TheoWinterhalter]

Well, typing also exists for Template: https://github.com/MetaCoq/metacoq/blob/coq-8.16/template-coq/theories/Typing.v#L741 and the translations between Template and PCUIC are both shown to be type preserving I think.

[JasonGross]

Ah, neat, thank you! How much of the theory is present for typing derivations in Template? (Is there a fueled axiom-free reflective typechecker for typing deriviations, for example?)

[mattam82]

I guess once we get the trailing whitespace one we can revisit this. Having a monad that works on the PCUIC presentation does not sound bad to me, it's a lot easier to program in Coq on PCUIC terms without having to worry about well-formendness than on "template" ones.

[JasonGross]

I guess once we get the trailing whitespace one we can revisit this.

Trailing whitespace has been merged, and I've rebased this. Still on top of #790 and #789, but it should be reviewable now.

[mattam82]

Let's have #789 and #790 first

[JasonGross]

Dependencies have been merged, this should finally be ready for review and hopefully merging. I've added some tests to the test-suite as well.

[mattam82]

LGTM !