### Install coq-itree via opam

Source: https://github.com/deepspec/interactiontrees/blob/master/README.md

This command installs the coq-itree library using the opam package manager. It is a straightforward installation process for users who have opam set up.

```bash
opam install coq-itree
```

--------------------------------

### Manage State Events with ITree

Source: https://context7.com/deepspec/interactiontrees/llms.txt

Demonstrates how to define and run stateful programs using stateE, which provides get and put operations. It includes examples of interpreting state events into the state monad transformer.

```coq
From ITree Require Import ITree Events.State Events.StateFacts.
Import ITreeNotations.
Import Basics.Basics.Monads.

Definition counter_program : itree (stateE nat +' void1) nat :=
  x <- get ;;
  put (x + 1) ;;
  y <- get ;;
  put (y + 1) ;;
  get.

Definition run_counter : nat -> itree void1 (nat * nat) :=
  run_state counter_program.

Record game_state := { score : nat; lives : nat }.

Definition add_score (n : nat) : itree (stateE game_state +' void1) unit :=
  s <- get ;;
  put {| score := s.(score) + n; lives := s.(lives) |}.
```

--------------------------------

### Reason about Equivalence with eutt

Source: https://context7.com/deepspec/interactiontrees/llms.txt

Covers the eutt (Equivalence Up To Taus) relation, which is used to reason about program equivalence by treating Tau steps as invisible. Includes examples of rewriting lemmas and the tau_steps tactic.

```coq
From ITree Require Import ITree ITreeFacts Simple.
Import ITreeNotations.

Example tau_invisible : Tau (Tau (Ret 42)) ≈ Ret 42.
Proof. rewrite tau_eutt. rewrite tau_eutt. reflexivity. Qed.

Example factorial_5 : rec (fun n => match n with
  | 0 => Ret 1
  | S m => y <- call m ;; Ret (n * y)
  end) 5 ≈ Ret 120.
Proof. tau_steps. reflexivity. Qed.
```

--------------------------------

### Sequence Computations with ITree.bind

Source: https://context7.com/deepspec/interactiontrees/llms.txt

Shows how to use ITree.bind to sequence computations, supporting both explicit function application and monadic do-notation. It highlights the fundamental monadic laws that hold for ITrees.

```Coq
From ITree Require Import ITree ITreeFacts.
Import ITreeNotations.

(* Define a simple event type *)
Variant ioE : Type -> Type :=
| Read  : ioE nat
| Write : nat -> ioE unit.

(* Bind with explicit function *)
Definition read_and_double : itree ioE nat :=
  ITree.bind (ITree.trigger Read) (fun x => Ret (x * 2)).

(* Using do-notation style *)
Definition read_write_read : itree ioE nat :=
  x <- ITree.trigger Read ;;
  ITree.trigger (Write x) ;;
  y <- ITree.trigger Read ;;
  Ret (x + y).
```

--------------------------------

### Accumulating Logs with Writer Events

Source: https://context7.com/deepspec/interactiontrees/llms.txt

Illustrates the use of writerE to emit logs during computation. The run_writer_list function collects these logs into a list for inspection.

```Coq
From ITree Require Import ITree Events.Writer.
Import ITreeNotations.

Definition log_steps : itree (writerE string +' void1) nat :=
  tell "Starting computation" ;;
  tell "Step 1 complete" ;;
  tell "Step 2 complete" ;;
  Ret 42.

Definition collected_logs : itree void1 (list string * nat) :=
  run_writer_list log_steps.
```

--------------------------------

### Managing Immutable State with Reader Events

Source: https://context7.com/deepspec/interactiontrees/llms.txt

Shows how to use readerE to access an immutable configuration environment. The run_reader function is used to inject the environment into the computation.

```Coq
From ITree Require Import ITree Events.Reader.
Import ITreeNotations.

Definition Config := { debug : bool; max_size : nat }.

Definition check_debug : itree (readerE Config +' void1) bool :=
  cfg <- ask ;;
  Ret cfg.(debug).

Definition run_with_config : itree void1 bool :=
  run_reader {| debug := true; max_size := 100 |} check_debug.
```

--------------------------------

### Compose Events with Sum Types

Source: https://context7.com/deepspec/interactiontrees/llms.txt

Shows how to combine multiple event types using the sum1 (+' ) operator and how to define handlers to interpret these combined effects.

```coq
From ITree Require Import ITree Indexed.Sum Interp.Handler.
Import ITreeNotations.

Variant logE : Type -> Type := | Log : string -> logE unit.
Variant dbE : Type -> Type := | Query : nat -> dbE string | Store : nat -> string -> dbE unit.

Definition appE := logE +' dbE +' void1.

Definition log_and_query (id : nat) : itree appE string :=
  ITree.trigger (inl1 (Log "Starting query")) ;;
  result <- ITree.trigger (inr1 (inl1 (Query id))) ;;
  ITree.trigger (inl1 (Log "Query complete")) ;;
  Ret result.

Definition app_handler : appE ~> itree void1 :=
  case_ log_handler (case_ db_handler Handler.empty).
```

--------------------------------

### Handling Exceptions with exceptE

Source: https://context7.com/deepspec/interactiontrees/llms.txt

Demonstrates how to use the exceptE event to throw errors and handle them using try_catch. This allows for safe computation termination within the ITree monad.

```Coq
From ITree Require Import ITree Events.Exception.
Import ITreeNotations.

Definition safe_divide (n m : nat) : itree (exceptE string +' void1) nat :=
  match m with
  | 0 => throw "Division by zero"
  | S _ => Ret (n / m)
  end.

Definition compute_with_errors : itree (exceptE string +' void1) nat :=
  x <- safe_divide 10 2 ;;
  y <- safe_divide 20 0 ;;
  Ret (x + y).

Definition handled_compute : itree (exceptE string +' void1) nat :=
  try_catch compute_with_errors (fun _ => Ret 0).
```

--------------------------------

### Define ITree Constructors

Source: https://context7.com/deepspec/interactiontrees/llms.txt

Demonstrates the core ITree constructors: Ret for returning values, Tau for internal steps, and Vis for triggering external events. These form the basis of the coinductive tree structure.

```Coq
From ITree Require Import ITree ITreeFacts.
Import ITreeNotations.

(* The itree type has three constructors via notations *)

(* Ret x: Return a value x *)
Definition return_42 : itree void1 nat := Ret 42.

(* Tau t: Internal computation step, continues with t *)
Definition delayed_ret : itree void1 nat := Tau (Tau (Ret 42)).

(* Vis e k: Trigger event e, continue with k applied to the response *)
(* Custom event type for input *)
Variant inputE : Type -> Type :=
| Input : inputE nat.

Definition read_input : itree inputE nat :=
  Vis Input (fun x => Ret x).
```

--------------------------------

### Transform Events with Morphisms

Source: https://context7.com/deepspec/interactiontrees/llms.txt

Explains how to use the translate function to apply event morphisms, allowing for the transformation of event types while preserving the tree structure and strong bisimulation.

```coq
From ITree Require Import ITree Interp.Interp.
Import ITreeNotations.

Variant simpleE : Type -> Type := | SimpleRead : simpleE nat.
Variant detailedE : Type -> Type := | DetailedRead : string -> detailedE nat.

Definition add_context : simpleE ~> detailedE :=
  fun _ e => match e with | SimpleRead => DetailedRead "default_source" end.

Definition simple_program : itree simpleE nat :=
  x <- ITree.trigger SimpleRead ;;
  y <- ITree.trigger SimpleRead ;;
  Ret (x + y).

Definition detailed_program : itree detailedE nat :=
  translate add_context simple_program.
```

--------------------------------

### UIP Axiom for Inversion Lemma in Coq

Source: https://github.com/deepspec/interactiontrees/blob/master/README.md

This Coq code defines a lemma `eqit_inv_Vis` that depends on the Unique Interval Property (UIP) axiom. It demonstrates how UIP is used for inversion lemmas related to the `Vis` constructor in interaction trees.

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

--------------------------------

### Defining Imp Language Semantics

Source: https://context7.com/deepspec/interactiontrees/llms.txt

Provides a denotational semantics implementation for an imperative language (Imp) using ITrees. It defines state events for variable access and recursion via ITree.iter.

```Coq
From ITree Require Import ITree ITreeFacts Events.MapDefault Events.StateFacts.
Import Monads MonadNotation.

Variant ImpState : Type -> Type :=
| GetVar (x : string) : ImpState nat
| SetVar (x : string) (v : nat) : ImpState unit.

Fixpoint denote_expr {E} `{ImpState -< E} (e : expr) : itree E nat :=
  match e with
  | Var v => trigger (GetVar v)
  | Lit n => ret n
  | Plus a b => l <- denote_expr a ;; r <- denote_expr b ;; ret (l + r)
  end.

Definition while {E} (step : itree E (unit + unit)) : itree E unit :=
  ITree.iter (fun _ => step) tt.
```

--------------------------------

### Emit Events with ITree.trigger

Source: https://context7.com/deepspec/interactiontrees/llms.txt

Illustrates the use of ITree.trigger to lift individual events into the ITree monad. This creates a Vis node that pauses execution to interact with the environment.

```Coq
From ITree Require Import ITree.
Import ITreeNotations.

(* Define events for a key-value store *)
Variant kvE (K V : Type) : Type -> Type :=
| Get : K -> kvE K V V
| Put : K -> V -> kvE K V unit.

(* trigger creates a Vis node that immediately returns the response *)
Definition get_key {K V} (k : K) : itree (kvE K V) V :=
  ITree.trigger (Get k).

Definition put_key {K V} (k : K) (v : V) : itree (kvE K V) unit :=
  ITree.trigger (Put k v).

(* Using trigger in a larger program *)
Definition increment_key {K} (k : K) : itree (kvE K nat) nat :=
  v <- ITree.trigger (Get k) ;;
  ITree.trigger (Put k (v + 1)) ;;
  Ret (v + 1).
```

--------------------------------

### ITree.iter: Tail-Recursive Iteration with ITrees in Coq

Source: https://context7.com/deepspec/interactiontrees/llms.txt

The `ITree.iter` combinator provides a loop construct for tail-recursive iteration. The loop body returns either `inl` to continue the iteration with a new state or `inr` to exit the loop with a final result. This is useful for implementing iterative processes within ITrees.

```coq
From ITree Require Import ITree ITreeFacts.
Import ITreeNotations.

(* iter : (I -> itree E (I + R)) -> I -> itree E R *)

(* Simple countdown loop *)
Definition countdown : nat -> itree void1 unit :=
  ITree.iter (fun n =>
    match n with
    | 0 => Ret (inr tt)         (* Exit loop *)
    | S m => Ret (inl m)        (* Continue with m *)
    end).

(* While loop helper *)
Definition while {E} (step : itree E (unit + unit)) : itree E unit :=
  ITree.iter (fun _ => step) tt.

(* Example: sum from n down to 0 *)
Variant sumE : Type -> Type :=
| GetAcc : sumE nat
| AddAcc : nat -> sumE unit.

Definition sum_to (n : nat) : itree sumE unit :=
  ITree.iter (fun i =>
    match i with
    | 0 => Ret (inr tt)
    | S m =>
      ITree.trigger (AddAcc i) ;;
      Ret (inl m)
    end) n.

(* iter is used internally by interp and rec *)

```

--------------------------------

### Strong Bisimulation as Propositional Equality Axiom in Coq

Source: https://github.com/deepspec/interactiontrees/blob/master/README.md

This Coq code exports an axiom `bisimulation_is_eq` which states that strong bisimulation is equivalent to propositional equality. This axiom is provided for convenience and is not a core dependency for the rest of the library.

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

--------------------------------

### Rec and Call: General Recursion with ITrees in Coq

Source: https://context7.com/deepspec/interactiontrees/llms.txt

The `rec` combinator allows defining recursive functions as ITrees without relying on Coq's strict termination checker. The `call` function is used within the recursive function's body to make the recursive calls. This enables defining functions like factorial and Fibonacci directly as ITrees.

```coq
From ITree Require Import ITree Simple.
Import ITreeNotations.

(* Empty event type for pure computations *)
Definition E := void1.

(* Factorial using rec *)
(* rec : (A -> itree (callE A B +' E) B) -> A -> itree E B *)
Definition factorial (n : nat) : itree E nat :=
  rec (fun x ->
    match x with
    | 0 => Ret 1
    | S m ->
      y <- call m ;;  (* Recursive call *)
      Ret (x * y)
    end) n.

(* Alternative syntax using rec-fix notation *)
Definition factorial' : nat -> itree E nat :=
  rec-fix fact n :=
    match n with
    | 0 => Ret 1
    | S m => y <- fact m ;; Ret (n * y)
    end.

(* Fibonacci using rec (multiple recursive calls) *)
Definition fib : nat -> itree E nat :=
  rec-fix fib_rec n :=
    match n with
    | 0 => Ret 0
    | 1 => Ret 1
    | S (S m as n') =>
      a <- fib_rec m ;;
      b <- fib_rec n' ;;
      Ret (a + b)
    end.

(* Compute with fuel using burn *)
(* burn : nat -> itree E R -> itree E R *)
Compute (burn 100 (factorial 5)).  (* Returns Ret 120 *)

```

--------------------------------

### Excluded Middle and Choice Axiom in Coq

Source: https://github.com/deepspec/interactiontrees/blob/master/README.md

This Coq code defines a theorem `classicT_inhabited` which relies on excluded middle and a type-theoretic axiom of choice. This is used in the `itree-extra` library for reasoning about traces and Dijkstra monads.

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

--------------------------------

### Interp: Event Interpretation with Handlers in Coq

Source: https://context7.com/deepspec/interactiontrees/llms.txt

The `interp` combinator transforms an ITree by replacing events with computations defined by an event handler. This is fundamental for assigning semantics to events. It takes a handler (mapping events to computations) and an ITree, returning a new ITree with events replaced. Key equations show how `interp` distributes over `Ret`, `Tau`, `trigger`, and `bind`.

```coq
From ITree Require Import ITree ITreeFacts.
Import ITreeNotations.

(* Define a simple event type *)
Variant counterE : Type -> Type :=
| Inc : counterE unit
| Get : counterE nat.

(* A handler maps events to computations in a target monad *)
(* Handler type: E ~> itree F  means  forall T, E T -> itree F T *)
Definition counter_handler : counterE ~> itree void1 :=
  fun _ e =>
    match e with
    | Inc => Ret tt      (* In a real handler, this would modify state *)
    | Get => Ret 0       (* Returns a default value *)
    end.

(* interp applies the handler to every event in the tree *)
Definition run_counter (t : itree counterE nat) : itree void1 nat :=
  interp counter_handler t.

(* Key equations for interp (up to ≈):
   interp h (Ret x)       ≈ Ret x
   interp h (Tau t)       ≈ Tau (interp h t)
   interp h (trigger e)   ≈ h _ e
   interp h (bind t k)    ≈ bind (interp h t) (fun x => interp h (k x))
*)
```

--------------------------------

### Functional Extensionality Axiom in Coq

Source: https://github.com/deepspec/interactiontrees/blob/master/README.md

This Coq code snippet indicates the use of the `functional_extensionality` axiom. It is assumed in the context of the closed category of functions, specifically within `Basics.FunctionFacts.CartesianClosed_Fun`.

```coq
functional_extensionality
```

--------------------------------

### Mrec: Mutual Recursion with ITrees in Coq

Source: https://context7.com/deepspec/interactiontrees/llms.txt

The `mrec` combinator facilitates mutually recursive definitions using an indexed event type. It allows defining functions that call each other indirectly. The `mrec-fix` notation provides a more concise syntax for these definitions, similar to `rec-fix`.

```coq
From ITree Require Import ITree ITreeFacts.
From ITree Require Import Interp.Recursion.
Import ITreeNotations.

(* Define signature for mutually recursive even/odd *)
Inductive evenoddE : Type -> Type :=
| IsEven : nat -> evenoddE bool
| IsOdd  : nat -> evenoddE bool.

(* Definition body - uses trigger_inl1 for recursive calls *)
Definition evenodd_body : evenoddE ~> itree (evenoddE +' void1) :=
  fun _ e =>
    match e with
    | IsEven n =>
      match n with
      | 0 => Ret true
      | S m => trigger_inl1 (IsOdd m)  (* Call IsOdd *)
      end
    | IsOdd n =>
      match n with
      | 0 => Ret false
      | S m => trigger_inl1 (IsEven m) (* Call IsEven *)
      end
    end.

(* mrec ties the knot *)
Definition is_even (n : nat) : itree void1 bool :=
  mrec evenodd_body (IsEven n).

Definition is_odd (n : nat) : itree void1 bool :=
  mrec evenodd_body (IsOdd n).

(* Alternative using mrec-fix notation *)
Definition evenodd' : evenoddE ~> itree void1 :=
  mrec-fix rec T (d : evenoddE T) :=
    match d with
    | IsEven n => match n with 0 => Ret true  | S m => rec _ (IsOdd m) end
    | IsOdd n  => match n with 0 => Ret false | S m => rec _ (IsEven m) end
    end.

```

=== COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.