(* Copyright (C) 2005-2008 Sebastien Briais *)
(* http://lamp.epfl.ch/~sbriais/ *)

(* This library is free software; you can redistribute it and/or modify *)
(* it under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation; either version 2.1 of the *)
(* License, or (at your option) any later version. *)

(* This library is distributed in the hope that it will be useful, but *)
(* WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU *)
(* Lesser General Public License for more details. *)

(* You should have received a copy of the GNU Lesser General Public *)
(* License along with this library; if not, write to the Free Software *)
(* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA *)
(* 02110-1301 USA *)

Require Import missing.
Require Import division.

Unset Standard Proposition Elimination Names.

(** definition of square *)
Definition square (x:nat) := x*x.

(** (x*y)^2 = x^2*y^2 *)
Lemma square_mult_lemma : forall (a b:nat),(square (a*b))=((square a)*(square b)).
(* Goal: forall a b : nat, @eq nat (square (Init.Nat.mul a b)) (Init.Nat.mul (square a) (square b)) *)
  unfold square.
(* Goal: forall (x n m : nat) (_ : gt x (S O)) (_ : divides (power x n) (power x m)), le m n *)
  intros.
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul a b) (Init.Nat.mul a b)) (Init.Nat.mul (Init.Nat.mul a a) (Init.Nat.mul b b)) *)
  ring.
Qed.

(** we now generalize the theorem to the nth-root *)
Fixpoint power (x n:nat) {struct n} : nat :=
  match n with
    O => 1
    | (S n) => (x*(power x n))
  end.

Lemma power_mult_lemma1 : forall (n x y:nat),(power (x*y) n)=(power x n)*(power y n).
(* Goal: forall n : nat, @eq nat (power (S O) n) (S O) *)
  induction n;simpl;trivial.
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul a b) (Init.Nat.mul a b)) (Init.Nat.mul (Init.Nat.mul a a) (Init.Nat.mul b b)) *)
  intros;rewrite (IHn x y);ring.
Qed.

Lemma power_plus_lemma1 : forall (n m x:nat),(power x (n+m))=(power x n)*(power x m).
(* Goal: forall (x n m : nat) (_ : gt x (S O)) (_ : divides (power x n) (power x m)), le m n *)
  induction n;simpl;intros.
(* Goal: @eq nat (power x m) (Init.Nat.add (power x m) O) *)
(* Goal: @eq nat (Init.Nat.mul x (power x (Init.Nat.add n m))) (Init.Nat.mul (Init.Nat.mul x (power x n)) (power x m)) *)
  auto with arith.
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul a b) (Init.Nat.mul a b)) (Init.Nat.mul (Init.Nat.mul a a) (Init.Nat.mul b b)) *)
  rewrite IHn;ring.
Qed.

Lemma power_divides_lemma1 : forall (n x:nat),(0<n)->(divides (power x n) x).
(* Goal: forall (x n m : nat) (_ : gt x (S O)) (_ : divides (power x n) (power x m)), le m n *)
  induction n;simpl;intros.
(* Goal: divides (S O) x *)
(* Goal: divides (Init.Nat.mul x (power x n)) x *)
  inversion H.
(* Goal: divides (Init.Nat.mul x (power x n)) x *)
  exists (power x n);trivial.
Qed.

Lemma power_power_lemma1 : forall (n m x:nat),(power (power x n) m)=(power x (n*m)).
(* Goal: forall (x n m : nat) (_ : gt x (S O)) (_ : divides (power x n) (power x m)), le m n *)
  induction n;simpl;intros.
(* Goal: @eq nat (power x m) (Init.Nat.add (power x m) O) *)
(* Goal: @eq nat (Init.Nat.mul x (power x (Init.Nat.add n m))) (Init.Nat.mul (Init.Nat.mul x (power x n)) (power x m)) *)
  induction m;simpl;auto with arith.
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul a b) (Init.Nat.mul a b)) (Init.Nat.mul (Init.Nat.mul a a) (Init.Nat.mul b b)) *)
  rewrite IHm;ring.
(* Goal: @eq nat (power (Init.Nat.mul x (power x n)) m) (power x (Init.Nat.add m (Init.Nat.mul n m))) *)
  rewrite power_mult_lemma1;rewrite IHn;rewrite <- power_plus_lemma1;trivial.
Qed.

Lemma power_zero : forall (n x:nat),(power x n)=O->x=O.
(* Goal: forall (x n m : nat) (_ : gt x (S O)) (_ : divides (power x n) (power x m)), le m n *)
  induction n;simpl;intros.
(* Goal: @eq nat x O *)
(* Goal: @eq nat x O *)
  discriminate.
(* Goal: @eq nat x O *)
  case (mult_lemma2 x (power x n) H);auto.
Qed.

(** if 1<p and 0<m then p^m>1 *)
Lemma power_lt : forall (p m:nat),(1<p)->(0<m)->1<(power p m).
(* Goal: forall (x n m : nat) (_ : gt x (S O)) (_ : divides (power x n) (power x m)), le m n *)
  induction m;simpl;try omega;intros.
(* Goal: lt (S O) (Init.Nat.mul p (power p m)) *)
  destruct m;simpl;try omega.
(* Goal: lt (S O) (Init.Nat.mul p (Init.Nat.mul p (power p m))) *)
  simpl in IHm.
(* Goal: lt (S O) (Init.Nat.mul p (Init.Nat.mul p (power p m))) *)
  assert (1 < p*(power p m)).
(* Goal: @eq nat (power x m) (Init.Nat.add (power x m) O) *)
(* Goal: @eq nat (Init.Nat.mul x (power x (Init.Nat.add n m))) (Init.Nat.mul (Init.Nat.mul x (power x n)) (power x m)) *)
  apply IHm;auto with arith.
(* Goal: lt (S O) (Init.Nat.mul p (Init.Nat.mul p (power p m))) *)
  rewrite mult_comm.
(* Goal: lt (S O) (Nat.mul (Init.Nat.mul p (power p m)) p) *)
  apply lt_trans with (1*p);try omega.
(* Goal: lt (Init.Nat.mul (S O) p) (Nat.mul (Init.Nat.mul p (power p m)) p) *)
  apply mult_lt_compat_r;try omega.
Qed.

(** 1^n = 1 *)
Lemma power_one : forall (n:nat),(power 1 n)=1.
(* Goal: forall n : nat, @eq nat (power (S O) n) (S O) *)
  induction n;simpl;trivial.
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul a b) (Init.Nat.mul a b)) (Init.Nat.mul (Init.Nat.mul a a) (Init.Nat.mul b b)) *)
  rewrite IHn;ring.
Qed.

(** if x>1 and x^m | x^n then m<=n *)
Lemma power_divides_power : forall (x n m:nat),(x>1)->(divides (power x n) (power x m))->(m<=n).
(* Goal: forall (x n m : nat) (_ : gt x (S O)) (_ : divides (power x n) (power x m)), le m n *)
  intros.
(* Goal: le m n *)
  case (le_lt_dec m n);trivial.
(* Goal: forall _ : lt n m, le m n *)
  intro.
(* Goal: forall _ : lt n m, le m n *)
  generalize (le_plus_minus n m);intro.
(* Goal: le m n *)
  rewrite H1 in H0;try omega.
(* Goal: forall _ : lt n m, le m n *)
  elim H0;intro q;rewrite power_plus_lemma1;intro.
(* Goal: le m n *)
  assert (1=(power x (m-n))*q).
(* Goal: @eq nat (S O) (Init.Nat.mul (power x (Init.Nat.sub m n)) q) *)
(* Goal: le m n *)
  apply mult_lemma6 with (power x n).
(* Goal: not (@eq nat (power x n) O) *)
(* Goal: @eq nat (Init.Nat.mul (power x n) (S O)) (Init.Nat.mul (power x n) (Init.Nat.mul (power x (Init.Nat.sub m n)) q)) *)
(* Goal: le m n *)
  intro;generalize (power_zero n x H3);omega.
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul a b) (Init.Nat.mul a b)) (Init.Nat.mul (Init.Nat.mul a a) (Init.Nat.mul b b)) *)
  rewrite mult_assoc;rewrite <- H2;ring.
(* Goal: forall (x n m : nat) (_ : gt x (S O)) (_ : divides (power x n) (power x m)), le m n *)
  symmetry in H3;elim (mult_lemma5 (power x (m-n)) q H3);intros.
(* Goal: le m n *)
  case (eq_nat_dec (m-n) 0);intro;try omega.
(* Goal: le m n *)
  assert (x=1);try omega.
(* Goal: @eq nat x (S O) *)
  apply divides_antisym;[apply one_min_div | rewrite <- H4;apply power_divides_lemma1;omega].
Qed.

