From 6f9d30528866b0b0c8d5e87c31991a1fc0de4cf5 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Tue, 15 Oct 2024 15:25:21 -0500
Subject: [PATCH 1/4] fix: correct the definition of `ITree`

---
 ITree/Basic.lean | 30 +++++++++++++++++++++++++++---
 1 file changed, 27 insertions(+), 3 deletions(-)

diff --git a/ITree/Basic.lean b/ITree/Basic.lean
index 20edf44..932850c 100644
--- a/ITree/Basic.lean
+++ b/ITree/Basic.lean
@@ -36,10 +36,10 @@ 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
+codata ITree (α : Type) ε ρ where
   | ret (r : ρ)
   | tau (t : ITree α ε ρ)
-  | vis : ε → α → ITree α ε ρ → ITree α ε ρ
+  | vis : ε → (α → ITree α ε ρ) → ITree α ε ρ
 
 
 namespace ITree
@@ -48,7 +48,31 @@ namespace ITree
 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
+  MvQPF.Cofix.corec (F := TypeFun.ofCurried (ITree.Base α)) f b
+
+@[cases_eliminator, elab_as_elim]
+def cases {α ε ρ : Type} {motive : ITree α ε ρ → Sort u}
+    (ret : (r : ρ) → motive (.ret r))
+    (tau : (x : ITree α ε ρ) → motive (.tau x))
+    (vis : (e : ε) → (k : α → ITree α ε ρ) → motive (.vis e k)) :
+    ∀ (x : ITree α ε ρ), motive x :=
+  fun x =>
+    match h : MvQPF.Cofix.dest x with
+    | .ret r =>
+      have h : x = ITree.ret r := by
+        apply_fun MvQPF.Cofix.mk at h
+        simpa [MvQPF.Cofix.mk_dest] using h
+      h ▸ ret r
+    | .tau y =>
+      have h : x = ITree.tau y := by
+        apply_fun MvQPF.Cofix.mk at h
+        simpa [MvQPF.Cofix.mk_dest] using h
+      h ▸ tau y
+    | .vis e k =>
+      have h : x = ITree.vis e k := by
+        apply_fun MvQPF.Cofix.mk at h
+        simpa [MvQPF.Cofix.mk_dest] using h
+      h ▸ vis e k
 
 /-- `ITree.spin` is an infinite sequence of tau-nodes. -/
 def spin : ITree α ε ρ :=

From b30bbd4a77093bd7c01bd6093b61c94c9a2e4fb9 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Tue, 15 Oct 2024 15:26:23 -0500
Subject: [PATCH 2/4] feat: define weak bisimulation for ITrees

---
 ITree/Basic.lean | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/ITree/Basic.lean b/ITree/Basic.lean
index 932850c..befaf67 100644
--- a/ITree/Basic.lean
+++ b/ITree/Basic.lean
@@ -78,4 +78,22 @@ def cases {α ε ρ : Type} {motive : ITree α ε ρ → Sort u}
 def spin : ITree α ε ρ :=
   corec (fun () => .tau ()) ()
 
+inductive EquivUTT.F (R : ITree α ε ρ → ITree α ε ρ → Prop) :
+    ITree α ε ρ → ITree α ε ρ → Prop
+  | ret : EquivUTT.F R (.ret r) (.ret r)
+  | vis :
+    (∀ a, R (k₁ a) (k₂ a))
+    → EquivUTT.F R (.vis e k₁) (.vis e k₂)
+  | tau : R x y → EquivUTT.F R (.tau x) (.tau y)
+  | taul : R x y → EquivUTT.F R (.tau x) y
+  | taur : R x y → EquivUTT.F R x (.tau y)
+
+/-- Equivalence-up-to-tau, i.e., weak bisimiulation.
+
+This is called `eutt` in the Coq development -/
+inductive EquivUTT (x y : ITree α ε ρ) : Prop where
+  | intro (R : ITree α ε ρ → ITree α ε ρ → Prop)
+    (h_fixpoint : ∀ a b, R a b → EquivUTT.F R a b)
+    (h_R : R x y)
+
 end ITree

From 90a28c5610b25209ceeed5ecc6f0d77c171c46a6 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Tue, 15 Oct 2024 15:27:00 -0500
Subject: [PATCH 3/4] feat:  prove that `EquivUTT` is reflexive and transitive

---
 ITree/Basic.lean | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/ITree/Basic.lean b/ITree/Basic.lean
index befaf67..4ee5e1c 100644
--- a/ITree/Basic.lean
+++ b/ITree/Basic.lean
@@ -96,4 +96,26 @@ inductive EquivUTT (x y : ITree α ε ρ) : Prop where
     (h_fixpoint : ∀ a b, R a b → EquivUTT.F R a b)
     (h_R : R x y)
 
+namespace EquivUTT
+
+theorem refl (x : ITree α ε ρ) : EquivUTT x x := by
+  apply EquivUTT.intro (R := (· = ·))
+  · rintro a - rfl
+    cases a
+    · constructor
+    · constructor; rfl
+    · constructor; intro; rfl
+  · rfl
+
+theorem symm {x y : ITree α ε ρ} : EquivUTT x y → EquivUTT y x := by
+  rintro ⟨R, isFixpoint, h_R⟩
+  apply EquivUTT.intro (R := flip R)
+  · rintro a b h_fR
+    cases isFixpoint _ _ h_fR
+    <;> constructor
+    <;> assumption
+  · exact h_R
+
+end EquivUTT
+
 end ITree

From 4f96f192e7ff0ba85833cbd776d69ffe7c6e309b Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Tue, 15 Oct 2024 15:27:24 -0500
Subject: [PATCH 4/4] WIP: feat: prove that EquivUTT is transitive

---
 ITree/Basic.lean | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/ITree/Basic.lean b/ITree/Basic.lean
index 4ee5e1c..4d99aea 100644
--- a/ITree/Basic.lean
+++ b/ITree/Basic.lean
@@ -116,6 +116,30 @@ theorem symm {x y : ITree α ε ρ} : EquivUTT x y → EquivUTT y x := by
     <;> assumption
   · exact h_R
 
+theorem trans {x y z : ITree α ε ρ} : EquivUTT x y → EquivUTT y z → EquivUTT x z := by
+  rintro ⟨R₁, isFixpoint₁, h_R₁⟩ ⟨R₂, isFixpoint₂, h_R₂⟩
+  let R' (a c) := ∃ b, R₁ a b ∧ R₂ b c
+  apply EquivUTT.intro (R := R')
+  · rintro a c ⟨b, h_fR₁, h_fR₂⟩
+    specialize isFixpoint₁ _ _ h_fR₁
+    specialize isFixpoint₂ _ _ h_fR₂
+    clear h_fR₁ h_fR₂
+    -- have r'_of_left (a c) : R' a c
+
+    cases isFixpoint₁
+    case ret r =>
+      generalize ret r = retr
+      -- split at isFixpoint₂
+      -- cases isFixpoint₂
+      · sorry
+    · sorry
+    · sorry
+    · sorry
+    · sorry
+  · exact ⟨y, h_R₁, h_R₂⟩
+
+
+
 end EquivUTT
 
 end ITree