Jason Gross (Feb 11 2023 at 22:15): 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.
Yannick Forster (Feb 11 2023 at 22:20):I think there'd be huge interest :)
Jason Gross (Feb 11 2023 at 22:41):Should the target of quotation be Template.Ast, or PCUIC.Ast? Or should I do both?
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?
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?
Yannick Forster (Feb 11 2023 at 22:47):Yes, that sounds reasonable
Yannick Forster (Feb 11 2023 at 22:48):You get a quotation function for reduction as well then, right?
Jason Gross (Feb 11 2023 at 22:48):Yes
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: Jun 03 2023 at 15:31 UTC