proposition: Lemma r_reflexivity_alt : ∀ {A : choiceType} {L} pre (c : raw_code A), ValidCode L [interface] c → (∀ ℓ, ℓ \in L → get_pre_cond ℓ pre) → (∀ ℓ v, ℓ \in L → put_pre_cond ℓ v pre) → ⊢ ⦃ λ '(s₀, s₁), pre (s₀, s₁) ⦄ c ≈ c ⦃ λ '(b₀, s₀) '(b₁, s₁), b₀ = b₁ ∧ pre (s₀, s₁) ⦄.
proof: Proof. intros A L pre c h hget hput. induction h. - apply r_ret. auto. - eapply fromEmpty. rewrite fset0E. eauto. - eapply (rsame_head_cmd_alt (cmd_get _)). + eapply cmd_get_preserve_pre. apply hget. auto. + eauto. - eapply (@rsame_head_cmd_alt _ _ (λ z, _) (λ z, _) (cmd_put _ _)). + eapply cmd_put_preserve_pre. apply hput. auto. + eauto. - eapply (rsame_head_cmd_alt (cmd_sample _)). + eapply cmd_sample_preserve_pre with (pre := λ '(s₀, s₁), pre (s₀, s₁)). + eauto. 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)