coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] opaque -> transparent : workarounds?

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] opaque -> transparent : workarounds?
Date: Tue, 15 Nov 2016 12:03:37 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f170.google.com
Ironport-phdr: 9a23:cOkXdBwVMCdaXIDXCy+O+j09IxM/srCxBDY+r6Qd2+gQIJqq85mqBkHD//Il1AaPBtSArasewLuP+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZPebgFGiTanfL9+Mhq6oAHMusILnYZsN6E9xwfTrHBVYepW32RoJVySnxb4+Mi9+YNo/jpTtfw86cNOSL32cKskQ7NWCjQmKH0169bwtRbfVwuP52ATXXsQnxFVHgXK9hD6XpP2sivnqupw3TSRMMPqQbwoXzmp8qFmQwLqhigaLT406GHZhMJzgqxGvhyuuwdyzJTIbIyPLvdyYr/RcNEcSGFcXshRTStBAoakYoYTFOUBPedYr5L9p1QQrhu1GBWhBOX1xT9Om3D9wKo33P46HgHG3QwgBNIOv2rXrNnvLqgSV/q6zK/VwjnZbvNW2Cv96IfTfxAupPGDR7Nwcc7LxUYzEAPFi0ydpIr4ND2b0eQNtnKU7+tmVe+3l2EnrBtxoj6xyccojonFnJwaxU3Z9Slhz4Y1JMG4SE5mYdG/CpdfqyaaN45wT8g/QG9ooD43xqMatZO/ZiQHy5QqywTBZ/CZb4SE+A/vWeSNLTp+mXlrYqiwhwyo/kil0uD8Vte70FJNriddl9nDrHEN1xjK5sieSftx4l6t2TiS2w3R9u1IO080la3cK54uxr4/iIAfvljEHi/zgEn2jamWeVs4+uWw9ejrfrHrqoWfOoJ0kA3yLLoiltClDeglMAUCQ3CX+eGm273i+U35Tq9KjvozkqTBqp/VPsQbpq+iAw9VzIkj6AyzAC2g0NsCm3kIMUhJeBOGj4j1NFHDO//4DfKljFStlDdn3ezJPrrkApnVNHjMjK/hfaph605b0Ac80ddf54tNBr4dJPLzR1T+ucfDDh45Ngy02/zoBM981oMYQ2KPA7WWPLncsV+StaoTJLyHY5ZQszLgIbBx7Pn3yHQ9hFU1fK+z3JJRZmruTdp8JEDMSHDsg8wBHGRClww3SuCi3FSIUT9IZ3uxGas67zc3ToOnEYjrSYWkgbjH1yC+SM4FLltaA0yBRC+7P76PXO0BPXqf

My understanding is that once a definition is saved with Qed, there is no way to make it transparent.

Is that true?

If so, has someone written a plugin/tool to take a definition (say of X) with possibly opaque parts and recursively transparently duplicate those parts to create a new totally transparent definition (say X_t)?

Perhaps no new Coq plugin is needed -- template-coq's `Quote Recursively` already reifies opaque bodies. Also, it has "Make Definition" to reflect back encodings of definitions. It seems possible to write Ltac/Gallina functions that use template-coq commands to achieve the above-mentioned transparentification. Am I overlooking some difficulty?

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[Coq-Club] opaque -> transparent : workarounds?, Abhishek Anand, 11/15/2016
- Re: [Coq-Club] opaque -> transparent : workarounds?, Maxime Dénès, 11/15/2016
  - Re: [Coq-Club] opaque -> transparent : workarounds?, Abhishek Anand, 11/15/2016
    - Re: [Coq-Club] opaque -> transparent : workarounds?, Jonathan Leivent, 11/15/2016
      - Re: [Coq-Club] opaque -> transparent : workarounds?, Abhishek Anand, 11/15/2016
        
        Re: [Coq-Club] opaque -> transparent : workarounds?, Jonathan Leivent, 11/15/2016