proposition: Lemma r_get_remember_lhs : ∀ {A B : choiceType} ℓ r₀ r₁ (pre : precond) (post : postcond A B), (∀ x, ⊢ ⦃ λ '(s₀, s₁), (pre ⋊ rem_lhs ℓ x) (s₀, s₁) ⦄ r₀ x ≈ r₁ ⦃ post ⦄ ) → ⊢ ⦃ λ '(s₀, s₁), pre (s₀, s₁) ⦄ x ← get ℓ ;; r₀ x ≈ r₁ ⦃ post ⦄.
proof: Proof. intros A B ℓ r₀ r₁ pre post h. change ( ⊢ ⦃ λ '(s₀, s₁), pre (s₀, s₁) ⦄ x ← (x ← get ℓ ;; ret x) ;; r₀ x ≈ ret Datatypes.tt ;; r₁ ⦃ post ⦄ ). eapply r_bind with (mid := λ '(b₀, s₀) '(b₁, s₁), b₀ = get_heap s₀ ℓ ∧ pre (s₀, s₁) ). - apply from_sem_jdg. intros [s₀ s₁]. hnf. intro P. hnf. intros [hpre hpost]. simpl. eexists (dunit (_,_)). split. + unfold coupling. split. * unfold lmg, dfst. apply distr_ext. intro. rewrite dlet_unit. reflexivity. * unfold rmg, dsnd. apply distr_ext. intro. rewrite dlet_unit. reflexivity. + intros [] [] e. rewrite dunit1E in e. apply ge0_eq in e. noconf e. eapply hpost. intuition auto. - intros x _. apply rpre_hypothesis_rule. intros s₀ s₁ [? hpre]. subst. eapply rpre_weaken_rule. + eapply h. + simpl. intuition subst. split. 1: auto. simpl. reflexivity. 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)