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
17 stars 2 forks source link

Trocq command opening goals #26

Open ecranceMERCE opened 7 months ago

ecranceMERCE commented 7 months ago

In order not to require the user to know how parametricity works, it would be interesting to be able to give both terms t and u one wants to relate, then let Trocq open a goal with the right type expected for the parametricity witness:

Trocq Prove t u.

It looks hard right now, because of a limitation in Coq-Elpi IIUC.

CohenCyril commented 7 months ago

CC @gares