NyaOJ

题目描述

本试题涉及 modulo 相关定理与中国剩余定理的形式化。请完成下列定理和引理的证明部分。

modulo 的传递性：

theorem modulo_tran (a b c n : Int) :
    modulo n a b → modulo n b c → modulo n a c

modulo 的乘法性质：

theorem modulo_mult_subst (a b c n : Int) :
    modulo n a b → modulo n (a * c) (b * c)

若 $m$ 和 $n$ 互素 (rel_prime)，则存在 $x$ 满足 $x$ 是 $m$ 在模 $n$ 下的乘法逆元。

theorem modulo_inv (m n : Int) :
    rel_prime m n → ∃ x : Int, modulo n (m * x) 1

提示：可以使用 Bézout 定理。在 Mathlib 中使用 Int.gcd_eq_gcd_ab。

简单版本中国剩余定理：对任意两个整数 $a$ 和 $b$ ，如果我们已经知道 $m$ 和 $n$ 是互素的整数，那么我们总可以找到一个整数 $x$ ，使得 $x \equiv a \pmod{m}$ 并且 $x \equiv b \pmod{n}$ 。

theorem SimpleChineseRemainder (m n : Int) :
    rel_prime m n →
    ∀ (a b : Int), ∃ x : Int, modulo m x a ∧ modulo n x b

提示：首先获得 $m'$ 使得 $m \cdot m' \equiv 1 \pmod{n}$ ，然后设 $x = a + m \cdot m' \cdot (b - a)$ 。

总计: 200 分