Commit ca158e30 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix Coq files after removal of axioms.

parent 59603e04
......@@ -16,48 +16,6 @@ Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Axiom Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z.
Axiom Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
(x = ((y * (ZOdiv x y))%Z + (ZOmod x y))%Z).
Axiom Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
((0%Z <= (ZOdiv x y))%Z /\ ((ZOdiv x y) <= x)%Z).
Axiom Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
(((-(Zabs y))%Z < (ZOmod x y))%Z /\ ((ZOmod x y) < (Zabs y))%Z).
Axiom Div_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
(0%Z <= (ZOdiv x y))%Z.
Axiom Div_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ (0%Z < y)%Z) ->
((ZOdiv x y) <= 0%Z)%Z.
Axiom Mod_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ ~ (y = 0%Z)) ->
(0%Z <= (ZOmod x y))%Z.
Axiom Mod_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ ~ (y = 0%Z)) ->
((ZOmod x y) <= 0%Z)%Z.
Axiom Rounds_toward_zero : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
((Zabs ((ZOdiv x y) * y)%Z) <= (Zabs x))%Z.
Axiom Div_1 : forall (x:Z), ((ZOdiv x 1%Z) = x).
Axiom Mod_1 : forall (x:Z), ((ZOmod x 1%Z) = 0%Z).
Axiom Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) ->
((ZOdiv x y) = 0%Z).
Axiom Mod_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) ->
((ZOmod x y) = x).
Axiom Div_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
(0%Z <= z)%Z)) -> ((ZOdiv ((x * y)%Z + z)%Z x) = (y + (ZOdiv z x))%Z).
Axiom Mod_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
(0%Z <= z)%Z)) -> ((ZOmod ((x * y)%Z + z)%Z x) = (ZOmod z x)).
Definition lt_nat(x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z.
Inductive lex : (Z* Z)%type -> (Z* Z)%type -> Prop :=
......@@ -140,19 +98,6 @@ Axiom divides_trans : forall (a:Z) (b:Z) (c:Z), (divides a b) -> ((divides b
Axiom divides_bounds : forall (a:Z) (b:Z), (divides a b) -> ((~ (b = 0%Z)) ->
((Zabs a) <= (Zabs b))%Z).
Axiom Div_mod1 : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
(x = ((y * (Zdiv x y))%Z + (Zmod x y))%Z).
Axiom Div_bound1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
((0%Z <= (Zdiv x y))%Z /\ ((Zdiv x y) <= x)%Z).
Axiom Mod_bound1 : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
((0%Z <= (Zmod x y))%Z /\ ((Zmod x y) < (Zabs y))%Z).
Axiom Mod_11 : forall (x:Z), ((Zmod x 1%Z) = 0%Z).
Axiom Div_11 : forall (x:Z), ((Zdiv x 1%Z) = x).
Axiom mod_divides_euclidean : forall (a:Z) (b:Z), (~ (b = 0%Z)) ->
(((Zmod a b) = 0%Z) -> (divides b a)).
......@@ -300,13 +245,14 @@ rewrite <- p0. apply sorted; omega.
apply small_divisors; auto.
omega.
intros.
assert (ne0: (get p3 k <> 0)%Z) by omega.
generalize (Div_mod n1 (get p3 k)%Z ne0). intro div.
generalize (ZO_div_mod_eq n1 (get p3 k)). intro div.
assert (ne1: (0 <= n1 /\ get p3 k <> 0)%Z) by omega.
generalize (Mod_sign_pos n1 (get p3 k)%Z ne1). intro mod1.
generalize (Mod_bound n1 (get p3 k)%Z ne0).
rewrite Zabs_eq; try omega.
intros (_, mod2).
assert (mod1: (0 <= ZOmod n1 (get p3 k))%Z).
destruct (not_Zeq_inf _ _ (proj2 ne1)) as [Zm|Zm].
now apply ZOmod_lt_pos_neg.
now apply ZOmod_lt_pos_pos.
assert (mod2: (ZOmod n1 (get p3 k) < get p3 k)%Z).
apply ZOmod_lt_pos_pos ; omega.
assert (d <= get p3 k)%Z.
assert (d < get p3 k+1)%Z. 2: omega.
apply Zle_sqrt; try omega.
......@@ -335,7 +281,7 @@ red; intro; apply H21 with i; try omega.
auto.
subst i.
intro. apply H10.
apply divides_mod_computer; auto.
apply divides_mod_computer; auto; omega.
Qed.
(* DO NOT EDIT BELOW *)
......
......@@ -16,48 +16,6 @@ Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Axiom Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z.
Axiom Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
(x = ((y * (ZOdiv x y))%Z + (ZOmod x y))%Z).
Axiom Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
((0%Z <= (ZOdiv x y))%Z /\ ((ZOdiv x y) <= x)%Z).
Axiom Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
(((-(Zabs y))%Z < (ZOmod x y))%Z /\ ((ZOmod x y) < (Zabs y))%Z).
Axiom Div_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
(0%Z <= (ZOdiv x y))%Z.
Axiom Div_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ (0%Z < y)%Z) ->
((ZOdiv x y) <= 0%Z)%Z.
Axiom Mod_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ ~ (y = 0%Z)) ->
(0%Z <= (ZOmod x y))%Z.
Axiom Mod_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ ~ (y = 0%Z)) ->
((ZOmod x y) <= 0%Z)%Z.
Axiom Rounds_toward_zero : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
((Zabs ((ZOdiv x y) * y)%Z) <= (Zabs x))%Z.
Axiom Div_1 : forall (x:Z), ((ZOdiv x 1%Z) = x).
Axiom Mod_1 : forall (x:Z), ((ZOmod x 1%Z) = 0%Z).
Axiom Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) ->
((ZOdiv x y) = 0%Z).
Axiom Mod_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) ->
((ZOmod x y) = x).
Axiom Div_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
(0%Z <= z)%Z)) -> ((ZOdiv ((x * y)%Z + z)%Z x) = (y + (ZOdiv z x))%Z).
Axiom Mod_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
(0%Z <= z)%Z)) -> ((ZOmod ((x * y)%Z + z)%Z x) = (ZOmod z x)).
Definition lt_nat(x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z.
Inductive lex : (Z* Z)%type -> (Z* Z)%type -> Prop :=
......@@ -140,19 +98,6 @@ Axiom divides_trans : forall (a:Z) (b:Z) (c:Z), (divides a b) -> ((divides b
Axiom divides_bounds : forall (a:Z) (b:Z), (divides a b) -> ((~ (b = 0%Z)) ->
((Zabs a) <= (Zabs b))%Z).
Axiom Div_mod1 : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
(x = ((y * (Zdiv x y))%Z + (Zmod x y))%Z).
Axiom Div_bound1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
((0%Z <= (Zdiv x y))%Z /\ ((Zdiv x y) <= x)%Z).
Axiom Mod_bound1 : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
((0%Z <= (Zmod x y))%Z /\ ((Zmod x y) < (Zabs y))%Z).
Axiom Mod_11 : forall (x:Z), ((Zmod x 1%Z) = 0%Z).
Axiom Div_11 : forall (x:Z), ((Zdiv x 1%Z) = x).
Axiom mod_divides_euclidean : forall (a:Z) (b:Z), (~ (b = 0%Z)) ->
(((Zmod a b) = 0%Z) -> (divides b a)).
......@@ -298,10 +243,12 @@ subst k.
assert (2 < get p3 (j-1))%Z.
red in H21. destruct H21 as (h1, (h2, _)).
rewrite <- h1. apply h2; omega.
assert (ne0: (get p3 (j-1) <> 0)%Z) by omega.
generalize (Div_mod n1 (get p3 (j-1))%Z ne0). intro div.
generalize (ZO_div_mod_eq n1 (get p3 (j-1))%Z). intro div.
assert (ne1: (0 <= n1 /\ get p3 (j-1) <> 0)%Z) by omega.
generalize (Mod_sign_pos n1 (get p3 (j-1))%Z ne1). intro mod_.
assert (mod_: (0 <= ZOmod n1 (get p3 (j-1)))%Z).
destruct (not_Zeq_inf _ _ (proj2 ne1)) as [Zm|Zm].
now apply ZOmod_lt_pos_neg.
now apply ZOmod_lt_pos_pos.
assert (n1 > get p3 (j - 1) * get p3 (j-1))%Z.
assert (get p3 (j - 1) * (ZOdiv n1 (get p3 (j - 1))) > get p3 (j - 1) * get p3 (j-1))%Z.
apply Zmult_gt_compat_l.
......
......@@ -15,48 +15,6 @@ Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Axiom Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z.
Axiom Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
(x = ((y * (ZOdiv x y))%Z + (ZOmod x y))%Z).
Axiom Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
((0%Z <= (ZOdiv x y))%Z /\ ((ZOdiv x y) <= x)%Z).
Axiom Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
(((-(Zabs y))%Z < (ZOmod x y))%Z /\ ((ZOmod x y) < (Zabs y))%Z).
Axiom Div_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
(0%Z <= (ZOdiv x y))%Z.
Axiom Div_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ (0%Z < y)%Z) ->
((ZOdiv x y) <= 0%Z)%Z.
Axiom Mod_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ ~ (y = 0%Z)) ->
(0%Z <= (ZOmod x y))%Z.
Axiom Mod_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ ~ (y = 0%Z)) ->
((ZOmod x y) <= 0%Z)%Z.
Axiom Rounds_toward_zero : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
((Zabs ((ZOdiv x y) * y)%Z) <= (Zabs x))%Z.
Axiom Div_1 : forall (x:Z), ((ZOdiv x 1%Z) = x).
Axiom Mod_1 : forall (x:Z), ((ZOmod x 1%Z) = 0%Z).
Axiom Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) ->
((ZOdiv x y) = 0%Z).
Axiom Mod_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) ->
((ZOmod x y) = x).
Axiom Div_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
(0%Z <= z)%Z)) -> ((ZOdiv ((x * y)%Z + z)%Z x) = (y + (ZOdiv z x))%Z).
Axiom Mod_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
(0%Z <= z)%Z)) -> ((ZOmod ((x * y)%Z + z)%Z x) = (ZOmod z x)).
Parameter power: Z -> Z -> Z.
......@@ -86,6 +44,10 @@ Definition contents (a:Type)(u:(ref a)): a :=
end.
Implicit Arguments contents.
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem WP_parameter_fast_exp_imperative : forall (x:Z), forall (n:Z),
(0%Z <= n)%Z -> forall (e:Z), forall (p:Z), forall (r:Z), ((0%Z <= e)%Z /\
((r * (power p e))%Z = (power x n))) -> ((0%Z < e)%Z ->
......@@ -99,17 +61,9 @@ apply f_equal.
subst.
assert ((e = e/2 + e/2)%Z).
assert (e mod 2 = 0).
assert (0 <= e mod 2)%Z.
apply Mod_sign_pos.
intuition.
assert (-(Zabs 2) < e mod 2 < (Zabs 2)).
apply Mod_bound.
omega.
assert (Zabs 2 = 2).
auto.
rewrite H6 in H5; omega.
assert (e = 2 * (e/2) + e mod 2).
apply Div_mod; omega.
generalize (ZOmod_lt_pos e 2).
unfold Zabs; omega.
rewrite (ZO_div_mod_eq e 2) at 1.
omega.
rewrite Power_mult2.
rewrite H0 at 3.
......
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