modulo.v

Require Import ZArith_base.
Require Import ZArith.BinInt.
Require Import Classes.RelationClasses.
Require Import Omega.

Local Open Scope Z_scope.

Definition Divisible (x n : Z) : Prop := exists (k : Z), k*n = x.
Definition Modulo (n x y : Z) : Prop := Divisible (x - y) n.
Notation "( x == y ) 'mod' n" := (Modulo n x y) (at level 50).
Definition Even (x : Z) := (x == 0) mod 2.
Definition Odd (x : Z) := (x == 1) mod 2.

Theorem refl_mod : forall n x : Z, (x == x) mod n.
Proof.
  unfold Modulo, Divisible.
  intros until 0.
  exists 0.
  omega.
Qed.

Instance refl_mod_inst : forall n : Z, Reflexive (Modulo n) :=
  { reflexivity := refl_mod n
  }.

Theorem symm_mod : forall n x y : Z, (x == y) mod n -> (y == x) mod n.
Proof.
  unfold Modulo, Divisible.
  intros until 0.
  intros [ k ].
  exists (-k).
  rewrite Z.mul_opp_l.
  omega.
Qed.

Instance symm_mod_inst : forall n : Z, Symmetric (Modulo n) :=
  { symmetry := symm_mod n
  }.

Theorem trans_mod : forall n x y z : Z, (x == y) mod n -> (y == z) mod n -> (x == z) mod n .
Proof.
  intros until 0.
  unfold Modulo, Divisible.
  intros [ k ] [ k' ].
  exists (k + k').
  rewrite Zmult_plus_distr_l.
  omega.
Qed.

Instance trans_mod_inst : forall n : Z, Transitive (Modulo n) :=
  { transitivity := trans_mod n
  }.

Theorem modulo_addition : forall n a x y : Z,
    (x == y) mod n -> (x + a == y + a) mod n.
Proof.
  intros until 0.
  unfold Modulo, Divisible.
  unfold "x - y".
  intros [ k ].
  exists k.
  omega.
Qed.

Theorem addition_modulo : forall n x y a b : Z,
    (x == y) mod n -> (a == b) mod n -> (x + a == y + b) mod n.
Proof.
  intros.
  apply (modulo_addition n a) in H.
  apply (modulo_addition n y) in H0.
  rewrite Zplus_comm, (Zplus_comm b y) in H0.

  apply (trans_mod _ _ _ _ H H0).
Qed.

Theorem even_additon : forall x y : Z,
    Even x -> Even y -> Even (x + y).
Proof.
  unfold Even.
  intros.
  rewrite <- Z.add_0_l.
  apply (addition_modulo _ _ _ _ _ H H0).
Qed.

Theorem odd_additon : forall x y : Z,
    Even x -> Odd y -> Odd (x + y).
Proof.
  unfold Even, Odd.
  intros.
  rewrite <- Z.add_0_l.
  apply (addition_modulo _ _ _ _ _ H H0).
Qed.

Theorem odd2_additon : forall x y : Z,
    Odd x -> Odd y -> Even (x + y).
Proof.
  unfold Even, Odd.
  intros.

  assert ((2 == 0) mod 2).
  unfold Modulo, Divisible.
  exists 1.
  auto.

  assert ((x + y == 1 + 1) mod 2) as H2 by apply (addition_modulo _ x 1 y 1 H H0) .
  simpl in H2.
  apply (trans_mod _ _ _ _ H2 H1).
Qed.