Email Gateway (Aug 18 2022 at 09:58): Email Gateway (Aug 18 2022 at 09:58):From: kuecuek@rbg.informatik.tu-darmstadt.de
Hallo everybody
i have some problems with modulo and power :(
i need following prooofs but i couldn't show these.
1) ((a::int) - b) mod p = (a mod p - b mod p) mod p
there is a lemma called zmod_zadd1_eq in IntDiv. i have tried to use this
lemma with the variable "-b" but it doesn't help.
2)"(a::int) mod p = b mod p ==> a ^ k mod p = b ^ k mod p"
by this lemma i have problems too.
could anyone help me?
thanks for your helps
best regards
Email Gateway (Aug 18 2022 at 09:59):From: Amine Chaieb <chaieb@in.tum.de>
Sorry, I forgot to CC.
Cheers,
Amine.
Email Gateway (Aug 18 2022 at 09:59):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
kuecuek@rbg.informatik.tu-darmstadt.de wrote:
Hallo everybody
i have some problems with modulo and power :(
i need following prooofs but i couldn't show these.
1) ((a::int) - b) mod p = (a mod p - b mod p) mod p
there is a lemma called zmod_zadd1_eq in IntDiv. i have tried to use this
lemma with the variable "-b" but it doesn't help.[zmod_zsub_left_eq, zmod_zsub_right_eq] MRS trans RS sym
2)"(a::int) mod p = b mod p ==> a ^ k mod p = b ^ k mod p"
by this lemma i have problems too.This would be proved by induction on k, I think for the induction step
you would use the corresponding theorem for multiplication which would be
[zmod_zmult1_eq, zmod_zmult1_eq_rev] MRS trans RS sym ;
Regards,
Jeremy
could anyone help me?
thanks for your helps
best regards
Email Gateway (Aug 18 2022 at 09:59):From: Brian Huffman <brianh@csee.ogi.edu>
On Tuesday 12 December 2006 03:32, kuecuek@rbg.informatik.tu-darmstadt.de
wrote:
Hallo everybody
i have some problems with modulo and power :(
i need following prooofs but i couldn't show these.
1) ((a::int) - b) mod p = (a mod p - b mod p) mod p
there is a lemma called zmod_zadd1_eq in IntDiv. i have tried to use this
lemma with the variable "-b" but it doesn't help.
For this one you will need a lemma about unary negation:
lemma zminus_zmod: "- ((x::int) mod p) mod p = - x mod p"
by (simp only: zmod_zminus1_eq_if mod_mod_trivial)
Now you can use transitive reasoning with this and other lemmas about mod and
addition to build a proof:
lemma "((a::int) - b) mod p = (a mod p - b mod p) mod p"
proof -
have "(a - b) mod p = (a + - b) mod p" by (simp only: diff_def)
also have "... = (a mod p + - b) mod p" by (rule zmod_zadd_left_eq)
also have "... = (a mod p + - b mod p) mod p" by (rule zmod_zadd_right_eq)
also have "... = (a mod p + - (b mod p) mod p) mod p" by (simp only:
zminus_zmod)
also have "... = (a mod p + - (b mod p)) mod p" by (rule zmod_zadd_right_eq
[symmetric])
also have "... = (a mod p - b mod p) mod p" by (simp only: diff_def)
finally show ?thesis .
qed
2)"(a::int) mod p = b mod p ==> a ^ k mod p = b ^ k mod p"
by this lemma i have problems too.
This one follows easily from lemma zpower_zmod:
lemma "(a::int) mod p = b mod p ==> a ^ k mod p = b ^ k mod p"
proof -
assume "a mod p = b mod p"
hence "(a mod p) ^ k mod p = (b mod p) ^ k mod p" by simp
thus "a ^ k mod p = b ^ k mod p" by (simp only: zpower_zmod)
qed
Email Gateway (Aug 18 2022 at 09:59):From: Brian Huffman <brianh@csee.ogi.edu>
On Tuesday 12 December 2006 03:32, kuecuek@rbg.informatik.tu-darmstadt.de
wrote:
Hallo everybody
i have some problems with modulo and power :(
i need following prooofs but i couldn't show these.
1) ((a::int) - b) mod p = (a mod p - b mod p) mod p
there is a lemma called zmod_zadd1_eq in IntDiv. i have tried to use this
lemma with the variable "-b" but it doesn't help.
For this one you will need a lemma about unary negation:
lemma zminus_zmod: "- ((x::int) mod p) mod p = - x mod p"
by (simp only: zmod_zminus1_eq_if mod_mod_trivial)
Now you can use transitive reasoning with this and other lemmas about mod and
addition to build a proof:
lemma "((a::int) - b) mod p = (a mod p - b mod p) mod p"
proof -
have "(a - b) mod p = (a + - b) mod p" by (simp only: diff_def)
also have "... = (a mod p + - b) mod p" by (rule zmod_zadd_left_eq)
also have "... = (a mod p + - b mod p) mod p" by (rule zmod_zadd_right_eq)
also have "... = (a mod p + - (b mod p) mod p) mod p" by (simp only:
zminus_zmod)
also have "... = (a mod p + - (b mod p)) mod p" by (rule zmod_zadd_right_eq
[symmetric])
also have "... = (a mod p - b mod p) mod p" by (simp only: diff_def)
finally show ?thesis .
qed
2)"(a::int) mod p = b mod p ==> a ^ k mod p = b ^ k mod p"
by this lemma i have problems too.
This one follows easily from lemma zpower_zmod:
lemma "(a::int) mod p = b mod p ==> a ^ k mod p = b ^ k mod p"
proof -
assume "a mod p = b mod p"
hence "(a mod p) ^ k mod p = (b mod p) ^ k mod p" by simp
thus "a ^ k mod p = b ^ k mod p" by (simp only: zpower_zmod)
qed
Last updated: May 03 2024 at 04:19 UTC