Patrick Nicodemus (Nov 29 2021 at 21:23): Patrick Nicodemus (Nov 29 2021 at 21:23):I have heard that one of the tradeoffs between different proof systems is that something like Isabelle/HOL has a slightly less expressive logic compared to dependent type theory, but proof search is better understood for HOL, which makes automated theorem proving easier. I am wondering whether there is some way for me to isolate different parts of my Coq code depending on how sophisticated the necessary logic is to formalize it. Let us say for example that I want to build up a basic library of facts about natural number arithmetic for use in proofs, none of these facts rely on sophisticated concepts of dependent type theory. I am wondering if there is a way to tell Coq, or tell a piece of proof search software, that the logic being used is of a certain simple form. Or if there is a way to tell Coq to weaken the base logic, so that it doesn't accept a proposition as being well-defined unless it is expressed in some subset of the logic.
Karl Palmskog (Nov 29 2021 at 22:01):Most people handle this (the problem of getting better automation) either using shallow or deep embeddings of some restricted logic in Coq. Then you write specialized tactics, plugins, etc., for your restricted logic, maybe develop some metatheory of your logic and lift the results back into regular Coq. See for example: https://arxiv.org/pdf/2003.06458.pdf#page=80
Karl Palmskog (Nov 29 2021 at 22:05):the attractiveness of using HOL directly is that people have already spent 30+ years writing good general automation for it, so less effort needed in coming up with embeddings. Only recently has there been convincing general automation for Coq, e.g., https://coqhammer.github.io/#sauto
Patrick Nicodemus (Nov 29 2021 at 22:39):Thanks for the papers.
Last updated: Oct 04 2023 at 23:01 UTC