proposition: Lemma put_case : ∀ {LA} (I : heap_choiceType * heap_choiceType → Prop) l v, INV LA I → l \in LA → r⊨ ⦃ λ '(s0, s3), I (s0, s3) ⦄ putr l v (ret tt) ≈ putr l v (ret tt) ⦃ λ '(b1, s1) '(b2, s2), b1 = b2 ∧ I (s1, s2) ⦄.
proof: Proof. intros LA I l v hinv hin. intros [s1 s2]. simpl. rewrite /SpecificationMonads.MonoCont_bind /=. rewrite /SpecificationMonads.MonoCont_order /SPropMonadicStructures.SProp_op_order /Morphisms.pointwise_relation /Basics.flip /SPropMonadicStructures.SProp_order /=. intuition eauto. eexists (SDistr_unit _ _). split. + apply SDistr_unit_F_choice_prod_coupling. reflexivity. + intros [b1 s3] [b2 s4]. intros Hd. apply H1. unfold SDistr_unit in Hd. rewrite dunit1E in Hd. assert ((tt, set_heap s1 l v, (tt, set_heap s2 l v)) = (b1, s3, (b2, s4))) as Heqs. { destruct ((tt, set_heap s1 l v, (tt, set_heap s2 l v)) == (b1, s3, (b2, s4))) eqn:Heqd. - move: Heqd. move /eqP => Heqd. assumption. - rewrite Heqd in Hd. simpl in Hd. rewrite order.Order.POrderTheory.ltxx in Hd. discriminate. } inversion Heqs. intuition eauto. eapply hinv. all: eauto. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr seq all_algebra fintype realsum) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd SubDistr Couplings RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation pkg_tactics pkg_composition pkg_heap pkg_semantics pkg_lookup pkg_advantage pkg_invariants pkg_distr) Equations.Prop.DepElim Equations(Equations) Crypt(FreeProbProg)