Require Export power_ind.
Require Export lemmas.
| in this case, recursive calls (even) are performed with x^2 |
Definition F :
forall n : nat, forall g : (forall m : nat, m < n -> Z -> Z), forall x:Z, Z.
intros n g x.
case (zerop n).
intros h ; exact 1%Z.
intros h'.
case (even_odd_dec n).
intros H.
apply (g (div2 n) (lt_div2 n h') (sqr x)).
intros H.
apply Zmult.
apply x.
apply (g (n-1) (lt_minus_1 n h') x).
Defined.
F shown as a function
Definition F : Z -> forall n : nat, (forall m : nat, m < n -> Z -> Z) -> Z :=
fun (n : nat) (g : forall m : nat, m < n -> Z -> Z) (x : Z) =>
match zerop n with
| left _ => 1%Z
| right h' =>
if even_odd_dec n
then g (div2 n) (lt_div2 n h') (sqr x)
else (x * g (n - 1)%nat (lt_minus_1 n h') x)%Z
end
|
Definition power (x:Z) (n:nat) :=
((Fix lt_wf (fun _:nat => Z -> Z) F) n x).
| "expected" reduction rules, simulated by equations |
Lemma local_proof_irr :
forall (x0 : nat) (f g : forall y : nat, y < x0 -> 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,
power x n = F n (fun (m : nat) (H' : (lt m n)) (y:Z) => power y m) x.
intros x n.
unfold power at 1.
rewrite Fix_eq.
trivial.
exact local_proof_irr.
Qed.
| Fixpoint equations for each case |
Lemma real_red1 : forall a:Z,power a 0%nat=1%Z.
intros a.
rewrite red.
unfold F.
simpl;trivial.
Qed.
Lemma real_red2 : forall a:Z, forall n:nat, (0<n)->(even n) ->
power a n = power (sqr a) (div2 n).
intros a 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 n:nat, (0<n)->(odd n) ->
power a n = (a*(power a (n-1)))%Z.
intros a 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)=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) =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) =a*a*a*a*a)%Z.
intros a.
rewrite real_red3; [simpl|omega|idtac].
rewrite real_red2; [simpl|omega|idtac].
rewrite reduction_2.
unfold sqr; ring.
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 :
forall a:Z,forall n:nat,(a<>0)%Z -> ((power a n)<>0)%Z.
intros a n ha; generalize ha; generalize a; clear ha a.
elim n using power_ind.
intros m Hm.
rewrite Hm.
intros a Ha.
rewrite real_red1.
omega.
intros n' h' heven' hr' a ha.
rewrite real_red2; [idtac|assumption|assumption].
apply hr'.
unfold sqr; simpl.
apply mult_diff; [exact ha | exact ha].
intros.
rewrite (real_red3); [idtac|assumption|assumption].
apply mult_diff.
apply ha.
apply H1.
apply ha.
Qed.
| x^n with x positive is positive |
Lemma power_pos_pos :
forall a:Z, (0<a)%Z -> forall n:nat, (0<power a n)%Z.
intros a Ha n;generalize Ha; generalize a; clear Ha a.
elim n using power_ind.
intros m Hm; rewrite Hm.
intros a Ha; rewrite real_red1.
omega.
intros n0 H0 Heven0 hr a Ha.
rewrite real_red2.
apply hr.
unfold sqr; apply signe2; [exact Ha | exact Ha].
apply H0.
apply Heven0.
intros n0 H0 Hodd0 hr a Ha.
rewrite real_red3.
apply signe2.
apply Ha.
apply hr.
apply Ha.
apply H0.
apply Hodd0.
Qed.
| x^n with x negative and n even is positive |
Lemma power_neg_even_pos :
forall a:Z, (a<0)%Z -> forall n:nat, (even n)->(0<power a n)%Z.
intros a Ha n; generalize Ha; generalize a; clear Ha a.
elim n using power_ind.
intros m Hm; rewrite Hm.
intros a Ha; 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 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)%Z.
intros a Ha.
intros n ; elim n using power_ind.
intros m Hm; rewrite Hm.
rewrite real_red1.
intros h; inversion h.
intros m H0m Hem hr.
rewrite real_red2; [idtac | apply H0m | apply Hem].
simpl.
intros v.
cut False.
intros Hf; elim Hf.
apply (not_even_and_odd m Hem v).
intros m h1 hodd1 hr hodd3.
rewrite real_red3.
clear hr.
cut (even (m-1)).
intros heven.
apply Zlt_gt.
apply signe1.
apply Ha.
apply (power_neg_even_pos a Ha (m-1) heven).
apply odd_even_minus;assumption.
exact h1.
exact hodd1.
Qed.