proposition: Theorem if_rule {A1 A2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2} (c1 c2 : MFreePr (Choice.Pack chA1)) (c1' c2' : MFreePr (Choice.Pack chA2)) {b1 b2 : bool} {pre : Prop} {post : A1 -> A2 -> Prop} {pre_b1b2 : pre -> b1 = b2} { H1 : ⊨ ⦃ pre /\ b1 = true ⦄ c1 ≈ c1' ⦃ post ⦄ } { H2 : ⊨ ⦃ pre /\ 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=> pre_holds. specialize (pre_b1b2 pre_holds). destruct pre_b1b2. destruct b1. apply (pre_weaken_rule (pre /\ true = true) True). - assumption. - intuition. apply (pre_weaken_rule (pre /\ false = false) True). - assumption. - intuition. 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)