Somewhat relatedly to https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Soliciting.20feedback.20on.20kernel.20reduction.20primitives/near/395856098 there was a question raised at CoqPL on controlling reduction and through discussions with @Gregory Malecha and @Clément Pit-Claudel it seems there is an interest to extend the calculus with a way to record reduction steps performed during proofs so that they are reliably replayed the same way during re-typechecking e.g., to avoid dreaded seemingly non-terminating Qeds.

In a slightly different direction, I would like to be able to inject back in Coq's kernel the certified evaluator we have built in MetaCoq / CertiCoq, which should also bring benefits in the evaluation of reflexive tactics. This `CertiCoq Eval`

extracts, compiles to assembly and can read back values of closed first-order inductive types from the evaluated program, and it is proven correct (reduction is weak call-by-value).

I think an interface like a new cast kind `type cast_kind = Strategy of strategy`

with strategy representing a reification of a reduction strategy including paths in the inferred type, applications of a specific reduction rule, ... or call to a specific evaluator could be the way to represent both of these functionalities. This is just an idea at the moment, we should brainstorm some more about this.

ACTION: please give a thumbs up to this message if you would be available in the coming weeks to chat about this, I'll set up a doodle if there is interest.

Let's gather use cases and constraints such an extension should satisfy here :)

@Janno and @Rodolphe Lepigre would be interested in this.

@Matthieu Baty did a 6-months internship in my lab to explore some of this, but it didn't lead to patches. He has notes here: https://mbty.fr/blog/coq/expr_transfo/intro (the final thing we had was Coq patches to do atomic reductions, but not recorded in the kernel).

Last updated: Jun 22 2024 at 16:02 UTC