coqhott / coq-forcing Goto Github PK

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:

• It does not support (co)fixpoints: were there particular difficulties to support them? The guard condition?
• It seems that more possible interpretations of the universes have been investigated nowadays (I'm thinking e.g. to Sattler's construction of universes in presheaves, or also the "optimization" interpreting 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 Props:

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.