Stream: Coq users

Topic: Discharging power mod proof

Mukesh Tiwari (Jul 16 2022 at 21:21):

Hi Everyone, is there an easy way to discharge this proof? (One idea that I am thinking is generalising the lemma and replacing pt - 2 by n and induction on n but I haven't tried it).

Lemma power_mod :
      forall (pt : Z),
      prime pt ->
      forall au,
      0 < au < pt ->
      0 < au ^ (pt - 2) mod pt.
    Proof.
      intros * Hw ? [Ha Hb].
      assert (Ht : 0 <= pt - 2).
      nia.
      pose proof Z.pow_pos_nonneg au (pt - 2) Ha Ht as Hpp.

p: Z
Hp: prime p
pt: Z
Hw: prime pt
au: Z
Ha: 0 < au
Hb: au < pt
Ht: 0 <= pt - 2
Hpp: 0 < au ^ (pt - 2)
1/1
0 < au ^ (pt - 2) mod pt

Paolo Giarrusso (Jul 16 2022 at 22:10):

do you have Fermat's little theorem available? https://en.wikipedia.org/wiki/Fermat%27s_little_theorem. From that and the properties of modular arithmetic, it follows (informally) that au ^ (pt - 2) = au^-1 mod pt, and since pt is prime and does not divide au, au^-1 can't be 0.

Paolo Giarrusso (Jul 16 2022 at 22:11):

so I guess I'm assuming that theorem _and_ the surrounding theory

Paolo Giarrusso (Jul 16 2022 at 22:20):

One idea that I am thinking is generalising the lemma and replacing pt - 2 by n and induction on n but I haven't tried it

That might be a simpler idea, once you import a proof of unicity of prime decompositions — but once again I'll stick to an informal sketch. As a corollary of unique prime decomposition, you have that if a prime pt doesn't divide au, pt cannot divideau^n, so au^n mod pt > 0.

Paolo Giarrusso (Jul 16 2022 at 22:22):

And some fancy arith is necessary, because the theorem is false without the prime pt assumption: setting au = 2, pt = 4 gives au ^ (pt - 2) mod pt = 2 ^ (4 - 2) mod 4 = 0.

Paolo Giarrusso (Jul 16 2022 at 22:22):

"fancy arith" = relying on the theory of primality.

Paolo Giarrusso (Jul 16 2022 at 22:24):

Recent threads on unicity of prime decomposition:
https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/.E2.9C.94.20Unicity.20of.20prime.20decomposition
https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/More.20like.20a.20math.20question.2C.20but.20still

Paolo Giarrusso (Jul 16 2022 at 22:31):

As a corollary of unique prime decomposition, you have that if a prime pt doesn't divide au, pt cannot divideau^n, so au^n mod pt > 0.

The proof proceeds by contradiction: we assume that pt dividesau^n, and prove that pt divides au. We can do this constructively since divisibility is decidable. Now, au can be written as \Pi_i p_i^a_i where p_i is the sequence of primes and a_i are suitable coefficients. Then au^n = \Pi_i p_i^(a_i * n). Since pt is prime there is a j such that pt = p_j; then pt | au^n means that a_j * n > 0 so a_j > 0, hence pt divides au! But that contradicts 0 < au < pt, so pt cannot divideau^n.

Mukesh Tiwari (Jul 17 2022 at 08:23):

Thank you very much @Paolo Giarrusso . Yeah, I have Fermat's little theorem available.

Karl Palmskog (Jul 17 2022 at 09:34):

I think the final step is more technically a proof of negation

Last updated: Sep 30 2023 at 06:01 UTC