Stream: Coq users

Topic: Controlling and remembering reductions


view this post on Zulip Matthieu Sozeau (Feb 01 2024 at 13:37):

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 :)

view this post on Zulip Gregory Malecha (Feb 01 2024 at 17:21):

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

view this post on Zulip Clément Pit-Claudel (Feb 05 2024 at 21:40):

@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: Oct 13 2024 at 01:02 UTC