Exponentiation.v 3.29 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   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 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65
Section Exponentiation.

(* Why3 goal *)
Variable t : Type.
Hypothesis t_WhyType : WhyType t.
Existing Instance t_WhyType.

(* Why3 goal *)
Variable one: t.

(* Why3 goal *)
Variable infix_as: t -> t -> t.

(* Why3 goal *)
Hypothesis Assoc : forall (x:t) (y:t) (z:t), ((infix_as (infix_as x y)
  z) = (infix_as x (infix_as y z))).

(* Why3 goal *)
Hypothesis Unit_def_l : forall (x:t), ((infix_as one x) = x).

(* Why3 goal *)
Hypothesis Unit_def_r : forall (x:t), ((infix_as x one) = x).

(* Why3 goal *)
Hypothesis Comm : forall (x:t) (y:t), ((infix_as x y) = (infix_as y x)).

(* Why3 goal *)
Definition power: t -> Z -> t.
intros x n.
exact (iter_nat (Zabs_nat n) t (fun acc => infix_as x acc) one).
Defined.

(* Why3 goal *)
Lemma Power_0 : forall (x:t), ((power x 0%Z) = one).
Proof.
easy.
Qed.

(* Why3 goal *)
Lemma Power_s : forall (x:t) (n:Z), (0%Z <= n)%Z -> ((power x
  (n + 1%Z)%Z) = (infix_as x (power x n))).
Proof.
intros x n h1.
unfold power.
fold (Zsucc n).
now rewrite Zabs_nat_Zsucc.
Qed.

66 67 68 69 70 71 72 73
(* Why3 goal *)
Lemma Power_s_alt : forall (x:t) (n:Z), (0%Z < n)%Z -> ((power x
  n) = (infix_as x (power x (n - 1%Z)%Z))).
intros x n h1.
rewrite <- Power_s; auto with zarith.
f_equal; omega.
Qed.

74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126
(* Why3 goal *)
Lemma Power_1 : forall (x:t), ((power x 1%Z) = x).
Proof.
exact Unit_def_r.
Qed.

(* Why3 goal *)
Lemma Power_sum : forall (x:t) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
  ((power x (n + m)%Z) = (infix_as (power x n) (power x m)))).
Proof.
intros x n m Hn Hm.
revert n Hn.
apply natlike_ind.
apply sym_eq, Unit_def_l.
intros n Hn IHn.
replace (Zsucc n + m)%Z with ((n + m) + 1)%Z by ring.
rewrite Power_s by auto with zarith.
rewrite IHn.
now rewrite <- Assoc, <- Power_s.
Qed.

(* Why3 goal *)
Lemma Power_mult : forall (x:t) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
  ((power x (n * m)%Z) = (power (power x n) m))).
Proof.
intros x n m Hn Hm.
revert m Hm.
apply natlike_ind.
now rewrite Zmult_0_r, 2!Power_0.
intros m Hm IHm.
replace (n * Zsucc m)%Z with (n * m + n)%Z by ring.
rewrite Power_sum by auto with zarith.
rewrite IHm.
now rewrite Comm, <- Power_s.
Qed.

(* Why3 goal *)
Lemma Power_mult2 : forall (x:t) (y:t) (n:Z), (0%Z <= n)%Z ->
  ((power (infix_as x y) n) = (infix_as (power x n) (power y n))).
Proof.
intros x y.
apply natlike_ind.
apply sym_eq.
rewrite 3!Power_0.
apply Unit_def_r.
intros n Hn IHn.
unfold Zsucc.
rewrite 3!(Power_s _ _ Hn).
rewrite IHn.
now rewrite Assoc, <- (Assoc y), (Comm y), 2!Assoc.
Qed.

End Exponentiation.