coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Intermixing of Nat and Z
- Date: Fri, 18 Dec 2020 13:30:18 +1100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f43.google.com
- Ironport-phdr: 9a23:hzLbgRVh8lmvH5af1dbrz7a/xojV8LGtZVwlr6E/grcLSJyIuqrYbB2Pt8tkgFKBZ4jH8fUM07OQ7/m/HzVRvN3d6zgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrrwjdrNQajI9iJ6o+xRbErGZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhNww4DaboKbOudgcKzBZt4VX3ZNU9xLWiBdHo+xbY0CBPcBM+ZCqIn9okMDrR6jBQmvGuzv0T9IjWLq3a073eUuCxvG3A09FN8JtXTUsdb1O7kJUeC10KnIzDvCYOlM2Tf88oTIcxEhofCQXbJ1asfRxkwvGBnEjlWUs4DqIzSV1uEUvmWd8uFvWv6hhXQ9pAFtvjig2N0sio/Ri44LxF3J9Dt0zZopKdCkTEN1YdCqHpReuSyZKYZ4Qs0vTm9ntSs+yrALpZG2ciYXxJkp2xLSaOGKf5SH7B/hSeucJypzinxieLK6nRmy8E6gx/XyV8m101ZKrzJFncfRuXAMzRPf8M+HSuFy/ku51jaP1hzT6uFZIU8vj6bUN5khwrs2m5EOskrDBjf7lFvqgKKSbEkp+eil5/76brjnp5KQLYB5hw/4P68zgMKwG/44PRILX2WD+eSzyrnj/UrhTbVPlPI2k63ZvInbJcQcu6K1GgFV34kt5hqlADem19MYnXYDLF1bYh6Ik4/pO1TWLPD5C/ewnUisnS91y/zaOrDtGJbAI3jZnLv8fLtw6lRQxQU9wNxH4pJbELABIPb9Wk/rs9zYCwc0Mwmpw+bkFtp9zYMeWX6OAq6XKqzSq16I6vguI+mNZY8VpDP9JuMq5/7rl3A5mFsdcbO10psQbXC0Bu5mLFmBYXrwntcBFn8HsRY5TOzzkVGNTTpTZ2upUK8n/TE6CIemDZ/ZSYy3gbyB2j27HpxMaWxcBFCMCySgS4LRUPAVLSmWP8VJkzoeVLHnRZVy+wupsVr/1rlqNeqc5iwHvIjinIxw+u7ejhEu9CN9FcXb0mCMU2RckWYBRjtw16d69x8ugmyf2LR11qQLXedY4OlEB19jZMzsitdiAtW3YTrvO9KASVKoWNKjWGhjQdc4wttIaEF4SYz70kLzmhGyCrpQrISlQYQu+/uFjXf0Lsd5jX3B0ft51gR0co50LWSjw5VH2U3TCorOyRjLkq+rceEd23eI+jvYi2WJu05cXUh7VqCXBX0=
I am trying to prove that g is a generator of a Schnorr group [1], g^q % p = 1, and for this I need to use Euler_exp_totient [2], but I can not use it because I am using the definition of standard library where prime is of type Z, while in ssreflect its type is Nat.
So my question is how can I move between Nat and Z without much hassle in my proofs, given that I want to use the standard library but also the proof infrastructure of ssreflect (I don't understand ssreflect very well; hence trying to avoid it).
Theorem g_is_generator_of_subgroup_of_order_q : Zpow_mod g q p = 1.
Proof.
rewrite Zpow_mod_correct.
rewrite Zpow_mod_correct in H5.
rewrite H5. rewrite <- Zpower_mod.
rewrite <- Z.pow_mul_r.
assert (Ht : k * q = p - 1) by lia.
rewrite Ht.
From mathcomp Require Import all_ssreflect cyclic.
Check (Z.to_N p). (* rewrite the lemma below
assert (totient p = p - 1).
apply Euler_exp_totient. *)
admit.
lia. lia. lia. lia. lia.
Admitted.
Check (Z.to_N p). (* rewrite the lemma below
assert (totient p = p - 1).
apply Euler_exp_totient. *)
admit.
lia. lia. lia. lia. lia.
Admitted.
Best,
Mukesh
Complete source code:
Require Import Lia Ring Field ZArith Znumtheory Zdiv Zpow_facts.
Open Scope Z_scope.
Section Encryption.
Variables
(p q k g r : Z)
(p_prime : prime p) (q_prime : prime q)
(H1 : 2 <= k) (H2 : p = k * q + 1)
(H3 : 1 < r < p) (H4 : Zpow_mod r k p <> 1)
(H5 : g = Zpow_mod r k p).
Theorem p_pos : 0 < p.
pose (prime_ge_2 _ p_prime); lia.
Qed.
Theorem q_pos : 0 < q.
pose (prime_ge_2 _ p_prime); lia.
Qed.
Theorem g_is_generator_of_subgroup_of_order_q : Zpow_mod g q p = 1.
Proof.
rewrite Zpow_mod_correct.
rewrite Zpow_mod_correct in H5.
rewrite H5. rewrite <- Zpower_mod.
rewrite <- Z.pow_mul_r.
assert (Ht : k * q = p - 1) by lia.
rewrite Ht. From mathcomp Require Import all_ssreflect cyclic.
Check (Z.to_N p). (* rewrite the lemma below
assert (totient p = p - 1).
apply Euler_exp_totient. *)
admit.
lia. lia. lia. lia. lia.
Admitted.
Open Scope Z_scope.
Section Encryption.
Variables
(p q k g r : Z)
(p_prime : prime p) (q_prime : prime q)
(H1 : 2 <= k) (H2 : p = k * q + 1)
(H3 : 1 < r < p) (H4 : Zpow_mod r k p <> 1)
(H5 : g = Zpow_mod r k p).
Theorem p_pos : 0 < p.
pose (prime_ge_2 _ p_prime); lia.
Qed.
Theorem q_pos : 0 < q.
pose (prime_ge_2 _ p_prime); lia.
Qed.
Theorem g_is_generator_of_subgroup_of_order_q : Zpow_mod g q p = 1.
Proof.
rewrite Zpow_mod_correct.
rewrite Zpow_mod_correct in H5.
rewrite H5. rewrite <- Zpower_mod.
rewrite <- Z.pow_mul_r.
assert (Ht : k * q = p - 1) by lia.
rewrite Ht. From mathcomp Require Import all_ssreflect cyclic.
Check (Z.to_N p). (* rewrite the lemma below
assert (totient p = p - 1).
apply Euler_exp_totient. *)
admit.
lia. lia. lia. lia. lia.
Admitted.
- [Coq-Club] Intermixing of Nat and Z, mukesh tiwari, 12/18/2020
- Re: [Coq-Club] Intermixing of Nat and Z, Laurent Thery, 12/18/2020
- Re: [Coq-Club] Intermixing of Nat and Z, mukesh tiwari, 12/29/2020
- Re: [Coq-Club] Intermixing of Nat and Z, Laurent Thery, 12/18/2020
Archive powered by MHonArc 2.6.19+.