proposition: Theorem async_retL { A B : ord_choiceType } (m : MFreePr A) (f : A -> B ) : ⊨ ⦃ True ⦄ x <- m ;; retF (f x) ≈ m ⦃ fun fx x => fx = (f x) ⦄.
proof: Proof. apply (rewrite_eqDistrR _ (x <- m ;; retF x)). apply (seq_rule_ch _ _ True eq). - by apply: reflexivity_rule. - move => a1 a2. apply: pre_hypothesis_rule_ch => Heq. rewrite -Heq. rewrite /fromPrePost. destruct A as [A chA]. destruct B as [B chB]. apply (weaken_rule (ret (f a1, a1))). -- by apply: ret_rule. -- rewrite /=. move => predBA [H1 H2] /=. apply H2. reflexivity. - by rewrite ord_relmon_law1 /=. Qed.
imports: Coq(RelationClasses Morphisms Utf8) 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 RelativeMonadMorph_prod)