proposition: Theorem rswap_rule_ctx : ∀ {A : ord_choiceType} {I pre} {post Q : postcond A A} (l r c₀ c₁ : raw_code A), ⊢ ⦃ pre ⦄ l ≈ l ⦃ λ '(a₀, s₀) '(a₁, s₁), I (s₀, s₁) ⦄ → (∀ a₀ a₁, ⊢ ⦃ λ '(s₁, s₀), Q (a₀,s₀) (a₁,s₁) ⦄ r ≈ r ⦃ post ⦄) → ⊢ ⦃ I ⦄ c₀ ≈ c₁ ⦃ λ '(a₀, s₀) '(a₁, s₁), I (s₀, s₁) ∧ Q (a₀, s₀) (a₁, s₁) ⦄ → ⊢ ⦃ I ⦄ c₁ ≈ c₀ ⦃ λ '(a₁, s₁) '(a₀, s₀), I (s₀, s₁) ∧ Q (a₀, s₀) (a₁, s₁) ⦄ → ⊢ ⦃ pre ⦄ l ;; c₀ ;; c₁ ;; r ≈ l ;; c₁ ;; c₀ ;; r ⦃ post ⦄.
proof: Proof. intros A I pre post Q l r c₀ c₁ hl hr h₀ h₁. eapply from_sem_jdg. rewrite !repr_bind. eapply swap_rule_ctx. 1:{ eapply to_sem_jdg. exact hl. } 2:{ eapply to_sem_jdg. exact h₀. } 2:{ eapply to_sem_jdg. exact h₁. } intros a₀ a₁. eapply to_sem_jdg. eapply hr. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr seq all_algebra fintype realsum) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd SubDistr Couplings RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation pkg_tactics pkg_composition pkg_heap pkg_semantics pkg_lookup pkg_advantage pkg_invariants pkg_distr) Equations.Prop.DepElim Equations(Equations) Crypt(FreeProbProg)