Interaction Trees Coq Library

The library is organized into several core modules depending on your task:

• ITree.ITree: Contains the primary definitions used to program with interaction trees.
• ITree.ITreeFacts: Contains theorems used for reasoning about interaction trees.
• ITree.Events: Provides standard event types.

Interaction Trees relies on several Coq axioms and external libraries. If you are building proofs that must be axiom-free, be aware of the following:

Required Axioms

• UIP (Uniqueness of Identity Proofs): Used for the inversion lemma eqit_inv_Vis. Note that an axiom-free version eqit_inv_Vis_weak using heterogeneous equality is available if you wish to avoid UIP.
• Functional Extensionality: Assumed in Basics.FunctionFacts.CartesianClosed_Fun for the closed category of functions.
• Excluded Middle and Choice: The itree-extra library (specifically the theory of traces in extra/ITrace/) assumes excluded middle and a type-theoretic axiom of choice (classicT_inhabited) to decide if an itree diverges.

External Dependencies

• coq
• coq-paco
• coq-ext-lib

You can use make as an alternative build system (primarily for legacy reasons or documentation generation). This requires coq-paco and coq-ext-lib, but does not require dune.

Install dependencies:

opam install coq-paco coq-ext-lib

Build targets:

• make all -j: Builds the library, tutorial, and tests using parallel jobs.
• make: Builds only the library.
• make tutorial: Builds the tutorial.
• make tests: Builds the tests (and runs extracted test executables).

The primary build system for Interaction Trees is dune. To build the library, tutorials, and tests, first install the required dependencies via opam:

opam install coq-paco coq-ext-lib dune

Then, run dune build to compile everything. You can also build specific components:

• dune build theories: Build the core theories.
• dune build tutorial: Build the toy compiler tutorial.
• dune build tests: Build the test suite.
• dune build examples: Build the examples.

To run the extracted test examples, use:

dune runtest

Note for Coq users: To enable interactive editing of Coq files, you must copy the _CoqProject.dune file to _CoqProject:

cp _CoqProject.dune _CoqProject

Warning: If you switch between dune and make builds, clean the project to avoid conflicts.

You can install the Interaction Trees library using the OCaml package manager (opam) with the following command:

opam install coq-itree

The library includes a comprehensive case study demonstrating a compiler from a minimal imperative language (Imp) to a control-flow-graph language (Asm). This case study covers language definitions, high-level combinators, compiler implementation, and formal correctness proofs.

(* The case study components include: *)

(* 1. Language Definitions *) 
Require Import tutorial.Imp.      (* The Imp language definition *) 
Require Import tutorial.Asm.      (* The Asm language definition *) 

(* 2. Compiler Implementation *) 
Require Import tutorial.AsmCombinators. (* High-level combinators for Asm *) 
Require Import tutorial.Imp2Asm.        (* The compiler itself *) 

(* 3. Correctness Proof *) 
Require Import tutorial.Imp2AsmCorrectness. (* The correctness theorem: compile_correct *) 

Documentation is generated using coqdoc.

Basic HTML Documentation

Run make html to generate HTML files. The entry point is html/toc.html.

Enhanced Documentation with coqdocjs

To use modern CSS/JS via coqdocjs:

1. Download and unzip coqdocjs-master.zip.
2. Create a symbolic link to the directory in the repository:

   ln -s path/to/coqdocjs-master coqdocjs

3. Run make html.

Updating GitHub Pages

To update the documentation on the gh-pages branch:

1. Clone the branch into a doc directory:

   git clone -b gh-pages git@github.com:DeepSpec/InteractionTrees doc

2. Run the update script:

   cd doc
   sh ./update.sh
   git add -u
   git commit -m "Update"

   This script runs make html in the parent directory and moves the output to doc/docs/master (or doc/docs/$VERSION for past releases).

For a simplified entry point into the library, use the ITree.Simple module. This module provides a streamlined interface designed specifically for learning and quick experimentation with the core concepts of Interaction Trees without the full complexity of the complete library.

(* Access the simplified tutorial interface via: *) 
Require Import ITree.Simple.

Interaction Trees supports equational reasoning using the approximation relation (≈). You can prove that an interpreted program is equivalent to a pure program by using standard Coq tactics and library-specific rewrites such as:

• interp_bind: Distributes interp over a monadic bind.
• interp_trigger: Handles the interaction between interp and trigger.
• bind_ret_l: Simplifies binds involving Ret on the left.
• interp_ret: Simplifies the interpretation of a Ret value.

Theorem echoed_id : forall n, echoed n ≈ Ret n.
Proof.
  intros n.
  unfold echoed, echo.
  rewrite interp_bind.
  rewrite interp_trigger.
  cbn.
  rewrite bind_ret_l.
  rewrite interp_ret.
  reflexivity.
Qed.

To use Interaction Trees, you define your effects using a Variant type and then construct programs using the itree type. Programs use the trigger keyword to request an effect and the Ret constructor to return a pure value.

Example workflow:

1. Define an effect type (e.g., inputE).
2. Define a program (e.g., echo) that uses trigger to interact with that effect.
3. Use itree to wrap the effect type and the return type.

(* Custom effects *)
Variant inputE : Type -> Prop :=
| Input : inputE nat.

(* Effectful programs *)
Definition echo : itree inputE nat
  := x <- trigger Input ;;
     Ret x.