From 4ed6f50761cfec176b27ac9903ff3e80abe0ccd4 Mon Sep 17 00:00:00 2001 From: Plisp Date: Sat, 16 Sep 2023 11:38:33 +1000 Subject: [PATCH 01/10] proof of itree_bind respecting weak bisimulation --- src/coalgebras/itreeTauScript.sml | 139 +++++++++++++++++++++++++++++- 1 file changed, 138 insertions(+), 1 deletion(-) diff --git a/src/coalgebras/itreeTauScript.sml b/src/coalgebras/itreeTauScript.sml index ab5b550984..72b6f0b821 100644 --- a/src/coalgebras/itreeTauScript.sml +++ b/src/coalgebras/itreeTauScript.sml @@ -638,6 +638,12 @@ Proof rw[Once itree_unfold,FUN_EQ_THM] QED +Theorem itree_bind_left_identity: + itree_bind (Ret x) k = k x +Proof + rw[itree_bind_thm] +QED + Theorem itree_bind_right_identity: itree_bind t Ret = t Proof @@ -802,7 +808,7 @@ Theorem itree_wbisim_strong_coind: (?t2 t3. t = Tau t2 /\ t' = Tau t3 /\ (R t2 t3 \/ itree_wbisim t2 t3)) \/ (?e k k'. strip_tau t (Vis e k) /\ strip_tau t' (Vis e k') /\ - !r. R (k r) (k' r) \/ itree_wbisim(k r) (k' r)) \/ + !r. R (k r) (k' r) \/ itree_wbisim (k r) (k' r)) \/ ?r. strip_tau t (Ret r) /\ strip_tau t' (Ret r)) ==> !t t'. R t t' ==> itree_wbisim t t' Proof @@ -818,6 +824,38 @@ Proof metis_tac[] QED +Triviality itree_wbisim_coind_upto_equiv: + !R t t'. + itree_wbisim t t' ==> + (?t2 t3. t = Tau t2 /\ t' = Tau t3 /\ (R t2 t3 \/ itree_wbisim t2 t3)) \/ + (?e k k'. + strip_tau t (Vis e k) /\ strip_tau t' (Vis e k') /\ + !r. R (k r) (k' r) \/ itree_wbisim (k r) (k' r)) \/ + (?r. strip_tau t (Ret r) /\ strip_tau t' (Ret r)) +Proof + metis_tac[itree_wbisim_cases] +QED + +Theorem itree_wbisim_coind_upto: + !R. + (!t t'. + R t t' ==> + (?t2 t3. t = Tau t2 /\ t' = Tau t3 /\ (R t2 t3 \/ itree_wbisim t2 t3)) \/ + (?e k k'. + strip_tau t (Vis e k) /\ strip_tau t' (Vis e k') /\ + !r. R (k r) (k' r) \/ itree_wbisim (k r) (k' r)) \/ + (?r. strip_tau t (Ret r) /\ strip_tau t' (Ret r)) + \/ itree_wbisim t t') + ==> !t t'. R t t' ==> itree_wbisim t t' +Proof + rpt strip_tac >> + irule itree_wbisim_strong_coind >> + qexists_tac ‘R’ >> + fs[] >> + pop_assum kall_tac >> + metis_tac[itree_wbisim_coind_upto_equiv] +QED + Theorem itree_wbisim_tau: !t t'. itree_wbisim (Tau t) t' ==> itree_wbisim t t' Proof @@ -898,6 +936,105 @@ Proof itree_wbisim_sym] QED +Theorem itree_bind_strip_tau_wbisim: + !u u' k. strip_tau u u' ==> itree_wbisim (itree_bind u k) (itree_bind u' k) +Proof + Induct_on ‘strip_tau’ >> + rpt strip_tac >- + (CONV_TAC $ RATOR_CONV $ ONCE_REWRITE_CONV[itree_bind_thm] >> + ‘itree_wbisim (itree_bind u k) (itree_bind u' k)’ + suffices_by metis_tac[itree_wbisim_trans, itree_wbisim_sym, + itree_wbisim_tau_eq] >> + rw[]) >- + rw[itree_wbisim_refl] >> + rw[itree_wbisim_refl] +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)) +Proof + strip_tac >> strip_tac >> strip_tac >> strip_tac >> + Induct_on ‘strip_tau’ >> + rpt strip_tac >> + rw[itree_bind_thm] +QED + +Triviality itree_bind_vis_tau_wbisim: + itree_wbisim (Vis a g) (Tau u) ==> + (?e k' k''. + strip_tau (itree_bind (Vis a g) k) (Vis e k') /\ + strip_tau (itree_bind (Tau u) k) (Vis e k'') /\ + !r. (?t1 t2. itree_wbisim t1 t2 /\ + k' r = itree_bind t1 k /\ k'' r = itree_bind t2 k) \/ + itree_wbisim (k' r) (k'' r)) +Proof + rpt strip_tac >> + fs[Once itree_wbisim_cases, itree_bind_thm] >> + fs[Once $ GSYM itree_wbisim_cases] >> + Cases_on ‘u’ >- + fs[Once strip_tau_cases] >- + (rw[itree_bind_thm] >> + qexists_tac ‘(λx. itree_bind (k' x) k)’ >> + CONJ_TAC >- + (fs[] >> irule itree_bind_vis_strip_tau >> metis_tac[]) >- + metis_tac[]) >- + (fs[itree_bind_thm] >> metis_tac[]) +QED + +Theorem itree_bind_resp_t_wbisim: + !a b k. (itree_wbisim a b) ==> (itree_wbisim (itree_bind a k) (itree_bind b k)) +Proof + rpt strip_tac >> + qspecl_then [‘λa b. ?t1 t2. (itree_wbisim t1 t2) /\ + a = (itree_bind t1 k) /\ b = (itree_bind t2 k)’] + strip_assume_tac itree_wbisim_coind_upto >> + pop_assum irule >> + rw[] >- + (last_x_assum kall_tac >> + Cases_on ‘t1’ >> + Cases_on ‘t2’ >- + (fs[Once itree_wbisim_cases, itree_bind_thm] >> + Cases_on ‘k x’ >> rw[itree_wbisim_refl]) >- + (disj2_tac >> disj2_tac >> disj2_tac >> + irule itree_wbisim_sym >> + irule itree_bind_strip_tau_wbisim >> + fs[Once itree_wbisim_cases]) >- + (fs[Once itree_wbisim_cases]) >- + (disj2_tac >> disj2_tac >> disj2_tac >> + irule itree_bind_strip_tau_wbisim >> + fs[Once itree_wbisim_cases]) >- + (rw[itree_bind_thm] >> + ‘itree_wbisim u u'’ by metis_tac[itree_wbisim_tau, itree_wbisim_sym] >> + metis_tac[]) >- + (metis_tac[itree_wbisim_sym, itree_bind_vis_tau_wbisim]) >- + (fs[Once itree_wbisim_cases]) >- + (metis_tac[itree_wbisim_sym, itree_bind_vis_tau_wbisim]) >- + (fs[itree_bind_thm, Once itree_wbisim_cases] >> metis_tac[])) + >- metis_tac[] +QED + +Theorem itree_bind_resp_k_wbisim: + !t k1 k2. (!r. itree_wbisim (k1 r) (k2 r)) ==> + (itree_wbisim (itree_bind t k1) (itree_bind t k2)) +Proof + rpt strip_tac >> + qspecl_then [‘λa b. ?t. a = (itree_bind t k1) /\ b = (itree_bind t k2)’] + strip_assume_tac itree_wbisim_coind_upto >> + pop_assum irule >> + rw[] >- + (Cases_on ‘t''’ >> rw[itree_bind_thm] >> metis_tac[]) >- + metis_tac[] +QED + +Theorem itree_bind_resp_wbisim: + !a b k1 k2. (itree_wbisim a b) ==> (!r. itree_wbisim (k1 r) (k2 r)) ==> + (itree_wbisim (itree_bind a k1) (itree_bind b k2)) +Proof + metis_tac[itree_bind_resp_t_wbisim, itree_bind_resp_k_wbisim, itree_wbisim_trans] +QED + (* misc *) Definition spin: From 01dce4e5c89e68179d1a91c1c6661e9329c9b04f Mon Sep 17 00:00:00 2001 From: Plisp Date: Sun, 17 Sep 2023 16:19:42 +1000 Subject: [PATCH 02/10] shorten proof of lemma --- src/coalgebras/itreeTauScript.sml | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/src/coalgebras/itreeTauScript.sml b/src/coalgebras/itreeTauScript.sml index 72b6f0b821..4604e2defc 100644 --- a/src/coalgebras/itreeTauScript.sml +++ b/src/coalgebras/itreeTauScript.sml @@ -973,14 +973,9 @@ Proof rpt strip_tac >> fs[Once itree_wbisim_cases, itree_bind_thm] >> fs[Once $ GSYM itree_wbisim_cases] >> - Cases_on ‘u’ >- - fs[Once strip_tau_cases] >- - (rw[itree_bind_thm] >> - qexists_tac ‘(λx. itree_bind (k' x) k)’ >> - CONJ_TAC >- - (fs[] >> irule itree_bind_vis_strip_tau >> metis_tac[]) >- - metis_tac[]) >- - (fs[itree_bind_thm] >> metis_tac[]) + qexists_tac ‘(λx. itree_bind (k' x) k)’ >> + rw[itree_bind_vis_strip_tau] >> + metis_tac[] QED Theorem itree_bind_resp_t_wbisim: From e4a8c8d83f876aef0508ae5706e714681fc59e66 Mon Sep 17 00:00:00 2001 From: Plisp Date: Wed, 20 Sep 2023 22:04:10 +1000 Subject: [PATCH 03/10] remove unused exists var --- src/coalgebras/itreeTauScript.sml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/coalgebras/itreeTauScript.sml b/src/coalgebras/itreeTauScript.sml index 4604e2defc..a349f965f2 100644 --- a/src/coalgebras/itreeTauScript.sml +++ b/src/coalgebras/itreeTauScript.sml @@ -511,7 +511,7 @@ Theorem itree_bisimulation: ?R. R t1 t2 /\ (!x t. R (Ret x) t ==> t = Ret x) /\ (!u t. R (Tau u) t ==> ?v. t = Tau v /\ R u v) /\ - (!a f t. R (Vis a f) t ==> ?b g. t = Vis a g /\ !s. R (f s) (g s)) + (!a f t. R (Vis a f) t ==> ?g. t = Vis a g /\ !s. R (f s) (g s)) Proof rw [] \\ eq_tac \\ rw [] THEN1 (qexists_tac ‘(=)’ \\ fs [itree_11]) @@ -580,7 +580,7 @@ Definition itree_bind_def: Ret s => Ret' s | Tau t => - Tau'(INR t) + Tau' (INR t) | Vis e g => Vis' e (INR o g)) | INL(Vis e g) => Vis' e (INL o g) @@ -1024,7 +1024,7 @@ Proof QED Theorem itree_bind_resp_wbisim: - !a b k1 k2. (itree_wbisim a b) ==> (!r. itree_wbisim (k1 r) (k2 r)) ==> + !a b k1 k2. (itree_wbisim a b) /\ (!r. itree_wbisim (k1 r) (k2 r)) ==> (itree_wbisim (itree_bind a k1) (itree_bind b k2)) Proof metis_tac[itree_bind_resp_t_wbisim, itree_bind_resp_k_wbisim, itree_wbisim_trans] From ef1b6e2144a2930832d1289687cbe2c9b0c8306b Mon Sep 17 00:00:00 2001 From: Plisp Date: Thu, 21 Sep 2023 15:44:24 +1000 Subject: [PATCH 04/10] remove itree_bind_left_id and unnecessary parens --- src/coalgebras/itreeTauScript.sml | 36 +++++++++++++------------------ 1 file changed, 15 insertions(+), 21 deletions(-) diff --git a/src/coalgebras/itreeTauScript.sml b/src/coalgebras/itreeTauScript.sml index a349f965f2..d6b84d415d 100644 --- a/src/coalgebras/itreeTauScript.sml +++ b/src/coalgebras/itreeTauScript.sml @@ -638,12 +638,6 @@ Proof rw[Once itree_unfold,FUN_EQ_THM] QED -Theorem itree_bind_left_identity: - itree_bind (Ret x) k = k x -Proof - rw[itree_bind_thm] -QED - Theorem itree_bind_right_identity: itree_bind t Ret = t Proof @@ -831,7 +825,7 @@ Triviality itree_wbisim_coind_upto_equiv: (?e k k'. strip_tau t (Vis e k) /\ strip_tau t' (Vis e k') /\ !r. R (k r) (k' r) \/ itree_wbisim (k r) (k' r)) \/ - (?r. strip_tau t (Ret r) /\ strip_tau t' (Ret r)) + ?r. strip_tau t (Ret r) /\ strip_tau t' (Ret r) Proof metis_tac[itree_wbisim_cases] QED @@ -963,27 +957,27 @@ QED Triviality itree_bind_vis_tau_wbisim: itree_wbisim (Vis a g) (Tau u) ==> - (?e k' k''. - strip_tau (itree_bind (Vis a g) k) (Vis e k') /\ - strip_tau (itree_bind (Tau u) k) (Vis e k'') /\ - !r. (?t1 t2. itree_wbisim t1 t2 /\ - k' r = itree_bind t1 k /\ k'' r = itree_bind t2 k) \/ - itree_wbisim (k' r) (k'' r)) + ?e k' k''. + strip_tau (itree_bind (Vis a g) k) (Vis e k') /\ + strip_tau (itree_bind (Tau u) k) (Vis e k'') /\ + !r. (?t1 t2. itree_wbisim t1 t2 /\ + k' r = itree_bind t1 k /\ k'' r = itree_bind t2 k) \/ + itree_wbisim (k' r) (k'' r) Proof rpt strip_tac >> fs[Once itree_wbisim_cases, itree_bind_thm] >> fs[Once $ GSYM itree_wbisim_cases] >> - qexists_tac ‘(λx. itree_bind (k' x) k)’ >> + qexists_tac ‘λx. itree_bind (k' x) k’ >> rw[itree_bind_vis_strip_tau] >> metis_tac[] QED Theorem itree_bind_resp_t_wbisim: - !a b k. (itree_wbisim a b) ==> (itree_wbisim (itree_bind a k) (itree_bind b k)) + !a b k. itree_wbisim a b ==> itree_wbisim (itree_bind a k) (itree_bind b k) Proof rpt strip_tac >> - qspecl_then [‘λa b. ?t1 t2. (itree_wbisim t1 t2) /\ - a = (itree_bind t1 k) /\ b = (itree_bind t2 k)’] + qspecl_then [‘λa b. ?t1 t2. itree_wbisim t1 t2 /\ + a = itree_bind t1 k /\ b = itree_bind t2 k’] strip_assume_tac itree_wbisim_coind_upto >> pop_assum irule >> rw[] >- @@ -1012,10 +1006,10 @@ QED Theorem itree_bind_resp_k_wbisim: !t k1 k2. (!r. itree_wbisim (k1 r) (k2 r)) ==> - (itree_wbisim (itree_bind t k1) (itree_bind t k2)) + itree_wbisim (itree_bind t k1) (itree_bind t k2) Proof rpt strip_tac >> - qspecl_then [‘λa b. ?t. a = (itree_bind t k1) /\ b = (itree_bind t k2)’] + qspecl_then [‘λa b. ?t. a = itree_bind t k1 /\ b = itree_bind t k2’] strip_assume_tac itree_wbisim_coind_upto >> pop_assum irule >> rw[] >- @@ -1024,8 +1018,8 @@ Proof QED Theorem itree_bind_resp_wbisim: - !a b k1 k2. (itree_wbisim a b) /\ (!r. itree_wbisim (k1 r) (k2 r)) ==> - (itree_wbisim (itree_bind a k1) (itree_bind b k2)) + !a b k1 k2. itree_wbisim a b /\ (!r. itree_wbisim (k1 r) (k2 r)) ==> + itree_wbisim (itree_bind a k1) (itree_bind b k2) Proof metis_tac[itree_bind_resp_t_wbisim, itree_bind_resp_k_wbisim, itree_wbisim_trans] QED From 13c15fd2edc9cfaed0b2e1e162078b410a609e2d Mon Sep 17 00:00:00 2001 From: Plisp Date: Mon, 25 Sep 2023 22:14:06 +1000 Subject: [PATCH 05/10] added wbisim of bind-tau simp Michael suggested --- src/coalgebras/itreeTauScript.sml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/coalgebras/itreeTauScript.sml b/src/coalgebras/itreeTauScript.sml index d6b84d415d..1c7c3d4a9d 100644 --- a/src/coalgebras/itreeTauScript.sml +++ b/src/coalgebras/itreeTauScript.sml @@ -930,18 +930,18 @@ Proof itree_wbisim_sym] QED +Theorem itree_bind_wbisim_tau_eq[simp]: + !x k y. itree_wbisim (itree_bind (Tau x) k) y <=> itree_wbisim (itree_bind x k) y +Proof + metis_tac[itree_bind_thm, itree_wbisim_tau_eq, + itree_wbisim_sym, itree_wbisim_trans] +QED + Theorem itree_bind_strip_tau_wbisim: !u u' k. strip_tau u u' ==> itree_wbisim (itree_bind u k) (itree_bind u' k) Proof Induct_on ‘strip_tau’ >> - rpt strip_tac >- - (CONV_TAC $ RATOR_CONV $ ONCE_REWRITE_CONV[itree_bind_thm] >> - ‘itree_wbisim (itree_bind u k) (itree_bind u' k)’ - suffices_by metis_tac[itree_wbisim_trans, itree_wbisim_sym, - itree_wbisim_tau_eq] >> - rw[]) >- - rw[itree_wbisim_refl] >> - rw[itree_wbisim_refl] + rpt strip_tac >> rw[itree_wbisim_refl] QED (* note a similar theorem does NOT hold for Ret because bind expands to (k x) *) From 67643ff5a58cfe0349a911a3d2321efca4f35f81 Mon Sep 17 00:00:00 2001 From: Plisp Date: Thu, 5 Oct 2023 00:07:11 +1100 Subject: [PATCH 06/10] added itree simps that should exist --- src/coalgebras/itreeTauScript.sml | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) diff --git a/src/coalgebras/itreeTauScript.sml b/src/coalgebras/itreeTauScript.sml index 054f3326f5..ce9670e94d 100644 --- a/src/coalgebras/itreeTauScript.sml +++ b/src/coalgebras/itreeTauScript.sml @@ -628,7 +628,7 @@ Proof gvs[] QED -Theorem itree_bind_thm: +Theorem itree_bind_thm[simp]: itree_bind (Ret r) k = k r /\ itree_bind (Tau t) k = Tau (itree_bind t k) /\ itree_bind (Vis e k') k = Vis e (λx. itree_bind (k' x) k) @@ -640,7 +640,7 @@ Proof rw[Once itree_unfold,FUN_EQ_THM] QED -Theorem itree_bind_right_identity: +Theorem itree_bind_right_identity[simp]: itree_bind t Ret = t Proof rw[Once itree_bisimulation] >> @@ -932,18 +932,12 @@ Proof itree_wbisim_sym] QED -Theorem itree_bind_wbisim_tau_eq[simp]: - !x k y. itree_wbisim (itree_bind (Tau x) k) y <=> itree_wbisim (itree_bind x k) y -Proof - metis_tac[itree_bind_thm, itree_wbisim_tau_eq, - itree_wbisim_sym, itree_wbisim_trans] -QED - Theorem itree_bind_strip_tau_wbisim: !u u' k. strip_tau u u' ==> itree_wbisim (itree_bind u k) (itree_bind u' k) Proof Induct_on ‘strip_tau’ >> - rpt strip_tac >> rw[itree_wbisim_refl] + rw[] >> + 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) *) @@ -951,7 +945,8 @@ 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)) Proof - strip_tac >> strip_tac >> strip_tac >> strip_tac >> + rpt strip_tac >> + pop_assum mp_tac >> Induct_on ‘strip_tau’ >> rpt strip_tac >> rw[itree_bind_thm] From 99de5ed5edb8e0a8764165b79549842ed1c5b70d Mon Sep 17 00:00:00 2001 From: Plisp Date: Thu, 5 Oct 2023 15:37:54 +1100 Subject: [PATCH 07/10] itree_iter respects weak bisimilarity --- src/coalgebras/itreeTauScript.sml | 108 +++++++++++++++++++++++++++++- 1 file changed, 107 insertions(+), 1 deletion(-) diff --git a/src/coalgebras/itreeTauScript.sml b/src/coalgebras/itreeTauScript.sml index ce9670e94d..e261416919 100644 --- a/src/coalgebras/itreeTauScript.sml +++ b/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: From 8be71406006ca3f18305c45078c18ee40f015493 Mon Sep 17 00:00:00 2001 From: Plisp Date: Fri, 6 Oct 2023 00:00:50 +1100 Subject: [PATCH 08/10] remove unicode --- src/coalgebras/itreeTauScript.sml | 41 ++++++++++++++++--------------- 1 file changed, 21 insertions(+), 20 deletions(-) diff --git a/src/coalgebras/itreeTauScript.sml b/src/coalgebras/itreeTauScript.sml index e261416919..bb0b372f40 100644 --- a/src/coalgebras/itreeTauScript.sml +++ b/src/coalgebras/itreeTauScript.sml @@ -1022,22 +1022,23 @@ Proof 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) + 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] >> @@ -1069,7 +1070,7 @@ Proof QED Theorem itree_iter_resp_wbisim: - ∀t k1 k2. (∀r. itree_wbisim (k1 r) (k2 r)) ⇒ + !t k1 k2. (!r. itree_wbisim (k1 r) (k2 r)) ==> itree_wbisim (itree_iter k1 t) (itree_iter k2 t) Proof rpt strip_tac >> @@ -1077,9 +1078,9 @@ Proof | 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’] + 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[] >- From 9c6512c905467b4cd9158bf6db96572553d1ae09 Mon Sep 17 00:00:00 2001 From: Plisp Date: Sat, 7 Oct 2023 10:57:25 +1100 Subject: [PATCH 09/10] add Johannes' itree strong bisimulation --- src/coalgebras/itreeTauScript.sml | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/coalgebras/itreeTauScript.sml b/src/coalgebras/itreeTauScript.sml index bb0b372f40..978845ceba 100644 --- a/src/coalgebras/itreeTauScript.sml +++ b/src/coalgebras/itreeTauScript.sml @@ -525,6 +525,23 @@ Proof \\ Cases_on ‘h’ \\ fs [] QED +Theorem itree_strong_bisimulation: + !t1 t2. + t1 = t2 <=> + ?R. R t1 t2 /\ + (!x t. R (Ret x) t ==> t = Ret x) /\ + (!u t. R (Tau u) t ==> ?v. t = Tau v /\ (R u v \/ u = v)) /\ + (!a f t. R (Vis a f) t ==> ?g. t = Vis a g /\ + !s. R (f s) (g s) \/ f s = g s) +Proof + rpt strip_tac >> + EQ_TAC + >- (strip_tac >> first_x_assum $ irule_at $ Pos hd >> metis_tac[]) >> + strip_tac >> + ONCE_REWRITE_TAC[itree_bisimulation] >> + qexists_tac ‘\x y. R x y \/ x = y’ >> + metis_tac[] +QED (* register with TypeBase *) From 5923911d6adae6b1b931a319f988c8626c278a54 Mon Sep 17 00:00:00 2001 From: Plisp Date: Mon, 9 Oct 2023 15:23:52 +1100 Subject: [PATCH 10/10] added local annotation to iter_resp_wbisim ret tau case --- src/coalgebras/itreeTauScript.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coalgebras/itreeTauScript.sml b/src/coalgebras/itreeTauScript.sml index 978845ceba..3f9bd8e7c5 100644 --- a/src/coalgebras/itreeTauScript.sml +++ b/src/coalgebras/itreeTauScript.sml @@ -1038,7 +1038,7 @@ Proof metis_tac[itree_bind_resp_t_wbisim, itree_bind_resp_k_wbisim, itree_wbisim_trans] QED -Theorem itree_iter_ret_tau_wbisim: +Theorem itree_iter_ret_tau_wbisim[local]: 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))