coqhott / coq-forcing Goto Github PK

A plugin for Coq that implements the call-by-name forcing translation

Coq 73.10% Makefile 0.23% OCaml 26.67%

coq-forcing's Introduction

Call-by-name Forcing in Coq

Description

This is a plugin for Coq v8.6 that implements the call-by-name forcing translation. The translation is described in this draft.

Install

You need Coq v8.6 development files. The COQBIN environment variable should be pointing to the Coq binaries folder. Echoing make should be enough then.

Use

The main features added by the plugin are the two following commands.

Forcing Translation

Forcing Translate foo using Obj Hom.

This translates the term foo in the forcing layer described by the Obj and Hom argument. Obj must have type Type and Hom must have type Obj -> Obj -> Type. The translation takes care of the Yoneda embedding so nothing more is expected. The translation currently works for global constants and inductive types.

All constants the term foo depends on must have been translated prior to the invocation of this command, otherwise it will fail.

Forcing Translate foo as id1 ... idn using Obj Hom.

Same as the above but allow to give a name to the translated constants. Without the provided name, the automatically generated constant is named fooᶠ. Note that the translation may generate several new constants, for instance in the inductive cases where in addition to the type, constructors are generated.

Forcing Implementation

Forcing Definition foo : type using Obj Hom.

This command starts the proof mode and let the user provide a term whose type is the forcing translation of type. When the proof is finished, an axiom foo is added to the environment and the term provided by the user is added as the forcing translation of foo.

Forcing Definition foo : type as id using Obj Hom.

Same as above but allows to give a name to the translated constant instead of the automatic fooᶠ.

coq-forcing's People

Contributors

Stargazers

Watchers

Forkers

skyskimmer herbelin bthecat

coq-forcing's Issues

Readability of the Yoneda encoding and of the forcing modality

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.

Forcing translation of propositions

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.

Dead link in the README; question on examples of use

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)?

Support for `Fixpoint` in the translation

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?

Future of the coq-forcing plugin?

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.