Skip to content

DeepSpec/InteractionTrees

master
Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Interaction Trees Build Status

A Library for Representing Recursive and Impure Programs in Coq

Introduction

For a quick overview of the core features of the library, see examples/ReadmeExample.v.

See also the tutorial.

The coqdoc documentation for this library is available here.

Top-level modules

  • ITree.ITree: Definitions to program with interaction trees.
  • ITree.ITreeFacts: Theorems to reason about interaction trees.
  • ITree.Events: Some standard event types.

Installation

Via opam

opam install coq-itree

Dependencies

See coq-itree.opam for version details.

Axioms

This library currently depends on UIP, functional extensionality, excluded middle, and choice; see also theories/Axioms.v.

UIP

This library depends on UIP for the inversion lemma:

Lemma eqit_inv_Vis
  : eutt eq (Vis e k1) (Vis e k2) ->
    forall x, eutt eq (k1 x) (k2 x).

There are a few more lemmas that depend on it, but you might not actually need it. For example, the compiler proof in tutorial doesn't need it and is axiom-free.

That lemma also has a weaker, but axiom-free version using heterogeneous equality: eqit_inv_Vis_weak.

The axiom that's technically used here is eq_rect_eq (and also JMeq_eq in old versions of Coq), which is equivalent to UIP.

Functional extensionality

The closed category of functions assumes functional_extensionality, in Basics.FunctionFacts.CartesianClosed_Fun.

Excluded middle and choice

The theory of traces (theories/ITrace/)—which Dijkstra monads for ITree depend on (theories/Dijkstra)—assumes excluded middle, to decide whether an itree diverges, and a type-theoretic axiom of choice, which provides a strong excluded middle in propositional contexts:

Theorem classicT_inhabited : inhabited (forall T : Type, T + (T -> False)).

Remark: excluded middle implies UIP, but we still consider UIP as a separate dependency because it's used in a more central part of the library.

Exported: strong bisimulation is propositional equality

The library exports the following axiom for convenience, though it's unlikely you'll need it, and the rest of the library does not depend on it:

Axiom bisimulation_is_eq : t1 ≅ t2 -> t1 = t2.

Contributions welcome

Feel free to open an issue or a pull request!

See also DEV.md for working on this library.

About

A Library for Representing Recursive and Impure Programs in Coq

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages