proposition: Lemma compute_key'_equiv (i j : pid) (x : Secret) (zk : choiceTranscript1) (keys : chMap pid (chProd public choiceTranscript1)): (i != j) → compute_key (setm keys j (fto (g ^+ x), zk)) i = compute_key' (remm keys j) i j x.
proof: Proof. intro ij_neq. unfold compute_key, compute_key'. simpl. rewrite <- setm_rem. rewrite domm_set domm_rem. set X := domm _. rewrite !big_fsetU1. 2-3: subst X; apply not_in_domm. rewrite setm_rem. have set_rem_eq : forall P x, \big[finGroup_com_law/1]_(k <- X :\ j | P k) get_value (setm keys j x) k = \prod_(k <- X :\ j | P k) get_value (remm keys j) k. { intros. rewrite big_seq_cond. rewrite [RHS] big_seq_cond. unfold get_value. erewrite eq_bigr. 1: done. intros k. move => /andP [k_in _]. simpl. rewrite setmE remmE. case (k == j) eqn:eq. - move: eq => /eqP eq. rewrite eq in_fsetD1 in k_in. move: k_in => /andP [contra]. rewrite eq_refl in contra. discriminate. - reflexivity. } case (j < i)%ord eqn:e. - rewrite !e. rewrite -2!mulgA. f_equal. 1: unfold get_value ; by rewrite setmE eq_refl otf_fto. f_equal. + apply set_rem_eq. + rewrite Ord.ltNge Ord.leq_eqVlt in e. rewrite negb_or in e. move: e => /andP [_ e]. apply negbTE in e. rewrite e. f_equal. apply set_rem_eq. - rewrite e. rewrite Ord.ltNge in e. apply negbT in e. apply negbNE in e. rewrite Ord.leq_eqVlt in e. move: e => /orP [contra|e]. 1: by rewrite contra in ij_neq. rewrite e !invMg. f_equal. { apply set_rem_eq. } rewrite group_prodC. f_equal. { unfold get_value. by rewrite setmE eq_refl otf_fto. } f_equal. apply set_rem_eq. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum fingroup.fingroup solvable.cyclic prime ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_composition Package Prelude SigmaProtocol Schnorr DDH) Coq(Utf8 Lia) extructures(ord fset fmap) Equations(Equations)