Commit 647d63e7 authored by MARCHE Claude's avatar MARCHE Claude

preuve de power_sum

parent b50c3f74
...@@ -20,9 +20,22 @@ Theorem Power_sum : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) -> ...@@ -20,9 +20,22 @@ Theorem Power_sum : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z). ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z).
(* YOU MAY EDIT THE PROOF BELOW *) (* YOU MAY EDIT THE PROOF BELOW *)
intros n m Hmn. intros n m Hmn.
cut (0 <= m); auto with zarith.
apply Z_lt_induction with
(P:= fun m =>
0 <= m -> pow2 (n + m) = pow2 n * pow2 m);
auto with zarith.
intros x Hind Hxpos.
assert (h:(x = 0 \/ x > 0)) by omega.
destruct h.
subst x.
rewrite Power_0.
(*
auto with zarith.
elim n. elim n.
replace (0+m) with m by omega. replace (0+m) with m by omega.
rewrite Power_0.
replace (1* pow2 m) with (pow2 m) by omega. replace (1* pow2 m) with (pow2 m) by omega.
auto. auto.
intro. intro.
...@@ -37,7 +50,7 @@ replace (2 * Zpos p0) with (Zpos p0 * 2) by omega. ...@@ -37,7 +50,7 @@ replace (2 * Zpos p0) with (Zpos p0 * 2) by omega.
rewrite<-Zplus_diag_eq_mult_2. rewrite<-Zplus_diag_eq_mult_2.
rewrite Power_s. rewrite Power_s.
*)
Qed. Qed.
......
...@@ -1036,7 +1036,7 @@ ...@@ -1036,7 +1036,7 @@
<theory <theory
name="Pow2real" name="Pow2real"
verified="false" verified="false"
expanded="true"> expanded="false">
<goal <goal
name="Power_1" name="Power_1"
sum="05eff9d48281eb24cb06eb9caecf811e" sum="05eff9d48281eb24cb06eb9caecf811e"
...@@ -1118,7 +1118,7 @@ ...@@ -1118,7 +1118,7 @@
<theory <theory
name="BitVector" name="BitVector"
verified="false" verified="false"
expanded="true"> expanded="false">
<goal <goal
name="Nth_bw_xor_v1true" name="Nth_bw_xor_v1true"
sum="3ea193c399b136e4f0619cc666a98664" sum="3ea193c399b136e4f0619cc666a98664"
...@@ -1305,7 +1305,7 @@ ...@@ -1305,7 +1305,7 @@
name="nth_from_int_low_even" name="nth_from_int_low_even"
sum="5de955fad899fb21842dc88dddf9eef7" sum="5de955fad899fb21842dc88dddf9eef7"
proved="true" proved="true"
expanded="true" expanded="false"
shape="ainfix =anthafrom_intV0c0aFalseIainfix =amodV0c2c0F"> shape="ainfix =anthafrom_intV0c0aFalseIainfix =amodV0c2c0F">
<proof <proof
prover="coq" prover="coq"
...@@ -1417,28 +1417,28 @@ ...@@ -1417,28 +1417,28 @@
name="nth_from_int2c_low_even_positive" name="nth_from_int2c_low_even_positive"
sum="69f18f37edd8fc04bfdf09f8bb8a8f85" sum="69f18f37edd8fc04bfdf09f8bb8a8f85"
proved="false" proved="false"
expanded="true" expanded="false"
shape="ainfix =anthafrom_int2cV0c0aFalseIainfix =amodV0c2c0Aainfix >=V0c0F"> shape="ainfix =anthafrom_int2cV0c0aFalseIainfix =amodV0c2c0Aainfix >=V0c0F">
</goal> </goal>
<goal <goal
name="nth_from_int2c_low_odd_positive" name="nth_from_int2c_low_odd_positive"
sum="475988455b849e1fbc62bc87c2a4b147" sum="475988455b849e1fbc62bc87c2a4b147"
proved="false" proved="false"
expanded="true" expanded="false"
shape="ainfix =anthafrom_int2cV0c0aTrueIainfix =amodV0c2c0NAainfix >=V0c0F"> shape="ainfix =anthafrom_int2cV0c0aTrueIainfix =amodV0c2c0NAainfix >=V0c0F">
</goal> </goal>
<goal <goal
name="nth_from_int2c_low_even_negative" name="nth_from_int2c_low_even_negative"
sum="5ffbc4d5d31761cff206901e8b5f825a" sum="5ffbc4d5d31761cff206901e8b5f825a"
proved="false" proved="false"
expanded="true" expanded="false"
shape="ainfix =anthafrom_int2cV0c0aTrueIainfix =amodV0c2c0Aainfix <V0c0F"> shape="ainfix =anthafrom_int2cV0c0aTrueIainfix =amodV0c2c0Aainfix <V0c0F">
</goal> </goal>
<goal <goal
name="nth_from_int2c_low_odd_negative" name="nth_from_int2c_low_odd_negative"
sum="043edbe6d2a94a92420cb81b9b134329" sum="043edbe6d2a94a92420cb81b9b134329"
proved="false" proved="false"
expanded="true" expanded="false"
shape="ainfix =anthafrom_int2cV0c0aFalseIainfix =amodV0c2c0NAainfix <V0c0F"> shape="ainfix =anthafrom_int2cV0c0aFalseIainfix =amodV0c2c0NAainfix <V0c0F">
</goal> </goal>
</theory> </theory>
...@@ -2969,14 +2969,14 @@ ...@@ -2969,14 +2969,14 @@
name="x_negative" name="x_negative"
sum="75aca8e6393ca908f8163a9722aeb5e8" sum="75aca8e6393ca908f8163a9722aeb5e8"
proved="false" proved="false"
expanded="true" expanded="false"
shape="ainfix =ato_nat_subavarV0c30c0aprefix -V0Iainfix =anthavarV0c31aFalseF"> shape="ainfix =ato_nat_subavarV0c30c0aprefix -V0Iainfix =anthavarV0c31aFalseF">
</goal> </goal>
<goal <goal
name="mantissa_var_x_negative" name="mantissa_var_x_negative"
sum="af80cf6d8e488e18405d3f91f4ce940f" sum="af80cf6d8e488e18405d3f91f4ce940f"
proved="false" proved="false"
expanded="true" expanded="false"
shape="ainfix =amantissaavarV0ainfix -apow2c31V0Iainfix =anthavarV0c31aFalseF"> shape="ainfix =amantissaavarV0ainfix -apow2c31V0Iainfix =anthavarV0c31aFalseF">
<proof <proof
prover="coq" prover="coq"
...@@ -3067,7 +3067,7 @@ ...@@ -3067,7 +3067,7 @@
name="from_int_sum" name="from_int_sum"
sum="a1bb3937bfed62df0155e2517454c2d0" sum="a1bb3937bfed62df0155e2517454c2d0"
proved="false" proved="false"
expanded="true" expanded="false"
shape="ainfix =afrom_intainfix +apow2c31V0ainfix +.afrom_intapow2c31afrom_intV0F"> shape="ainfix =afrom_intainfix +apow2c31V0ainfix +.afrom_intapow2c31afrom_intV0F">
</goal> </goal>
<goal <goal
......
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