Théo Zimmermann (Jun 24 2020 at 11:17): Théo Zimmermann (Jun 24 2020 at 11:17):This is the topic to ask questions on the talk "FPC-Coq: Using ELPI to elaborate external proof evidence into Coq proofs".
Enrico Tassi (Jul 05 2020 at 12:22):Bump
Enrico Tassi (Jul 05 2020 at 12:47):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?
Samuel Gruetter (Jul 05 2020 at 12:47):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)?
Karl Palmskog (Jul 05 2020 at 12:48):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?
Andreas Röhler (Jul 05 2020 at 12:48):Is there a link to underlying logic foundations (intuitionistic vs. classical etc)
Enrico Tassi (Jul 05 2020 at 12:51):Cool!
Michael Soegtrop (Jul 05 2020 at 12:51):Would ELPI be a good framework to write rule based simplifers?
Michael Soegtrop (Jul 05 2020 at 12:52):I mean fine controled term transformations
Michael Soegtrop (Jul 05 2020 at 12:52):Thanks!
Dale Miller (Jul 05 2020 at 13:01):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.
Dale Miller (Jul 05 2020 at 13:04):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.
Roberto Blanco (Jul 05 2020 at 15:32):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.
Roberto Blanco (Jul 05 2020 at 15:35):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.
Roberto Blanco (Jul 05 2020 at 15:39):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.
Roberto Blanco (Jul 05 2020 at 15:41):@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:
Michael Soegtrop (Jul 05 2020 at 16:00):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.
Enrico Tassi (Jul 05 2020 at 18:24):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.
Michael Soegtrop (Jul 05 2020 at 19:16):@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: Jun 01 2023 at 11:01 UTC