Докажите существование модульного мультипликативного обратного, используя Coq - PullRequest
Новая
       7

Докажите существование модульного мультипликативного обратного, используя Coq

0 голосов
/ 27 ноября 2018

Я пытаюсь доказать теорему об остатках в Китае, используя Coq.в настоящее время я пытаюсь доказать существование модульного обратного мультипликатива, это то, что я сделал до сих пор: 

Theorem modulo_inv : forall m n : Z, rel_prime m n -> exists x : Z, (m * x == 1 [ n ]) .
Proof .
  intros m0 n0 co_prime0 .
  destruct (rel_prime_bezout _ _ co_prime0) as [u v Eq].
  cut (u * m0 = 1 - v * n0); auto with zarith .
  intros Eq0 .
  exists u.
  (* the subgoal is Eq0 *)
  Abort.

, и все, что осталось сейчас, это одна подцель, что означает то же, что Eq0 какпоказано ниже: 

1 subgoal
m, n : Z
co_prime : rel_prime m n
m0, n0 : Z
co_prime0 : rel_prime m0 n0
u, v : Z
Eq : u * m0 + v * n0 = 1
Eq0 : u * m0 = 1 - v * n0
______________________________________(1/1)
(m0 * u == 1 [n0])

Кто-нибудь знает, как показать, что подцель равен Eq0?

PS Определение Модуло дано ниже: 

Definition modulo (a b n : Z) : Prop := (n | (a - b)) .
Notation "( a == b [ n ])" := (modulo a b n) .
...