Require Export power_ind.
Require Export lemmas.
Definition F :
forall x:Z, forall n : nat, forall g : (forall m : nat, m < n -> Z),Z.
intros x n g.
case (zerop n).
intros h ; exact 1%Z.
intros h'.
case (even_odd_dec n).
intros H.
exact (let tmp := (g (div2 n) (lt_div2 n h')) in (sqr tmp)%Z).
intros H.
apply Zmult.
apply x.
apply (g (n-1)).
apply (lt_minus_1 n h').
Defined.
| in this example, x does not change, every recursive call is performed with x |
F shown as a function
Definition F :
fun (x : Z) (n : nat) (g : forall m : nat, m < n -> Z) =>
match zerop n with
| left _ => 1%Z
| right h' =>
if even_odd_dec n
then let tmp := g (div2 n) (lt_div2 n h') in sqr tmp
else (x * g (n - 1)%nat (lt_minus_1 n h'))%Z
end
|
Definition power (x:Z)(n:nat) : Z := (Fix lt_wf (fun _:nat=>Z) (F x) n).
| "expected" reduction rules, simulated by equations |
Lemma local_proof_irr :
forall x:Z,
forall (x0 : nat) (f g : forall y : nat, y < x0 -> Z),
(forall (y : nat) (p : y < x0), f y p = g y p) ->
F x x0 f = F x x0 g.
intros x 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 x n (fun (m : nat) (H' : (lt m n)) => power x m).
intros x n.
unfold power at 1.
rewrite Fix_eq.
trivial.
exact (local_proof_irr x ).
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 = let tmp := (power a (div2 n)) in (tmp*tmp)%Z.
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.
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.
elim n using power_ind.
intros m Hm.
rewrite Hm.
rewrite real_red1.
omega.
intros n' h' heven' hr'.
rewrite real_red2; [idtac|assumption|assumption].
simpl.
apply mult_diff.
apply hr'.
apply hr'.
intros.
rewrite (real_red3).
apply mult_diff.
apply ha.
apply H1.
apply H.
apply H0.
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.
intros n Hn;generalize Hn; elim n using power_ind.
intros m Hm.
rewrite Hm.
rewrite real_red1.
auto with zarith.
intros m H0m Hem hr.
rewrite real_red2; [idtac | apply H0m | apply Hem].
simpl.
intros v.
apply not_zero_implies_square_pos.
apply power_not_zero.
omega.
intros.
rewrite (real_red2).
simpl.
apply not_zero_implies_square_pos.
apply power_not_zero.
omega.
apply H.
apply Hn0.
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; elim n using power_ind.
intros m Hm.
rewrite Hm.
rewrite real_red1.
omega.
intros n0 H Heven hr.
rewrite real_red2.
simpl.
apply signe2;assumption.
exact H.
exact Heven.
intros n0 H Heven hr.
rewrite real_red3.
apply signe2;assumption.
exact H.
exact Heven.
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.