NDiv.v

(****************************************************************************                                                                                         IEEE754  :  NDiv                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** Definition of the quotient and divisibility for natural and relative numbers*)
Require Import Omega.
Require Import Arith.
Require Import Compare.
Require Import Faux.
Require Import Euclid_proof.
Require Import Zpower.
Require Import Zcomplements.
Require Import Reals.
Require Import sTactic.
Require Import Digit.

(* We use the quotient function in Euclid proof to build our Nquotient *)

Definition Nquotient :=
   [m, n:nat]
      Cases n of
          O => O
         | (S n') =>
             Cases (quotient (S n') (lt_le_S O (S n') (lt_O_Sn n')) m) of
                 (exist x _) => x
             end
      end.
(* It has the required property *)

Theorem NquotientProp:
  (m, n:nat) (lt O n) ->
  (ex nat [r:nat]m=(plus (mult (Nquotient m n) n) r) /\ (lt r n)).
Intros m n; Unfold Nquotient; Case n; Auto with arith.
Intros H'; Inversion H'.
Intros n0 H'; Case (quotient (S n0) (lt_le_S O (S n0) (lt_O_Sn n0)) m).
Intros x H'0; Elim H'0; Intros r E; Exists r; Intuition.
Qed.

(* We lift this quotient to relative numbers *)

Definition ZNquotient :=
   [m:Z] [n:nat]
      Cases m of
          ZERO => ZERO
         | (POS x) => (INZ (Nquotient (absolu m) n))
         | (NEG x) => (Zopp (INZ (Nquotient (absolu m) n)))
      end.

Theorem ZNquotientProp:
  (m:Z) (n:nat) (lt O n) -> (absolu m)=(mult (Nquotient (absolu m) n) n) ->
  m=(Zmult (ZNquotient m n) (INZ n)).
Intros m n; Case m; Simpl; Auto.
Intros p H' H'0.
Unfold INZ; Rewrite <- inj_mult; Auto.
Rewrite <- H'0; Auto with zarith.
Apply sym_equal.
Apply inject_nat_convert; Auto.
Intros p H' H'0.
Rewrite Zopp_Zmult.
Unfold INZ; Rewrite <- inj_mult; Auto.
Rewrite <- H'0; Auto with zarith.
Replace (NEG p) with (Zopp (POS p)).
Cut (POS p)=(INZ (convert p)).
Intros H'1; Rewrite H'1; Auto.
Apply sym_equal.
Apply inject_nat_convert; Auto.
Simpl; Auto.
Qed.

(* The property of a  number to divide another one      (Ndivides n m) shoud be read as m divides n *)

Definition Ndivides := [n, m:nat](Ex [q:nat] n=(mult m q)).

Theorem NdividesNquotient:
  (n, m:nat) (lt O m) -> (Ndivides n m) ->n=(mult (Nquotient n m) m).
Intros n m H' H'0.
Red in H'0.
Elim H'0; Intros q E; Clear H'0.
Elim (NquotientProp n m);
[Intros r E0; Elim E0; Intros H'3 H'4; Clear E0 | Idtac]; Auto.
Pattern 1 n; Rewrite E.
Case (le_or_lt q (Nquotient n m)); Intros H'5; Auto with arith.
Case (le_lt_or_eq ? ? H'5); Intros H'6; Auto with arith.
2:Elim H'6; Auto with arith.
Absurd (lt (mult m q) (mult m (Nquotient n m))); Auto with arith.
Rewrite <- E.
Pattern 1 n; Rewrite H'3; Rewrite (mult_sym m); Auto with arith.
Absurd (le (mult (S (Nquotient n m)) m) (mult m q)).
Simpl; Auto with zarith.
Rewrite (mult_sym m).
Apply lte_comp_mult; Auto with arith.
Qed.

Theorem NdividesNquotientInv:
  (n, m:nat) n=(mult (Nquotient n m) m) ->(Ndivides n m).
Intros n m H'; Red.
Exists (Nquotient n m); Auto.
Pattern 1 n; Rewrite H'; Auto with arith.
Qed.

Theorem NdividesMult:
  (n, m, p:nat) (Ndivides n m) ->(Ndivides (mult p n) (mult p m)).
Intros n m p H'; Red in H'.
Elim H'; Intros q E.
Red.
Exists q.
Rewrite E.
Auto with arith.
Qed.

Theorem NdividesDiv:
  (n, m, p:nat) (lt O p) -> (Ndivides (mult p n) (mult p m)) ->(Ndivides n m).
Intros n m p H' H'0; Red in H'0.
Elim H'0; Intros q E; Clear H'0.
Red.
Exists q.
Apply mult_eq_inv with n := p; Auto with arith; Rewrite mult_assoc_l; Auto.
Qed.

Definition dividesP: (n, m:nat){(Ndivides n m)}+{~ (Ndivides n m)}.
Intros n m; Case m.
Case n.
Left; Red; Exists O; Auto with arith.
Intros n0; Right; Red; Intros H'; Red in H'.
Elim H'; Intros q; Simpl; Intros; Discriminate.
Intros n0.
Case (natEq n (mult (Nquotient n (S n0)) (S n0))).
Intros H'; Left.
Apply NdividesNquotientInv; Auto.
Intros H'; Right; Red; Intros H'0; Case H'.
Apply NdividesNquotient; Auto with arith.
Defined.

Theorem Nquotient1: (m:nat)(Nquotient m (1))=m.
Intros m.
Elim (NquotientProp m (1)); Auto.
Intros x H'; Elim H'; Intros H'0 H'1.
Pattern 2 m; Rewrite H'0.
Auto with zarith.
Qed.

Theorem ZNquotient1: (m:Z)(ZNquotient m (1))=m.
Intros m; Case m; Auto.
Intros p; Generalize (Nquotient1 (convert p)); Simpl.
Case (quotient (1) (lt_le_S O (1) (lt_O_Sn O)) (convert p)).
Intros x H' H'0; Rewrite H'0; Simpl; Auto with arith zarith.
Rewrite (inject_nat_convert (POS p)); Auto.
Intros p; Generalize (Nquotient1 (convert p)); Simpl.
Case (quotient (1) (lt_le_S O (1) (lt_O_Sn O)) (convert p)).
Intros x H' H'0; Rewrite H'0; Simpl; Auto with arith zarith.
Rewrite (inject_nat_convert (POS p)); Auto.
Qed.

Theorem Ndivides1: (m:nat)(Ndivides m (1)).
Intros m; Exists m; Auto with arith.
Qed.

Theorem NquotientUnique:
  (m, n, q, r:nat) (lt O n) -> m=(plus (mult q n) r) -> (lt r n) ->
  q=(Nquotient m n).
Intros m n q r H' H'0 H'1.
Elim (NquotientProp m n);
[Intros r1 E; Elim E; Intros H'7 H'8; Clear E | Idtac]; Auto.
Case (le_or_lt q (Nquotient m n)); Intros H'2; Auto with arith.
Case (le_lt_or_eq ? ? H'2); Clear H'2; Intros H'3; Auto with arith.
Contradict H'1.
Apply le_not_lt.
Apply le_trans with m := (plus n r1); Auto with arith.
Apply simpl_le_plus_l with p := m.
Pattern 1 m; Rewrite H'0.
Rewrite H'7.
Cut (le (plus (mult q n) n) (mult (Nquotient m n) n)); Auto with zarith.
Replace (plus (mult q n) n) with (mult (S q) n); Auto with arith; Simpl;
Auto with arith.
Contradict H'8.
Apply le_not_lt.
Apply le_trans with m := (plus n r); Auto with arith.
Apply simpl_le_plus_l with p := m.
Pattern 2 m; Rewrite H'0.
Rewrite H'7.
Cut (le (plus (mult (Nquotient m n) n) n) (mult q n)); Auto with zarith.
Replace (plus (mult (Nquotient m n) n) n) with (mult (S (Nquotient m n)) n);
Auto with arith; Simpl; Auto with arith.
Qed.

Theorem NquotientMonotone:
  (n, m, q:nat) ~ q=O -> (lt n m) ->(le (Nquotient n q) (Nquotient m q)).
Intros n m q H' H'0.
Case (le_or_lt (Nquotient n q) (Nquotient m q)); Auto.
Intros H'1.
Elim (NquotientProp m q);
[Intros r1 E; Elim E; Intros H'5 H'6; Clear E | Idtac]; Auto with zarith.
Elim (NquotientProp n q);
[Intros r2 E; Elim E; Intros H'7 H'8; Try Exact H'7; Clear E | Idtac];
Auto with zarith.
Contradict H'0.
Apply le_not_lt.
Apply le_trans with m := (plus (plus m (minus q r1)) r2); Auto with zarith.
Apply simpl_le_plus_l with p := r1; Auto with zarith.
Replace (plus r1 (plus (plus m (minus q r1)) r2)) with (plus (plus m q) r2);
Auto with zarith.
Rewrite H'5.
Rewrite H'7.
Replace (plus (plus (plus (mult (Nquotient m q) q) r1) q) r2)
     with (plus r1 (plus (mult (S (Nquotient m q)) q) r2));
Auto with zarith arith.
Simpl; Auto with zarith arith.
Qed.

Theorem ZNquotientMonotone:
  (n, m:Z) (q:nat) ~ q=O -> (Zlt n m) ->(Zle (ZNquotient n q) (ZNquotient m q)).
Intros n m; Case n; Case m; Simpl; Auto with zarith arith.
Intros p q H' H'0; Replace ZERO with (INZ O); Auto with zarith arith.
Intros p q H' H'0; Inversion H'0.
Intros p q H' H'0; Inversion H'0.
Intros p p0 q H' H'0; Apply inj_le; Auto.
Apply NquotientMonotone; Auto.
Apply lt_Zlt_inv; Auto.
Simpl; Auto.
Unfold INZ; Rewrite (inject_nat_convert (POS p0) p0); Auto.
Unfold INZ; Rewrite (inject_nat_convert (POS p) p); Auto.
Intros p p0 q H' H'0; Inversion H'0.
Intros p q H' H'0; Replace ZERO with (Zopp (INZ O)); Auto with zarith arith.
Intros p p0 q H' H'0.
Apply Zle_trans with m := ZERO; Auto with zarith arith.
Replace ZERO with (Zopp (INZ O)); Auto with zarith arith.
Replace ZERO with (INZ O); Auto with zarith arith.
Intros p p0 q H' H'0.
Apply Zle_Zopp; Apply inj_le.
Apply NquotientMonotone; Auto.
Apply lt_Zlt_inv; Auto with zarith arith.
Unfold INZ; Rewrite (inject_nat_convert (Zopp (NEG p0)) p0); Auto.
Unfold INZ; Rewrite (inject_nat_convert (Zopp (NEG p)) p); Auto.
Auto with zarith arith.
Qed.

Theorem NotDividesDigit:
  (r:nat) (v:nat) (lt (1) r) -> ~ v=O ->~ (Ndivides v (exp r (digit r v))).
Intros r v H H'; Red; Intros H'0; Red in H'0.
Elim H'0; Intros q E; Clear H'0.
Absurd (lt v (exp r (digit r v))); Auto with arith.
Generalize H'; Pattern 1 2 v; Rewrite E; Auto.
Case q; Simpl; Auto with arith.
Intros n H'0; Rewrite mult_sym; Simpl; Auto with arith.
Qed.

Theorem NDividesLt: (n, m:nat) ~ n=O -> (Ndivides n m) ->(le m n).
Intros n m H' H'0; Red in H'0.
Elim H'0; Intros q E; Generalize H'; Rewrite E; Clear H'0.
Repeat Rewrite (mult_sym m); Case q; Simpl; Auto with zarith arith.
Qed.

Theorem Nquotient_mult_comp:
  (m, n, p:nat) ~ n=O -> ~ p=O ->
  (Nquotient (mult m p) (mult n p))=(Nquotient m n).
Intros m n p H' H'0.
Elim (NquotientProp m n); [Intros r E; Elim E; Intros H'4 H'5; Clear E | Idtac];
Auto with arith zarith.
Apply sym_equal.
Apply NquotientUnique with r := (mult r p); Auto with arith zarith.
Generalize H' H'0; Case n; Case p; Simpl; Auto with arith zarith.
Pattern 1 m; Rewrite H'4; Auto with arith zarith.
Rewrite mult_plus_distr; Auto with arith zarith.
Qed.

Theorem ZNquotient_INZ:
  (m, n:nat) ~ n=O ->(ZNquotient (INZ m) n)=(inject_nat (Nquotient m n)).
Intros m; Case m; Simpl; Auto with arith zarith.
Intros n H'.
Rewrite <- (NquotientUnique O n O O); Auto with arith zarith.
Intros n n0 H'.
Rewrite bij1; Auto.
Qed.

Theorem ZNquotient_Zopp:
  (m:Z) (n:nat)(ZNquotient (Zopp m) n)=(Zopp (ZNquotient m n)).
Intros m; Case m; Simpl; Auto with arith zarith.
Qed.

Theorem ZNquotient_mult_comp:
  (m:Z) (n, p:nat) ~ n=O -> ~ p=O ->
  (ZNquotient (Zmult m (inject_nat p)) (mult n p))=(ZNquotient m n).
Intros m n p H' H'0; Case m; Auto.
Intros p0.
Replace (ZNquotient (POS p0) n) with (INZ (Nquotient (absolu (POS p0)) n)); Auto.
Replace (Zmult (POS p0) (inject_nat p)) with (INZ (mult (absolu (POS p0)) p));
Auto.
Simpl; Auto.
Rewrite ZNquotient_INZ; Auto with arith zarith.
Rewrite Nquotient_mult_comp; Auto.
Generalize H' H'0; Case n; Case p; Simpl; Auto with arith zarith.
Rewrite inj_mult; Auto with arith zarith.
Replace (absolu (POS p0)) with (convert p0); Auto.
Rewrite (inject_nat_convert (POS p0)); Auto.
Intros p0.
Replace (ZNquotient (NEG p0) n)
     with (Zopp (INZ (Nquotient (absolu (NEG p0)) n))); Auto.
Replace (Zmult (NEG p0) (inject_nat p))
     with (Zopp (INZ (mult (absolu (NEG p0)) p))); Auto.
Rewrite ZNquotient_Zopp.
Simpl.
Rewrite ZNquotient_INZ; Auto with arith zarith.
Rewrite Nquotient_mult_comp; Auto.
Generalize H' H'0; Case n; Case p; Simpl; Auto with arith zarith.
Replace (absolu (NEG p0)) with (convert p0); Auto.
Replace (NEG p0) with (Zopp (POS p0)); Auto.
Rewrite <- (inject_nat_convert (POS p0) p0); Auto with arith zarith.
Rewrite Zmult_Zopp_left; Auto.
Rewrite <- Zopp_Zmult_r; Auto with arith zarith.
Rewrite inj_mult; Auto with arith zarith.
Qed.

Theorem NDivides_add:
  (n, m, p:nat) (Ndivides n p) -> (Ndivides m p) ->(Ndivides (plus n m) p).
Intros n m p H' H'0.
Inversion H'0; Inversion H'.
Exists (plus x0 x).
Rewrite H0; Rewrite H.
Repeat Rewrite (mult_sym p); Auto with arith.
Qed.

Theorem NDivides_minus:
  (n, m, p:nat) (Ndivides n p) -> (Ndivides m p) ->(Ndivides (minus n m) p).
Intros n m p H' H'0.
Inversion H'0; Inversion H'.
Exists (minus x0 x).
Rewrite H0; Rewrite H.
Repeat Rewrite (mult_sym p); Auto with arith.
Qed.

Theorem NDivides_mult:
  (n, m, p, q:nat) (Ndivides n p) -> (Ndivides m q) ->
  (Ndivides (mult n m) (mult p q)).
Intros n m p q H' H'0.
Inversion H'0; Inversion H'.
Exists (mult x0 x).
Rewrite H0; Rewrite H.
Ring.
Qed.

22/10/100, 19:44