Fix Dijkstra.StateIOTrace with updated stateT

Author: Lysxia

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.