A Library for Representing Recursive and Impure Programs in Coq
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.
ITree.ITree: Definitions to program with interaction trees.ITree.ITreeFacts: Theorems to reason about interaction trees.ITree.Events: Some standard event types.
opam install coq-itree
See coq-itree.opam for version details.
This library currently depends on UIP, functional extensionality, excluded middle,
and choice; see also theories/Axioms.v.
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.
The closed category of functions assumes functional_extensionality,
in Basics.FunctionFacts.CartesianClosed_Fun.
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.
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.Feel free to open an issue or a pull request!
See also DEV.md for working on this library.