You can also just use reification inside tactics — basically, you *can* analyze formulas in Ltac(1/2) or other tactic languages.

That lets you convert formulas from a shallow to a deep embedding; however, in this scenario there's no need for a deep embedding of *derivations*

I think the Diaframe automation for Iris implements quite a lot directly using typeclass inference, which doesn't even need a deep embedding

Thanks! Do you know of examples of how to perform this conversion using Ltac?

I was thinking of proving soundness of the entailment procedure too - would that be doable for a procedure written in Ltac?

http://adam.chlipala.net/cpdt/html/Cpdt.Reflection.html is an introduction to proof by reflection. While for instance https://arxiv.org/abs/1102.1323 Sec. 9 shows how to achieve quoting using typeclass search.

You can't do proofs about Ltac, but to prove entailment correct, you can still write it in Coq — only "reification" must happen via metaprogramming.

Concretely, once you have quoted your shallowly embedded goal `g`

to a deeply embedded goal `G`

such that `eval G = g`

, you _can_ perform your transformation via a _Coq_ (Gallina) function `f : tactic`

transforming the goal to a new one — for instance you could define `tactic`

as `∀ G : Goal, { newG | eval newG -> eval G }`

.

Thanks, will check those out!

@towokit928 also you _might_ be interested in https://iris-project.org/ — the Iris separation logic framework is very flexible, its engineering is pretty robust, and the ecosystem includes projects on automation like Diaframe. But probably less appropriate if you want a minimal system.

Foundations of separation logic teaching material links: https://chargueraud.org/teach/verif/

Last updated: Jun 23 2024 at 05:02 UTC