proposition: Lemma eq_up_to_inv_adversary_link : ∀ {L₀ L₁ LA E} (p₀ p₁ : raw_package) (I : precond) {B} (A : raw_code B) `{ValidPackage L₀ Game_import E p₀} `{ValidPackage L₁ Game_import E p₁} `{@ValidCode LA E B A}, INV LA I → eq_up_to_inv E I p₀ p₁ → r⊨ ⦃ I ⦄ code_link A p₀ ≈ code_link A p₁ ⦃ λ '(b₀, s₀) '(b₁, s₁), b₀ = b₁ ∧ I (s₀, s₁) ⦄.
proof: Proof. intros L₀ L₁ LA E p₀ p₁ I B A vp₀ vp₁ vA hLA hp. induction A in vA |- *. - cbn - [semantic_judgement]. eapply weaken_rule. 1: apply ret_rule. intros [h₀ h₁] post. cbn. unfold SPropMonadicStructures.SProp_op_order. unfold Basics.flip, SPropMonadicStructures.SProp_order. intros [HI Hp]. apply Hp. intuition auto. - cbn - [semantic_judgement lookup_op]. apply inversion_valid_opr in vA as hA. destruct hA as [hi vk]. destruct o as [id [S T]]. eapply from_valid_package in vp₀. specialize (vp₀ _ hi). simpl in vp₀. destruct vp₀ as [f₀ [e₀ h₀]]. eapply from_valid_package in vp₁. specialize (vp₁ _ hi). simpl in vp₁. destruct vp₁ as [f₁ [e₁ h₁]]. erewrite lookup_op_spec_inv. 2: eauto. erewrite lookup_op_spec_inv. 2: eauto. specialize (hp id S T x hi). erewrite get_op_default_spec in hp. 2: eauto. erewrite get_op_default_spec in hp. 2: eauto. rewrite !repr_bind. eapply bind_rule_pp. 1:{ eapply to_sem_jdg in hp. exact hp. } cbn - [semantic_judgement]. intros a₀ a₁. apply pre_hypothesis_rule. intros s₀ s₁ [? ?]. subst. eapply pre_weaken_rule. 1: eapply H. + eapply vk. + cbn. intros s₀' s₁' [? ?]. subst. auto. - cbn - [semantic_judgement bindrFree]. apply inversion_valid_getr in vA as hA. destruct hA as [hi vk]. match goal with | |- ⊨ ⦃ ?pre_ ⦄ bindrFree ?m_ ?f1_ ≈ bindrFree _ ?f2_ ⦃ ?post_ ⦄ => eapply (bind_rule_pp (f1 := f1_) (f2 := f2_) m_ m_ pre_ _ post_) end. + eapply (get_case LA). all: auto. + intros a₀ a₁. cbn - [semantic_judgement]. eapply pre_hypothesis_rule. intros s₀ s₁ [? ?]. subst a₁. eapply pre_weaken_rule. 1: eapply H. * eapply vk. * cbn. intros s₀' s₁' [? ?]. subst. auto. - cbn - [semantic_judgement bindrFree]. apply inversion_valid_putr in vA as hA. destruct hA as [hi vk]. match goal with | |- ⊨ ⦃ ?pre_ ⦄ bindrFree ?m_ ?f1_ ≈ bindrFree _ ?f2_ ⦃ ?post_ ⦄ => eapply (bind_rule_pp (f1 := f1_) (f2 := f2_) m_ m_ pre_ _ post_) end. + eapply (@put_case LA). all: auto. + intros a₀ a₁. cbn - [semantic_judgement]. eapply pre_hypothesis_rule. intros s₀ s₁ [? ?]. subst a₁. eapply pre_weaken_rule. 1: eapply IHA. * eapply vk. * cbn. intros s₀' s₁' [? ?]. subst. auto. - cbn - [semantic_judgement bindrFree]. eapply bind_rule_pp. + eapply (@sampler_case LA). auto. + intros a₀ a₁. cbn - [semantic_judgement]. eapply pre_hypothesis_rule. intros s₀ s₁ [? ?]. subst a₁. eapply pre_weaken_rule. 1: eapply H. * eapply inversion_valid_sampler. eauto. * cbn. intros s₀' s₁' [? ?]. subst. 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)