From 2ea86fee3f2b301e8e53cfb5194456ae4ba35d75 Mon Sep 17 00:00:00 2001
From: Li-yao Xia <lysxia@gmail.com>
Date: Thu, 3 Oct 2024 00:53:03 +0200
Subject: [PATCH] Fix Dijkstra.StateIOTrace with updated stateT

---
 extra/Dijkstra/StateIOTrace.v | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/extra/Dijkstra/StateIOTrace.v b/extra/Dijkstra/StateIOTrace.v
index 0c21ebd6..13322c46 100644
--- a/extra/Dijkstra/StateIOTrace.v
+++ b/extra/Dijkstra/StateIOTrace.v
@@ -258,7 +258,11 @@ Section PrintMults.
     setoid_rewrite bind_ret_l in H.
     unf_res.
     punfold H. red in H. cbn in *.
-    dependent induction H.
+    match type of H with
+    | ruttF _ _ _ _ _ (VisF _ ?kk) => remember kk as k' eqn:Ek'
+    end.
+    revert Ek'.
+    dependent induction H; intros Ek'.
     2:{ rewrite <- x. constructor; auto. eapply IHruttF; eauto; reflexivity. }
     inversion H; ddestruction; subst; ddestruction; try contradiction.
     subst. specialize (H0 tt tt).
@@ -274,8 +278,6 @@ Section PrintMults.
     eapply CIH with (Maps.add Y (n + m) si); try apply lookup_eq.
     2: { rewrite lookup_neq; subst; auto. }
     rewrite tau_eutt in Hk1.
-    (* TODO: not sure why this is failing *)
-    (*
     setoid_rewrite bind_trigger in Hk1.
     setoid_rewrite interp_state_vis in Hk1. cbn in *.
     rewrite bind_ret_l in Hk1. rewrite tau_eutt in Hk1.
@@ -286,13 +288,11 @@ Section PrintMults.
     rewrite interp_state_ret in Hk1. rewrite bind_ret_l in Hk1.
     cbn in *.
     rewrite tau_eutt in Hk1.
-    unfold Basics.iter, MonadIter_stateT0, Basics.iter, MonadIter_itree.
+    unfold Basics.iter, MonadIter_itree.
     match goal with
       H : _ ⊑ ITree.iter _ (?s1, _) |- _ ⊑ ITree.iter _ (?s2, _) =>
       enough (Hseq : s2 = s1) end; try rewrite Hseq; auto.
     subst. rewrite Nat.add_comm. auto.
-    *)
-    admit.
-  Admitted.
+Qed.
 
 End PrintMults.