search

coq-community / trocq

A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi]
http://coq-community.org/trocq/
GNU Lesser General Public License v3.0
18 stars 3 forks source link

WIP: decorrelates knowing translations from using translations #18

Open CohenCyril opened 9 months ago

CohenCyril commented 9 months ago

Here is a tentative of an interface to add things to trocq, and then use relations as argument to the trocq tactic to trigger some translations rather than others. This works well, but the example of summable shows that it is not always possible to decorrelate relations between themselves, so there is probably a better strategy than this one...

CC @ecranceMERCE @amahboubi

CohenCyril commented 3 months ago

@amahboubi what do you think of this user interface with Trocq?