proposition: Lemma r_dead_sample : ∀ (A B : choiceType) (op : Op) r₀ r₁ (pre : precond) (post : postcond A B), LosslessOp op → (∀ s₀ s₁, pre (s₀, s₁) → post (r₀, s₀) (r₁, s₁)) → ⊢ ⦃ pre ⦄ _ ← sample op ;; ret r₀ ≈ ret r₁ ⦃ post ⦄.
proof: Proof. intros A B op r₀ r₁ pre post hop hpp. 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. simpl. unfold SDistr_bind, SDistr_unit. rewrite [RHS]dletE. simpl in x. erewrite eq_psum. 2:{ intro. rewrite GRing.mulrC. reflexivity. } rewrite psumZ. 2:{ rewrite dunit1E. apply ler0n. } rewrite hop. rewrite GRing.mulr1. reflexivity. + unfold rmg, dsnd. apply distr_ext. intro. rewrite dlet_unit. simpl. unfold SDistr_bind, SDistr_unit. reflexivity. - intros [] [] e. rewrite dunit1E in e. apply ge0_eq in e. noconf e. apply hpost. apply hpp. auto. 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)