proposition: Theorem RndGrpElem_uniform : forall x y, evalDist RndGrpElem x == evalDist RndGrpElem y.
proof: Proof. intuition. unfold RndGrpElem. eapply (evalDist_iso (fun z => (modNat (z + (modNatAddInverse (groupLog g y) order) + (groupLog g x))) order) (fun z => (modNat (z + (groupLog g y) + (modNatAddInverse (groupLog g x) order)) order))); intuition. rewrite <- Nat.add_assoc. rewrite <- modNat_plus. assert ((x0 + groupLog g y + modNatAddInverse (groupLog g x) order + (modNatAddInverse (groupLog g y) order + groupLog g x)) = ((groupLog g y + modNatAddInverse (groupLog g y) order) + (groupLog g x + modNatAddInverse (groupLog g x) order + x0)))%nat. lia. rewrite H0. rewrite modNat_plus. rewrite modNatAddInverse_correct. rewrite Nat.add_0_l. rewrite modNat_plus. rewrite modNatAddInverse_correct. rewrite Nat.add_0_l. eapply modNat_eq. eapply RndNat_support_lt. trivial. rewrite <- Nat.add_assoc. rewrite <- modNat_plus. assert ((x0 + modNatAddInverse (groupLog g y) order + groupLog g x + (groupLog g y + modNatAddInverse (groupLog g x) order)) = (groupLog g x + modNatAddInverse (groupLog g x) order + (groupLog g y + modNatAddInverse (groupLog g y) order + x0)))%nat. lia. rewrite H0. rewrite modNat_plus. rewrite modNatAddInverse_correct. rewrite Nat.add_0_l. rewrite modNat_plus. rewrite modNatAddInverse_correct. rewrite Nat.add_0_l. eapply modNat_eq. eapply RndNat_support_lt. trivial. eapply in_getSupport_RndNat. eapply modNat_lt. eapply RndNat_uniform. eapply modNat_lt. eapply RndNat_support_lt. trivial. subst. rewrite <- groupExp_mod. simpl. destruct (EqDec_dec GroupElement_EqDec (groupExp g x0) y); subst. rewrite groupExp_mod. rewrite modNat_plus. rewrite modNatAddInverse_correct_gen. rewrite Nat.add_0_l. rewrite <- groupExp_mod. rewrite group_cyclic. destruct (EqDec_dec GroupElement_EqDec x x). intuition. congruence. apply g_generator. apply g_generator. symmetry. eapply groupLog_correct. apply g_generator. apply g_generator. destruct (EqDec_dec GroupElement_EqDec (groupExp g (x0 + modNatAddInverse (groupLog g y) order + groupLog g x)) x); intuition. exfalso. eapply n. rewrite groupExp_plus in e. rewrite group_cyclic in e. eapply ident_l_unique in e. rewrite <- (@groupIdent _ _ _ _ _ _ _ _ FCG g) in e. eapply groupExp_eq in e. rewrite (@modNat_eq order 0) in e. eapply modNatAddInverse_sum_0 in e. rewrite groupExp_mod. rewrite e. rewrite <- groupExp_mod. rewrite group_cyclic. trivial. apply g_generator. apply g_generator. apply g_generator. eapply posnat_pos. apply g_generator. apply g_generator. apply g_generator. apply g_generator. Qed.
imports: FCF.FCF FCF.GroupTheory