Commit 97987740 authored by MARCHE Claude's avatar MARCHE Claude Committed by Guillaume Melquiond

update theory int.Exponentiation and its Coq realization

parent 5eac33de
......@@ -38,9 +38,6 @@ 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.
......@@ -66,6 +63,7 @@ Qed.
(* 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))).
Proof.
intros x n h1.
rewrite <- Power_s; auto with zarith.
f_equal; omega.
......@@ -101,26 +99,47 @@ 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.
replace (n * Zsucc m)%Z with (n + n * m)%Z by ring.
rewrite Power_sum by auto with zarith.
rewrite IHm.
now rewrite Comm, <- Power_s.
now rewrite <- Power_s.
Qed.
(* Why3 goal *)
Lemma Power_comm1 : forall (x:t) (y:t), ((infix_as x y) = (infix_as y x)) ->
forall (n:Z), (0%Z <= n)%Z -> ((infix_as (power x n) y) = (infix_as y
(power x n))).
Proof.
intros x y comm.
apply natlike_ind.
now rewrite Power_0, Unit_def_r, Unit_def_l.
intros n Hn IHn.
unfold Zsucc.
rewrite (Power_s _ _ Hn).
rewrite Assoc.
rewrite IHn.
rewrite <- Assoc.
rewrite <- Assoc.
now rewrite comm.
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))).
Lemma Power_comm2 : forall (x:t) (y:t), ((infix_as x y) = (infix_as y x)) ->
forall (n:Z), (0%Z <= n)%Z -> ((power (infix_as x y)
n) = (infix_as (power x n) (power y n))).
Proof.
intros x y.
intros x y comm.
apply natlike_ind.
apply sym_eq.
rewrite 3!Power_0.
apply Unit_def_r.
now rewrite 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.
rewrite <- Assoc.
rewrite (Assoc x).
rewrite <- (Power_comm1 _ _ comm _ Hn).
now rewrite <- 2!Assoc.
Qed.
End Exponentiation.
......@@ -82,12 +82,21 @@ apply Power_mult ; auto with zarith.
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).
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).
Proof.
intros x y n Hn.
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.
rewrite 3!power_is_exponentiation ; auto with zarith.
apply Power_mult2 ; auto with zarith.
apply Power_comm2 ; auto with zarith.
Qed.
(* Why3 goal *)
......
......@@ -14,11 +14,6 @@
Require Import BuiltIn.
Require BuiltIn.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require Import ClassicalEpsilon.
Inductive _map (a b:Type) :=
......
......@@ -88,12 +88,21 @@ apply Power_mult ; auto with real.
Qed.
(* Why3 goal *)
Lemma Power_mult2 : forall (x:R) (y:R) (n:Z), (0%Z <= n)%Z ->
Lemma Power_comm1 : forall (x:R) (y:R), ((x * y)%R = (y * x)%R) ->
forall (n:Z), (0%Z <= n)%Z ->
(((Reals.Rfunctions.powerRZ x n) * y)%R = (y * (Reals.Rfunctions.powerRZ x n))%R).
intros x y h1 n h2.
apply Rmult_comm.
Qed.
(* Why3 goal *)
Lemma Power_comm2 : forall (x:R) (y:R), ((x * y)%R = (y * x)%R) ->
forall (n:Z), (0%Z <= n)%Z ->
((Reals.Rfunctions.powerRZ (x * y)%R n) = ((Reals.Rfunctions.powerRZ x n) * (Reals.Rfunctions.powerRZ y n))%R).
Proof.
intros x y n h1.
intros x y h1 n h2.
rewrite 3!power_is_exponentiation by auto with zarith.
apply Power_mult2 ; auto with real.
apply Power_comm2 ; auto with real.
Qed.
(* Why3 goal *)
......
......@@ -226,7 +226,12 @@ theory Exponentiation
lemma Power_mult : forall x:t, n m : int. 0 <= n -> 0 <= m ->
power x (Int.( * ) n m) = power (power x n) m
lemma Power_mult2 : forall x y: t, n: int. 0 <= n ->
lemma Power_comm1 : forall x y: t. x * y = y * x ->
forall n:int. 0 <= n ->
power x n * y = y * power x n
lemma Power_comm2 : forall x y: t. x * y = y * x ->
forall n:int. 0 <= n ->
power (x * y) n = power x n * power y n
(* TODO
......
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