Commit 618edb93 authored by MARCHE Claude's avatar MARCHE Claude

power example with Coq proofs

parent d600fbf4
theory Power
use import int.Int
logic power int int : int
axiom Power_0 : forall x : int. power x 0 = 1
axiom Power_s : forall x n : int. 0 < n -> power x n = x * power x (n-1)
lemma Power_1 : forall x : int. power x 1 = x
lemma Power_sum : forall x n m : int. 0 <= n -> 0 <= m ->
power x (n + m) = power x n * power x m
lemma Power_mult : forall x n m : int. 0 <= n -> 0 <= m ->
power x (n * m) = power (power x n) m
end
module M
use import int.Int
use import int.ComputerDivision
use import int.Power
use import Power
let rec fast_exp x n variant { n } =
{ 0 <= n }
......@@ -27,7 +48,7 @@ module M
variant { e }
if mod !e 2 = 1 then r := !r * !p;
p := !p * !p;
e := div !e 2
e := div !e 2
done;
!r
{ result = power x n }
......
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter ignore: forall (a:Type), a -> unit.
Implicit Arguments ignore.
Parameter label_ : Type.
Parameter at1: forall (a:Type), a -> label_ -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Parameter power: Z -> Z -> Z.
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).
Axiom 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)).
Theorem 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))).
(* 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.
apply Power_0.
replace (n*n0)%Z with (n*(n0-1)+n)%Z by ring.
rewrite Power_sum; auto with zarith.
rewrite Hind; auto with zarith.
rewrite <- (Power_1 (power x n)) at 2.
rewrite <- Power_sum; auto with zarith.
ring_simplify (n0 - 1 + 1)%Z; auto.
Qed.
(* DO NOT EDIT BELOW *)
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter ignore: forall (a:Type), a -> unit.
Implicit Arguments ignore.
Parameter label_ : Type.
Parameter at1: forall (a:Type), a -> label_ -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Parameter power: Z -> Z -> Z.
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 *)
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment