power.mlw_Power_Power_sum_1.v 1.19 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
(* This file is generated by Why3's Coq driver *)
MARCHE Claude's avatar
MARCHE Claude committed
2
(* Beware! Only edit allowed sections below    *)
MARCHE Claude's avatar
MARCHE Claude committed
3 4 5 6 7
Require Import ZArith.
Require Import Rbase.
Definition unit  := unit.

Parameter ignore: forall (a:Type), a  -> unit.
MARCHE Claude's avatar
MARCHE Claude committed
8

MARCHE Claude's avatar
MARCHE Claude committed
9 10 11 12 13
Implicit Arguments ignore.

Parameter label_ : Type.

Parameter at1: forall (a:Type), a -> label_  -> a.
MARCHE Claude's avatar
MARCHE Claude committed
14

MARCHE Claude's avatar
MARCHE Claude committed
15 16 17
Implicit Arguments at1.

Parameter old: forall (a:Type), a  -> a.
MARCHE Claude's avatar
MARCHE Claude committed
18

MARCHE Claude's avatar
MARCHE Claude committed
19 20 21 22
Implicit Arguments old.

Parameter power: Z -> Z  -> Z.

MARCHE Claude's avatar
MARCHE Claude committed
23

MARCHE Claude's avatar
MARCHE Claude committed
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
Axiom Power_0 : forall (x:Z), ((power x 0%Z) = 1%Z).

Axiom Power_s : forall (x:Z) (n:Z), (0%Z <  n)%Z -> ((power x
  n) = (x * (power x (n - 1%Z)%Z))%Z).

Axiom Power_1 : forall (x:Z), ((power x 1%Z) = x).

Theorem 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)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x n m Hn Hm.
generalize Hm.
pattern m.
apply Z_lt_induction; auto.
intros n0 Hind Hn0.
assert (h:(n0 = 0 \/ n0 > 0)%Z) by omega.
destruct h.
subst n0; rewrite Power_0; ring_simplify (n+0)%Z; ring.
rewrite Power_s; auto with zarith.
replace (n+n0-1)%Z with (n+(n0-1))%Z by omega.
rewrite Hind; auto with zarith.
rewrite (Power_s x n0).
ring.
omega.
Qed.
(* DO NOT EDIT BELOW *)