coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Coq code/theory manipulation tool (abstract syntax tree manipulation tool) - heurisitc transformation instead of rigorous rewriting

From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Coq code/theory manipulation tool (abstract syntax tree manipulation tool) - heurisitc transformation instead of rigorous rewriting
Date: Fri, 24 Aug 2018 21:01:48 +0000
Accept-language: en-CA, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM04-CO1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:or3/rxwBmRBq9tDXCy+O+j09IxM/srCxBDY+r6Qd2+keIJqq85mqBkHD//Il1AaPAd2Eraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HRbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHolikJKiI5/m/UhMx+jq1UvB2uqgdlzILIfI2YLuZycr/Dcd4cWGFPXtxRVytEAo6ka4UAFfEBPeFer4LgvlcBrhu+BQ6qBOPg1zRGm3/20rM80+QuCA3NwQ4uH88Tu3nTotX6KacSUOGuzKXW0TnPcu9a1Cz96IjPbhAhpOuDXbN0ccbL1UYvEAbFg0yWpIf4PD2VzvwAvmeH4+Z6Ue+jlXQrpxxtrjS1yMohipHFhowLxV3H6Sl0xYM4KsOkREN4YdOpFYdfui6AOIRoR84vQ39ntSYkxbADu5O2ciYKxZI6zBDFcfOHaZKH4hf7WeaRPzh4gHVldaqniRuu9kas1uLxWtCq3VhTsyZJi97MuWsT2BDJ7ciHV+d98Vym2TaS0QDc9/tIIVgularcN54u3KI/loYSsUTEGC/6gkL2jLKKdkUg/eio7Ofnbq/6qZ+bMo94kgD+MqIwlcyjGek1PRQCU3Kf9OiizrHv4FH1TK9Eg/A2iqXZtYrVJcUfpq63GQ9V1YMj5g6xDzi70NQZnGIHIExZdB6ak4TkIFHOIPfkDfe6mVuskTNry+raMb3mB5XBNmLDn6v5fbZh905czxI+wsxY55JNE70OPPbzWlLqu9HDFR84Mwm0w/79B9ln14MeX3iPAq6DP6/Iv1+I/LFnH+7ZLoQSoXP2L+Uvz//ol34w31EHN+H91pwOLXu8A/5OIkODYHOqjM1XQkkQuQ9rbuXxj1vKFAxTYHC9F5k86zc0TcqGEM+XSIytkqfbhH7jNp1RemVPC1TKGnDtIdbXE8wQYT6fd5cy2gcPUqKsHtd4hEOe8TTiwr8iFdL6vygRtJbtzt9wvraBlRYu8DV1C4KW1GTfFjgozFNNfCc/2eVEmWI40k2KiPMqg/tEENVS47VCVQJobceBndw/MMj7X0f6RvnMSFuiRYn5UxcYa4pthvQpOgN6EdjkiQ3f1S23BbNTj6aMGJE/7qPb2T72Otp5zHHFkqImigt/Tw==

Hi Alex,

Have you looked into Coq's notation system? It allows you to print your AST differently.

Thanks,

Jason Hu

-------- Original message --------

From: Alex Meyer <alex153 AT outlook.lv>

Date: 8/24/18 16:55 (GMT-05:00)

To: coq-club AT inria.fr

Subject: [Coq-Club] Coq code/theory manipulation tool (abstract syntax tree manipulation tool) - heurisitc transformation instead of rigorous rewriting

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

[Coq-Club] Coq code/theory manipulation tool (abstract syntax tree manipulation tool) - heurisitc transformation instead of rigorous rewriting, Alex Meyer, 08/24/2018
- RE: [Coq-Club] Coq code/theory manipulation tool (abstract syntax tree manipulation tool) - heurisitc transformation instead of rigorous rewriting, Jason -Zhong Sheng- Hu, 08/24/2018
  - [Coq-Club] Coq code/theory manipulation tool (abstract syntax tree manipulation tool) - heurisitc transformation instead of rigorous rewriting, Alex Meyer, 08/26/2018