Power.v 2.89 KB
Newer Older
1 2 3 4 5 6 7 8
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10 11
(********************************************************************)

12
(* This file is generated by Why3's Coq-realize driver *)
13
(* Beware! Only edit allowed sections below    *)
14 15
Require Import BuiltIn.
Require BuiltIn.
16 17
Require int.Int.

18 19
Require Import Exponentiation.

20
(* Why3 goal *)
21 22 23 24 25 26 27 28 29 30 31
Notation power := Zpower.

Lemma power_is_exponentiation :
  forall x n, (0 <= n)%Z -> power x n = Exponentiation.power _ 1%Z Zmult x n.
Proof.
intros x [|n|n] H.
easy.
2: now elim H.
unfold Exponentiation.power, power, Zpower_pos.
now rewrite iter_nat_of_P.
Qed.
32 33 34

(* Why3 goal *)
Lemma Power_0 : forall (x:Z), ((power x 0%Z) = 1%Z).
35
Proof.
36
intros x.
37 38
apply refl_equal.
Qed.
39 40 41 42

(* Why3 goal *)
Lemma Power_s : forall (x:Z) (n:Z), (0%Z <= n)%Z -> ((power x
  (n + 1%Z)%Z) = (x * (power x n))%Z).
43
Proof.
44
intros x n h1.
45 46 47 48 49 50
rewrite Zpower_exp.
change (power x 1) with (x * 1)%Z.
ring.
now apply Zle_ge.
easy.
Qed.
51

52 53 54 55 56 57 58 59 60
(* Why3 goal *)
Lemma Power_s_alt : forall (x:Z) (n:Z), (0%Z < n)%Z -> ((power x
  n) = (x * (power x (n - 1%Z)%Z))%Z).
intros x n h1.
rewrite <- Power_s.
f_equal; auto with zarith.
omega.
Qed.

61 62
(* Why3 goal *)
Lemma Power_1 : forall (x:Z), ((power x 1%Z) = x).
63 64 65
Proof.
exact Zmult_1_r.
Qed.
66 67

(* Why3 goal *)
68 69 70 71 72
Lemma Power_sum : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
  ((power x (n + m)%Z) = ((power x n) * (power x m))%Z)).
Proof.
intros x n m Hn Hm.
now apply Zpower_exp; apply Zle_ge.
73 74 75 76 77
Qed.

(* Why3 goal *)
Lemma Power_mult : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
  ((power x (n * m)%Z) = (power (power x n) m))).
78
Proof.
79
intros x n m Hn Hm.
80 81
rewrite 3!power_is_exponentiation ; auto with zarith.
apply Power_mult ; auto with zarith.
82 83 84 85 86
Qed.

(* Why3 goal *)
Lemma Power_mult2 : forall (x:Z) (y:Z) (n:Z), (0%Z <= n)%Z ->
  ((power (x * y)%Z n) = ((power x n) * (power y n))%Z).
87
Proof.
88
intros x y n Hn.
89 90
rewrite 3!power_is_exponentiation ; auto with zarith.
apply Power_mult2 ; auto with zarith.
91 92
Qed.

93 94 95 96 97 98 99
(* Why3 goal *)
Lemma Power_non_neg : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <= y)%Z) ->
  (0%Z <= (power x y))%Z.
intros x y (h1,h2).
now apply Z.pow_nonneg.
Qed.

100 101 102 103 104 105 106 107 108
Open Scope Z_scope.

(* Why3 goal *)
Lemma Power_monotonic : forall (x:Z) (n:Z) (m:Z), ((0%Z < x)%Z /\
  ((0%Z <= n)%Z /\ (n <= m)%Z)) -> ((power x n) <= (power x m))%Z.
intros.
apply Z.pow_le_mono_r; auto with zarith.
Qed.