proposition: Theorem bounded_do_while_rule {A1 A2 : ord_choiceType} {S1 S2 : choiceType} {n : nat} (c1 : FrStP S1 bool_choiceType) (c2 : FrStP S2 bool_choiceType) {inv : bool -> bool -> (S1 * S2) -> Prop} {H : ⊨ ⦃ inv true true ⦄ c1 ≈ c2 ⦃ fun bs1 bs2 => (inv bs1.1 bs2.1) (bs1.2, bs2.2) /\ bs1.1 = bs2.1 ⦄ } : ⊨ ⦃ inv true true ⦄ bounded_do_while n c1 ≈ bounded_do_while n c2 ⦃ fun ls rs => (ls.1 = false /\ rs.1 = false) \/ (inv false false) (ls.2, rs.2) ⦄.
proof: Proof. induction n. - simpl. eapply weaken_rule. apply ret_rule. simpl. intros [? ?] ?. simpl. cbv. intuition eauto. - simpl. eapply weaken_rule. apply bind_rule. apply H. move => b1 b2. eapply weaken_rule. apply if_rule. move => st. instantiate (1 := fun s => inv b1 b2 s /\ b1 = b2). rewrite /=. move => [hfoo heq]. assumption. instantiate (1 := fun ls rs => ls.1 = false /\ rs.1 = false \/ (inv false false) (ls.2, rs.2)). eapply weaken_rule. apply IHn. simpl. intros [? ?] ?. cbv. intuition eauto. rewrite -H3. rewrite {2}H4. assumption. eapply weaken_rule. apply ret_rule. simpl. intros [? ?] ?. cbv. intuition eauto. apply H2. right. rewrite -H3. rewrite {2}H4. assumption. instantiate (1 := fun '(b1, b2) => fromPrePost (fun st => (inv b1 b2 st) /\ b1 = b2) (fun ls rs => ls.1 = false /\ rs.1 = false \/ (inv false false (ls.2, rs.2)))). move => [st1 st2] /=. cbv; intuition. move => [st1 st2] /=. move => β /=. move => [h1 h2]. split; auto. move => [b1 s1] [b2 s2] /= [hh1 hh2]. 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)