proposition: Lemma compute_key_set_i (i : pid) (v : (chProd public choiceTranscript1)) (m : chMap pid (chProd public choiceTranscript1)): compute_key (setm m i v) i = compute_key m i.
proof: Proof. unfold compute_key. simpl. case (i \in domm m) eqn:i_in. all: simpl in i_in. - have -> : forall v, domm (setm m i v) = domm m. { intros. simpl. rewrite domm_set. rewrite -eq_fset. intro k. rewrite in_fsetU1. case (eq_op) eqn:e. + move: e => /eqP ->. by rewrite i_in. + done. } simpl. f_equal. + apply eq_big. 1: done. intros k k_lt. unfold get_value. rewrite setmE. rewrite Ord.lt_neqAle in k_lt. move: k_lt => /andP [k_lt _]. move: k_lt => /negbTE ->. done. + f_equal. apply eq_big. 1: done. intros k k_lt. unfold get_value. rewrite setmE. rewrite Ord.lt_neqAle in k_lt. move: k_lt => /andP [k_lt _]. rewrite eq_sym. move: k_lt => /negbTE ->. done. - have -> : domm m = domm (remm m i). { simpl. rewrite -eq_fset. intro k. rewrite domm_rem. rewrite in_fsetD1. case (eq_op) eqn:e. + simpl. move: e => /eqP ->. assumption. + done. } simpl. f_equal. + rewrite -setm_rem domm_set domm_rem. rewrite big_fsetU1. all: simpl. 2: by rewrite in_fsetD1 eq_refl. rewrite Ord.ltxx. apply eq_big. 1: done. intros k k_lt. unfold get_value. rewrite setmE remmE. rewrite Ord.lt_neqAle in k_lt. move: k_lt => /andP [k_lt _]. move: k_lt => /negbTE ->. done. + f_equal. rewrite -setm_rem domm_set domm_rem. rewrite big_fsetU1. all: simpl. 2: by rewrite in_fsetD1 eq_refl. rewrite Ord.ltxx. apply eq_big. 1: done. intros k k_lt. unfold get_value. rewrite setmE remmE. rewrite Ord.lt_neqAle in k_lt. move: k_lt => /andP [k_lt _]. rewrite eq_sym. move: k_lt => /negbTE ->. done. 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)