提交 #26

import Init.Data.Int
import Mathlib.Data.Int.GCD
abbrev Z := Int

def modulo (n a b : Z) : Prop := n ∣ (a - b)
notation " ( " a " ≡ " b " mod " n  " ) "=> modulo n a b

def modulo_tran : ∀ (a b c n : Z),
  (a ≡ b mod n) -> (b ≡ c mod n) -> (a ≡ c mod n)
:= by
  intros a b c n
  unfold modulo
  intros H1 H2
  let ⟨ k1 , H1 ⟩ := H1
  let ⟨ k2 , H2 ⟩ := H2
  exists k1 + k2
  rw [Int.mul_add, <-H1, <-H2, <-Int.add_sub_assoc, Int.sub_add_cancel]

instance {n} : Trans (modulo n) (modulo n) (modulo n) where
  trans {a} {b} {c} := modulo_tran a b c n

def modulo_plus_subst : ∀ (a b c n : Z),
  (a ≡ b mod n) -> (a + c ≡ b + c mod n)
:= by
  intros a b c n
  unfold modulo
  intros H
  let ⟨ k, H ⟩ := H
  exists k
  rw [<- Int.sub_sub, Int.add_comm, Int.add_sub_assoc, Int.add_comm, Int.add_sub_cancel, H]

def modulo_mult_subst : ∀ (a b c n : Z),
  (a ≡ b mod n) -> (a * c ≡ b * c mod n)
:= by
  intros a b c n
  unfold modulo
  intros H
  let ⟨ k , H ⟩ := H
  exists k * c
  rw [<-Int.sub_mul, <-Int.mul_assoc, H]


abbrev rel_prime m n := Int.gcd m n = 1

theorem modulo_inv : ∀ (m n : Z), rel_prime m n -> ∃ x : Z, (m * x ≡ 1 mod n)
:= by
  intros m n Hrel
  let H := Int.gcd_eq_gcd_ab m n -- require Mathlib's Bezout Theorem for Int
  simp [Hrel] at H
  exists Int.gcdA m n
  unfold modulo
  exists -(Int.gcdB m n)
  rw [H, <-Int.sub_sub, Int.sub_self, Int.zero_sub, Int.mul_neg]


theorem SimpleChineseRemainder :
  ∀ m n : Z, rel_prime m n ->
  ∀ a b : Z, ∃ x : Z, (x ≡ a mod m) ∧ (x ≡ b mod n)
:= by
  intros m n co_prime a b
  let ⟨ u, H ⟩ := modulo_inv m n co_prime
  exists a + (b - a) * u * m
  apply And.intro
  {
    unfold modulo
    rw [Int.add_comm, Int.add_sub_cancel]
    exists (b - a) * u
    rw [Int.mul_comm]
  }
  {
    let H := modulo_mult_subst (m * u) 1 (b - a) n H
    simp [Int.mul_comm m u, Int.mul_comm (u*m), <-Int.mul_assoc] at H
    let H := modulo_plus_subst _ _ a n H
    simp [Int.add_comm] at H
    exact H
  }