Skip to content

why3
why3
Commit e5ba6705 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

update theory int.Exponentiation and its Coq realization 

fix obsolete sessions
parent d980d7b2
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 838 additions and 801 deletions
examples/binomial_heap/why3session.xml
View file @ e5ba6705
This diff is collapsed.
examples/bitvector_examples/why3session.xml
View file @ e5ba6705
This diff is collapsed.
examples/braun_trees/why3session.xml
View file @ e5ba6705
This diff is collapsed.
examples/power/why3session.xml
View file @ e5ba6705
......@@ -2,66 +2,63 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="2" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="6" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../power.mlw" proved="true">
<theory name="FastExponentiation" proved="true" sum="1f5c79140ef99b7be78acc3f17360559">
<theory name="FastExponentiation" proved="true" sum="a45a8b2cf3372db4ce8f0c0af52c2a0a">
<goal name="WP_parameter fast_exp" expl="VC for fast_exp" proved="true">
<proof prover="0" timelimit="3"><result status="valid" time="0.57" steps="55"/></proof>
<proof prover="4" timelimit="3"><result status="valid" time="0.12" steps="44"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative" expl="VC for fast_exp_imperative" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter fast_exp_imperative.0" expl="loop invariant init" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="1" timelimit="10"><result status="valid" time="0.00"/></proof>
<proof prover="4" timelimit="5"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.1" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.19" steps="14"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.2" expl="loop invariant preservation" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter fast_exp_imperative.2.0" expl="VC for fast_exp_imperative" proved="true">
<proof prover="0" memlimit="1000"><result status="valid" time="0.13" steps="13"/></proof>
<proof prover="4" memlimit="1000"><result status="valid" time="0.13" steps="11"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.2.1" expl="VC for fast_exp_imperative" proved="true">
<proof prover="2"><result status="valid" time="0.80" steps="19"/></proof>
<proof prover="4" timelimit="6" memlimit="1000"><result status="valid" time="0.46" steps="20"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter fast_exp_imperative.3" expl="loop variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.09" steps="13"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.52" steps="11"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.4" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.10" steps="21"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.5" expl="loop invariant preservation" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter fast_exp_imperative.5.0" expl="VC for fast_exp_imperative" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.02" steps="16"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.08" steps="16"/></proof>
<proof prover="4" timelimit="5"><result status="valid" time="0.02" steps="17"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.5.1" expl="VC for fast_exp_imperative" proved="true">
<proof prover="2"><result status="valid" time="1.81" steps="25"/></proof>
<proof prover="4" timelimit="6" memlimit="1000"><result status="valid" time="0.50" steps="24"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter fast_exp_imperative.6" expl="loop variant decrease" proved="true">
<proof prover="0"><result status="valid" time="1.15" steps="21"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.29" steps="22"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.7" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.00" steps="6"/></proof>
<proof prover="4" timelimit="1" memlimit="1000"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
</transf>
</goal>
......
examples/sum_of_digits/why3session.xml
View file @ e5ba6705
......@@ -4,75 +4,75 @@
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../sum_of_digits.mlw" expanded="true">
<theory name="Euler290" sum="983835c6b3afb74dc6896a5de1ee7386" expanded="true">
<goal name="Base" expl="">
<proof prover="4" timelimit="10"><result status="valid" time="0.01" steps="5"/></proof>
<file name="../sum_of_digits.mlw">
<theory name="Euler290" sum="331b1074d09b0ddc7bd65a0dff93eab5">
<goal name="Base" proved="true">
<proof prover="2" timelimit="10"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="Empty" expl="">
<proof prover="4" timelimit="10"><result status="valid" time="0.07" steps="71"/></proof>
<goal name="Empty" proved="true">
<proof prover="2" timelimit="10"><result status="valid" time="0.07" steps="56"/></proof>
</goal>
<goal name="Induc" expl="" expanded="true">
<goal name="Induc">
</goal>
<goal name="WP_parameter sd" expl="VC for sd">
<goal name="WP_parameter sd" expl="VC for sd" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.44"/></proof>
</goal>
<goal name="WP_parameter f" expl="VC for f">
<transf name="split_goal_wp">
<goal name="WP_parameter f.1" expl="assertion">
<goal name="WP_parameter f" expl="VC for f" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter f.0" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter f.2" expl="assertion">
<proof prover="1"><result status="valid" time="2.70"/></proof>
<goal name="WP_parameter f.1" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="3.11"/></proof>
</goal>
<goal name="WP_parameter f.3" expl="precondition">
<goal name="WP_parameter f.2" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter f.4" expl="postcondition">
<goal name="WP_parameter f.3" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter f.5" expl="postcondition">
<goal name="WP_parameter f.4" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="3"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="4"/></proof>
</goal>
<goal name="WP_parameter f.6" expl="loop invariant init">
<goal name="WP_parameter f.5" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="6"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="6"/></proof>
</goal>
<goal name="WP_parameter f.7" expl="variant decrease">
<goal name="WP_parameter f.6" expl="variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="7"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="WP_parameter f.8" expl="precondition">
<goal name="WP_parameter f.7" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="10"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
<goal name="WP_parameter f.9" expl="assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter f.9.1" expl="VC for f">
<goal name="WP_parameter f.8" expl="assertion" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter f.8.0" expl="VC for f" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="11"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="WP_parameter f.9.2" expl="VC for f">
<goal name="WP_parameter f.8.1" expl="VC for f" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="4"><result status="valid" time="0.07" steps="13"/></proof>
<proof prover="2"><result status="valid" time="0.07" steps="14"/></proof>
</goal>
<goal name="WP_parameter f.9.3" expl="VC for f">
<proof prover="4"><result status="valid" time="0.01" steps="14"/></proof>
<goal name="WP_parameter f.8.2" expl="VC for f" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="29"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter f.10" expl="loop invariant preservation">
<goal name="WP_parameter f.9" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="16"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
<goal name="WP_parameter f.11" expl="postcondition">
<goal name="WP_parameter f.10" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="6"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
</transf>
</goal>
......
examples/tests-provers/coq-interval/why3session.xml
View file @ e5ba6705
......@@ -3,10 +3,10 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../coq-interval.why" expanded="true">
<theory name="P" sum="72361b88738cd9a546e50ed08ba8c423" expanded="true">
<goal name="pow_eps2_max_int" expl="" expanded="true">
<proof prover="1" edited="coqmninterval_P_pow_eps2_max_int_1.v"><result status="valid" time="1.21"/></proof>
<file name="../coq-interval.why" proved="true">
<theory name="P" proved="true" sum="1e4fe85b7d4e5d74721c865ee586cec8">
<goal name="pow_eps2_max_int" proved="true">
<proof prover="1" edited="coqmninterval_P_pow_eps2_max_int_1.v"><result status="valid" time="0.83"/></proof>
</goal>
</theory>
</file>
......
examples/tree_of_array/why3session.xml
View file @ e5ba6705
......@@ -4,47 +4,48 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../tree_of_array.mlw" expanded="true">
<theory name="TreeOfArray" sum="e6cc07771b58c81603582477098238ac" expanded="true">
<goal name="WP_parameter tree_of_array_aux" expl="VC for tree_of_array_aux" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter tree_of_array_aux.1" expl="postcondition">
<prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../tree_of_array.mlw" proved="true">
<theory name="TreeOfArray" proved="true" sum="ca512e46cd4640bfe836ac9f7544989f">
<goal name="WP_parameter tree_of_array_aux" expl="VC for tree_of_array_aux" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter tree_of_array_aux.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter tree_of_array_aux.2" expl="variant decrease">
<goal name="WP_parameter tree_of_array_aux.1" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter tree_of_array_aux.3" expl="precondition">
<goal name="WP_parameter tree_of_array_aux.2" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="WP_parameter tree_of_array_aux.4" expl="variant decrease">
<goal name="WP_parameter tree_of_array_aux.3" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter tree_of_array_aux.5" expl="precondition">
<goal name="WP_parameter tree_of_array_aux.4" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="25"/></proof>
</goal>
<goal name="WP_parameter tree_of_array_aux.6" expl="index in array bounds">
<goal name="WP_parameter tree_of_array_aux.5" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter tree_of_array_aux.7" expl="postcondition" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter tree_of_array_aux.7.1" expl="postcondition">
<goal name="WP_parameter tree_of_array_aux.6" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter tree_of_array_aux.6.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="WP_parameter tree_of_array_aux.7.2" expl="postcondition">
<proof prover="0"><result status="valid" time="0.17" steps="274"/></proof>
<goal name="WP_parameter tree_of_array_aux.6.1" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.17" steps="270"/></proof>
</goal>
<goal name="WP_parameter tree_of_array_aux.7.3" expl="postcondition">
<proof prover="0"><result status="valid" time="2.41" steps="1188"/></proof>
<goal name="WP_parameter tree_of_array_aux.6.2" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="WP_parameter tree_of_array_aux.7.4" expl="postcondition">
<goal name="WP_parameter tree_of_array_aux.6.3" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.13"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter tree_of_array" expl="VC for tree_of_array" expanded="true">
<goal name="WP_parameter tree_of_array" expl="VC for tree_of_array" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
</theory>
......
examples/tree_of_list/why3session.xml
View file @ e5ba6705
......@@ -3,49 +3,49 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../tree_of_list.mlw">
<theory name="TreeOfList" sum="12d1a0ff628823b4f6f62c68ba956168">
<goal name="WP_parameter tree_of_list_aux" expl="VC for tree_of_list_aux">
<transf name="split_goal_wp">
<goal name="WP_parameter tree_of_list_aux.1" expl="postcondition">
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../tree_of_list.mlw" proved="true">
<theory name="TreeOfList" proved="true" sum="2050454f03b72dc532ec8a04d950d1c0">
<goal name="WP_parameter tree_of_list_aux" expl="VC for tree_of_list_aux" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter tree_of_list_aux.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter tree_of_list_aux.2" expl="variant decrease">
<proof prover="2"><result status="valid" time="0.02" steps="6"/></proof>
<goal name="WP_parameter tree_of_list_aux.1" expl="variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="WP_parameter tree_of_list_aux.3" expl="precondition">
<proof prover="2"><result status="valid" time="0.03" steps="7"/></proof>
<goal name="WP_parameter tree_of_list_aux.2" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.03" steps="10"/></proof>
</goal>
<goal name="WP_parameter tree_of_list_aux.4" expl="unreachable point">
<proof prover="2"><result status="valid" time="0.01" steps="29"/></proof>
<goal name="WP_parameter tree_of_list_aux.3" expl="unreachable point" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter tree_of_list_aux.5" expl="variant decrease">
<proof prover="2"><result status="valid" time="0.01" steps="8"/></proof>
<goal name="WP_parameter tree_of_list_aux.4" expl="variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter tree_of_list_aux.6" expl="precondition">
<proof prover="2"><result status="valid" time="0.01" steps="47"/></proof>
<goal name="WP_parameter tree_of_list_aux.5" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="48"/></proof>
</goal>
<goal name="WP_parameter tree_of_list_aux.7" expl="postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter tree_of_list_aux.7.1" expl="postcondition">
<proof prover="2"><result status="valid" time="0.00" steps="47"/></proof>
<goal name="WP_parameter tree_of_list_aux.6" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter tree_of_list_aux.6.0" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="25"/></proof>
</goal>
<goal name="WP_parameter tree_of_list_aux.7.2" expl="postcondition">
<proof prover="2"><result status="valid" time="0.02" steps="15"/></proof>
<goal name="WP_parameter tree_of_list_aux.6.1" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="20"/></proof>
</goal>
<goal name="WP_parameter tree_of_list_aux.7.3" expl="postcondition">
<goal name="WP_parameter tree_of_list_aux.6.2" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter tree_of_list_aux.7.4" expl="postcondition">
<goal name="WP_parameter tree_of_list_aux.6.3" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.08"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter tree_of_list" expl="VC for tree_of_list">
<proof prover="2"><result status="valid" time="0.02" steps="99"/></proof>
<goal name="WP_parameter tree_of_list" expl="VC for tree_of_list" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="99"/></proof>
</goal>
</theory>
</file>
......
lib/coq/int/Exponentiation.v
View file @ e5ba6705
......@@ -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.
......@@ -102,25 +100,48 @@ 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.
unfold Zsucc.
rewrite 2!Power_sum by auto with zarith.
rewrite IHm.
now rewrite Comm, <- Power_s.
now rewrite Power_1.
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.
lib/coq/int/Power.v
View file @ e5ba6705
......@@ -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 *)
......
lib/coq/map/Map.v
View file @ e5ba6705
......@@ -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) :=
......
lib/coq/real/PowerInt.v
View file @ e5ba6705
......@@ -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 *)
......
theories/int.why
View file @ e5ba6705
......@@ -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