Giter Club home page Giter Club logo

coq-forcing's Introduction

Call-by-name Forcing in Coq

Description

This is a plugin for Coq v8.5 that implements the call-by-name forcing translation.

Install

You need Coq v8.5 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

lewer avatar mattam82 avatar ppedrot avatar tabareau avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar

Forkers

tabareau mattam82

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.