search

CoqHott / coq-forcing

A plugin for Coq that implements the call-by-name forcing translation
12 stars 3 forks source link

Dead link in the README; question on examples of use #2

Open herbelin opened 3 years ago

herbelin commented 3 years ago

Hi, the link https://www.pédrot.fr/articles/draft-forcing.pdf in the readme fails. Should it be e.g. https://www.pédrot.fr/articles/lics2016.pdf ?

Incidentally, do you have a list of examples of proofs done with the plugin. I'm thinking in particular to possible adaptations of standard set-theoretic proofs to type theory (when those proofs are constructive)?

ppedrot commented 3 years ago

Should it be e.g. https://www.pédrot.fr/articles/lics2016.pdf ?

I believe so.

Incidentally, do you have a list of examples of proofs done with the plugin.

Nothing involved, I am afraid. IIRC the most we tried to do were fixpoints with the later modality. What kind of standard proofs were you thinking about?

herbelin commented 3 years ago

Nothing involved, I am afraid. IIRC the most we tried to do were fixpoints with the later modality. What kind of standard proofs were you thinking about?

I had in mind a constructive adaptation of the proof of the negation of the continuum hypothesis to type theory, but also a forcing-based proof of Tarski completeness of my own vintage. As far as I understand, the Forcing Translate command of the plugin would allow to do that relatively easily without having to prove every sublemma in forcing style.