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

Require ZArith.

Require lemmas.
Require natZ.

(* Exponential function with exponent in nat. *)

Fixpoint Exp [a:Z;n:nat]: Z :=
    Cases n of
         O     => `1`
       | (S m) => `a * (Exp a m)`
    end.

Lemma exp_0: (n:nat)(Exp `0` (S n))=`0`.
Proof.
   Simpl. Intros. Reflexivity.
Qed.

Lemma exp_1: (n:nat)(Exp `1` n)=`1`.
Proof.
   Induction n.
   Simpl. Reflexivity.
   Simpl. Intros m IH. Rewrite IH. Reflexivity.
Qed.

Lemma exp_S: (a:Z)(n:nat)(Exp a (S n))=`a*(Exp a n)`.
Proof.
   Simpl. Reflexivity.
Qed.

Lemma exp_plus: (a:Z)(n,m:nat)(Exp a (plus n m))=`(Exp a n)*(Exp a m)`.
Proof.
   Induction n.
   Simpl. Intros. Elim (Exp a m). Reflexivity. Reflexivity. Reflexivity.
   Intros n1 IH. Simpl. Intros.
   Rewrite (IH m).
   Apply Zmult_assoc_l.
Qed.

Lemma exp_abn: (a,b:Z)(n:nat)(Exp `a*b` n)=`(Exp a n) * (Exp b n)`.
Proof.
   Induction n.
   Simpl. Reflexivity.
   Intros m IH. Simpl.
   Rewrite IH.
   Rewrite (Zmult_assoc_l `a*((Exp a) m)` b (Exp b m)).
   Rewrite (Zmult_assoc_r a (Exp a m) b).
   Rewrite (Zmult_sym (Exp a m) b).
   Rewrite (Zmult_assoc_l a b (Exp a m)).
   Apply Zmult_assoc_l.
Qed.

Lemma exp_mult: (a:Z)(n,m:nat)(Exp a (mult n m))=(Exp (Exp a n) m).
Proof.
   Induction n.
   Simpl. Intro. Rewrite exp_1. Reflexivity.
   Intros m IH. Simpl. Intros.
   Rewrite exp_plus.
   Rewrite exp_abn.
   Rewrite IH.
   Reflexivity.
Qed.

Lemma exp_not0: (a:Z)`a<>0`->(m:nat)`(Exp a m) <> 0`.
Proof.
   Intros a Ha. Induction m.
   Simpl. Discriminate.
   Intros n IH. Simpl. Intro.
   Elim (Zmult_ab0a0b0 a (Exp a n)).
   Assumption. Assumption. Assumption.
Qed.

(* Convenience lemma for changing exponent. *)

Lemma exp_eq: (n,m:nat; a:Z)n=m->`(Exp a n) = (Exp a m)`.
Proof.
   Intros. Rewrite H. Reflexivity.
Qed.

Lemma exp_pred_succ: (a:Z)(n:nat)(Exp a (pred (S n)))=(Exp a n).
Proof.
   Intros. Simpl. Reflexivity.
Qed.

(* Exponential function with exponent in Z. *)

Definition ZExp[a,n:Z]: Z :=
   Cases n of
      ZERO    => `1`
    | (POS p) => (Exp a (convert p))
    | (NEG p) => (Exp a (convert p))
   end.

Lemma zexp_pred_succ: (a,x:Z)`(ZExp a (x+1-1)) = (ZExp a x)`.
Proof.
   Unfold Zminus.
   Intros.
   Rewrite Zplus_assoc_r.
   Rewrite Zplus_inverse_r.
   Rewrite <- Zplus_n_O.
   Reflexivity.
Qed.

(* Convenience lemma for changing exponent. *)

Lemma zexp_eq: (x,y:Z; a:Z)x=y->`(ZExp a x) = (ZExp a y)`.
Proof.
   Intros.
   Rewrite H.
   Reflexivity.
Qed.

Lemma inj_zexp: (n:nat)(a:Z)(ZExp a (inject_nat n))=(Exp a n).
Proof.
   Induction n.
   Simpl. Reflexivity.
   Intros m IH. Intros.
   Simpl. Rewrite bij1.
   Simpl. Reflexivity.
Qed.

Lemma expzexp: (x:Z)`0<=x`->(a:Z)(ZExp a x)=(Exp a (absolu x)).
Proof.
   Intros.
   Elim (inject_nat_complete x H).
   Intros n Hn.
   Rewrite Hn.
   Rewrite abs_inj.
   Rewrite inj_zexp.
   Reflexivity.
Qed.

Lemma zexp_S1: (a:Z)(n:Z)`0<=n`->(ZExp a `n+1`)=`a*(ZExp a n)`.
Proof.
   Intros.
   Rewrite expzexp.
   Rewrite expzexp.
   Rewrite abs_plus_pos.
   Rewrite plus_sym.
   Change `((Exp a) (S (absolu n))) = a*((Exp a) (absolu n))` .
   Apply exp_S.
   Assumption.
   Unfold Zle.
   Simpl.
   Discriminate.
   Assumption.
   Apply Zle_trans with n.
   Assumption.
   Change `n <= (Zs n)` .
   Apply Zle_n_Sn.
Qed.

Lemma zexp_S: (a:Z)(n:Z)`0<=n`->(ZExp a (Zs n))=`a*(ZExp a n)`.
Proof.
   Intros.
   Change (ZExp a `n+1`)=(`a*((ZExp a) n)`) .
   Apply zexp_S1.
   Assumption.
Qed.

Lemma zexp_plus:
   (a:Z)(n,m:Z)`0<=n`->`0<=m`->`(ZExp a n+m)=(ZExp a n)*(ZExp a m)`.
Proof.
   Intros.
   Rewrite expzexp.
   Rewrite expzexp.
   Rewrite expzexp.
   Rewrite abs_plus_pos.
   Apply exp_plus. Assumption. Assumption.
   Assumption.
   Assumption.
   Apply isnat_plus. Assumption. Assumption.
Qed.