Alex Meyer
2018-08-24 20:53:43 UTC
Hello!
Is there tool for Coq code/theory manipulation. Maybe there is more or less universl third party tool, that takes Coq BNF grammar as input and that generates AST manipulation tool. Or maybe Coq suite itself has such facility, of course, Coq parses code and have some inner representation of the code.
At the first glance one can say that such code transformation is against all the idea of formally proven reasoning. But I am trying to use Coq for natural language semantics and here rigorous reasoning (e.g. logical thinking) mixes with the probabilistic/heurisitic reasoning (e.g. what logical function to use for approximation of the semantics of some word or phrase). So - it is quite rational to do some transformation of Coq code using tools that are not formally verified and that do not give guarantees and then do some logical reasoning using logic that is mechanized in Coq. Striving for the best that can be achieved.
Alex
Is there tool for Coq code/theory manipulation. Maybe there is more or less universl third party tool, that takes Coq BNF grammar as input and that generates AST manipulation tool. Or maybe Coq suite itself has such facility, of course, Coq parses code and have some inner representation of the code.
At the first glance one can say that such code transformation is against all the idea of formally proven reasoning. But I am trying to use Coq for natural language semantics and here rigorous reasoning (e.g. logical thinking) mixes with the probabilistic/heurisitic reasoning (e.g. what logical function to use for approximation of the semantics of some word or phrase). So - it is quite rational to do some transformation of Coq code using tools that are not formally verified and that do not give guarantees and then do some logical reasoning using logic that is mechanized in Coq. Striving for the best that can be achieved.
Alex