Require Import ZArith.

Require Import lemmas.
Require Import natZ.

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 : ∀ n : nat, Exp 0 (S n) = 0%Z.
Proof.
   simpl in |- ×. intros. reflexivity.
Qed.

Lemma exp_1 : ∀ n : nat, Exp 1 n = 1%Z.
Proof.
   simple induction n.
   simpl in |- ×. reflexivity.
   simpl in |- ×. intros m IH. rewrite IH. reflexivity.
Qed.

Lemma exp_S : ∀ (a : Z) (n : nat), Exp a (S n) = (a × Exp a n)%Z.
Proof.
   simpl in |- ×. reflexivity.
Qed.

Lemma exp_plus :
 ∀ (a : Z) (n m : nat), Exp a (n + m) = (Exp a n × Exp a m)%Z.
Proof.
   simple induction n.
   simpl in |- ×. intros. elim (Exp a m). reflexivity. reflexivity. reflexivity.
   intros n1 IH. simpl in |- ×. intros.
   rewrite (IH m).
   apply Zmult_assoc.
Qed.

Lemma exp_abn :
 ∀ (a b : Z) (n : nat), Exp (a × b) n = (Exp a n × Exp b n)%Z.
Proof.
   simple induction n.
   simpl in |- ×. reflexivity.
   intros m IH. simpl in |- ×.
   rewrite IH.
   rewrite (Zmult_assoc (a × Exp a m) b (Exp b m)).
   rewrite (Zmult_assoc_reverse a (Exp a m) b).
   rewrite (Zmult_comm (Exp a m) b).
   rewrite (Zmult_assoc a b (Exp a m)).
   apply Zmult_assoc.
Qed.

Lemma exp_mult : ∀ (a : Z) (n m : nat), Exp a (n × m) = Exp (Exp a n) m.
Proof.
   simple induction n.
   simpl in |- ×. intro. rewrite exp_1. reflexivity.
   intros m IH. simpl in |- ×. intros.
   rewrite exp_plus.
   rewrite exp_abn.
   rewrite IH.
   reflexivity.
Qed.

Lemma exp_not0 : ∀ a : Z, a ≠ 0%Z → ∀ m : nat, Exp a m ≠ 0%Z.
Proof.
   intros a Ha. simple induction m.
   simpl in |- ×. discriminate.
   intros n IH. simpl in |- ×. intro.
   elim (Zmult_ab0a0b0 a (Exp a n)).
   assumption. assumption. assumption.
Qed.

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 in |- ×. reflexivity.
Qed.

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 : ∀ a x : Z, ZExp a (x + 1 - 1) = ZExp a x.
Proof.
   unfold Zminus in |- ×.
   intros.
   rewrite Zplus_assoc_reverse.
   rewrite Zplus_opp_r.
   rewrite <- Zplus_0_r_reverse.
   reflexivity.
Qed.

Lemma zexp_eq : ∀ x y 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 (Z_of_nat n) = Exp a n.
Proof.
   simple induction n.
   simpl in |- ×. reflexivity.
   intros m IH. intros.
   simpl in |- ×. rewrite nat_of_P_o_P_of_succ_nat_eq_succ.
   simpl in |- ×. reflexivity.
Qed.

Lemma expzexp : ∀ x a : Z, ZExp a x = Exp a (Zabs_nat x).
Proof.
   intros.
   induction x as [| p| p].
   simpl in |- ×. reflexivity.
   simpl in |- ×. reflexivity.
   simpl in |- ×. reflexivity.
Qed.

Lemma zexp_S1 :
 ∀ a n : Z, (0 ≤ n)%Z → ZExp a (n + 1) = (a × ZExp a n)%Z.
Proof.
   intros.
   rewrite expzexp.
   rewrite expzexp.
   rewrite abs_plus_pos.
   rewrite plus_comm.
   change (Exp a (S (Zabs_nat n)) = (a × Exp a (Zabs_nat n))%Z) in |- ×.
   apply exp_S.
   assumption.
   unfold Zle in |- ×.
   simpl in |- ×.
   discriminate.
Qed.

Lemma zexp_S :
 ∀ a n : Z, (0 ≤ n)%Z → ZExp a (Zsucc n) = (a × ZExp a n)%Z.
Proof.
   intros.
   change (ZExp a (n + 1) = (a × ZExp a n)%Z) in |- ×.
   apply zexp_S1.
   assumption.
Qed.

Lemma zexp_plus :
 ∀ a n m : Z,
 (0 ≤ n)%Z → (0 ≤ m)%Z → ZExp a (n + m) = (ZExp a n × ZExp a m)%Z.
Proof.
   intros.
   rewrite expzexp.
   rewrite expzexp.
   rewrite expzexp.
   rewrite abs_plus_pos.
   apply exp_plus. assumption. assumption.
Qed.

Lemma zexp_mult :
 ∀ a n m : Z,
 (0 ≤ n)%Z → (0 ≤ m)%Z → ZExp a (n × m) = ZExp (ZExp a n) m.
Proof.
   intros.
   rewrite expzexp.
   rewrite expzexp.
   rewrite expzexp.
   rewrite abs_mult.
   apply exp_mult.
Qed.