Understand how the Coq decision procedure approach works

[ana-pantilie]

No description provided.

[ana-pantilie]

• the technique is called proof by reflection (http://adam.chlipala.net/cpdt/html/Reflection.html, https://softwarefoundations.cis.upenn.edu/vfa-current/Decide.html), which allows one to switch between the Prop and Bool contexts (the "proof" world and the "computational" world) -> this should be very do-able in Agda as well (confirmed by our Agda experts)!
• Coq has tactics which allow the user to write proofs in a "procedural" way, and some tactics run some proof-searching algorithms behind the scenes -> this might become cumbersome in Agda, but we have agreed that we can leverage our vast Agda resources here
• a "proof certificate" for a translation relation can be either the Coq/Agda script which is used to generate the response, or the Coq/Agda type which embeds the equivalence of the two ASTs; this type can then be checked by Coq/Agda; IMO, I'd say we ideally want the latter because this moves the trusted core to just the type-checker