proposition: Theorem if_rule {A1 A2 : ord_choiceType} {S1 S2 : choiceType} (c1 c2 : FrStP S1 A1) (c1' c2' : FrStP S2 A2) {b1 b2 : bool} {pre : S1 * S2 -> Prop} {post : A1 * S1 -> A2 * S2 -> Prop} {pre_b1b2 : forall st, pre st -> b1 = b2} { H1 : ⊨ ⦃ fun st => pre st /\ b1 = true ⦄ c1 ≈ c1' ⦃ post ⦄ } { H2 : ⊨ ⦃ fun st => pre st /\ b1 = false ⦄ c2 ≈ c2' ⦃ post ⦄ } : ⊨ ⦃ pre ⦄ (if b1 then c1 else c2) ≈ (if b2 then c1' else c2') ⦃ post ⦄.
proof: Proof. apply pre_hypothesis_rule. move=> st1 st2 pre_holds. specialize (pre_b1b2 (st1, st2) pre_holds). subst. destruct b2 eqn:Hb. - apply (pre_weaken_rule (fun st => pre st /\ true = true)). assumption. rewrite /= => st1' st2' [Heq1 Heq2]. subst. split; auto. - apply (pre_weaken_rule (fun st => pre st /\ false = false)). assumption. rewrite /= => st1' st2' [Heq1 Heq2]. subst. split; auto. Qed.
imports: Coq(RelationClasses Morphisms Utf8) Mon(SPropMonadicStructures SpecificationMonads MonadExamples SPropBase FiniteProbabilities) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum finmap.set finmap.finmap xfinmap) Crypt(Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg RelativeMonadMorph_prod StateTransformingLaxMorph choice_type)