proposition: Lemma TAG_EVAL_equiv_false: TAG_GUESS_pkg ∘ GUESS false ≈₀ TAG_EVAL_pkg_ff ∘ EVAL false.
proof: Proof. apply eq_rel_perf_ind with ( (fun '(h0, h1) => h0 = h1) ⋊ couple_rhs T_loc S_loc (fun T S => forall m t, ((m, t) \in domm S) = (Some t == getm T m)) ). 1: { ssprove_invariant=> /=. 1,2: by rewrite /GUESS_locs /TAG_GUESS_locs !fset_cons !in_fsetU !in_fset1 eq_refl ?Bool.orb_true_r. move=> m t. by rewrite domm0 in_fset0 get_empty_heap emptymE. } simplify_eq_rel m. 2: case: m => [m t]. all: simplify_linking. all: simplify_linking. - apply: r_get_vs_get_remember => S. apply: r_get_vs_get_remember => T. destruct (getm T m) as [t|] eqn:Heqt. all: rewrite Heqt /=. + apply: r_put_vs_put. ssprove_restore_mem; last by apply: r_ret. ssprove_invariant=> s0 s1 [[[[Hinv _] H1] _] H2] m' t'. rewrite get_set_heap_eq get_set_heap_neq // domm_set in_fsetU in_fset1. case: (eq_dec (m', t') (m, t)) => Heq. * case: Heq => [-> ->]. by rewrite H2 Heqt /= !eq_refl. * move /eqP /negPf in Heq. by rewrite Heq -H1 Hinv. + ssprove_sync=> k. apply: (r_rem_couple_rhs T_loc S_loc) => Hinv. apply: r_put_vs_put. apply: r_put_vs_put. ssprove_restore_mem; last by apply: r_ret. ssprove_invariant=> m' k'. rewrite domm_set in_fsetU in_fset1 setmE. case: (eq_dec (m', k') (m, k)) => Heq. 1: { case: Heq => [-> ->]. by rewrite !eq_refl /= eq_refl. } move /eqP /negPf in Heq. rewrite Heq /=. rewrite xpair_eqE in Heq. case: (eq_dec m' m) => Heqm. * rewrite Heqm eq_refl /= in Heq*. by rewrite Heq Hinv Heqt. * move /eqP /negPf in Heqm. by rewrite Heqm Hinv. - ssprove_code_simpl. ssprove_code_simpl_more. apply: r_get_remember_lhs => T. apply: r_get_remember_rhs => S. apply: (r_rem_couple_rhs T_loc S_loc) => [|Hinv]. 1: by apply: (Remembers_rhs_from_tracked_lhs _). rewrite Hinv. ssprove_forget_all. by apply: r_ret. 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)