Stream: MetaCoq

Topic: Gallina quotation functions


view this post on Zulip Jason Gross (Feb 11 2023 at 22:15):

Would there be interest in having functions building up to things like quote : Ast.term -> { t : Ast.term & Σ ;;; [] |- t <% Ast.term %> } and quote : forall t Γ t T, (Σ ;;; Γ |- t : T) -> { qt : Ast.term & Σ ;;; [] |- qt : <% Σ ;;; Γ |- t : T %> } (roughly, the latter doesn't actually use <% but splices in some quotation functions for Γ, t and T)?

The use-case would be being able to do metatheory reasoning about what Coq can prove about itself.

I have functions for the first projections of these already that I can prepare a PR for, and am (slowly) working towards the typing derivations.

view this post on Zulip Yannick Forster (Feb 11 2023 at 22:20):

I think there'd be huge interest :)

view this post on Zulip Jason Gross (Feb 11 2023 at 22:41):

Should the target of quotation be Template.Ast, or PCUIC.Ast? Or should I do both?

view this post on Zulip Yannick Forster (Feb 11 2023 at 22:42):

I'd say whatever is easier. We can translate one to the other, even in practice, right?

view this post on Zulip Jason Gross (Feb 11 2023 at 22:44):

They're both pretty easy. In fact the code will be almost exactly the same, the question is just whether I build the automation in the Template monad or the PCUIC Template Monad, so submitting code for both will not be much harder than submitting code for one. But I guess PCUIC will probably be easier to build typing derivations for, if I want to eventually use the safechecker?

view this post on Zulip Yannick Forster (Feb 11 2023 at 22:47):

Yes, that sounds reasonable

view this post on Zulip Yannick Forster (Feb 11 2023 at 22:48):

You get a quotation function for reduction as well then, right?

view this post on Zulip Jason Gross (Feb 11 2023 at 22:48):

Yes

view this post on Zulip Jason Gross (Feb 12 2023 at 03:25):

https://github.com/MetaCoq/metacoq/pull/837 has the common automation that I used to write the quotation functions, and most of the decidability results I need. Let me know if I should adapt anything for the local style, or document tactics more, etc.

https://github.com/MetaCoq/metacoq/pull/838 is on top of that and contains the one Admitted I don't know how to resolve (about the spec mismatch between gc stuff and the non-gc stuff).

I hope to have the PR with quotation functions coming soon


Last updated: Mar 29 2024 at 09:02 UTC