Require Export power_ind.
Require Export lemmas.
Definition F :
forall n : nat, forall g : (forall m : nat, m < n -> Z -> Z -> Z), forall x:Z, Z -> Z.
intros n g x acc.
case (zerop n).
intros h ; exact acc.
intros h'.
case (even_odd_dec n).
intros H.
apply (g (div2 n) (lt_div2 n h') (sqr x) acc).
intros H.
apply (g (n-1) (lt_minus_1 n h') x (x*acc)%Z).
Defined.
| power with an accumulator |
F shown as a function
Definition F : Z -> forall n : nat, (forall m : nat, m < n -> Z -> Z) -> Z
(n : nat) (g : forall m : nat, m < n -> Z -> Z -> Z) (x acc : Z) =>
match zerop n with
| left _ => acc
| right h' =>
if even_odd_dec n
then g (div2 n) (lt_div2 n h') (sqr x) acc
else g (n - 1) (lt_minus_1 n h') x (x * acc)%Z
end
|
Definition power (x:Z) (n:nat) (acc:Z) :=
(Fix lt_wf (fun _:nat => Z -> Z -> Z) F n x acc).
| "expected" reduction rules, simulated by equations |
Lemma local_proof_irr :
forall (x0 : nat) (f g : forall y : nat, y < x0 -> Z -> Z -> Z),
(forall (y : nat) (p : y < x0), f y p = g y p) -> F x0 f = F x0 g.
intros n f g H'.
unfold F.
case (zerop n).
intros H ; trivial.
intros H.
case (even_odd_dec n).
intros Heven.
rewrite H'.
trivial.
intros Hodd.
rewrite H'.
trivial.
Qed.
| fixpoint equation |
Lemma red : forall x:Z, forall n:nat, forall acc:Z,
power x n acc = F n (fun (m : nat) (H':(lt m n)) (y:Z) (acc':Z) => power y m acc') x acc.
intros x n acc.
unfold power at 1.
rewrite Fix_eq.
trivial.
exact local_proof_irr.
Qed.
| Fixpoint equations for each case |
Lemma real_red1 : forall a:Z,forall acc:Z, power a 0%nat acc=acc.
intros a acc.
rewrite red.
unfold F.
simpl;trivial.
Qed.
Lemma real_red2 : forall a:Z, forall acc:Z, forall n:nat, (0<n)->(even n) ->
power a n acc = power (sqr a) (div2 n) acc.
intros a acc n H0 Heven.
rewrite red.
unfold F.
case (zerop n).
intros H; rewrite H in H0; inversion H0.
intros H0'.
case (even_odd_dec n).
intros Heven'.
trivial.
intros Hodd.
cut False ; [intros h; elim h| idtac].
apply (not_even_and_odd n Heven Hodd).
Qed.
Lemma real_red3 : forall a:Z, forall acc:Z, forall n:nat, (0<n)->(odd n) ->
power a n acc = (power a (n-1) (a*acc)%Z).
intros a acc n H0 Hodd.
rewrite red.
unfold F.
case (zerop n).
intros H; rewrite H in H0; inversion H0.
intros H0'.
case (even_odd_dec n).
intros Heven.
cut False ; [intros h; elim h| idtac].
apply (not_even_and_odd n Heven Hodd).
intros Hodd'.
trivial.
Qed.
| properties of power |
| "evaluation" |
Lemma reduction_1 : forall a:Z, (power a 1 1)=a.
intros a.
rewrite real_red3.
simpl.
rewrite real_red1.
auto with zarith.
auto with arith.
apply odd_S.
apply even_O.
Qed.
Lemma reduction_2 : forall a:Z, ((power a 2 1) =a*a)%Z.
intros a.
rewrite real_red2.
simpl.
rewrite reduction_1.
trivial.
omega.
apply even_S.
apply odd_S.
apply even_O.
Qed.
Lemma reduction_5 : forall a:Z, ((power a 5 1) =a*a*a*a*a)%Z.
intros a.
rewrite real_red3; [simpl|omega|idtac].
rewrite real_red2; [simpl|omega|idtac].
rewrite real_red2; [simpl|omega|idtac].
rewrite real_red3; [simpl|omega|idtac].
rewrite real_red1.
unfold sqr; ring.
apply odd_S ; apply even_O.
apply even_S; apply odd_S; apply even_O.
repeat (apply even_S ;apply odd_S); apply even_O.
repeat (apply odd_S ;apply even_S); apply odd_S; apply even_O.
Qed.
| x^n <> 0 if x <>0 |
Lemma power_not_zero_aux :
forall n:nat,forall (a:Z) (acc:Z),(acc<>0)%Z -> (a<>0)%Z -> ((power a n acc)<>0)%Z.
intros n; elim n using power_ind.
intros m Hm a acc Hacc Ha.
rewrite Hm.
rewrite real_red1.
assumption.
intros n' h' heven' hr a acc hacc ha.
rewrite real_red2; [idtac|assumption|assumption].
apply hr.
apply hacc.
unfold sqr; simpl.
apply mult_diff; [exact ha | exact ha].
intros.
rewrite (real_red3); [idtac|assumption|assumption].
apply H1.
apply mult_diff.
apply H3.
apply H2.
apply H3.
Qed.
Lemma power_not_zero :
forall n:nat,forall (a:Z), (a<>0)%Z -> ((power a n 1)<>0)%Z.
intros n a Ha.
apply power_not_zero_aux.
omega.
apply Ha.
Qed.
| x^n with x positive is positive (provided acc is positive) |
Lemma power_pos_pos_aux :
forall n:nat, forall (a:Z) (acc:Z), (0<a)%Z -> (0<acc)%Z -> (0<power a n acc)%Z.
intros n; elim n using power_ind.
intros m Hm a acc Ha Hacc.
rewrite Hm.
rewrite real_red1.
omega.
intros n0 H0 Heven0 hr a acc Ha Hacc.
rewrite real_red2.
apply hr.
unfold sqr; apply signe2; [exact Ha | exact Ha].
apply Hacc.
apply H0.
apply Heven0.
intros n0 H0 Hodd0 hr a acc Ha Hacc.
rewrite real_red3.
apply hr.
apply Ha.
apply signe2; [exact Ha | exact Hacc].
apply H0.
apply Hodd0.
Qed.
Lemma power_pos_pos :
forall n:nat, forall (a:Z), (0<a)%Z -> (0<power a n 1)%Z.
intros n a Ha.
apply power_pos_pos_aux.
apply Ha.
omega.
Qed.
| x^n with x negative and n even is positive (with acc=1) |
Lemma power_neg_even_pos :
forall a:Z, (a<0)%Z -> forall n:nat, (even n)->(0<power a n 1)%Z.
intros a Ha n; generalize Ha; generalize a; clear Ha a.
elim n using power_ind.
intros m Hm a Ha.
rewrite Hm.
rewrite real_red1.
auto with zarith.
intros m H0m Hem hr a Ha.
rewrite real_red2; [idtac | apply H0m | apply Hem].
unfold sqr;simpl.
intros v.
apply power_pos_pos.
apply signe3; [exact Ha|exact Ha].
intros m H0m Hem hr a Ha.
rewrite (real_red3); [idtac | apply H0m | apply Hem].
intros Hodd.
cut False.
intros hf; elim hf.
apply (not_even_and_odd m);assumption.
Qed.
| x^n with x positive (with acc negative) is negative |
Lemma power_neg_odd_neg_aux1 :
forall n:nat, forall (a:Z) (acc:Z),
(acc<0)%Z -> (0<a)%Z -> (0>power a n acc)%Z.
intros n; elim n using power_ind.
intros m Hm a acc Hacc Ha.
rewrite Hm.
rewrite real_red1.
omega.
intros m H0m Hem hr a acc Hacc Ha.
rewrite real_red2; [idtac|apply H0m|apply Hem].
apply hr.
apply Hacc.
unfold sqr;apply signe2;[apply Ha|apply Ha].
intros m H0m Hodd hr a acc Hacc Ha.
rewrite real_red3; [idtac|apply H0m|apply Hodd].
apply hr.
apply signe4;[apply Ha|apply Hacc].
apply Ha.
Qed.
| x^n with x <> 0 and n even (and acc negative) is negative |
Lemma power_neg_odd_neg_aux2 :
forall n:nat, (even n) -> forall (a:Z) (acc:Z),
(acc<0)%Z -> (a<>0)%Z -> (0>power a n acc)%Z.
intros n; elim n using power_ind.
intros m Hm Heven a acc Hacc Ha.
rewrite Hm.
rewrite real_red1.
omega.
intros m H0m Hem hr Heven a acc Hacc Ha.
rewrite real_red2; [idtac|apply H0m|apply Hem].
cut (0<sqr a)%Z.
intros Hcut.
apply power_neg_odd_neg_aux1.
apply Hacc.
apply Hcut.
unfold sqr; apply not_zero_implies_square_pos;apply Ha.
intros m H0m Hodd hr a acc Hacc Ha.
cut False.
intros hf; elim hf.
apply (not_even_and_odd m);assumption.
Qed.
| x^n with x negative, n odd (and acc positive) is negative |
Lemma power_neg_odd_neg_aux3 :
forall n:nat, (odd n) -> forall (a:Z) (acc:Z),
(0<acc)%Z -> (a<0)%Z -> (0>power a n acc)%Z.
intros n; elim n using power_ind; clear n.
intros m Hm Hodd a acc Ha Hacc.
rewrite Hm in Hodd.
inversion Hodd.
intros m H0m Hem hr Hodd' a acc Hacc Ha.
cut False.
intros hf; elim hf.
apply (not_even_and_odd m);[assumption|assumption].
intros m H0m Hodd' hr Hodd'' a acc Hacc Ha.
rewrite real_red3; [idtac|apply H0m|apply Hodd''].
apply power_neg_odd_neg_aux2.
inversion Hodd'.
replace (S n - 1)%nat with n;[assumption|omega].
apply signe1; [apply Ha|apply Hacc].
omega.
Qed.
| x^n with x negative and n odd is negative |
Lemma power_neg_odd_neg :
forall (a:Z), (a<0)%Z -> forall n:nat, (odd n) -> (0>power a n 1)%Z.
intros a Ha n Hodd.
apply power_neg_odd_neg_aux3.
apply Hodd.
omega.
apply Ha.
Qed.