proposition: Theorem bounded_do_while_rule {A1 A2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2} {n : nat} (c1 c2 : MFreePr bool_choiceType) {inv : bool -> bool -> Prop} {H : ⊨ ⦃ inv true true ⦄ c1 ≈ c2 ⦃ fun b1 b2 => inv b1 b2 /\ b1 = b2 ⦄ } : ⊨ ⦃ inv true true ⦄ bounded_do_while n c1 ≈ bounded_do_while n c2 ⦃ fun l r => (l = false /\ r = false) \/ inv false false ⦄.
proof: Proof. induction n. - simpl. eapply weaken_rule. apply ret_rule. cbv; intuition. - simpl. eapply weaken_rule. apply bind_rule. apply H. intros a1 a2. eapply weaken_rule. apply if_rule. instantiate (1 := inv a1 a2 /\ a1 = a2). intuition. instantiate (1 := fun l r : bool => l = false /\ r = false \/ inv false false). eapply weaken_rule. apply IHn. cbv; intuition. rewrite -H3. rewrite {2}H4. assumption. eapply weaken_rule. apply ret_rule. cbv; intuition. apply H2. right. rewrite -H3. rewrite {2}H4. assumption. instantiate (1 := fun '(a1, a2) => fromPrePost (inv a1 a2 /\ a1 = a2) (fun l r : bool => l = false /\ r = false \/ inv false false)). cbv; intuition. cbv; 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)