proposition: Lemma single_key_b : ∀ LD₀ LK₀ CK₀ CK₁ CD₀ CD₁ EK ED A, let K₀ := (par CK₀ (ID IGET)) ∘ KEY in let K₁ := (par CK₁ (ID IGET)) ∘ KEY in let D₀ := (par (ID IGEN) CD₀) ∘ KEY in let D₁ := (par (ID IGEN) CD₁) ∘ KEY in flat EK → flat ED → Parable CK₀ (ID IGET) → Parable CK₁ (ID IGET) → Parable (ID IGEN) CD₀ → Parable (ID IGEN) CD₁ → ValidPackage LD₀ IGET ED CD₀ → ValidPackage LD₀ IGET ED CD₁ → trimmed ED CD₀ → trimmed ED CD₁ → ValidPackage LK₀ ISET EK CK₀ → ValidPackage LK₀ IGEN EK CK₁ → trimmed EK CK₀ → trimmed EK CK₁ → AdvantageE ((par CK₀ CD₀) ∘ KEY) ((par CK₀ CD₁) ∘ KEY) A <= AdvantageE K₀ K₁ (A ∘ (par (ID EK) CD₀)) + AdvantageE D₀ D₁ (A ∘ (par CK₁ (ID ED))) + AdvantageE K₀ K₁ (A ∘ (par (ID EK) CD₁)).
proof: Proof. intros LD₀ LK₀ CK₀ CK₁ CD₀ CD₁ EK ED A K₀ K₁ D₀ D₁. intros fEK fED pCK₀ pCK₁ pCD₀ pCD₁ hCD₀ hCD₁ tCD₀ tCD₁ hCK₀ hCK₁ tCK₀ tCK₁. ssprove triangle (par CK₀ CD₀ ∘ KEY) [:: par CK₁ CD₁ ∘ KEY ] (par CK₀ CD₁ ∘ KEY) A as ineq. eapply le_trans. 1: exact ineq. clear ineq. eapply ler_add. - eapply single_key_a. all: eauto. - replace (par CK₀ CD₁) with ((par (ID EK) CD₁) ∘ (par CK₀ (ID IGET))). 2:{ erewrite <- interchange. all: eauto. 2-3: ssprove_valid. 2: apply trimmed_ID. erewrite link_id. all: eauto. 2: ssprove_valid. erewrite id_link. all: eauto. } replace (par CK₁ CD₁) with ((par (ID EK) CD₁) ∘ (par CK₁ (ID IGET))). 2:{ erewrite <- interchange. all: eauto. 2-3: ssprove_valid. 2: apply trimmed_ID. erewrite link_id. all: eauto. 2: ssprove_valid. erewrite id_link. all: eauto. } rewrite Advantage_link. unfold K₀, K₁. rewrite !link_assoc. rewrite Advantage_sym. apply lexx. Unshelve. all: exact fset0. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr fingroup.fingroup realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb Package Prelude pkg_composition) Coq(Utf8 Lia) extructures(ord fset fmap) Equations(Equations)