This is the topic to ask questions on the talk "FPC-Coq: Using ELPI to elaborate external proof evidence into Coq proofs".

Bump

Q: IIRC in FPC you had certificate formats for provers like E. Would it be feasible to call E and elaborate the certificate to CIC?

Why do you call the FPC kernel a "kernel"? Did I understand correctly that its role is proof search (as opposed to the Coq kernel, whose role is proof checking)?

are the FPC proofs (proof evidence) suitable for outside storage in some binary/textual format? how do they compare in size to storing proof terms?

Is there a link to underlying logic foundations (intuitionistic vs. classical etc)

Cool!

Would ELPI be a good framework to write rule based simplifers?

I mean fine controled term transformations

Thanks!

Zak Chihani and I wrote a paper where we developed some FPCs for rewriting/equality reasoning: http://dx.doi.org/10.1016/j.entcs.2016.06.007 This was largely a "proof of concept" paper but we see no problem in dealing with rewriting with low-level and high-level control.

Andreas Röhler said:

Is there a link to underlying logic foundations (intuitionistic vs. classical etc)

The current system only deals with essentially first-order intuitionistic logic. We do have simple techniques that can take proof certificates in first-order classical logic and use them as proof certificates for negation translations in intuitionistic logic.

Karl Palmskog said:

are the FPC proofs (proof evidence) suitable for outside storage in some binary/textual format? how do they compare in size to storing proof terms?

Coming back to your question, yes, proof certificates are absolutely suitable to be stored, and they frequently are. A certificate format definition includes the syntax and typing rules for the constructors, so other tools can resort to this to interpret concrete certificates. In the simple proof scripts inlined as calls to tactics defined by Elpi, the name of the tactic determined the initial certificate constructor, and the arguments were simply passed along.

Andreas Röhler said:

Is there a link to underlying logic foundations (intuitionistic vs. classical etc)

This paper also written by @Dale Miller offers a comprehensive overview of the framework, I think: https://hal.inria.fr/hal-01390912.

Enrico Tassi said:

Q: IIRC in FPC you had certificate formats for provers like E. Would it be feasible to call E and elaborate the certificate to CIC?

Thinking about it, I seem to recall the certification of E proofs covered a small fragment of the many rules that E output. On the other hand, more standardized proof evidence such as that produced by SAT or SMT solvers seems much easier to adapt.

@Michael Soegtrop Dale already commented on his paper with Zak, but if you want to discuss the kind of things you have in mind, that would certainly be interesting to me. :slight_smile:

Roberto Blanco: one of the larger projects for which I am looking for good ways of doing it is porting the rule based symbolic integrator Rubi (https://rulebasedintegration.org/) to Coq. The rules and preconditions in the rules are quite typical for other term rewriting / controlled simplification problems I have. Prolog would be a reasonable language to do this outside of Coq, so ELPI might be a good way for doing it inside Coq. What is your opinion?

Here is a link to an (arbitrary picked) rule file (Mathematica Syntax): (https://github.com/RuleBasedIntegration/Rubi/blob/master/Rubi/IntegrationRules/4%20Trig%20functions/4.1%20Sine/4.1.9%20trig%5Em%20(a%2Bb%20sin%5En%2Bc%20sin%5E(2%20n))%5Ep.m)

The predicates used in there are defined here (https://github.com/RuleBasedIntegration/Rubi/blob/master/Rubi/IntegrationUtilityFunctions.m)

Obviosuly one would need a way to translate the majority of this automatically to Coq, so it would help if one could translate it to something which is structurally similar.

One thing that is unclear to me is the order in which these rules are applied and how (is outside-in enough?). I admit I can't read mathematica code, so maybe these questions are trivial. It may also help to know how they index the rules. Elpi has decent indexing (https://github.com/LPCIC/elpi/blob/master/ELPI.md#configurable-argument-indexing) for a Prolog engine, but it is not like the index of an automated "rewriter" such as E, Waldmeister or Vampire. It's relatively easy to change, but today it uses just one 64 bit word. Maybe speed is not crucial, I'm just looking at possible issues.

@Enrico Tassi : I must admit I am not a Mathematica expert either, but as far as I know Mathematica will try the rules in the order they are defined until it finds a matching one (in some efficient way I don't know) and yes - outside in - but don't ask me about the backtracking sematics. In general in Mathematica functions can take patterns as arguments and it will pick the first matching function in order of definition. See e.g. (https://reference.wolfram.com/language/tutorial/Patterns.html, especially https://reference.wolfram.com/language/tutorial/Patterns.html#23271). When you call the Integrate function, it will only check if the term has the structure given and then go into the function. The function may then call Integrate recsursively to go deeper into terms. Speed should not be that much of an issue - afaik the rules are written such that each term takes a deterministic or almost deterministic path through them.

Last updated: Feb 06 2023 at 05:03 UTC