itree_iter respects weak bisimilarity

src/coalgebras/itreeTauScript.sml

@@ -932,6 +932,7 @@ Proof
             itree_wbisim_sym]
 QED
 
+(* combinators respect weak bisimilarity *)
 Theorem itree_bind_strip_tau_wbisim:
   !u u' k. strip_tau u u' ==> itree_wbisim (itree_bind u k) (itree_bind u' k)
 Proof
@@ -940,7 +941,6 @@ Proof
   metis_tac[itree_wbisim_refl, itree_wbisim_tau_eq, itree_wbisim_trans]
 QED
 
-(* note a similar theorem does NOT hold for Ret because bind expands to (k x) *)
 Theorem itree_bind_vis_strip_tau:
   !u k k' e. strip_tau u (Vis e k') ==>
              strip_tau (itree_bind u k) (Vis e (λx. itree_bind (k' x) k))
@@ -1021,6 +1021,112 @@ Proof
   metis_tac[itree_bind_resp_t_wbisim, itree_bind_resp_k_wbisim, itree_wbisim_trans]
 QED
 
+Theorem itree_iter_ret_tau_wbisim:
+    itcb1 = (λx. case x of INL a => Tau (itree_iter k1 a) | INR b => Ret b)
+  ⇒ itcb2 = (λx. case x of INL a => Tau (itree_iter k2 a) | INR b => Ret b)
+  ⇒ itree_wbisim (Ret x) (Tau u) ⇒ (∀r. itree_wbisim (k1 r) (k2 r))
+  ⇒ (∃t2 t3.
+      itree_bind (Ret x) itcb1 = Tau t2 ∧ itree_bind (Tau u) itcb2 = Tau t3 ∧
+      ((∃sa sb. itree_wbisim sa sb ∧
+                t2 = itree_bind sa itcb1 ∧ t3 = itree_bind sb itcb2)
+       ∨ itree_wbisim t2 t3)) ∨
+    (∃e k k'.
+      strip_tau (itree_bind (Ret x) itcb1) (Vis e k) ∧
+      strip_tau (itree_bind (Tau u) itcb2) (Vis e k') ∧
+      ∀r. (∃sa sb. itree_wbisim sa sb ∧
+                   k r = itree_bind sa itcb1 ∧ k' r = itree_bind sb itcb2)
+         ∨ itree_wbisim (k r) (k' r)) ∨
+    ∃r. strip_tau (itree_bind (Ret x) itcb1) (Ret r) ∧
+        strip_tau (itree_bind (Tau u) itcb2) (Ret r)
+Proof
+  rpt strip_tac >>
+  rw[itree_bind_thm] >>
+  qabbrev_tac ‘itcb1 = (λx. case x of INL a => Tau (itree_iter k1 a)
+                                   | INR b => Ret b)’ >>
+  qabbrev_tac ‘itcb2 = (λx. case x of INL a => Tau (itree_iter k2 a)
+                                   | INR b => Ret b)’ >>
+  fs[Once itree_wbisim_cases] >> fs[Once $ GSYM itree_wbisim_cases] >>
+  qpat_x_assum ‘strip_tau _ _’ mp_tac >>
+  Induct_on ‘strip_tau’ >>
+  rw[itree_bind_thm] >-
+   (disj1_tac >>
+    metis_tac[itree_bind_thm,
+              itree_wbisim_tau_eq, itree_wbisim_trans, itree_wbisim_sym]) >-
+   (disj1_tac >>
+    metis_tac[itree_wbisim_tau_eq, itree_wbisim_trans, itree_wbisim_sym]) >-
+   (disj2_tac >> disj1_tac >> metis_tac[]) >-
+   (disj2_tac >> disj2_tac >> metis_tac[]) >-
+   (Cases_on ‘v’ >-
+     (qunabbrev_tac ‘itcb1’ >> qunabbrev_tac ‘itcb2’ >>
+      rw[] >>
+      disj1_tac >> disj1_tac >>
+      qexistsl_tac [‘k1 x’, ‘Tau (k2 x)’] >>
+      simp[Once itree_iter_thm] >>
+      simp[Once itree_iter_thm, itree_bind_thm] >>
+      metis_tac[itree_wbisim_tau_eq, itree_wbisim_sym, itree_wbisim_trans]) >-
+     (qunabbrev_tac ‘itcb1’ >> qunabbrev_tac ‘itcb2’ >>
+      rw[]))
+QED
+
+Theorem itree_iter_resp_wbisim:
+  ∀t k1 k2. (∀r. itree_wbisim (k1 r) (k2 r)) ⇒
+            itree_wbisim (itree_iter k1 t) (itree_iter k2 t)
+Proof
+  rpt strip_tac >>
+  qabbrev_tac ‘itcb1 = (λx. case x of INL a => Tau (itree_iter k1 a)
+                                   | INR b => Ret b)’ >>
+  qabbrev_tac ‘itcb2 = (λx. case x of INL a => Tau (itree_iter k2 a)
+                                   | INR b => Ret b)’ >>
+  qspecl_then [‘λia ib.∃sa sb x. itree_wbisim sa sb ∧
+                                 ia = itree_bind sa itcb1 ∧
+                                 ib = itree_bind sb itcb2’]
+              strip_assume_tac itree_wbisim_strong_coind >>
+  pop_assum irule >>
+  rw[] >-
+   (Cases_on ‘sa’ >>
+    Cases_on ‘sb’ >-
+     (‘x' = x’ by fs[Once itree_wbisim_cases] >>
+      gvs[] >>
+      Cases_on ‘x’ >-
+       (disj1_tac >> (* Ret INL by wbisim *)
+        qexistsl_tac [‘itree_bind (k1 x') itcb1’, ‘itree_bind (k2 x') itcb2’] >>
+        qunabbrev_tac ‘itcb1’ >> qunabbrev_tac ‘itcb2’ >>
+        simp[Once itree_iter_thm, itree_bind_thm] >>
+        simp[Once itree_iter_thm, itree_bind_thm] >>
+        metis_tac[]) >-
+       (disj2_tac >> disj2_tac >> (* Ret INR by equality *)
+        qunabbrev_tac ‘itcb1’ >> qunabbrev_tac ‘itcb2’ >>
+        rw[Once itree_iter_thm, itree_bind_thm])) >-
+     (irule itree_iter_ret_tau_wbisim >> metis_tac[]) >-
+     (fs[Once itree_wbisim_cases]) >-
+     (‘itree_wbisim (Ret x) (Tau u)’ by fs[itree_wbisim_sym] >>
+      rpt $ qpat_x_assum ‘Abbrev _’
+          $ assume_tac o PURE_REWRITE_RULE[markerTheory.Abbrev_def] >>
+      pop_assum mp_tac >>
+      drule itree_iter_ret_tau_wbisim >>
+      rpt strip_tac >>
+      first_x_assum drule >>
+      disch_then drule >>
+      impl_tac >> metis_tac[itree_wbisim_sym]) >-
+     (disj1_tac >>
+      rw[itree_bind_thm] >>
+      metis_tac[itree_wbisim_tau_eq, itree_wbisim_sym, itree_wbisim_trans]) >-
+     (rw[itree_bind_thm] >>
+      fs[Once itree_wbisim_cases] >> fs[Once $ GSYM itree_wbisim_cases] >>
+      qexists_tac ‘(λx. itree_bind (k x) itcb1)’ >>
+      metis_tac[itree_bind_vis_strip_tau]) >-
+     (fs[Once itree_wbisim_cases]) >-
+     (rw[itree_bind_thm] >>
+      fs[Once itree_wbisim_cases] >> fs[Once $ GSYM itree_wbisim_cases] >>
+      qexists_tac ‘(λx. itree_bind (k' x) itcb2)’ >>
+      metis_tac[itree_bind_vis_strip_tau]) >-
+     (disj2_tac >> disj1_tac >>
+      simp[itree_bind_thm] >>
+      fs[Once itree_wbisim_cases] >> fs[GSYM $ Once itree_wbisim_cases] >>
+      metis_tac[]))
+  >- (qexistsl_tac [‘k1 t’, ‘k2 t’] >> rw[itree_iter_thm])
+QED
+
 (* misc *)
 
 Definition spin: