proposition: Theorem assert_rule_right { S1 S2 : choiceType } (b : bool) : ⊨ ⦃ fun (_ : S1 * S2) => b = true ⦄ (retF Datatypes.tt) ≈ (Assert b) ⦃ fun _ _ => b = true ⦄.
proof: Proof. intros [s1 s2]. hnf. intros post. hnf in *. cbv in post. intros H. cbv in H. destruct H as [Hpre K]. simpl. destruct b. all: simpl in *. - exists (SDistr_unit _ ((Datatypes.tt, s1), (Datatypes.tt, s2))). split. + unfold coupling. split. * unfold lmg. apply distr_ext. move => x0. unfold SDistr_unit, dfst. rewrite dlet_unit. reflexivity. * unfold rmg. apply distr_ext. move => x0. unfold SDistr_unit, dsnd. rewrite dlet_unit. reflexivity. + auto. - discriminate. Qed.
imports: Mon(FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum) Crypt(Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg UniformDistrLemmas Prelude choice_type StateTransformingLaxMorph RulesStateProb)