proposition: Lemma CTXT_HYB_equiv_3: CTXT_HYB_pkg_2 ≈₀ CTXT_HYB_pkg_3.
proof: Proof. apply eq_rel_perf_ind with ( (fun '(h0, h1) => h0 = h1) ⋊ triple_rhs S_loc Tinv_loc Tinv'_loc (fun S Tinv Tinv' => forall c, c \notin domm S -> getm Tinv c = getm Tinv' c) ). 1: { ssprove_invariant=> //. all: by rewrite /CTXT_HYB_locs_2 !fset_cons !in_fsetU !in_fset1 eq_refl !Bool.orb_true_r. } simplify_eq_rel m. all: ssprove_code_simpl. all: ssprove_code_simpl_more. - ssprove_sync=> r. ssprove_sync=> [|T]; first by move=> [? ?] [? ?] ->. ssprove_sync=> c. apply: r_get_vs_get_remember => Tinv. apply: r_get_vs_get_remember => S. ssprove_sync; first by move=> [? ?] [? ?] ->. apply: r_put_vs_put. apply: r_put_vs_put. ssprove_restore_mem; last by apply: r_ret. ssprove_invariant=> s0 s1 [[[[Hinv _] <-] _] <-] c'. specialize (Hinv c'). rewrite get_set_heap_eq domm_set in_fsetU => /norP [H H']. rewrite get_set_heap_neq. 2: by apply /eqP. rewrite get_set_heap_eq !get_set_heap_neq. 2,3: by apply /eqP. rewrite in_fset1 in H. move /negPf in H. by rewrite setmE H Hinv. - apply: r_get_vs_get_remember => S. ssprove_sync=> H1. apply: r_get_vs_get_remember => Tinv. apply: r_get_vs_get_remember => Tinv'. apply: (r_rem_triple_rhs S_loc Tinv_loc Tinv'_loc) => Hinv. rewrite Hinv //. case: (Tinv' m) => [c|]. 1: { ssprove_forget_all. by apply: r_ret. } ssprove_sync=> c. ssprove_sync=> [|T]; first by move=> ? ? ->. ssprove_sync; first by move=> ? ? ->. apply: r_put_vs_put. apply: r_put_vs_put. ssprove_restore_mem; last by apply: r_ret. apply: preserve_update_mem_conj. 1: by ssprove_invariant. move=> s0 s1 [[[[[[/= A B] Heq] C] D] E] F] c'. rewrite 3?get_set_heap_neq. 2-4: by apply /eqP. rewrite !get_set_heap_eq !setmE Heq. case: (c' == m) => //. by apply: Hinv. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Mon(SPropBase) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude) extructures(ord fset fmap) Equations(Equations)