Require Export power_ind.
Require Export lemmas.
Definition F :
forall n : nat,
forall g : (forall m : nat, m < n -> Z -> (Z -> Z) -> Z),
forall x:Z,
forall f:Z->Z, Z.
intros n g x f.
case (zerop n).
intros h ; exact (f 1%Z).
intros h'.
case (even_odd_dec n).
intros H.
apply (g (div2 n) (lt_div2 n h') (sqr x) (fun r:Z => f r)).
intros H.
apply (g (n-1) (lt_minus_1 n h') x (fun r:Z => f (x*r)%Z)).
Defined.
| power in cps-style |
F shown as a function
Definition F : forall n : nat,
(forall m : nat, m < n -> Z -> (Z -> Z) -> Z) -> Z -> (Z -> Z) -> Z
fun (n : nat) (g : forall m : nat, m < n -> Z -> (Z -> Z) -> Z)
(x : Z) (f : Z -> Z) =>
match zerop n with
| left _ => f 1%Z
| right h' =>
if even_odd_dec n
then g (div2 n) (lt_div2 n h') (sqr x) (fun r : Z => f r)
else g (n - 1) (lt_minus_1 n h') x (fun r : Z => f (x * r)%Z)
end
|
Definition power (x:Z) (n:nat) (f:Z->Z) :=
(Fix lt_wf (fun _:nat => Z -> (Z -> Z) -> Z) F n x f).
| "expected" reduction rules, simulated by equations |
Lemma local_proof_irr :
forall (n : nat) (f g : forall y : nat, y < n -> Z -> (Z -> Z) -> Z),
(forall (y : nat) (p0 : y < n), f y p0 = g y p0) -> F n f = F n 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 f:Z->Z,
power x n f = F n (fun (m : nat) (H':(lt m n)) (y:Z) (f':Z->Z) => power y m f') x f.
intros x n f.
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 f:Z->Z, power a 0%nat f=(f 1%Z).
intros a f.
rewrite red.
simpl;trivial.
Qed.
Lemma real_red2 : forall a:Z, forall f:Z->Z, forall n:nat, (0<n)->(even n) ->
power a n f = power (sqr a) (div2 n) (fun r:Z => f r).
intros a f 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 f:Z->Z, forall n:nat, (0<n)->(odd n) ->
power a n f = (power a (n-1) (fun r:Z => f (a*r)%Z)).
intros a f 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 (fun x:Z => x))=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 (fun x => x) =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 (fun x => x)) =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) (f:Z->Z),
(forall x:Z,(f x)<>0%Z) -> (a<>0)%Z -> ((power a n f)<>0)%Z.
intros n; elim n using power_ind.
intros m Hm a f Hf Ha.
rewrite Hm.
rewrite real_red1.
apply Hf.
intros n' h' heven' hr a f hf ha.
rewrite real_red2; [idtac|assumption|assumption].
apply hr.
apply hf.
unfold sqr; simpl.
apply mult_diff; [exact ha | exact ha].
intros.
rewrite (real_red3); [idtac|assumption|assumption].
apply H1.
intros x.
apply H2.
apply H3.
Qed.
Lemma power_not_zero :
forall n:nat,forall (a:Z), (a<>0)%Z ->
forall f:Z->Z, (forall x:Z,(f x)<>0%Z) -> ((power a n f)<>0)%Z.
intros n a Ha f Hf.
apply power_not_zero_aux.
apply Hf.
apply Ha.
Qed.
| x^n with x positive is positive (provided f transforms positive integers into positive integers) |
Lemma power_pos_pos_aux :
forall n:nat, forall (a:Z), (0<a)%Z ->
forall (f:Z->Z), (forall x:Z, 0<x -> 0<(f x))%Z -> (0<power a n f)%Z.
intros n; elim n using power_ind.
intros m Hm a Ha f Hf.
rewrite Hm.
rewrite real_red1.
apply Hf;omega.
intros n0 H0 Heven0 hr a Ha f Hf.
rewrite real_red2.
apply hr.
unfold sqr; apply signe2; [exact Ha | exact Ha].
apply Hf.
apply H0.
apply Heven0.
intros n0 H0 Hodd0 hr a Ha f Hf.
rewrite real_red3.
apply hr.
apply Ha.
intros x Hx; apply Hf.
apply signe2; [exact Ha | exact Hx].
apply H0.
apply Hodd0.
Qed.
Lemma power_pos_pos :
forall n:nat, forall (a:Z), (0<a)%Z -> (0<power a n (fun x:Z => x))%Z.
intros n a Ha.
apply power_pos_pos_aux.
apply Ha.
intros x Hx ; apply Hx.
Qed.
| x^n with x negative and n even is positive (provided f transforms positive integers into positive integers) |
Lemma power_neg_even_pos :
forall a:Z, (a<0)%Z -> forall n:nat, (even n)-> forall f:Z->Z,
(forall x:Z, 0<x -> 0<(f x))%Z -> (0<power a n f)%Z.
intros a Ha n; generalize Ha; generalize a; clear Ha a.
elim n using power_ind.
intros m Hm a Ha.
rewrite Hm.
intros Heven f Hf.
rewrite real_red1.
auto with zarith.
intros m H0m Hem hr a Ha.
intros Heven f Hf.
rewrite real_red2; [idtac | apply H0m | apply Hem].
unfold sqr;simpl.
apply power_pos_pos_aux.
apply signe3; [exact Ha|exact Ha].
apply Hf.
intros m H0m Hem hr a Ha Heven f Hf.
cut False.
intros hf; elim hf.
apply (not_even_and_odd m);assumption.
Qed.
| x^n with x positive is negative (provided f transforms positive integers into negative integers) |
Lemma power_neg_odd_neg_aux1 :
forall n:nat,
forall (a:Z), (0<a)%Z ->
forall f:Z->Z, (forall x:Z, 0<x -> 0>f x)%Z ->
(0>power a n f)%Z.
intros n; elim n using power_ind.
intros m Hm a Ha f Hf.
rewrite Hm.
rewrite real_red1.
apply Hf.
omega.
intros m H0m Hem hr a Ha f Hf.
rewrite real_red2; [idtac|apply H0m|apply Hem].
apply hr.
unfold sqr;apply signe2;[apply Ha|apply Ha].
exact Hf.
intros m H0m Hodd hr a Ha f Hf.
rewrite real_red3; [idtac|apply H0m|apply Hodd].
apply hr.
apply Ha.
intros x Hx ; apply Hf.
apply signe2;[apply Ha|apply Hx].
Qed.
| x^n with x <> 0 and n even is negative (provided f transforms positive integers into negative integers) |
Lemma power_neg_odd_neg_aux2 :
forall n:nat, (even n) -> forall (a:Z), (a<>0)%Z ->
forall (f:Z->Z),(forall x:Z, 0<x -> 0>f x)%Z ->
(0>power a n f)%Z.
intros n; elim n using power_ind.
intros m Hm Heven a Ha f Hf.
rewrite Hm.
rewrite real_red1.
apply Hf.
omega.
intros m H0m Hem hr Heven a Ha f Hf.
rewrite real_red2; [idtac|apply H0m|apply Hem].
cut (0<sqr a)%Z.
intros Hcut.
apply power_neg_odd_neg_aux1.
apply Hcut.
exact Hf.
unfold sqr; apply not_zero_implies_square_pos;apply Ha.
intros m H0m Hodd hr a Ha f Hf.
cut False.
intros hf; elim hf.
apply (not_even_and_odd m);assumption.
Qed.
| x^n with x negative, n odd is negative (provided f transforms negative integers into negative integers) |
Lemma power_neg_odd_neg_aux3 :
forall n:nat, (odd n) -> forall (a:Z), (a<0)%Z ->
forall (f:Z->Z),(forall x:Z, 0>x -> 0>f x)%Z ->
(0>power a n f)%Z.
intros n; elim n using power_ind; clear n.
intros m Hm Hodd a Ha f Hf.
rewrite Hm in Hodd.
inversion Hodd.
intros m H0m Hem hr Hodd' a Ha f Hf.
cut False.
intros hf; elim hf.
apply (not_even_and_odd m);[assumption|assumption].
intros m H0m Hodd' hr Hodd'' a Ha f Hf.
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].
omega.
intros x Hx; apply Hf.
apply Zlt_gt.
apply signe1; [apply Ha|apply Hx].
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 (fun x:Z => x))%Z.
intros a Ha n Hodd.
apply power_neg_odd_neg_aux3.
apply Hodd.
apply Ha.
intros x Hx ; apply Hx.
Qed.