coqhott / coq-forcing Goto Github PK
View Code? Open in Web Editor NEWA plugin for Coq that implements the call-by-name forcing translation
A plugin for Coq that implements the call-by-name forcing translation
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)?
Hi coq-forcing developers,
This plugin is very useful to play with models or with forcing in direct style. Do you have further plans with it? E.g. cubical presheaves?
I have a couple of questions:
Prop
by Prop
and Type(i)
by Type(i)
in case the Hom
are proof-irrelevant). There is also the combination with realisability (e.g. @ppedrot's "pre-prefascist" variant with parametricity). Do you have plans in this direction?Also, I wonder whether you'd be interested in moving the plugin to coq-community. Other limitations I collected include the support for polymorphism (which naively would require mapping universes of the source to universes of the target?) and the support for the new term constructors Int
, Float
, Array
, but that's maybe not a limitation enough to make it more visible.
Hi, I realized that Forcing Translate foo
is not implemented for fix
?
In principle, it should be possible to it by hand using Forcing Definition
but I wonder what would be the difficulties to do it automatically?
For the record, I found an issue with the forcing translation of Prop
s:
From Forcing Require Import Forcing.
Axiom Obj : Type.
Axiom Hom : Obj -> Obj -> Type.
Notation "P ≤ Q" := (forall R, Hom Q R -> Hom P R) (at level 70).
Forcing Translate and using Obj Hom.
Forcing Translate iff using Obj Hom.
(* error: ...
has type
"forall p : Obj,
(forall p0 : Obj, p ≤ p0 -> forall p1 : Obj, p0 ≤ p1 -> Prop) ->
(forall p0 : Obj, p ≤ p0 -> forall p1 : Obj, p0 ≤ p1 -> Prop) ->
forall p0 : Obj, p ≤ p0 -> Type" while it is expected to have type
"forall p : Obj,
(forall p0 : Obj, p ≤ p0 -> forall p1 : Obj, p0 ≤ p1 -> Prop) ->
(forall p0 : Obj, p ≤ p0 -> forall p1 : Obj, p0 ≤ p1 -> Prop) ->
forall p0 : Obj, p ≤ p0 -> Prop".
*)
Apparently due to andᶠ
declared in Type
instead of Prop
.
Hi, when using Forcing Definition
, one sees things like:
forall q, (forall R : Obj, Hom p R -> Hom q R)
Generalizing the example given in the test file, a forcing modality notation could also be obtained:
Notation "p ≤ q" := (forall (R : Obj), Hom p R -> Hom q R) (at level 70).
Definition Hom_force (p:Obj) (P:Obj -> Type) := forall q, q ≤ p -> P q.
Notation "▢_ p P" := (Hom_force p (fun p => P)) (at level 200, p ident, format "▢_ p P").
The drawback is to have to introduce an indirection constant Hom_force
.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.