Power.v 3.14 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

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

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
Qed.

(* Why3 goal *)
85 86
Lemma Power_comm1 : forall (x:Z) (y:Z), ((x * y)%Z = (y * x)%Z) ->
  forall (n:Z), (0%Z <= n)%Z -> (((power x n) * y)%Z = (y * (power x n))%Z).
87
Proof.
88 89 90 91 92 93 94 95 96 97
intros x y h1 n h2.
auto with zarith.
Qed.

(* Why3 goal *)
Lemma Power_comm2 : forall (x:Z) (y:Z), ((x * y)%Z = (y * x)%Z) ->
  forall (n:Z), (0%Z <= n)%Z -> ((power (x * y)%Z n) = ((power x
  n) * (power y n))%Z).
Proof.
intros x y h1 n h2.
98
rewrite 3!power_is_exponentiation ; auto with zarith.
99
apply Power_comm2 ; auto with zarith.
100 101
Qed.

102 103 104 105 106 107 108
(* 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.

109 110 111 112 113 114 115 116 117
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.