proposition: Lemma Advantage_par : ∀ G₀ G₁ G₁' A L₀ L₁ L₁' E₀ E₁, ValidPackage L₀ Game_import E₀ G₀ → ValidPackage L₁ Game_import E₁ G₁ → ValidPackage L₁' Game_import E₁ G₁' → flat E₁ → trimmed E₀ G₀ → trimmed E₁ G₁ → trimmed E₁ G₁' → AdvantageE (par G₀ G₁) (par G₀ G₁') A = AdvantageE G₁ G₁' (A ∘ par G₀ (ID E₁)).
proof: Proof. intros G₀ G₁ G₁' A L₀ L₁ L₁' E₀ E₁. intros Va0 Va1 Va1' Fe0 Te0 Te1 Te1'. replace (par G₀ G₁) with ((par G₀ (ID E₁)) ∘ (par (ID Game_import) G₁)). 2:{ erewrite <- interchange. all: ssprove_valid. 4:{ ssprove_valid. rewrite domm_ID_fset. rewrite -fset0E. apply fdisjoint0s. } 2:{ unfold Game_import. rewrite -fset0E. discriminate. } 2: apply trimmed_ID. rewrite link_id. 2:{ unfold Game_import. rewrite -fset0E. discriminate. } 2: assumption. rewrite id_link. 2: assumption. reflexivity. } replace (par G₀ G₁') with ((par G₀ (ID E₁)) ∘ (par (ID Game_import) G₁')). 2:{ erewrite <- interchange. all: ssprove_valid. 4:{ ssprove_valid. rewrite domm_ID_fset. rewrite -fset0E. apply fdisjoint0s. } 2:{ unfold Game_import. rewrite -fset0E. discriminate. } 2: apply trimmed_ID. rewrite link_id. 2:{ unfold Game_import. rewrite -fset0E. discriminate. } 2: assumption. rewrite id_link. 2: assumption. reflexivity. } rewrite -Advantage_link. unfold Game_import. rewrite -fset0E. rewrite Advantage_par_empty. reflexivity. Unshelve. all: 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) Equations.Prop.DepElim Equations(Equations) Crypt(FreeProbProg)