(* This program 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 program 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 General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(**
   exp.
   Exponential function on Z.
   
   @author Olga Caprotti and Martijn Oostdijk 
   @version $Revision$
*)

Require Import ZArith.

Require Import lemmas.
Require Import natZ.

(** * Exponential function with exponent in nat. *)

Fixpoint Exp (a : Z) (n : nat) {struct n} : Z :=
  match n with
  | O => 1%Z
  | S m => (a * Exp a m)%Z
  end.

Lemma exp_0 : forall n : nat, Exp 0 (S n) = 0%Z.
Proof.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
   simpl in |- *. intros. reflexivity.
Qed.

Lemma exp_1 : forall n : nat, Exp 1 n = 1%Z.
Proof.
(* Goal: forall (n : nat) (a : Z), @eq Z (ZExp a (Z.of_nat n)) (Exp a n) *)
   simple induction n.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
   simpl in |- *. reflexivity.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
   simpl in |- *. intros m IH. rewrite IH. reflexivity.
Qed.

Lemma exp_S : forall (a : Z) (n : nat), Exp a (S n) = (a * Exp a n)%Z.
Proof.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
   simpl in |- *. reflexivity.
Qed.

Lemma exp_plus :
 forall (a : Z) (n m : nat), Exp a (n + m) = (Exp a n * Exp a m)%Z.
Proof.
(* Goal: forall (n : nat) (a : Z), @eq Z (ZExp a (Z.of_nat n)) (Exp a n) *)
   simple induction n.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
   simpl in |- *. intros. elim (Exp a m). reflexivity. reflexivity. reflexivity.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
   intros n1 IH. simpl in |- *. intros.
(* Goal: @eq Z (Z.mul a (Exp a (Init.Nat.add n1 m))) (Z.mul (Z.mul a (Exp a n1)) (Exp a m)) *)
   rewrite (IH m).
(* Goal: @eq Z (Z.mul (Z.mul a b) (Z.mul (Exp a m) (Exp b m))) (Z.mul (Z.mul (Z.mul a b) (Exp a m)) (Exp b m)) *)
   apply Zmult_assoc.
Qed.

Lemma exp_abn :
 forall (a b : Z) (n : nat), Exp (a * b) n = (Exp a n * Exp b n)%Z.
Proof.
(* Goal: forall (n : nat) (a : Z), @eq Z (ZExp a (Z.of_nat n)) (Exp a n) *)
   simple induction n.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
   simpl in |- *. reflexivity.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
   intros m IH. simpl in |- *.
(* Goal: @eq Z (Z.mul (Exp a m0) (Exp a (Init.Nat.mul m m0))) (Z.mul (Exp a m0) (Exp (Exp a m) m0)) *)
   rewrite IH.
(* Goal: @eq Z (Z.mul (Z.mul a b) (Z.mul (Exp a m) (Exp b m))) (Z.mul (Z.mul a (Exp a m)) (Z.mul b (Exp b m))) *)
   rewrite (Zmult_assoc (a * Exp a m) b (Exp b m)).
(* Goal: @eq Z (Z.mul (Z.mul a b) (Z.mul (Exp a m) (Exp b m))) (Z.mul (Z.mul (Z.mul a (Exp a m)) b) (Exp b m)) *)
   rewrite (Zmult_assoc_reverse a (Exp a m) b).
(* Goal: @eq Z (Z.mul (Z.mul a b) (Z.mul (Exp a m) (Exp b m))) (Z.mul (Z.mul a (Z.mul (Exp a m) b)) (Exp b m)) *)
   rewrite (Zmult_comm (Exp a m) b).
(* Goal: @eq Z (Z.mul (Z.mul a b) (Z.mul (Exp a m) (Exp b m))) (Z.mul (Z.mul a (Z.mul b (Exp a m))) (Exp b m)) *)
   rewrite (Zmult_assoc a b (Exp a m)).
(* Goal: @eq Z (Z.mul (Z.mul a b) (Z.mul (Exp a m) (Exp b m))) (Z.mul (Z.mul (Z.mul a b) (Exp a m)) (Exp b m)) *)
   apply Zmult_assoc.
Qed.

Lemma exp_mult : forall (a : Z) (n m : nat), Exp a (n * m) = Exp (Exp a n) m.
Proof.
(* Goal: forall (n : nat) (a : Z), @eq Z (ZExp a (Z.of_nat n)) (Exp a n) *)
   simple induction n.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
   simpl in |- *. intro. rewrite exp_1. reflexivity.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
   intros m IH. simpl in |- *. intros.
(* Goal: @eq Z (Exp a (Init.Nat.add m0 (Init.Nat.mul m m0))) (Exp (Z.mul a (Exp a m)) m0) *)
   rewrite exp_plus.
(* Goal: @eq Z (Z.mul (Exp a m0) (Exp a (Init.Nat.mul m m0))) (Exp (Z.mul a (Exp a m)) m0) *)
   rewrite exp_abn.
(* Goal: @eq Z (Z.mul (Exp a m0) (Exp a (Init.Nat.mul m m0))) (Z.mul (Exp a m0) (Exp (Exp a m) m0)) *)
   rewrite IH.
(* Goal: @eq Z (Exp a (Pos.to_nat p)) (Exp a (Pos.to_nat p)) *)
   reflexivity.
Qed.

Lemma exp_not0 : forall a : Z, a <> 0%Z -> forall m : nat, Exp a m <> 0%Z.
Proof.
(* Goal: forall (a : Z) (_ : not (@eq Z a Z0)) (m : nat), not (@eq Z (Exp a m) Z0) *)
   intros a Ha. simple induction m.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
   simpl in |- *. discriminate.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
   intros n IH. simpl in |- *. intro.
(* Goal: False *)
   elim (Zmult_ab0a0b0 a (Exp a n)).
(* Goal: Z.le Z0 m *)
   assumption. assumption. assumption.
Qed.

(** Convenience lemma for changing exponent. *)

Lemma exp_eq : forall (n m : nat) (a : Z), n = m -> Exp a n = Exp a m.
Proof.
(* Goal: forall (a n m : Z) (_ : Z.le Z0 n) (_ : Z.le Z0 m), @eq Z (ZExp a (Z.mul n m)) (ZExp (ZExp a n) m) *)
   intros. rewrite H. reflexivity.
Qed.

Lemma exp_pred_succ : forall (a : Z) (n : nat), Exp a (pred (S n)) = Exp a n.
Proof.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
   intros. simpl in |- *. reflexivity.
Qed.

(** * Exponential function with exponent in Z. *)

Definition ZExp (a n : Z) : Z :=
  match n with
  | Z0 => 1%Z
  | Zpos p => Exp a (nat_of_P p)
  | Zneg p => Exp a (nat_of_P p)
  end.

Lemma zexp_pred_succ : forall a x : Z, ZExp a (x + 1 - 1) = ZExp a x.
Proof.
(* Goal: forall a x : Z, @eq Z (ZExp a (Z.sub (Z.add x (Zpos xH)) (Zpos xH))) (ZExp a x) *)
   unfold Zminus in |- *.
(* Goal: forall (a n m : Z) (_ : Z.le Z0 n) (_ : Z.le Z0 m), @eq Z (ZExp a (Z.mul n m)) (ZExp (ZExp a n) m) *)
   intros.
(* Goal: @eq Z (ZExp a (Z.add (Z.add x (Zpos xH)) (Z.opp (Zpos xH)))) (ZExp a x) *)
   rewrite Zplus_assoc_reverse.
(* Goal: @eq Z (ZExp a (Z.add x (Z.add (Zpos xH) (Z.opp (Zpos xH))))) (ZExp a x) *)
   rewrite Zplus_opp_r.
(* Goal: @eq Z (ZExp a (Z.add x Z0)) (ZExp a x) *)
   rewrite <- Zplus_0_r_reverse.
(* Goal: @eq Z (Exp a (Pos.to_nat p)) (Exp a (Pos.to_nat p)) *)
   reflexivity.
Qed.

(** Convenience lemma for changing exponent. *)

Lemma zexp_eq : forall x y a : Z, x = y -> ZExp a x = ZExp a y.
Proof.
(* Goal: forall (a n m : Z) (_ : Z.le Z0 n) (_ : Z.le Z0 m), @eq Z (ZExp a (Z.mul n m)) (ZExp (ZExp a n) m) *)
   intros.
(* Goal: @eq Z (ZExp a x) (ZExp a y) *)
   rewrite H.
(* Goal: @eq Z (Exp a (Pos.to_nat p)) (Exp a (Pos.to_nat p)) *)
   reflexivity.
Qed.

Lemma inj_zexp : forall (n : nat) (a : Z), ZExp a (Z_of_nat n) = Exp a n.
Proof.
(* Goal: forall (n : nat) (a : Z), @eq Z (ZExp a (Z.of_nat n)) (Exp a n) *)
   simple induction n.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
   simpl in |- *. reflexivity.
(* Goal: forall (a n m : Z) (_ : Z.le Z0 n) (_ : Z.le Z0 m), @eq Z (ZExp a (Z.mul n m)) (ZExp (ZExp a n) m) *)
   intros m IH. intros.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
   simpl in |- *. rewrite nat_of_P_o_P_of_succ_nat_eq_succ.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
   simpl in |- *. reflexivity.
Qed.

Lemma expzexp : forall x a : Z, ZExp a x = Exp a (Zabs_nat x).
Proof.
(* Goal: forall (a n m : Z) (_ : Z.le Z0 n) (_ : Z.le Z0 m), @eq Z (ZExp a (Z.mul n m)) (ZExp (ZExp a n) m) *)
   intros.
   induction  x as [| p| p].
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
   simpl in |- *. reflexivity.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
   simpl in |- *. reflexivity.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
   simpl in |- *. reflexivity.
Qed.

Lemma zexp_S1 :
 forall a n : Z, (0 <= n)%Z -> ZExp a (n + 1) = (a * ZExp a n)%Z.
Proof.
(* Goal: forall (a n m : Z) (_ : Z.le Z0 n) (_ : Z.le Z0 m), @eq Z (ZExp a (Z.mul n m)) (ZExp (ZExp a n) m) *)
   intros.
(* Goal: @eq Z (Exp a (Z.abs_nat (Z.mul n m))) (Exp (ZExp a n) (Z.abs_nat m)) *)
   rewrite expzexp.
(* Goal: @eq Z (Exp a (Z.abs_nat (Z.mul n m))) (Exp (ZExp a n) (Z.abs_nat m)) *)
   rewrite expzexp.
(* Goal: @eq Z (Exp a (Z.abs_nat (Z.add n m))) (Z.mul (Exp a (Z.abs_nat n)) (Exp a (Z.abs_nat m))) *)
   rewrite abs_plus_pos.
(* Goal: @eq Z (Exp a (Init.Nat.add (Z.abs_nat n) (Z.abs_nat (Zpos xH)))) (Z.mul a (Exp a (Z.abs_nat n))) *)
(* Goal: Z.le Z0 n *)
(* Goal: Z.le Z0 (Zpos xH) *)
   rewrite plus_comm.
(* Goal: @eq Z (Exp a (Nat.add (Z.abs_nat (Zpos xH)) (Z.abs_nat n))) (Z.mul a (Exp a (Z.abs_nat n))) *)
(* Goal: Z.le Z0 n *)
(* Goal: Z.le Z0 (Zpos xH) *)
   change (Exp a (S (Zabs_nat n)) = (a * Exp a (Zabs_nat n))%Z) in |- *.
(* Goal: @eq Z (Exp a (S (Z.abs_nat n))) (Z.mul a (Exp a (Z.abs_nat n))) *)
(* Goal: Z.le Z0 n *)
(* Goal: Z.le Z0 (Zpos xH) *)
   apply exp_S.
(* Goal: Z.le Z0 m *)
   assumption.
(* Goal: Z.le Z0 (Zpos xH) *)
   unfold Zle in |- *.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
   simpl in |- *.
(* Goal: not (@eq comparison Lt Gt) *)
   discriminate.
Qed.

Lemma zexp_S :
 forall a n : Z, (0 <= n)%Z -> ZExp a (Zsucc n) = (a * ZExp a n)%Z.
Proof.
(* Goal: forall (a n m : Z) (_ : Z.le Z0 n) (_ : Z.le Z0 m), @eq Z (ZExp a (Z.mul n m)) (ZExp (ZExp a n) m) *)
   intros.
(* Goal: @eq Z (ZExp a (Z.succ n)) (Z.mul a (ZExp a n)) *)
   change (ZExp a (n + 1) = (a * ZExp a n)%Z) in |- *.
(* Goal: @eq Z (ZExp a (Z.add n (Zpos xH))) (Z.mul a (ZExp a n)) *)
   apply zexp_S1.
(* Goal: Z.le Z0 m *)
   assumption.
Qed.

Lemma zexp_plus :
 forall a n m : Z,
 (0 <= n)%Z -> (0 <= m)%Z -> ZExp a (n + m) = (ZExp a n * ZExp a m)%Z.
Proof.
(* Goal: forall (a n m : Z) (_ : Z.le Z0 n) (_ : Z.le Z0 m), @eq Z (ZExp a (Z.mul n m)) (ZExp (ZExp a n) m) *)
   intros.
(* Goal: @eq Z (Exp a (Z.abs_nat (Z.mul n m))) (Exp (ZExp a n) (Z.abs_nat m)) *)
   rewrite expzexp.
(* Goal: @eq Z (Exp a (Z.abs_nat (Z.mul n m))) (Exp (ZExp a n) (Z.abs_nat m)) *)
   rewrite expzexp.
(* Goal: @eq Z (Exp a (Z.abs_nat (Z.mul n m))) (Exp (ZExp a n) (Z.abs_nat m)) *)
   rewrite expzexp.
(* Goal: @eq Z (Exp a (Z.abs_nat (Z.add n m))) (Z.mul (Exp a (Z.abs_nat n)) (Exp a (Z.abs_nat m))) *)
   rewrite abs_plus_pos.
(* Goal: Z.le Z0 m *)
   apply exp_plus. assumption. assumption.
Qed.

Lemma zexp_mult :
 forall a n m : Z,
 (0 <= n)%Z -> (0 <= m)%Z -> ZExp a (n * m) = ZExp (ZExp a n) m.
Proof.
(* Goal: forall (a n m : Z) (_ : Z.le Z0 n) (_ : Z.le Z0 m), @eq Z (ZExp a (Z.mul n m)) (ZExp (ZExp a n) m) *)
   intros.
(* Goal: @eq Z (Exp a (Z.abs_nat (Z.mul n m))) (Exp (ZExp a n) (Z.abs_nat m)) *)
   rewrite expzexp.
(* Goal: @eq Z (Exp a (Z.abs_nat (Z.mul n m))) (Exp (ZExp a n) (Z.abs_nat m)) *)
   rewrite expzexp.
(* Goal: @eq Z (Exp a (Z.abs_nat (Z.mul n m))) (Exp (ZExp a n) (Z.abs_nat m)) *)
   rewrite expzexp.
(* Goal: @eq Z (Exp a (Z.abs_nat (Z.mul n m))) (Exp (Exp a (Z.abs_nat n)) (Z.abs_nat m)) *)
   rewrite abs_mult.
(* Goal: @eq Z (Exp a (Init.Nat.mul (Z.abs_nat n) (Z.abs_nat m))) (Exp (Exp a (Z.abs_nat n)) (Z.abs_nat m)) *)
   apply exp_mult.
Qed.