Merge branch 'main' into itree-ci

ITree/Basic.lean

@@ -0,0 +1,57 @@
+import Qpf
+
+/-!
+# Interaction Trees
+
+We define interaction trees, a coinductive data-structure used for giving
+semantics of side-effecting, possibly non-terminating, programs
+
+[1] https://arxiv.org/abs/1906.00046
+[2] https://github.com/DeepSpec/InteractionTrees
+-/
+
+/-
+## Hacks / Workarounds
+
+We'd like to define interaction trees as follows:
+```
+codata ITree (ε : Type → Type) ρ where
+  | ret (r : ρ)
+  | tau (t : ITree ε ρ)
+  | vis {α : Type} (e : ε α) (k : α → ITree ε ρ)
+```
+Unfortunately, `vis` in that definition is a dependent arrow in disguise,
+and dependent arrows are currently not supported by the framework yet.
+
+What is supported, though, are sigma types, as in the following, equivalent,
+definition
+```
+codata ITree (ε : Type → Type) ρ where
+  | ret (r : ρ)
+  | tau (t : ITree ε ρ)
+  | vis (e : Σ α : Type, ε α × α → ITree ε ρ)
+```
+
+Unfortunately, this, too yields an error, so for now we settle for fixing a
+particular input type `α`, by making `α` a parameter of the type.
+-/
+
+codata ITree α ε ρ where
+  | ret (r : ρ)
+  | tau (t : ITree α ε ρ)
+  | vis : ε → α → ITree α ε ρ → ITree α ε ρ
+
+
+namespace ITree
+
+/-- the corecursion principle on itrees is the low-level way of defining a
+cotree, as being generated by some transition function `f`
+from initial state `b` -/
+def corec {β α ε ρ : Type} (f : β → ITree.Base α ε ρ β) (b : β) : ITree α ε ρ :=
+  MvQPF.Cofix.corec (F := TypeFun.ofCurried ITree.Base) f b
+
+/-- `ITree.spin` is an infinite sequence of tau-nodes. -/
+def spin : ITree α ε ρ :=
+  corec (fun () => .tau ()) ()
+
+end ITree

lakefile.lean

@@ -9,5 +9,7 @@ lean_lib Qpf
 
 lean_lib Test
 
+lean_lib ITree
+
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git"@"v4.12.0"